[TS PBT] Project observed relations and assertion goals into exact EtsIR bindings #398

Implementation child of #355. Builds on #350/#351/#352 and #396. Uses the typed hypothesis contract from #397; projection and inference can be developed against a shared fixture before both implementations finish.

Goal

Turn an observed relation at an identified execution point into a symbolic challenge with the same value, time and context semantics.

First checkpoint binding contract

#405 uses the exact bounded subset: arguments/returns, explicitly identified intermediate values, supported pre/post scalar or collection-length observations, original assertions and simple guarded hypotheses. Bind value, invocation, program point and time before issuing a challenge; source-line matches or sampled reachability are insufficient.

Demonstrate a supported-prefix/full-concrete-oracle case without claiming fabricated semantics past an unsupported prefix. Dedicated generator choices, cross-execution pairing, command-state continuation and helper-summary refinement are implemented and accepted in #400–#403. They do not block this binding contract.

Scope

• Bind property/assertion, call site, program point and pre/post value references to EtsIR expressions/slots/heap locations. Source-line coincidence is insufficient. Preserve invocation context, aliases and temporal identity within the supported subset.
• Start with arguments, returns and explicitly named observation points; extend to selected intermediate values. Reuse [TS PBT] Map Kotlin property definitions and source coverage to EtsIR #350 source normalization/bindings rather than duplicating the resolver.
• Validate source/build hashes and report EXACT, AMBIGUOUS, UNMAPPED or UNSUPPORTED with reasons. Publish capability by relation kind and value binding.
• Compile a challenge as declared domain AND admitted precondition AND reach(program point/context) AND NOT(hypothesis). Do not assume the hypothesis or the tested original postcondition. Preserve any hypothesis guard; do not silently globalize a local relation.
• Keep original property-failure targets and inferred-hypothesis targets distinct. Identify which target and state produced each candidate; reuse [TS PBT] Search for property violations with USVM #352 input extraction.
• Support a bounded useful-prefix case: reach and challenge a supported intermediate relation before an unsupported suffix/oracle, extract the original input, then let [TS PBT] Confirm, classify and shrink symbolic property and hypothesis witnesses #353 run the complete original TypeScript property. Unsupported prefixes remain unsupported; no fabricated state after an unknown call.
• Never use empirical observations as a proof of infeasibility or universal helper contracts. Search restrictions and approximate projections carry scope/provenance.
• Extend machine observers/targets only as needed; no parallel symbolic engine or generic expression platform.

Definition of Done

• Real frontend fixtures map and challenge input/result, pre/post and guarded intermediate relations.
• JavaScript special-value and context mismatches are rejected or faithfully represented.
• Ambiguous/stale/missing mappings cannot guide an allegedly exact symbolic challenge.
• A supported-prefix candidate is checked by a full concrete oracle, with hypothesis refutation distinguished from original property failure.
• Unsupported execution, UNKNOWN, timeout, extraction failure and reached-target metadata survive independently.