Run frozen public PBT comparisons with checked class coverage

[CaelmBleidd]

Add a reproducible experimental driver over the public PropertyCampaignRunner: one command freezes cases/build inputs and runs PBT_ONLY, SYMBOLIC_ONLY, SEQUENTIAL and COVERAGE_FEEDBACK; another regenerates the CSV from retained process records and raw native replay receipts. Original classes are never rewritten for frontend admission. Real/artificial/mutant/correct populations, seeds, sources, class statement universe, runtime dependencies, allocations and capture bounds are declared before treatment outcomes.

Each cell charges preparation, runtime verification, JVM/frontend startup, campaign execution and original/counter scenario replay to one outer deadline. Late native output is retained without credited hits. Preflight support, runtime limitations, timeouts, failures and omitted/unsupported inputs remain explicit. Primary coverage requires the same frozen class denominator, matching native scenario observations and complete checked input capture; other coverage remains a lower bound. PBT replay preserves the original input sequence in one process, while symbolic fixed inputs use isolated module instances inside one batch process.

The included small correct control is functional evidence only: the existing observation export supports at most 64 retained invocations, so this fixture fixes a 12-run PBT quota. The table records quota exhaustion explicitly. It does not establish a full-budget comparative study or measured advantage of coverage feedback over the sequential control. A separate compact input export is needed before larger equal-budget campaigns. No issue is closed by this smoke fixture.

Stacked on #585 at 8045533e76d1c4d2e916bb6248b2c4bed8a12553; own diff: 5 files, +566. Only the own commit should move after dependencies are merged. No path selector, retained session, generation return loop or README is added.

Validation: three Python orchestration regressions and three native replay regressions passed; the JSON/preflight real-backend tests and main/test Detekt passed. An installed-distribution four-cell smoke retained all inputs and checked native class coverage: PBT_ONLY 4/5, SYMBOLIC_ONLY 5/5, SEQUENTIAL 5/5, COVERAGE_FEEDBACK 5/5. Accountable times were 3.667s, 9.088s, 9.970s and 9.948s under a 30s ceiling; all cells had zero omissions. Separate native batch costs were 354–389ms on this development fixture. CSV regeneration from the raw receipts also passed. The first invalid-limit/restricted-process run remains separate failed evidence locally.

Run:

python3 usvm-ts-fast-check/scripts/pbt_experiment.py run usvm-ts-fast-check/experiments/two-phase-smoke/manifest.json <new-output-directory> --distribution usvm-ts-fast-check/build/install/usvm-ts-fast-check --adapter usvm-ts-fast-check/fast-check-adapter
python3 usvm-ts-fast-check/scripts/pbt_experiment.py summarize <output-directory>