[TS PBT] Preserve class verification after expected PBT budget expiry

Start with the #616 guard in pbt_experiment.py:512-522 and compare its exit-code handling with PropertyCampaignRunner.kt:200-219 and CampaignCli.kt:54-68. Read PRs #619 and #620 to see the published implementation and its focused regressions; verify the typed timeout and evidence checks against the acceptance criteria. Done means timely expected PBT-budget timeouts with complete captured inputs can attempt existing native verification, while omissions, invalid evidence, late or killed runs remain ineligible and coverage requires timely qualified replay receipts.

The class experiment caller rejects every campaign exit 2 before attempting native class-coverage verification. However, exit 2 also represents an expected PBT time allocation ending with a complete captured prefix. This conflates search completeness with the integrity and verifiability of saved inputs. Keep the timeout disposition, but allow qualified completed inputs to reach the existing verification path.

The completed 48-cell diagnostic pilot used assembly d6564365fc48edd43f81713421c110adbd358334. Two inspected examples under class-results demonstrate the mechanism:

• real-mailbox-fifo/20261018/PBT_ONLY: exit 2, timedOut=false, runner elapsed 17,908 ms versus a 19,227 ms post-spawn allowance, and no total-budget overrun. The artifact reports DEADLINE/PBT, a concrete timeout and 13,003 completed runs. Its export contains 13,003 records with zero dropped, unsupported or pending inputs; every stored omission counter is zero.
• sup-loiane-circular-list-removal/20261018/COVERAGE_FEEDBACK: exit 2, timedOut=false, runner elapsed 10,780 ms versus a 19,689 ms allowance, and no overrun. The artifact reports COMPLETED, symbolic NO_VIOLATION_REACHED and no symbolic diagnostics. The PBT allocation timed out before symbolic execution continued. It retains 2,367 input records, one symbolic replay and zero stored omissions.

Both cells report analysisSupported=true, but no class replay request is created: nativeReplayMillis=0, coverage remains unverified and primary eligibility is false. These are not measured zero-coverage outcomes.

The typed mechanism is explicit in the current code. PropertyCampaignRunner.kt:200-219 returns DEADLINE for an unpartitioned PBT timeout, or continues after a partitioned PBT timeout. CampaignCli.kt:54-68 returns 2 unless the campaign meets its complete-success conditions or confirms a property violation; a concrete timeout and its phase diagnostic prevent exit 0 even when symbolic execution later completes. The #616 guard in pbt_experiment.py:512-522 accepts only exit 0 or exit 1 with a confirmed original violation, then raises before native replay.

The inspected request/artifact controls, source roots, declared properties and verified export-source hashes agree, allowing for serialization defaults. The prepared class universes are supported with the SCENARIO_OBSERVATIONS boundary. The inspected driver matches its frozen hash. This issue does not attribute every ineligible pilot cell to this guard.

Acceptance:

• Separate timely process/artifact integrity from semantic search completeness. Existing CLI exit-code compatibility may remain unchanged.
• For structured expected PBT-budget timeouts with complete captured prefixes, allow an attempt at native verification using the existing source/runtime identities, capture checks and class universe. Do not match human diagnostic text or declare the search successful.
• Preserve all omission and unchecked-input checks. Unknown, unsupported, execution/contract failure, missing/invalid/mismatched artifacts, late publication, outer timeout or killed processes remain ineligible.
• Keep the same absolute total cutoff and replay reserve. Grant coverage only after actual timely, source-qualified original/counter replay receipts establish equivalence. Do not reset or extend any budget.
• Add focused regressions for the two expected-timeout cases and the rejected cases above.

Whether these omitted replays would finish within the remaining eight-second reserve or pass verification is unknown. No recovered coverage or improved eligibility is claimed. The pilot and earlier frozen data remain unchanged; assess any correction in a separately frozen follow-up.

Related: #613, #616, #354.

Published implementation and separate local admission check (2026-10-17)

The implementation is published in two open PRs and is not merged into main:

• #619 at 0b1ccf84dc19c519af5a0ef7028fd2ab17f40c33, based on #616: distinguish typed budget outcomes from invalid evidence; permit class replay only after request/artifact/source/runtime-command checks, zero omissions, matching completed input sets and grouped predictions. The original DEADLINE/TIMEOUT status remains visible. Timely native original/counter receipts determine coverage credit.
• #620 at 2239eb0dc471b0155821d568fa8928a8230f4c98, based on #615: validate newly captured passing symbolic inputs during search and reuse the existing same-phase replay cache. Search and validation retain their shared deadline; failing predictions remain on the canonical original-confirmation path.

The caller has 23 focused Python tests, including three regressions that fail on the previous #616 head. The native change has 33 focused tests and strict main/test Detekt checks in both modules. Independent review accepted both changes. All seven CI checks passed at each exact public head. The composed modern Python harness independently passed 35 tests.

A separate, frozen local admission check used assembly e1826f390843d52314dee41eb2b440bea2edc36b, combining these fixes with the existing compact capture, auxiliary verification and source-qualified native receipt checks. It covered the declared Mailbox, CircularLinkedList-removal and SinglyLinkedList-wide scenarios, four controls and two configured generator seeds: 24/24 cells admitted, giving six complete four-mode comparisons.

An independent raw audit verified input order/counts, original/counter oracle and scenario observations, statement hit sets, exact class universes and class unions. All 70,251 native input records verified: 70,245 HOLDS and six FALSE. These are replay records, not independent programs or defect counts. All seven omission counters were zero; no outer kills, queue errors or accounted budget overruns occurred. Post-checks matched all 1,440 runtime pins and 17 input pins, with sources preserved. The plan SHA-256 is c8438f654a0fe8290bfc9780136474103fbbfa839134c0955b665343572dd89b.

This establishes local admission for those three declared scenarios under that fixed protocol. It does not establish broader class support or a coverage/performance advantage. The earlier frozen pilot remains unchanged and was not rescored; its unattempted historical replays are not retroactively credited. This issue remains open for user-controlled review and merge of the published PRs.