[TS PBT] Schedule assertion, coverage and hypothesis targets under one budget #399

Implementation status (2026-10-14)

The supported exact c8/V8-to-EtsIR if-arm mapping is implemented on main at 19866c959dcf23d343132c9ab2ee5a3c15d41fe2. It still does not initialize USVM search from admitted PBT edge coverage: UsvmPropertySearcher does not consume mapping.coverage, and the machine creates fresh symbolic coverage statistics.

The first remaining delivery is the coverage-only cooperation slice specified below: choose reliably uncovered edges, preserve covered prefixes, and update the shared set only after admitted original-runtime replay. It can land independently of hypothesis inference or an adaptive scheduler. Keep the original-property objective and the shared validation budget; the later hypothesis/adaptive objectives remain separate integrations. Existing benchmark experiments remain paused.

Implementation child of #355. Integrates #397, #398, #382 and the budget/result boundary in #354.

Goal

Make concrete PBT feedback visibly change symbolic search decisions while preserving the original property objective and fair resource accounting.

First checkpoint policy

The core #355/#405 delivery uses the simple deterministic policy and bounded target queues below. It must independently demonstrate that exact coverage and observed relations change target selection, preserve original-property search, and charge all work to the same total budget. Adaptive scheduling and #400–#403 target kinds are later integrations and are not requirements for core completion.

Scope

• Maintain explicit queues for original assertion/property violations, exact uncovered source/CFG targets, and context-scoped hypothesis challenges. Track target origin, priority, attempts, cost and replay yield.
• Implement a simple deterministic budgeted policy first, with positive allocations for each enabled objective and protection against starvation. Prioritize property-relevant and previously productive goals; deduplicate semantically identical goals.
• Add a measured adaptive policy only as a separate ablation; freeze policy/weights on development cases. Account for infeasible, unsupported and repeatedly unproductive targets.
• Use per-property source coverage from admitted executions when available. Do not treat missing coverage as uncovered; preserve rejected/precondition/wrapper coverage distinctions.
• Edges confirmed covered by admitted PBT executions must be removed from the coverage-target queue. They remain traversable when needed to reach uncovered successors and remain available to original-property/hypothesis search; edge coverage does not prove a property for every input. Continue hypothesis/oracle search after coverage plateaus.
• Reserve replay/shrinking time before launching more search. All inference, mapping, search and feedback rounds share [TS PBT] Provide campaign controls, shared budgets and extensible run artifacts #354's monotonic total deadline.
• Prefer hypotheses as challenge targets or priorities. If experimental hints restrict the declared domain, record the restriction and reserve a positive bounded unrestricted-search allocation within the same budget. Fallback is not a completeness guarantee.
• Emit an auditable decision trace. Coverage-only, hypotheses-only, combined, randomized-target-order and no-feedback controls must share otherwise identical mechanisms.
• Relation mapping and exact branch mapping are separate capabilities; statement-only operation is explicit and cannot satisfy the exact-branch acceptance gate.

Definition of Done

• An exact mapped PBT coverage change changes the selected USVM target; an independently varied hypothesis changes a selected challenge.
• A fixture with saturated coverage still receives property/hypothesis search.
• Misleading hypotheses, starvation pressure, unsupported targets and deadline exhaustion retain an unrestricted/original-objective search share.
• Same configuration/evidence gives reproducible scheduling decisions apart from documented timeout/solver variability.
• Decision and cost artifacts support causal ablations in [TS PBT] Evaluate causal contributions of property-aware feedback and bounded extensions #357; a toy win is not sufficient to claim superiority.

Minimum delivery: PBT edge coverage changes USVM exploration

This is the first independently verifiable slice of this issue. It must work without waiting for hypothesis inference or an adaptive scheduler.

The inspected checkout at USVM commit 19866c959dcf23d343132c9ab2ee5a3c15d41fe2 (2026-10-14) already stores source coverage and maps supported branch arms to explicit EtsIR edges. However:

