fix: k-induction/BMC build each state from the previous input, not the current one - #147
Open
geofflittle wants to merge 1 commit into
Open
Conversation
…e current one
At depth k the state was built as next(in_k, prevState) using the CURRENT depth's input, so the
checked input was spuriously pinned to the state it produced. A state-reading assumption (e.g.
i.x' >= s.x) then collapsed to a tautology (in_k.x' >= in_k.x') and was not enforced, yielding a
spurious counterexample on a true property. More seriously, an invariant or assumption that reads
the current input alongside a state field could have a genuinely reachable violating state removed,
so the tool reported a false Valid / no counterexample and missed a real violation. This is a
soundness bug. The pseudocode has st_{i+1} = next in_i st_i, i.e. the state must be built from the
PREVIOUS input so it is independent of in_k.
Thread the previous step (state and input) through the k-induction and BMC recursions via a named
PrevStep record, and build each state from PrevStep.input. Add a regression test
(Tests/FixedIssues/Issue146.lean, registered in the index) covering #kind and #bmc on single- and
multi-field state, a 2-inductive case, the contradiction path, and both soundness directions (a
real counterexample is still found, and a false Valid is caught).
Counter05 goldens are regenerated for the corrected @0-based input indexing. Counter06's #kind
golden drops the counterexample detail (drop info, drop warning), since a non-inductive invariant's
witness is solver-choice-dependent. Goldens confirmed on the pinned z3 4.15.2.
Fixes input-output-hk#146
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.
Description
#kindand#bmcproduce wrong verdicts for aStateMachinewhose transition state depends on the current input. There are two symptoms. A state-readingassumptions(for examplei.x' ≥ s.x) yields a spurious counterexample for an invariant that actually holds. More seriously, when aninvariantsorassumptionsreads the current input alongside a state field, the tool can report a false✅ Valid(#kind) or✅ No counterexample(#bmc) and miss a real violation, so this is a soundness bug, not just a spurious-counterexample nuisance. Root cause: at each depth the state was built from the CURRENT input, so the checked input was spuriously pinned to the state it just produced. A state-reading assumptioni.x' ≥ s.xthen collapses to a tautology (inₖ.x' ≥ inₖ.x'), and an invariant reading the input can have a genuinely reachable violating state removed from the search. The fix threads aPrevSteprecord (the previous step's state and input) so each state is built from the PREVIOUS input, matching the pseudocodestᵢ₊₁ = next inᵢ stᵢalready documented in the strategy files. Input-only assumptions and input-independent invariants are unaffected, which is why this went unnoticed.Type of Change
Related Issue
Fixes #146
Changes Made
PrevStep { state, input }record through the#kindand#bmcrecursions and build each transition state fromPrevStep.input(the previous input) rather than the current one.Tests/FixedIssues/Issue146.lean(and register it in theTests/FixedIssues.leanindex):#kindand#bmcon single- and multi-field state, a 2-inductive (not 1-inductive) case, the contradiction path, and both soundness directions (a real counterexample is still found, and a falseValidis caught for an invariant that reads the current input). The soundness and induction cases usegen-cex: 0to keep solver-chosen witnesses out of the goldens.Counter05goldens for the corrected@0-based input indexing. The verdict is unchanged (stillFalsifiedat Depth 3, same induction-failure sequence). Only the input-index labels shift from 1-based to 0-based, itself a symptom of the fixed input attribution.Counter06's#kindgolden to#guard_msgs (drop info, drop warning), since a non-inductive invariant's counterexample-to-induction witness is z3-choice-dependent. This drops the multi-depth witness trace, so the#kindassertion is now "elaborates without an unexpected error".Testing
Built with
lake build, and verified the affected scope on Lean v4.24.0, z3 4.16.0: the fullTests/StateMachine/*suite plusTests.FixedIssues(which now includesIssue146) build and pass, green and stable across repeated runs. The regression test was confirmed to fail on the unpatched base (every guard flips: most to a spurious counterexample, and the forcing-assumption soundness cases to an earlyContradictory contextthat hides the real one) and to guard#kindand#bmcindependently (verified by reverting each strategy in isolation). Note: the change only touches the StateMachine strategies, so I checked those subsets directly rather than the fullmake check_all, which spends a long time in an unrelated pre-existing test (Tests/Smt/SmtNat/SmtNatMod.lean).Test Coverage
Tests/FixedIssues/folderDocumentation
Checklist
make check_allTests/FixedIssues/with reference to issue numberAdditional Notes
The example lives in
Tests/FixedIssues/(the template saysTests/Issues/, but the repo actually usesTests/FixedIssues/) and is registered in theTests/FixedIssues.leanindex. No external docs or README changes were needed, so those boxes are left unchecked. Code doc-comments were added.I did not run the full
make check_all: it blocks for a long time in an unrelated pre-existing test (Tests/Smt/SmtNat/SmtNatMod.lean, Nat-modulo). I built and ran the affected suites instead (Tests/StateMachine/*andTests.FixedIssues), both green and stable across repeated runs. Happy to let CI run the full suite.Counter05's goldens were regenerated for the corrected
@0-based indexing (deterministic across repeated runs here). Counter06's#kindgolden was already fragile on the base commit: its counterexample-to-induction witness, and even the final line's severity, varies by z3 build, so the golden now drops that detail. These goldens were developed on z3 4.16.0, and I confirmed the full StateMachine and FixedIssues suites also pass under the repo-pinned z3 4.15.2, so the goldens are stable across both solver builds.