Repository navigation
Check frozen class statement coverage by native batch replay - #585
Open
CaelmBleidd wants to merge 1 commit into
Open
CaelmBleidd wants to merge 1 commit into
CaelmBleidd wants to merge 1 commit into
Conversation
CaelmBleidd
force-pushed
the
caelmbleidd/pbt-experiment-preflight
branch
from
October 16, 2026 19:59
1c1d2a6 to
554d6b6
Compare
CaelmBleidd
force-pushed
the
caelmbleidd/pbt-checked-class-replay
branch
from
October 16, 2026 19:59
ea53db9 to
8045533
Compare
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.
Class coverage needs an outcome-independent universe and checked native hits of the original executable class statements. Add a bounded batch replay helper that reuses the existing TypeScript class AST instrumenter, checked local source-closure resolver, tagged value codec, native loader and
invokePropertyOnceadmission/clone contract. It leaves the symbolic/frontend source unchanged and applies counters only in separate native source overlays.The helper freezes source hashes and exact AST statement IDs before treatments. Original and counted variants run twice, with the same input sequence and original property outcome. An optional diagnostic scenario checks returned values/state through a separate module trajectory so it cannot mutate the oracle stream. Oracle-only verification stays explicitly weaker. Rejected preconditions, module loading and diagnostic execution do not add predicate coverage. The existing instrumenter rejects unsupported class static initialization rather than silently changing the denominator. Stale source, unsupported values, outcome/scenario mismatch, nondeterminism or unknown statement IDs produce no credited hits.
Stacked on #583 at
554d6b6b8f727163f23d26f17bedef42a74f48a7. Own diff: two files, +331. This introduces no runtime session, generation loop, selector policy or README. Only this PR's own commit should move after its dependencies are merged.Validation: three native regressions passed for exact two-branch statement coverage, an always-true oracle that must not hide changed scenario results, and a module-counter scenario whose diagnostic calls must not alter credited predicate paths. The installed public campaign plus this helper completed all four functional comparison modes. This verifies the declared native scenario observations, not complete symbolic heap equivalence or scientific superiority.