• UsvmPropertySearcher does not consume mapping.coverage when configuring search.
• TsMachine.analyzeWithMetadata creates fresh CoverageStatistics for each analysis.
• CoverageStatistics currently tracks statements reached by terminated symbolic states, rather than externally confirmed CFG edges.

Collecting or mapping PBT coverage therefore does not, by itself, implement coverage-guided cooperation.

Required behavior:

1. Carry PBT coverage through the actual hybrid entry point into symbolic target selection. Identify each supported CFG edge by its method, source statement and successor/outcome; statement or successor coverage alone must not substitute for edge identity.
2. Initialize the coverage objective with edges actually executed by admitted PBT inputs. Already covered edges are not selected, retried or rewarded as new coverage goals. Target the remaining reliably identified uncovered edges and use that set to guide exploration, rather than filtering duplicate results only after an independent full search.
3. Keep covered prefixes traversable: a covered edge can be on the only route to an uncovered successor. Remove it as a coverage goal, not from the control-flow graph. This requirement does not disable explicit property-violation or hypothesis goals within already covered code.
4. Accept exact compatible evidence only. Preserve property/domain/source/runtime identity, rejected-input and wrapper distinctions, and unknown/ambiguous/unsupported edge statuses. A missing report or an unrecognized branch record is not evidence that an edge is either covered or uncovered. The real c8/V8 path requires [TS PBT] Integrate exact c8/EtsIR edge feedback into target selection #382; supported binary records alone do not satisfy that end-to-end gate.
5. Replay symbolic candidates in the original TypeScript runtime. Update the shared edge set only after concrete execution confirms the claimed new edge on an admitted input, then remove that edge from subsequent coverage queues. A symbolic reachability claim or failed replay must not mark an edge concretely covered.
6. Record the initial PBT edge set, pending coverage goals, selected edge, replay-confirmed additions and remaining goals. When no known uncovered edge goals remain, stop that coverage objective and report its scope; retain the configured original-property/hypothesis objectives.

Acceptance:

• A real PBT run covers one outcome of a supported branch. USVM selects the other edge as its coverage goal; the PBT-covered outcome is absent from the coverage-target queue.
• Independently changing only the PBT edge evidence changes the selected goal or removes it entirely. Storing a different report with an unchanged search plan fails this check.
• A fixture whose statements are all covered but whose if without else has an unvisited outcome still gets a target for that missing edge.
• A nested fixture reaches an uncovered edge through a previously covered prefix. Replayed additions are removed from the next round; a failed/mismatched replay leaves the target uncovered.
• Fully covered, absent, stale and unsupported evidence have distinct results. No remaining coverage goals produces no redundant coverage search; explicit property search stays available.

Existing experiments remain paused. Focused implementation and integration checks for this slice are separate from restarting a benchmark campaign.

Shared original-objective exploration clarified on 2026-10-14

#481 owns retained work; this issue owns priorities and bounded allocations. Policy can be tested against the session contract before #355's full loop completes.

• Apply confirmed PBT evidence to the pending symbolic state/path selection of the original-property analysis. It must change where USVM next searches for NOT(original property/check), not merely append a separate coverage/helper run.
• Auxiliary coverage/hypothesis goals remain separately identified, budgeted and concretely confirmed. Retain the original entry/support/precondition/check for all claims about the main objective.
• Remove confirmed covered edges from coverage goals while preserving necessary covered prefixes and property search in covered code.
• Schedule using accumulated session evidence and previous scoped attempts. An unchanged semantic query/result must not be reissued solely because a new round started; UNKNOWN/timeouts follow an explicit budgeted retry policy.
• A fresh PBT evidence delta between two symbolic advances must demonstrably change the second advance. Emit evidence revision, affected pending work, selected state/goal, reused work and cost.
• The acceptance fixture holds the original predicate, template vocabulary and total budget fixed while independently changing evidence. Also exercise fully covered, insufficient relation evidence and misleading-hypothesis cases.