Repository navigation
[TS PBT] Replay and shrink external witnesses with the original oracle - #506
Open
CaelmBleidd wants to merge 4 commits into
Open
CaelmBleidd wants to merge 4 commits into
CaelmBleidd wants to merge 4 commits into
Conversation
CaelmBleidd
force-pushed
the
caelmbleidd/ts-pbt-external-witness-replay
branch
from
October 14, 2026 20:31
a5d134f to
2917263
Compare
CaelmBleidd
force-pushed
the
caelmbleidd/ts-pbt-external-witness-replay
branch
from
October 14, 2026 21:27
2917263 to
24f5aa5
Compare
This was referenced Oct 15, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Symbolic candidates could be extracted, but they had no external-witness pipeline that confirmed the complete original TypeScript oracle and reduced the same target. This change adds
ExternalWitnessBackend.confirmWitness, a serializable evidence delta, and native FastCheck reduction. For example, an external input of 80 forvalue < 10is replay-confirmed and shrinks to 10.Replay preserves declared support, original precondition admission, tagged input values, and exact named-check or guarded auxiliary identity. Replay forwards the explicit backend tsconfig to both original entrypoints, including admission, native coverage, and reduction. Fresh processes recheck the final oracle and target. Unsupported contextless shrinking, errors, drift, nondeterminism, and timeouts retain the original candidate. Coverage additions come from admitted, repeatable native replay of the original input; shrinking trials are excluded from that coverage. Expected budget exhaustion, supervised timeouts, stale source revisions, and shrinking/capture failures now travel as explicit results. Input wire eligibility is validated directly before serialization. Shared process cleanup and existing ordinary-backend error contracts are retained.
Refs #353. Hypothesis replay consumes explicit executable bindings and keeps hypothesis-only refutations distinct from original-property violations. Automatic hypothesis/EtsIR binding and its accepted integration remain in #398; the one-way campaign handoff remains in #355; no cross-round session is required. This PR does not complete the full coupled acceptance of #353. Selected source hashes attest only the listed modules; reproduction must also pin relevant transitive dependencies.
Validation on rebased head
24f5aa5e9:usvm-ts-pbt: 194 Kotlin tests passed.usvm-ts-fast-check: 115 Kotlin tests and 186 Node tests passed.ignoreFailures=false;git diff --checkpassed.The local pre-commit hook called a nonexistent Gradle
checkLicensetask. Existing license notices and the Apache project license were checked independently; that stale hook was skipped for these commits only.Timeout cleanup now reserves the configured graceful shutdown and forced-termination margin within the existing total deadline. Previously the grace deadline was already exhausted when shutdown began. Too-short supervised requests return timeout before spawning; direct transport keeps its previous policy. A SIGTERM cleanup-marker regression fails without this fix and passes with it. The focused timeout class passes all 8 tests directly on head
0715401d5; the same repair with #541's named-check slice passes 125 Kotlin and 186 Node tests. New CI is running for the updated head.