Repository navigation
[TS PBT] Use native witness results for coverage feedback - #572
Open
CaelmBleidd wants to merge 1 commit into
Open
CaelmBleidd wants to merge 1 commit into
CaelmBleidd wants to merge 1 commit into
Conversation
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
1 participant
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.
Coverage feedback previously required a fabricated PBT-shaped result or another generator call to verify a symbolic input. Expose fixed-input native replay through the existing witness operation and accept its existing WitnessNativeReplay directly. Collect coverage from the first invocation, check repeatability with the same input, and retain admission, oracle and source diagnostics. A native callback never falls back to the legacy PBT callback, including on failure; existing callbacks remain source compatible. Scheduling policy is unchanged.
Own diff: 7 files, +212/-13, one commit. Immediate base is the DSL deadline-retention branch at
619d80f4b; that branch depends on #5697e6d9b9c9and its frozen assembly. After those dependencies merge, move only this own commit onto main and retarget. No dependency implementation is copied into this commit.Validation: 10 real backend coverage contracts passed, including native edge confirmation with exactly one admitted coverage receipt, stale source rejection, preservation of uncovered goals after failure, no legacy fallback, and the absolute caller deadline. Portable trace serialization is provided by #569. Comparative performance or class coverage benefit is not established by these checks.