Repository navigation
[TS PBT] Project observed relations and assertion goals into exact EtsIR bindings #398
Description
Current state (2026-10-14)
Audited against usvm main at 19866c959d.
Original entrypoint/domain mapping and exact supported source coverage mapping are implemented. There is no completed observation-point/hypothesis challenge projection path.
Remaining acceptance boundary
Bind each observed value/relation/assertion to the exact EtsIR point, invocation and source/context revision; generate challenge targets and replay at the same point. Distinguish unsupported/stale/ambiguous bindings and never substitute entrypoint coverage for intermediate relation semantics.
Original-property-directed feedback clarified on 2026-10-14
The primary supported analysis executes the original entry point and searches:
declared support AND admitted precondition AND original path constraints AND NOT(original property/check).
PBT feedback must change exploration within that analysis, not only select a separate easier predicate. A focused query may additionally require reach(edge/point/context) when the complete relevant symbolic suffix is supported. Keep this focus explicit and retain the configured unfocused original-objective share.
- Emit original-failure, coverage-exploration and hypothesis-exploration goals with distinct roles and original named-check identity.
- Auxiliary hypothesis goals use exact original reach/value/time/call context and
NOT(hypothesis); the hypothesis is never silently assumed true. - A direct call to an internal helper requires an explicitly justified equivalent entry/context binding. Ordinary source-line matching or eventual native rejection is not that justification.
- For a supported-prefix/unsupported-suffix case, report the auxiliary target and symbolic boundary. The full original oracle still runs concretely; no original-property symbolic suffix is fabricated.
- Integrate binding updates into [TS PBT] Preserve a shared incremental search session across feedback rounds #481's shared work; changing a formula/context invalidates dependent goals and cached decisions.
- Acceptance independently varies PBT evidence and demonstrates changed symbolic state/path selection while keeping the original property/check unchanged. A changed auxiliary query list alone does not satisfy this requirement.
Original report and acceptance context, retained for traceability
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.
Activity