[TS PBT] Transfer exact admitted c8/EtsIR edges into one USVM search #382

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

#409 is merged: supported original TypeScript if arms are mapped to ordered EtsIR successors, with unsupported/ambiguous constructs kept explicit. #524 implements admitted coverage transfer and evidence-sensitive exploration in the original-property search.

Remaining work

• Accept and integrate [TS PBT] Guide original property search with admitted edge coverage #524 with its core dependencies [Util] Fix cached priority ordering after insertion #538/[TS] Reuse closest-to-uncovered NURS for external coverage #526 and [TS PBT] Integrate one PBT evidence phase followed by guided USVM search #355's single PBT-to-USVM handoff.
• Keep source/property/runtime identity, phase/admission checks and the wrapper/precondition/shrinking separation.
• Retain true-only, false-only, mixed, nested and if-without-else fixtures. Saturated statement coverage with an unvisited edge must still produce the appropriate edge goal.
• Preserve exact statement mappings when a branch cannot be mapped. Missing coverage is not evidence that every edge is uncovered.
• Incorporate the checked local performance fixes: source paths are cached for one mapping, and initial guidance maps one report once. The single-report fix is now based on [TS PBT] Guide original property search with admitted edge coverage #524 without [TS PBT] Preserve a shared incremental search session across feedback rounds #481/[TS PBT] Retain original-property search across native coverage updates #549.

Acceptance

One real PBT run changes the next selected symbolic path through exact edge evidence. Covered prefixes remain traversable and original-property search continues after edge saturation. No second PBT generation round or public retained-session API is required. This issue can close on that integration rather than waiting for unrelated research extensions.