[TS PBT] Project property domains and preconditions into USVM #351

Delivery boundary in the full #345 roadmap

Preserve the direct-domain/precondition implementation in PR #387 as this issue's scope. #395 owns richer declared/generator semantics, #400 owns bounded generator-choice projection, and #398 owns empirical-relation challenge binding. Any required projection extensions land as separately reviewed follow-ups. Observed distributions are never silently promoted to declared domains.

Part of #345. Depends on #350 and the shared-contract gate #384.

Goal

Construct symbolic inputs and precondition constraints from the existing Kotlin property domains, with an explicit supported subset.

Scope

• Reuse PropertyManifest, JsConcreteValue, the mapped entry-point bindings and the current machine initial-state mechanism.
• Establish exact projection for booleans, bounded numeric inputs and supported primitive constants first. Add optional values, bounded tuples and bounded arrays only where the current heap/value representation supports them.
• Publish a small per-domain table for strings, unbounded collections and every remaining common domain: supported representation, limits, and exact/approximate/unsupported status. A domain appearing in the common API does not require complete symbolic support here.
• Respect JavaScript binary64, declared NaN/infinity/negative-zero policy, inclusive bounds, optional null versus undefined and argument order.
• Execute supported pure preconditions according to [TS PBT][P0] Align and simplify property execution semantics before integration #384. false discards the input; a thrown exception or invalid result is an error. Do not silently drop those errors or present solver UNKNOWN as UNSAT.
• Report symbolic capability and derive concrete-only when the concrete backend supports an unsupported symbolic case.
• For an approximate projection, state whether it adds values, omits values, does both, or has an unestablished relation to the declared domain. Replay is still required and unsuccessful search proves nothing.
• Keep one capability decision path; do not duplicate domain definitions, value codecs or validators between the capability checker and projector.

Definition of Done

• The documented exact subset instantiates inputs in the correct slots with satisfiable constraints matching the declared domains.
• Focused conformance fixtures compare concrete accepted values with symbolic constraints, including boundary and special-value cases.
• Preconditions follow the shared classification and purity contract.
• Unsupported/approximate projections cannot be labeled exact.
• Collection limits are explicit configuration/implementation limits, not silent truncation.
• String support may remain approximate or unsupported; no full string solver or arbitrary object graph support is required.
• Existing implementation work is reused and aligned with [TS PBT][P0] Align and simplify property execution semantics before integration #384, with focused usvm-ts-pbt/usvm-ts checks.

Predicate violation targets, concrete replay and runtime-derived hints belong to later issues.