[TS PBT] Prioritize original-property, uncovered-edge and optional relation goals in one USVM phase #399

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

#524 transfers admitted concrete edges into the original-property analysis, uses #526's selector, retains covered prefixes and allocates at least half of turns to the original BFS objective. Keep this implementation; do not replace it with a generic scheduler framework.

Remaining work

• Integrate the initial PBT evidence snapshot through [TS PBT] Integrate one PBT evidence phase followed by guided USVM search #355 under [TS PBT] Run two-phase campaigns with shared budgets and result artifacts #354's single deadline.
• With [TS PBT] Infer bounded numeric hypotheses once from PBT observations #397/[TS PBT] Bind one-time observed relations to exact symbolic challenges #398 explicitly enabled, schedule exact one-time relation challenges alongside original-property and edge goals. Keep target roles, scope and outcomes separate.
• Do not turn sampled relations into universal assumptions. Record any focused query and retain a positive bounded unrestricted original-property allocation.
• Remove only natively confirmed covered goals. Failed replay, UNKNOWN, model limitations and unsupported prefixes remain incomplete outcomes, not global infeasibility proofs.
• Bound retries and avoid repeatedly spending the budget on a target whose supported execution cannot reach it. Keep the diagnosed PGOrbit unsupported-prefix case in the regression plan; use [TS PBT] Preserve runtime limitation reasons in property-search results #555's diagnostics rather than silently discarding it.
• Reuse existing deterministic selection, deadline and trace mechanisms. No new public round/revision protocol, adaptive-policy project or persistent query cache is required.

Acceptance

Independently changed admitted PBT edges change the selected symbolic work. An enabled exact relation independently changes its challenge. Original-property search survives covered code, misleading relations, failed replay and unusable targets. The complete decisions and elapsed costs remain inspectable. No second PBT generation phase is required.

Delivery status (2026-10-17)

The existing admitted-edge transfer and core selector delivery are retained; selector policy remains owned by its separate executor and is not changed by this update. The PBT integration work publishes one-time optional exact relation scheduling in #603 on dependency composition #602. Each selected relation is challenged at most once; complete target roles, decisions, source-qualified confirmations and elapsed allocations remain in relationGuidance. A timely native original fault ends auxiliary work and prevents a redundant original query.

Coverage-only and bounded relation fixtures are integrated in a local common assembly. A 100-input public regression also identified the retained-observation sampling gate tracked under #397; its verified correction is published as #610 before full-budget relation comparisons. Passing auxiliary witnesses require exact official replay receipts before experimental coverage credit. These are open PR/integration gates, not evidence of a merged implementation or comparative gain. No second random-generation phase, adaptive policy or new selector change is introduced here.