[TS PBT] Bind one-time observed relations to exact symbolic challenges #398

Scope agreed on 2026-10-16

One concrete PBT generation phase is followed by one USVM search phase. No return to random generation is required. Concrete replay and optional shrinking validate a USVM candidate; they are not a second PBT generation phase. This replaces the previous repeated-round acceptance.

Existing implementation

#543 provides adapter-owned numeric entry focus. The published follow-up PRs listed below add standalone entry refutation and an explicit numeric local/result point; retain the unfocused original-objective alternative. Arbitrary observation/heap binding remains outside the supported subset.

Bounded delivery acceptance scope

• Reuse source normalization and input bindings. Bind selected operands to exact entry slots or one supported explicit result/intermediate point with source, call-site and temporal identity.
• Add an auxiliary refutation target: declared domain AND original admitted precondition AND reach(point/context) AND NOT(observed relation). Preserve any supported guard.
• Keep this auxiliary target distinct from NOT(original property). Its concrete witness may refute the relation while the original property holds.
• Preserve the original input for full native oracle/check validation through [TS PBT] Confirm and shrink witnesses from two-phase property search #353. No isolated-helper outcome can stand in for the original public property.
• Keep EXACT, AMBIGUOUS, UNMAPPED, UNSUPPORTED and stale bindings explicit; unverified executable/body identity must not be called exact.
• Leave unsupported aliases, nested invocation matching and arbitrary heap bindings outside the declared subset. No summary-substitution engine or cross-round session is required.

Acceptance

Real frontend/native fixtures cover entry relations and at least one explicit result/intermediate relation, including a passing original-property hypothesis refutation and an original-property violation. Changed source, wrong point/time/context and unsupported values cannot activate exact guidance. #399/#355 combine enabled challenges with a bounded unrestricted original-objective share in the same USVM phase.

Delivery status (2026-10-17)

The bounded entry and explicitly captured numeric local/result paths are published: #576 (standalone entry refutation), #580/#584 (capture and exact local binding), #590 (local refutation), #596 (selection), composed in #602 and scheduled once by #603. Compiler-owned local capture remains typed in-memory authority; source hashes cannot reconstruct it. Unsupported executable prefixes, wrong context/point/time and stale source remain exclusions.

#610/#611 are integrated in frozen local assembly c447392006cb72b06ead3d857b639a23d7e259c9; 42 focused integration tests passed. Final actual-budget scalar cells retain exact challenges, official original confirmations and distinct passing-hypothesis refutations. The actual failure is original named check receipt at mutant input 417 (result 415), while the observed bound predicate stays true. The correct variant returns 416 and holds under the full original oracle even though the learned equality fails.

This establishes the supported entry/local binding contract, not arbitrary heap binding, nested invocation matching, helper-body proof or comparative research value. The completed independent prefix/native diagnostic reaches the same input without the learned equality, so #404 must not attribute the scalar result to observations alone. All implementation PRs remain open for user review/merge.