[TS] Audit and formalize the type relations used by usvm-ts

[CaelmBleidd]

Context

PR #344 exposed a semantic coupling in the current TypeScript type implementation. TsTypeSystem.isSupertype is used by the symbolic type-constraint machinery, but related type decisions also affect structural property access, virtual call target selection, and runtime checks such as instanceof.

These operations do not necessarily use the same relation:

• TypeScript assignability is primarily structural and depends on compiler options;
• instanceof follows the JavaScript runtime prototype chain;
• property reads and writes require a structural shape/capability constraint;
• UTypeRegion needs a coherent order and auxiliary operations for pruning symbolic type alternatives.

The fix in #344 introduces an internal nominal wrapper for instanceof so that a runtime hierarchy check does not change the established EtsAuxiliaryType behavior. This fixes the observed regression, but it also shows that the boundaries and laws of the type model are not yet explicit. TsTypeSystem is still marked as a draft, and several cases are unsupported or handled by provisional rules.

Problem

We need to establish which type relations USVM for TypeScript actually requires, formalize them, and verify that every consumer uses the appropriate relation.

The audit should cover at least:

• the intended meaning of EtsAuxiliaryType and whether it is a TypeScript structural type, an abstract-domain constraint such as “has these properties”, or both;
• nominal class hierarchy versus structural compatibility;
• any, unknown, never, null, and undefined, including the assumed strictNullChecks mode;
• literal and primitive types;
• unions and intersections;
• arrays and tuples;
• function types and variance;
• classes, interfaces, unclear reference types, aliases, and synthetic structural types;
• coherence of isSupertype, hasCommonSubtype, isFinal, isInstantiable, findSubtypes, and topTypeStream with the expectations of UTypeRegion and USupportTypeStream.

Some current rules are candidates for errors, but should be checked against the chosen semantics rather than changed independently. Examples include intersection subtyping, bidirectional relations between auxiliary and class types, treatment of unknown with nullish types, and whether findSubtypes returns direct successors as required by UTypeSystem.

Proposed work

1. Map the consumers. List every use of the type-system operations and classify it as static assignability, runtime membership/prototype testing, structural capability checking, call dispatch, or abstract-domain ordering.
2. Specify the relations. Define the supported type universe, normalization rules, compiler-option assumptions, and the meaning of each public operation. State the laws required by the constraint engine, such as reflexivity/transitivity where applicable and coherence between subtype checks, common-subtype checks, finality, and subtype enumeration.
3. Build an executable conformance matrix. Cover every supported pair/family of types and explicitly record unsupported cases and conservative fallbacks.
4. Add independent oracles. Compare static assignability cases with the TypeScript compiler API under the selected compiler options. Check runtime predicates such as instanceof with JavaScript/Node.js examples instead of deriving them from static assignability.
5. Add property-based/metamorphic tests. Generate small type graphs and validate the stated laws and UTypeRegion pruning behavior. Keep minimal counterexamples for every discovered violation.
6. Separate relations where necessary. If one API cannot represent the required semantics without ambiguity, introduce explicit operations or typed wrappers rather than encoding the distinction through accidental call-site conventions.
7. Fix discovered defects in focused follow-up changes. Classify every known deviation as a sound over-approximation, an under-approximation, or an implementation bug.

Deliverables / acceptance criteria

• A checked-in design note defining the supported TypeScript and runtime type semantics and the assumptions made about compiler options.
• A consumer map showing which relation each analysis operation requires.
• An executable test matrix covering all currently supported EtsType families.
• Differential tests against the TypeScript compiler for static assignability and against Node.js for runtime type predicates.
• Property tests for the laws relied upon by UTypeRegion/USupportTypeStream.
• Minimal regression tests for every defect found during the audit.
• Unsupported or intentionally approximate cases are documented and handled conservatively.
• Follow-up implementation issues/PRs are split by independently reviewable semantic change.

Non-goal

This issue does not require implementing the entire TypeScript type system at once. Advanced features that are not represented by the current IR may remain unsupported, but their behavior must be explicit and must not silently make the symbolic type constraints unsound.