[TS PBT] Provide campaign controls, shared budgets and extensible run artifacts #354

Part of #345. Depends on #353/#384. Supplies the common campaign shell and controls; #355 owns the repeated observation-driven feedback algorithm.

Goal

Provide one reproducible command and artifact contract for direct PBT, direct symbolic search, sequential control and the full feedback configurations, with identical original property semantics and accountable budgets.

Staged delivery

This issue delivers the campaign shell and direct controls before #355 completes the core feedback modes. #405 consumes both implementations using the same deadline, artifact and oracle contracts. Extension configuration/reduction for #400–#403 is implemented and accepted in those issues; no extension is a prerequisite for the shell or pilot. Core and extension results carry an explicit stage/capability label.

Initial controls

• PBT_ONLY: concrete generation plus backend shrinking under the deadline.
• SYMBOLIC_ONLY: original-predicate search plus concrete candidate validation; no random PBT phase.
• SEQUENTIAL: concrete campaign followed, when appropriate, by original-predicate USVM search, replay and reduction. Preserve found violations without requiring another engine. Use this explicit name in reports; legacy HYBRID, if retained, is documented as an alias for SEQUENTIAL.
• Unsupported phases can be skipped with capability diagnostics; definition errors stop the affected property. No semantic substitution on failure.
• Preserve optional coverage and observations from the actual PBT run. The controls do not consume them as search feedback.

Shared extension boundary

• Reuse property IDs, source/tool hashes, tagged values, run results and existing CLI options. Add a small mode/round/target record rather than a generic plugin framework.
• [TS PBT] Integrate the core iterative property-observation feedback loop #355 registers COVERAGE_FEEDBACK, RELATION_FEEDBACK and COMBINED_FEEDBACK and repeated-round execution using [TS PBT] Schedule assertion, coverage and hypothesis targets under one budget #399. [TS PBT] Search bounded generator choices while preserving dependent input structure #400, [TS PBT] Guide relational and metamorphic properties across multiple executions #401, [TS PBT] Reuse bounded command models and state invariants in hybrid search #402 and [TS PBT] Challenge context-scoped observed function summaries during symbolic search #403 add explicitly reported supported configurations.
• Record original property/assertion, generator support, observation requests, phase/round, origin engine, source point, target/hypothesis, input provenance, coverage granularity and all replay outcomes.
• Concrete values must be consumable by inference/mapping without rerunning PBT. Selected returned seeds and bounded neighborhood-generation decisions are recorded separately from mere explicit replay.
• Unsupported observation/coverage/shrinking capabilities remain partial capabilities, not fabricated data.

Budgets

• One monotonic total deadline per property/campaign with declared bounded rounds and phase caps; reserve concrete validation time before symbolic work.
• Include relevant startup/frontend/adapter work, instrumentation, inference, mapping, search, replay and shrinking. Report one-time reusable setup and cold/warm assumptions consistently.
• Allocation may transfer unused time within the total deadline. Adaptive changes belong to a named scheduler policy and are frozen before final evaluation.
• Bound observation storage, candidate queues and returned-seed corpus; record truncation and stop reasons.
• Fixed seeds do not promise deterministic timeout-limited solver behavior. Record actual tool/runtime/backend versions, settings and task revisions.

Definition of Done

• One command runs the three controls over the same examples and exposes a documented integration path for [TS PBT] Integrate the core iterative property-observation feedback loop #355 and the bounded extensions.
• Full feedback mode wiring is tested with its owning implementations; this issue may complete its shell/control contract before those mechanisms finish and cannot close [Epic][TS PBT] Build and evaluate a property-aware PBT–USVM feedback system #345 by itself.
• No-feedback/no-coverage/no-observation/no-shrinking cases remain valid controls.
• Violation, hypothesis-only refutation, no finding, timeout, unsupported, invalid property and infrastructure failure stay distinguishable.
• Artifacts retain unconfirmed candidates and confirmed originals when replay or shrinking cannot finish.
• Focused end-to-end and deadline tests exercise the real concrete backend; reproduction commands and result schema are documented.