[TS PBT] Project property domains and preconditions into USVM

Start with PropertyManifest, JsConcreteValue, the mapped entry-point bindings, and the current machine initial-state mechanism. Review the shared-contract gate in #384 and the focused usvm-ts-pbt/usvm-ts checks before defining the supported projection subset. Done means satisfiable constraints match declared domains, preconditions follow the shared contract, and unsupported or approximate cases are explicitly reported rather than labeled exact.

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 #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 #384, with focused usvm-ts-pbt/usvm-ts checks.

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