Remove looping asWord-eq-false lemma and expose --equation-max-local-steps#2863
Merged
Conversation
…on-max-local-steps to booster servers
Exposes the haskell-backend's new recursive-simplification budget
(equation evaluation applied in place at rewritten subterms, hb #4153;
backend default 0 = restart-only) through kevm prove and the pytest
harness:
- cli.py: ProveOptions.equation_max_local_steps + kevm prove flag.
- __main__.py: appends the flag to the resolved kore-rpc-booster /
booster-dev command; rejects non-booster servers explicitly.
- conftest.py / test_prove.py: pytest --equation-max-local-steps option
threaded through all prove suites.
(cherry picked from commit e6597556e913f1a6340fcb7f959a84422976a772)
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…ion-max-local-steps to 20
Turn the booster recursive-simplification budget on by default (20) for
kevm prove and all pytest prove suites, instead of deferring to the
backend's restart-only default of 0:
- cli.py / conftest.py: default 20; option type narrows to int.
- __main__.py: with the budget now always set, a non-booster server
skips the flag with a warning instead of raising.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…op_harness.py: asWord-eq-false loop regression test Adds a functional regression test that guards against reintroducing the non-terminating `asWord-eq-false` simplification (evm-semantics #2859 / kontrol #1153): three claims that evaluate `#asWord ==Int #asWord` known-unequal from the path condition. With the looping rule present each claim's simplification does not terminate and the proof times out; with the rule gone they discharge. Collected by the functional suite (`functional/*-spec.k`) against the shared VERIFICATION definition. `scripts/asword_loop_harness.py` runs such loop specs standalone under a per-claim timeout (LOOP / PASS / FAILED) for local triage, since a non-terminating RPC request produces no per-request log bundle. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…se simplification `asWord-eq-false` (added in #2859) loops in the Kore simplifier when both operands of the `==Int` are `#asWord` terms: applying it rewrites the equality into its own `requires` with the operands swapped (still `#asWord`-on-the-left), so it re-matches and recurses without bound. This was the root cause of the CSE-proof timeouts (kontrol #1153). Removing the rule ends the loop; the `<Int`/`<=Int` siblings are antisymmetric and stay. Regression test: tests/specs/functional/asword-eq-false-loop-spec.k. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The asWord-eq-false regression is guarded by the functional spec alone (tests/specs/functional/asword-eq-false-loop-spec.k); the standalone triage harness is not needed in this branch. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…e relocated eq-false-lt CSE loop Captures the second CSE non-termination layer (evm-semantics #2859 / kontrol #1153) that remains after asWord-eq-false is removed: eq-false-lt × AccountCellMap definedness, a Kore constraint-simplifier fixpoint failure on undetermined account-id comparisons. Kept under loops/ (not collected by the functional suite) because it is UNVERIFIED and, per the change request, does not reproduce in a fresh single proof — the spin only arises on a long-lived server once constraints accumulate. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…CSE Kore non-termination) eq-false-lt (`A ==Int B => false requires A <Int B [simplification, concrete(B)]`, added in #2859) is the rule that drives the CSE Kore-simplifier non-termination that removing asWord-eq-false only relocated to (kontrol #1153). During the Kore definedness check of `#Ceil(<accounts> AccountCellMap)`, the account-distinctness predicates `ACCT_ID ==Int <concrete address> => false` invite this rule, whose side condition `A <Int B` is undetermined for a range-bounded symbolic account id vs a large concrete address, spawning a ~500ms SMT round-trip per attempt that the constraint simplifier repeats without reaching a fixpoint. Confirmed via per-request logs to be the sole rule driving those SMT calls (removing it took the rule-driven SMT count from 45 to 0 on the exemplar). Disabled for now; re-introduce once Booster performs definedness without falling back to the Kore simplifier. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…xemplar for CI collection
Move the eq-false-lt
loop exemplar out of the non-collected loops/ subdir into tests/specs/functional/
so the functional test harness picks it up via spec_files('functional', '*-spec.k').
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
… to close asWord-unif-03/04 without asWord-eq-false Removing the looping asWord-eq-false lemma un-masked a coverage gap: the lemmas-spec asWord-unif-03/04 claims (#2604) decompose an out-of-range #asWord(B) ==Int CONST via asWord-eq-num into CONST <Int #powByteLen(N), which must reduce to false. #powByteLen is [no-evaluators] and #2859 added only the true-direction powByteLen-lt-concrete rule, leaving the false direction to asWord-eq-false. Add the mutually-exclusive, loop-safe false-direction companion so the concrete comparison is total, plus a focused regression claim alongside the existing true-direction test. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
palinatolmach
approved these changes
Jun 15, 2026
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
2 participants
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.
The haskell backend now supports recursive local simplification behind a budget flag (see runtimeverification/haskell-backend#4153), and the
asWord-eq-falsesimplification added in #2859 loops in the Kore simplifier on a term shape that arises in CSE proofs. This branch exposes the backend flag through the prover and removes the looping lemma, with a regression test guarding against its reintroduction.Changes:
kevm prove+ the pytest proof harness gain--equation-max-local-steps, threaded through to thekore-rpc-booster/booster-devservers and defaulting to 20 (the backend's recursive local-simplification budget; backend default = restart-only). Non-booster servers skip the flag with a warning.asWord-eq-falsefromlemmas/evm-int-simplification.k. When both operands of the==Intare#asWordterms it rewrites the equality into its ownrequireswith the operands swapped — still#asWord-on-the-left — so it re-matches and recurses without bound in the Kore simplifier (the root cause of the CSE-proof timeouts, kontrol Fix documentation for #range and codeblocks #1153). The antisymmetric<Int/<=Intsiblings are loop-safe and stay.tests/specs/functional/asword-eq-false-loop-spec.k, a functional regression test (auto-collected by the functional suite) whose claims time out if the looping rule is reintroduced and discharge once it is gone.Validation:
make -C kevm-pyk checkandmake -C kevm-pyk test-unitpass.test_prove_functional[functional/asword-eq-false-loop-spec.k]passes (~103 s); confirmed the same spec does not terminate against the pre-removal lemma, and that the loop reproduces even with--equation-max-local-steps 20.