[TS PBT] Retain original-property search across native coverage updates

[CaelmBleidd]

Withdrawn on 2026-10-16

Cross-round retained property sessions are not needed for one PBT evidence phase followed by one USVM search. Do not merge the public session/late-PBT-update layer. The useful initial-report mapping fix has been detached from this branch as local commit 42dfc324d on #524.

The project owner changed scope; the authoritative plan is #345. This PR is closed without merging and does not establish completed delivery of the former task. Keep the historical experimental snapshots reproducible.

---

Repeated property searches previously rebuilt the symbolic analysis, losing its pending queue and completed work between native PBT runs. UsvmPropertySearcher.openSession() now prepares the original manifest, mapping, domain projection, observer, queue and solver resources once. advance(maxSteps) continues that analysis, and applyCoverage(nativeArtifact) updates the existing coverage selector without rebuilding the frontend or initial states.

search() remains the one-shot wrapper. A yielded phase reports IN_PROGRESS, retaining any already found candidate input and violation target. Partial unsupported paths keep their diagnostics while pending work continues. A valid initial admitted-native coverage report anchors later updates; stale, incompatible, unsupported and no-admission reports have explicit rejection outcomes. The manifest and native environment collections are snapshotted. A change to the current source invalidates the session and closes its resources, even if the source is subsequently restored. Coverage changes priorities only; it never adds path constraints or drops covered prefixes.

This is the retained original-property session and native-coverage update slice of #481. Campaign scheduling and hypothesis transfer remain separate. Analysis-wide limits stay cumulative and a finished analysis stays finished.

The PR is stacked on #524 at be0b569f6e8a1f7fe00665b29345d6fb11c94849. Its final head is c3ce550489f13b2200b406f77cde471bcb516552. The 22-file branch diff has three distinct parts:

• Already merged main ancestor [TS] Make string models cheaper for symbolic execution #525, b29e7d07edb12d12b4dfd511efbb6d2cf1e3d5a0: 10 inherited string-model files, +461/-58. The [TS PBT] Guide original property search with admitted edge coverage #524/[TS] Reuse closest-to-uncovered NURS for external coverage #526 branch point predates that main commit.
• Independent core dependency [TS] Preserve analysis work across bounded phases #546, 25f663469ad27929f41fe55146b8736762465210: three inherited files, +577/-73. It is integrated by a real merge with that exact second parent, not copied or cherry-picked. Merge resolution preserves [TS PBT] Guide original property search with admitted edge coverage #524's selector factory and caller deadline in the new helpers/stop gate and shares the two identical finished-analysis constructions.
• The PBT consumer commit c3ce55048: nine files, +690/-44; 366 added lines are tests/fixtures. Review this commit for the consumer itself. The merge parent is d0fe052be21985cf89c87173f616f2c0ce31eedf.

The selector chain inherits #524/#526's separate cached-priority ordering prerequisite #538. Merge that queue fix before using the chain.

Validation on Zulu JDK 11.0.32.1, Node 22.23.1 and npm 10.9.8:

• Both PBT/FastCheck check tasks passed: 204 PBT Kotlin tests, 113 FastCheck Kotlin tests and 204 Node tests, with zero failures/skips.
• All nine TsAnalysisSessionTest tests passed on the integrated core, covering retained initialization/queries, cumulative limits, lifecycle ownership and phase snapshots.
• Final strict Detekt for the TS integration files, PBT main sources and FastCheck tests passed with ignoreFailures=false and no findings. All seven new session tests passed again after the formatting-only lint corrections. git diff --check passed.
• The paired native-evidence fixture starts from the same property and first phase with three pending state IDs. Real FastCheck runs between advances vary only the supplied coverage; they change the next selected goal in that same queue. The selected state belongs to the existing state-ID set, the trace prefix is retained, and the original predicate completes without restart.
• Other regressions cover rejection without losing the session, mutation of caller-owned manifest/environment collections, permanent invalidation after current-source changes, partial unsupported paths, close behavior, and an early counterexample with a pending sibling. Exact native replay confirms that early candidate violates the unchanged predicate.

Current-head GitHub CI starts when this PR is opened and is separate from the local validation above. Benchmark campaigns remain paused.

Refs #481.