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

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.
• Already covered edges remain searchable: coverage does not summarize data states, path combinations or property correctness. 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.