Repository navigation
formal: kit v2.1 (stale mutant patch check) - #13
Merged
Merged
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.
Problem
govder nightly 38054717665 failed: a full-tier mutant no longer applied after govder#20 changed internal/enforce/kill.go, and full-tier mutants only run nightly, so the PR that made it stale went green.
Fix / Proof
Kit v2.1 vendored byte-identical (scripts/formal/ from plans/formal-02/kit): check_claims now runs
git apply --checkfor EVERY registered mutant patch against the current tree (no build), so a patch made stale by a source change fails formal-fast on the PR that changes it, not in the nightly. KIT_VERSION = "2.1". Inside check_mutants the tree is deliberately mutated, so it sets FORMAL_KIT_MUTATED_TREE=1 and the check is skipped there (the runner already proved the patch applied).No claims or patches changed (every averin patch applies).
Red-first / bite evidence
Kit unit tests added first for the stale-patch check (stale patch fails with a regenerate hint, shared patch checked once, mutated-tree env skips); the check flagged the two genuinely stale patches below on origin/main content (govder e2e-kill-reports-contained-without-effect, vultrino policy-write-warned-prompt-accepted).
Gates run
Kit unit tests (python3 -m unittest discover -s scripts/formal/tests, 103 pass), check_claims on this tree. averin kit-claims.json: 264 checks, 0 failures.
What this does NOT establish
Only that each patch APPLIES (no build, no kill): a patch that applies but no longer compiles or is no longer semantic is still caught only by the mutant run. Merge order: kit consumers, any order.