From 55a2659a8c478022425972f3fbbe2ceaad226426 Mon Sep 17 00:00:00 2001 From: Stevengre Date: Mon, 25 May 2026 08:59:08 +0000 Subject: [PATCH 1/4] evm-types: rewrite bool2Word rules with side conditions The legacy rules rule bool2Word( true ) => 1 rule bool2Word( false ) => 0 pattern-match on the argument position. Pattern matching only runs the simplifier, not the path-condition + SMT reasoning, so a goal like bool2Word(X >=Int 0) => 1 under path condition X >Int 0 leaves `bool2Word(X >=Int 0)` un-reduced even though the path condition strictly implies the argument. The implication check at the end then fails, and the proof gets stuck. Rewriting the rules as rule bool2Word( B:Bool ) => 1 requires B ==Bool true rule bool2Word( B:Bool ) => 0 requires notBool B ==Bool true moves the same question to a side condition, which Kore discharges against the full path condition (with SMT). The two forms agree on concrete inputs and on free Bool variables (Kore canonicalizes `requires B` into a substitution `B |-> true` before the rule is tried), but the new form additionally handles symbolic Bool *expressions* whose truth the path condition only implies. The new functional spec `tests/specs/functional/bool2Word-symbolic-spec.k` documents the behavior: claims 1-4 (free variable, syntactic equality) pass under both forms; claims 5-6 (path condition implies but does not equate the argument) fail under the legacy rules and pass under the new ones. Co-Authored-By: Claude Opus 4.7 (1M context) --- .../kevm_pyk/kproj/evm-semantics/evm-types.md | 4 +- kevm-pyk/src/tests/integration/test_prove.py | 1 + .../functional/bool2Word-symbolic-spec.k | 79 +++++++++++++++++++ 3 files changed, 82 insertions(+), 2 deletions(-) create mode 100644 tests/specs/functional/bool2Word-symbolic-spec.k diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md index d55b737ded..c5c24ce5a1 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md @@ -29,8 +29,8 @@ Primitives provide the basic conversion from K's sorts `Int` and `Bool` to EVM's ```k syntax Int ::= bool2Word ( Bool ) [symbol(bool2Word), function, total, injective, smtlib(bool2Word)] // ---------------------------------------------------------------------------------------------------- - rule bool2Word( true ) => 1 - rule bool2Word( false ) => 0 + rule bool2Word( B:Bool ) => 1 requires B ==Bool true + rule bool2Word( B:Bool ) => 0 requires notBool B ==Bool true syntax Bool ::= word2Bool ( Int ) [symbol(word2Bool), function, total] // ---------------------------------------------------------------------- diff --git a/kevm-pyk/src/tests/integration/test_prove.py b/kevm-pyk/src/tests/integration/test_prove.py index 61e8d1de3b..589ad17a59 100644 --- a/kevm-pyk/src/tests/integration/test_prove.py +++ b/kevm-pyk/src/tests/integration/test_prove.py @@ -110,6 +110,7 @@ def exclude_list(exclude_file: Path) -> list[Path]: 'functional/lemmas-no-smt-spec.k': 'lemmas-no-smt-spec.k', 'functional/lemmas-spec.k': 'lemmas-spec.k', 'functional/abi-spec.k': 'abi-spec.k', + 'functional/bool2Word-symbolic-spec.k': 'bool2Word-symbolic-spec.k', 'functional/merkle-spec.k': 'merkle-spec.k', 'functional/slot-updates-spec.k': 'slot-updates-spec.k', 'functional/storageRoot-spec.k': 'storageRoot-spec.k', diff --git a/tests/specs/functional/bool2Word-symbolic-spec.k b/tests/specs/functional/bool2Word-symbolic-spec.k new file mode 100644 index 0000000000..9a7cf0c717 --- /dev/null +++ b/tests/specs/functional/bool2Word-symbolic-spec.k @@ -0,0 +1,79 @@ +requires "edsl.md" +requires "lemmas/lemmas.k" + +module VERIFICATION + imports EDSL + imports LEMMAS + + syntax StepSort ::= Int | Bool + // ------------------------------ + + syntax KItem ::= runLemma ( StepSort ) [symbol(runLemma)] + | doneLemma( StepSort ) + // -------------------------------------- + rule runLemma( T ) => doneLemma( T ) + +endmodule + +// +// Regression tests for symbolic-argument reasoning over bool2Word. +// +// Each of these claims sends a `bool2Word( )` term whose +// argument is a *Bool expression* (not the literal `true`/`false`) +// and whose path condition entails — but is not syntactically equal to — +// that expression. The claim asserts the term reduces to 0/1. +// +// Under the legacy rules +// rule bool2Word( true ) => 1 +// rule bool2Word( false ) => 0 +// pattern matching on the argument position does NOT consult the path +// condition / SMT, so symbolic Bool expressions that the path condition +// only *implies* (not equates to true/false) leave bool2Word(_) un-reduced +// and the implication check at the end fails. +// +// Under the side-conditioned rules +// rule bool2Word( B ) => 1 requires B ==Bool true +// rule bool2Word( B ) => 0 requires notBool B ==Bool true +// the matcher binds B unconditionally and the side condition is discharged +// by Kore's full path-condition + SMT reasoning, so these claims pass. +// +module BOOL2WORD-SYMBOLIC-SPEC + imports VERIFICATION + + // Free Bool variable, path condition equates it to true/false. + // Both rule forms handle this — Kore canonicalizes `requires B` + // into substitution B |-> true before reaching bool2Word. + claim [b2w-var-true]: + runLemma ( bool2Word(B:Bool) ) => doneLemma( 1 ) ... + requires B + + claim [b2w-var-false]: + runLemma ( bool2Word(B:Bool) ) => doneLemma( 0 ) ... + requires notBool B + + // Argument is a Bool expression directly equated to itself in the + // path condition. Original rules also pass because Kore can rewrite + // the goal via the equality. + claim [b2w-expr-eq-true]: + runLemma ( bool2Word(X >Int Y) ) => doneLemma( 1 ) ... + requires X >Int Y + + claim [b2w-expr-eq-false]: + runLemma ( bool2Word(X >Int Y) ) => doneLemma( 0 ) ... + requires notBool (X >Int Y) + + // Path condition IMPLIES the argument, but is not syntactically equal + // to it: `X >Int 0` strictly implies `X >=Int 0`. + // Original rules FAIL this — pattern-match on `true` in argument + // position does not invoke SMT to discharge `X >=Int 0` under + // path condition `X >Int 0`. + // Side-conditioned rules PASS this — the side condition is checked + // against the full path condition. + claim [b2w-implied-true]: + runLemma ( bool2Word(X >=Int 0) ) => doneLemma( 1 ) ... + requires X >Int 0 + + claim [b2w-implied-false]: + runLemma ( bool2Word(X doneLemma( 0 ) ... + requires X >Int 0 +endmodule From 11588e7f6ca0ed468a215f0d7ed7d16d012dfa77 Mon Sep 17 00:00:00 2001 From: Stevengre Date: Mon, 25 May 2026 09:15:40 +0000 Subject: [PATCH 2/4] bool2Word-symbolic-spec: drop redundant inline comments Each claim's behavior is already evident from the path condition and target; the file-level comment retains the one fact that matters (why claims 5-6 are the diagnostic ones). Co-Authored-By: Claude Opus 4.7 (1M context) --- .../functional/bool2Word-symbolic-spec.k | 38 ++----------------- 1 file changed, 3 insertions(+), 35 deletions(-) diff --git a/tests/specs/functional/bool2Word-symbolic-spec.k b/tests/specs/functional/bool2Word-symbolic-spec.k index 9a7cf0c717..c4ce5bd1b6 100644 --- a/tests/specs/functional/bool2Word-symbolic-spec.k +++ b/tests/specs/functional/bool2Word-symbolic-spec.k @@ -15,34 +15,12 @@ module VERIFICATION endmodule -// -// Regression tests for symbolic-argument reasoning over bool2Word. -// -// Each of these claims sends a `bool2Word( )` term whose -// argument is a *Bool expression* (not the literal `true`/`false`) -// and whose path condition entails — but is not syntactically equal to — -// that expression. The claim asserts the term reduces to 0/1. -// -// Under the legacy rules -// rule bool2Word( true ) => 1 -// rule bool2Word( false ) => 0 -// pattern matching on the argument position does NOT consult the path -// condition / SMT, so symbolic Bool expressions that the path condition -// only *implies* (not equates to true/false) leave bool2Word(_) un-reduced -// and the implication check at the end fails. -// -// Under the side-conditioned rules -// rule bool2Word( B ) => 1 requires B ==Bool true -// rule bool2Word( B ) => 0 requires notBool B ==Bool true -// the matcher binds B unconditionally and the side condition is discharged -// by Kore's full path-condition + SMT reasoning, so these claims pass. -// +// Claims 5-6 fail under the legacy `bool2Word(true) => 1` rules: the path +// condition implies but does not equate the argument, so the argument-position +// matcher cannot discharge it without SMT. Side-conditioned rules pass them. module BOOL2WORD-SYMBOLIC-SPEC imports VERIFICATION - // Free Bool variable, path condition equates it to true/false. - // Both rule forms handle this — Kore canonicalizes `requires B` - // into substitution B |-> true before reaching bool2Word. claim [b2w-var-true]: runLemma ( bool2Word(B:Bool) ) => doneLemma( 1 ) ... requires B @@ -51,9 +29,6 @@ module BOOL2WORD-SYMBOLIC-SPEC runLemma ( bool2Word(B:Bool) ) => doneLemma( 0 ) ... requires notBool B - // Argument is a Bool expression directly equated to itself in the - // path condition. Original rules also pass because Kore can rewrite - // the goal via the equality. claim [b2w-expr-eq-true]: runLemma ( bool2Word(X >Int Y) ) => doneLemma( 1 ) ... requires X >Int Y @@ -62,13 +37,6 @@ module BOOL2WORD-SYMBOLIC-SPEC runLemma ( bool2Word(X >Int Y) ) => doneLemma( 0 ) ... requires notBool (X >Int Y) - // Path condition IMPLIES the argument, but is not syntactically equal - // to it: `X >Int 0` strictly implies `X >=Int 0`. - // Original rules FAIL this — pattern-match on `true` in argument - // position does not invoke SMT to discharge `X >=Int 0` under - // path condition `X >Int 0`. - // Side-conditioned rules PASS this — the side condition is checked - // against the full path condition. claim [b2w-implied-true]: runLemma ( bool2Word(X >=Int 0) ) => doneLemma( 1 ) ... requires X >Int 0 From 67575361b45bbd39a10d88327371373e3d1d16a6 Mon Sep 17 00:00:00 2001 From: Stevengre Date: Tue, 26 May 2026 00:33:38 +0000 Subject: [PATCH 3/4] switch to simplification lemmas in lemmas.k Per @ehildenb's review (#2848): rather than rewrite the bool2Word function rules in evm-types.md, add two [simplification] lemmas in lemmas/lemmas.k. Equivalent end behavior on the new spec, but: - Core semantics unchanged - Only spec files importing LEMMAS see the new behavior - Concrete bool2Word inputs still go through the original function rules at zero cost - Co-locates with the existing bool2Word simplification lemmas Reverts the evm-types.md change. Updates the spec comment. Co-Authored-By: Claude Opus 4.7 (1M context) --- kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md | 4 ++-- kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k | 8 ++++++++ tests/specs/functional/bool2Word-symbolic-spec.k | 7 ++++--- 3 files changed, 14 insertions(+), 5 deletions(-) diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md index c5c24ce5a1..d55b737ded 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md @@ -29,8 +29,8 @@ Primitives provide the basic conversion from K's sorts `Int` and `Bool` to EVM's ```k syntax Int ::= bool2Word ( Bool ) [symbol(bool2Word), function, total, injective, smtlib(bool2Word)] // ---------------------------------------------------------------------------------------------------- - rule bool2Word( B:Bool ) => 1 requires B ==Bool true - rule bool2Word( B:Bool ) => 0 requires notBool B ==Bool true + rule bool2Word( true ) => 1 + rule bool2Word( false ) => 0 syntax Bool ::= word2Bool ( Int ) [symbol(word2Bool), function, total] // ---------------------------------------------------------------------- diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k index 3dd3dfdf8b..743157f147 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k @@ -59,6 +59,14 @@ module LEMMAS-WITHOUT-SLOT-UPDATES [symbolic] // bool2Word reasoning // ######################## + // Direct reduction via the path condition. The function rules in + // evm-types.md pattern-match on `true`/`false` and so do not fire when + // the argument is a symbolic Bool expression that the path condition + // only implies. These lemmas move the decision to a side condition, + // which Kore discharges against the full path condition (with SMT). + rule [b2w-true]: bool2Word(B) => 1 requires B [simplification] + rule [b2w-false]: bool2Word(B) => 0 requires notBool B [simplification] + // Range rule [b2w-lb]: 0 <=Int bool2Word(_) => true [simplification, smt-lemma] rule [b2w-ub]: bool2Word(_) <=Int 1 => true [simplification, smt-lemma] diff --git a/tests/specs/functional/bool2Word-symbolic-spec.k b/tests/specs/functional/bool2Word-symbolic-spec.k index c4ce5bd1b6..07fca3ffa7 100644 --- a/tests/specs/functional/bool2Word-symbolic-spec.k +++ b/tests/specs/functional/bool2Word-symbolic-spec.k @@ -15,9 +15,10 @@ module VERIFICATION endmodule -// Claims 5-6 fail under the legacy `bool2Word(true) => 1` rules: the path -// condition implies but does not equate the argument, so the argument-position -// matcher cannot discharge it without SMT. Side-conditioned rules pass them. +// Without the `b2w-true` / `b2w-false` simplification lemmas in lemmas.k, +// claims 5-6 fail: the path condition implies but does not equate the +// argument, so the function-rule matcher cannot discharge it without SMT. +// With the simplification lemmas, all six claims pass. module BOOL2WORD-SYMBOLIC-SPEC imports VERIFICATION From a7ee100df63971edcb1451e69c43efca11a56556 Mon Sep 17 00:00:00 2001 From: Stevengre Date: Tue, 26 May 2026 00:51:44 +0000 Subject: [PATCH 4/4] lemmas: trim bool2Word simplification comment Co-Authored-By: Claude Opus 4.7 (1M context) --- kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k | 6 +----- 1 file changed, 1 insertion(+), 5 deletions(-) diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k index 743157f147..d6ae1bb695 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k @@ -59,11 +59,7 @@ module LEMMAS-WITHOUT-SLOT-UPDATES [symbolic] // bool2Word reasoning // ######################## - // Direct reduction via the path condition. The function rules in - // evm-types.md pattern-match on `true`/`false` and so do not fire when - // the argument is a symbolic Bool expression that the path condition - // only implies. These lemmas move the decision to a side condition, - // which Kore discharges against the full path condition (with SMT). + // Reduce when the path condition only implies the argument. rule [b2w-true]: bool2Word(B) => 1 requires B [simplification] rule [b2w-false]: bool2Word(B) => 0 requires notBool B [simplification]