Skip to content

Export and natively replay bounded completed symbolic inputs - #579

Open
CaelmBleidd wants to merge 2 commits into
caelmbleidd/pbt-guided-campaignfrom
caelmbleidd/pbt-completed-state-evidence
Open

CaelmBleidd wants to merge 2 commits into
caelmbleidd/pbt-guided-campaignfrom
caelmbleidd/pbt-completed-state-evidence

Conversation

@CaelmBleidd

@CaelmBleidd CaelmBleidd commented Oct 16, 2026 •

Copy link
Copy Markdown
Member

Completed symbolic executions currently contribute no reusable original inputs unless they violate the property. A healthy class method can therefore be explored by USVM while the public campaign records no native coverage for it. This change adds optional bounded completed-input export and verifies those fixed inputs through the existing native replay operation, without restarting random generation.

--completed-input-limit N enables capture; the default is disabled. Each saved receipt keeps the predicted symbolic outcome, actual native admission/outcome, original source snapshot, timing and coverage separately. Only fresh, timely, repeatable admitted HOLDS receipts matching the prediction expose checked coverage. Native FALSE/exceptions remain raw receipts; the existing original-property confirmation retains the actual fault coverage and confirmation status. The bounded cache shares guidance replays with subsequent input verification. Capture exhaustion records omissions and does not stop the original search.

This is stacked on #574 at 835f2c64ce51988235d424f61e903c677aaf9e7c; only this PR's commit belongs in the follow-up after its dependencies are merged. The own diff is 13 files, +701/-86. No path-selector policy or queue implementation is changed.

Validation: 33 focused native/campaign/artifact/CLI regressions passed, including healthy literal-true class execution, actual fault confirmation/coverage, rejected preconditions, unsupported async, bounded omissions, immutable inputs/deduplication, source drift, nondeterminism, oracle mismatch and native timeout. Main/test Detekt for both PBT modules reports zero findings. These checks establish fixed-input native source coverage; they do not establish equality of complete symbolic class state or comparative experimental benefit.

Includes the isolated Calls test-contract repair from #582: boxed conditional array identities are tested with explicit branch domains so shared coverage saturation cannot make a semantics assertion depend on traversal order. No production selection policy is changed; the exact CI failure cause was not reproduced locally. The repair passed all eight Calls registry tests on both frontend dependency pins before transfer.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant