[Epic][TS PBT] Deliver PBT evidence followed by guided USVM search #345

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.

Agreed execution model

1. Run concrete PBT once over the original declared property/support.
2. Retain its bounded inputs, outcomes, requested observations and admitted source coverage.
3. Run USVM over the original domain/precondition/property, using that fixed evidence to guide exploration.
4. Validate USVM candidates by executing the complete original TypeScript oracle; reduce eligible witnesses without changing their target.

Single-input replay/shrinking is validation, not renewed random PBT generation. Empirical relations never become proved contracts. No second PBT round, public cross-round session, returned-input generation, round/revision framework or general scheduler platform is required.

Already in main

Property/domain definitions, fast-check execution, per-property coverage, exact supported c8 if-arm mapping (#409), original domain/precondition/property search (#387), original assertions/joint support (#407), bounded observations (#411), plain-object support (#473), and the Kotlin DSL (#499). Reuse this code.

Keep the implemented open PRs

The scoped path cache is published as #565 (1eaf7754361e) with green CI. Initial-report mapping without retained sessions is preserved in #569 (46fdda2ee within that composition PR), replacing the session-dependent local variant d67c06af5 for the product path. The original checked local commits remain recoverable, and the historical experiment checkout remains pinned and unchanged.

Outside the current project

#481 and PR #549 (cross-round retained property search), plus PR #547 (returned-input neighborhood generation), are outside this delivery. Their unmerged implementation remains recoverable and no required open PR depends on them. #400-#403 are not planned: native generator-choice search, a dedicated multi-execution engine, a command-model framework and context-scoped helper summaries are outside the agreed delivery. Ordinary multi-call properties, existing joint support and bounded same-receiver wrappers remain usable.

These closures do not claim that the old features were completed. Experimental evidence and commits remain recoverable; there is no need to delete unrelated merged engine infrastructure.

Dependency, review and measurement order

1. Land the small useful changes. Review separately owned [Util] Fix cached priority ordering after insertion #538/[TS PBT] Guide original property search with admitted edge coverage #524 against their exact current parents; [TS] Reuse closest-to-uncovered NURS for external coverage #526 is already merged. The scoped mapping/cache fixes are published. This does not authorize selector-policy changes in this task. Review the replay/control stacks in their existing dependency order. Do not merge from an agent without the owner's separate request.
2. Review the published public two-phase path. [TS PBT] Run two-phase campaigns with shared budgets and result artifacts #354/[TS PBT] Integrate one PBT evidence phase followed by guided USVM search #355 share one deadline and evidence artifact; [TS PBT] Confirm and shrink witnesses from two-phase property search #353 preserves automatic DSL check identity through native validation. No random PBT generation occurs after the handoff.
3. Review separate real-program support and preserve its limits. [TS PBT] Preserve runtime limitation reasons in property-search results #555 runtime limitation reporting is published through [TS PBT] Preserve runtime limitation diagnostics in property search #560/[TS PBT] Retain residual unknown-call diagnostics in property results #608. [TS] Retain classes with supported constant computed member names jacodb#447 retains classes with supported constant computed names. [TS] Support array growth and sparse slots #388 owns sparse indexed growth. After each narrow fix, replay the previously frozen failing scenario; create further semantic work only from a remaining reproduction.
4. Review the published one-time property-observation guidance. [TS PBT] Infer bounded numeric hypotheses once from PBT observations #397/[TS PBT] Bind one-time observed relations to exact symbolic challenges #398's bounded numeric relation/result binding and [TS PBT] Prioritize original-property, uncovered-edge and optional relation goals in one USVM phase #399's original/edge/relation allocation are published and composed in Compose published relation consumers with the public PBT campaign #602/Guide one USVM phase with bounded empirical relation challenges #603, with [TS PBT] Keep complete bounded samples usable for relation guidance #610/Account for checked auxiliary inputs in PBT experiments #611 usability and receipt checks. No repeated inference or cross-round invalidation is required.
5. Validate and measure. [TS PBT][Checkpoint] Validate the two-phase handoff and assess its measured value #405 checks the one-way public handoff; [TS PBT] Prepare real and artificial benchmarks for the two-phase analysis #356/[TS PBT] Compare two-phase evidence-guided USVM with equal-budget controls #357 provide frozen real/artificial cases, equal total budgets, multiple predeclared seeds, checked per-class coverage and fault outcomes. Keep negative and unsupported results.
6. Assess the research claim. [TS PBT][Research] Assess and report the two-phase property-guided analysis #404 compares nearest work and writes only claims supported by the measurements.

Historical implementation status: published consumer route (2026-10-16)

• Core [TS] Reuse closest-to-uncovered NURS for external coverage #526 is merged into main. [Util] Fix cached priority ordering after insertion #538 and the selector-owned [TS PBT] Guide original property search with admitted edge coverage #524 remain separate review work; their implementation was not rewritten by the campaign consumer.
• Existing [TS PBT] Persist direct campaign results with existing evidence #542/[TS PBT] Run direct campaign controls from the existing CLI #545/[TS PBT] Record scoped campaign metadata and observed Node versions #548 timeout/CI repairs are published and all checks are green at the verified heads. [TS PBT] Preserve runtime limitation diagnostics in property search #560 runtime limitation diagnostics, [TS PBT] Cache source resolution within each mapping #565 scoped source caching and [TS PBT] Confirm DSL candidates without random regeneration #566 automatic native DSL confirmation are open PRs with green CI. JacoDB #448 is also green; the safe USVM signature consumer/pin remains separate work.
• The small consumer route is [TS PBT] Compose campaign artifacts and existing edge guidance #569 -> [TS PBT] Retain confirmed DSL faults before symbolic preparation #571 -> [TS PBT] Use native witness results for coverage feedback #572 -> [TS PBT] Run one PBT phase followed by coverage-guided USVM #574: compose portable artifacts/deadlines and single initial mapping; retain confirmed concrete DSL faults; accept typed native witness evidence without PBT fallback; expose one PBT phase followed by coverage-guided USVM through the existing runner/CLI/artifact. Exact frozen dependency parents and own/inherited diffs are documented in the PR bodies. These are published PRs, not merged main functionality.
• Local consumer checks passed: real PBT evidence changes the next symbolic work for the same property; covered prefixes stay traversable; saturated coverage still finds an original defect; native replay does not restart random generation; timeout/stale-source/replay failure remain explicit; checked trace and runtime diagnostics survive artifact roundtrip. The adapter suite passed 216 tests. This is functional evidence, not a comparative coverage win.
• [TS] Preserve analysis work across bounded phases #546/[TS PBT] Generate native integer neighborhoods from returned inputs #547/[TS PBT] Retain original-property search across native coverage updates #549 are closed without merge as unnecessary under the agreed scope. [TS PBT] Preserve a shared incremental search session across feedback rounds #481 and [TS PBT] Search bounded generator choices while preserving dependent input structure #400-[TS PBT] Challenge context-scoped observed function summaries during symbolic search #403 are not planned. No returned-input generator or retained cross-round session is reintroduced.
• [TS] Reject unrepresentable sparse and boxed array observations #567 sparse witness admission is now green at ff1d26cb3d19 after its regression fix. It is separate from [TS] Support array growth and sparse slots #388 engine sparse-growth work.
• Later published work now supplies completed symbolic input capture, native class replay and the optional relation coordinator; see the 2026-10-17 status below. The bounded-observation contract and checked auxiliary-input consumption are now published as [TS PBT] Keep complete bounded samples usable for relation guidance #610/Account for checked auxiliary inputs in PBT experiments #611. Remaining work is user-controlled review/merging, including the now published command-boundary fixes [TS PBT] Honor caller cutoff in campaign-file #615/Preserve the experiment caller deadline through campaign startup #616 under [TS PBT] Run two-phase campaigns with shared budgets and result artifacts #354/[TS PBT] Align experiment and campaign-file deadline origins #613, separate engine support, and evidence-backed research assessment of the completed development comparisons. Published PRs are not automatically main functionality.

Current delivery and evidence status (2026-10-17)

The agreed one-PBT-then-USVM model remains unchanged. Path-selector work is owned separately; this update does not change its policy or tasks. No agent merged a pull request into main.

#602 includes the previously published numeric stacks (+5015/-51 against its public-campaign parent); it is a composition review, not 5000 lines of newly added coordinator code. Its body lists the five semantic merge resolutions and the dependency review route. #603 is the separate coordinator diff. Review prerequisites and their exact heads first; leave merging to the owner.

Published implementation and remaining review / research

The core one-PBT -> USVM path is implemented in published open PRs. The installed-command publication and caller-deadline fixes are published as #614/#615/#616 under #354/#612/#613, with user-controlled review/merge still pending. Published implementation is not merged-main functionality and does not establish comparative benefit. No repeated-round/session/returned-input framework is required. Selector policy remains separately owned.

• Usable bounded empirical samples ([TS PBT] Infer bounded numeric hypotheses once from PBT observations #397/[TS PBT] Prioritize original-property, uncovered-edge and optional relation goals in one USVM phase #399): published [TS PBT] Keep complete bounded samples usable for relation guidance #610. Exact head f2c97a664f31cde9167fdb1ca04fe8e12f04ad1a keeps valid complete retained invocations usable as finite samples despite later recorder truncation. Dropped counts and INCOMPLETE_CAPTURE remain visible; missing/corrupt/repeated/ambiguous point evidence is not relaxed. A public 100-input regression fails on the clean prior base and passes with this change; 77 focused Kotlin and 50 native tests passed. In the current budget-driven campaign, thousands of PBT invocations now produce real one-time relation challenges without reducing the generation quota to a capture limit.
• Checked auxiliary metric consumption: published Account for checked auxiliary inputs in PBT experiments #611. Exact head ec2a4dc5a8f52781fb3cdbcc8aa56cb3ab63a994, two Python files, consumes timely exact official original-replay receipts from result.relationGuidance.attempts. It verifies source/manifest/context/binding/selected-target identity and admitted native coverage, retains the original candidate rather than reduction inputs, and distinguishes passing hypothesis refutation from an original named fault. Fifteen Python tests plus 19 adversarial variants of actual public artifacts passed. The positive original-HOLDS coverage receipt, canonical named original fault with a HYPOTHESIS role, and negative 5-second coverage-converter timeout are preserved. Raw/late/mismatched/unconfirmed candidates never gain coverage credit.
• Current local integration and review boundary. Final isolated assembly c447392006cb72b06ead3d857b639a23d7e259c9 includes [TS PBT] Keep complete bounded samples usable for relation guidance #610/Account for checked auxiliary inputs in PBT experiments #611 over the earlier frozen common assembly. Forty-two focused Kotlin integration tests, installation and the Python/actual-receipt checks passed. Guide one USVM phase with bounded empirical relation challenges #603/Allow explicitly larger compact input exports without changing default bounds #607/[TS PBT] Retain residual unknown-call diagnostics in property results #608/[TS PBT] Keep complete bounded samples usable for relation guidance #610/Account for checked auxiliary inputs in PBT experiments #611 have all seven CI checks successful at their exact verified heads. The old Run frozen public PBT comparisons with checked class coverage #586 TS check also passed on retry at its unchanged head; its original failure log is retained without an inferred root cause. Open PR implementation, local integration, current CI and merged main are distinct states. Review the documented prerequisite route; no agent merged main.
• Separate engine/runtime work, not missing PBT orchestration. [TS] Integrate computed class members without mixing symbol and string keys #575/[TS] Invoke declared class getters during property reads #577 remain open despite the narrower [TS] Integrate computed class members with distinct symbol identity #578/[TS] Stop unsupported accessor and method-value storage access #595 deliveries; [TS] Support array growth and sparse slots #388's broader sparse-array boundary remains open despite the bounded [TS] Support bounded sparse indexed writes with known own slots #573 support. [TS] Model Float64Array(length) construction instead of an unresolved receiver #604 separately tracks original Float64Array allocation. Do not rewrite original Adder/class bodies or claim arbitrary TypeScript support. SegmentTree/Matrix universe restrictions, Doc nested closures and PGOrbit helper/private-callable restrictions remain explicit. Source/frontend retention is not symbolic runtime support.
• Completed development measurements ([TS PBT] Prepare real and artificial benchmarks for the two-phase analysis #356/[TS PBT] Compare two-phase evidence-guided USVM with equal-budget controls #357/[TS PBT][Checkpoint] Validate the two-phase handoff and assess its measured value #405/[TS PBT][Research] Assess and report the two-phase property-guided analysis #404). Frozen assembly c447392006cb72b06ead3d857b639a23d7e259c9 completed all 108 scalar cells (all eligible under a charged outer 60-second deadline), 18 independent prefix/native attribution diagnostics (all complete), and 144 class cells. The scalar study is one artificial family with six source variants and three fast-check seeds; pure symbolic repeats use the same fixed machine configuration. Relation modes confirm the branching mutant in 3/3 seeds versus 0/3 in the four original-objective controls, but the prefix/native diagnostic reaches the same rare input without the learned equality. Additional learned-observation value is therefore not demonstrated. The class study has 89 full eligible cells and 55 incomplete outcomes, with 14/27 strict four-mode class-by-seed pairs, all zero coverage gain. Mailbox 18/22 on two paired seeds and CircularLinkedList 32/98 on three are the complete genuine-class comparisons; SinglyLinkedList, DoublyLinkedList and CircularQueue have no complete paired seed and receive no zero-gain conclusion. Artificial RingBuffer mutant 11/12 and both ClosedInterval bodies 5/5 are identical across their paired controls. No further tuning, reruns or families followed these outcomes.
• Published command-boundary follow-up ([TS PBT] Run two-phase campaigns with shared budgets and result artifacts #354/[TS PBT] Align experiment and campaign-file deadline origins #613). The frozen class pilot retains 47 external deadline kills, 45 missing-completed-artifact diagnostics, one unterminated JSON, eight saved native-incomplete cells (one also killed), and one Operation-not-permitted cell; counts overlap. The narrow file-before-stdout fix is [TS PBT] Save campaign artifacts before stdout publication #614. [TS PBT] Honor caller cutoff in campaign-file #615 (696e5e9946bb94c94339a1f4d45c6e0860c53736) carries the caller cutoff/publication reserve into the existing runner; Preserve the experiment caller deadline through campaign startup #616 (560b23d494509d726be2a6347e948b45e7dbf1aa) supplies that fixed cutoff, charges process creation and guards native replay credit. They are published open PRs, not remaining unpublished implementation. One separate 30-second delayed-launch functional check saved a valid DEADLINE/CONFIRMATION artifact without an outer kill and correctly withheld credit for 67 unchecked inputs. It does not alter the 270 frozen measurement attempts and diagnostic checks (252 comparative cells plus 18 prefix diagnostics) or establish additional coverage. The publication reserve and IR/filesystem cleanup remain cooperative; no main merge or universal repair of earlier missing artifacts is claimed.
• Coverage population is explicit. The class metric credits original class statements on admitted generation/explicit inputs and checked original symbolic/auxiliary search inputs. It excludes precondition execution, rejected inputs, shrinking/reduction trials, diagnostic calls and wrapper/foreign/model statements. All their costs still consume the declared budget. It is not coverage of every actual PBT invocation. Source-relative original class AST IDs are unioned with one denominator per class; repeat native checks do not create extra generated tests. Raw original/counter/repeated-oracle receipts must agree before timely credit.

Completed actual-budget calibration

Local common assembly 7b184d2a57e01bfee37319d1be7a3a379de1c270 combines the exact published coverage route, current engine/frontend, #603 (44a3f85a5), #607 and #608. Installation and 38 focused integration tests passed. It is a local integration assembly, not merged main functionality.

The first 30-second calibration on original Adder/ring wrappers was ineligible: generic unsupported symbolic calls remained, and the 2 MiB export dropped 9340/10313 PBT inputs. Those receipts remain preserved; they are not erased by the later run.

A support-selected second calibration used real Mailbox FIFO and a separately named indexed-oracle ring wrapper whose source/native parity was checked on 6018 inputs. With 30-second total budgets, seed 37, a 1,000,000 generation quota independent of the capture bound, explicit 100,000-record / 64 MiB export, and charged preparation/native replay, all eight four-control cells completed with zero omissions and zero native mismatches; primary/full-budget eligibility passed. PBT-only retained 8870 and 14404 inputs, with checked class replay taking 1.730 s and 2.259 s. Total accounted time was 24.527 s and 25.715 s. Every mode covered 18/22 Mailbox statements and 11/12 ring statements: the coverage differences were zero.

This calibrates the measurement path for those two 30-second cases. It is one seed, no evidence of superiority, no 60-second capacity validation, and no full-budget relation comparison. Raw artifacts and regenerated CSV are retained locally as pbt-supported-budget-calibration-20261017; the completed development comparison below still does not establish publication-ready superiority.

Historical evidence before the current public assembly

The local 24-cell, one-seed coverage rerun completed with 5,511 checked observations and no native/domain mismatches. PGOrbit's guided 30-second coverage improved from 67 to 78/104; its 120-second coverage stayed 79/104 versus PBT's 102/104. Matrix/SegmentTree did not symbolically execute their selected class. This supports the mapping-performance fix, not a coverage-superiority claim or closure of the public integration tasks.