From 75bd6a395f8b99a8579e96723c5e4030fa2ee44f Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Sat, 23 May 2026 01:25:22 +0000 Subject: [PATCH 01/25] lemmas/bytes-simplification.k: add preserves-definedness to lookup-as-asWord MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Without this attribute Booster refused to apply the rule because the LHS contains the non-total hook Lbl_[_]_BYTES-HOOKE. After the fix Booster correctly applies it (8× succeeded in the execute-node simplify request). Analysis: scripts/bench-prove.py --analyse-fallbacks shows the "Uncertain about definedness of rule due to: non-total symbol Lbl_[_]_BYTES-HOOKE" error gone, replaced by successful Booster applications. The rule-index gap and indeterminate-match cases for other equations remain and will be addressed in follow-up commits. Co-Authored-By: Claude Sonnet 4.6 (cherry picked from commit 25e00d935ac1f9ce25394e40865dbb36c0cbd80b) (cherry picked from commit 6ae0def0a1de63aa5ffb13d1cdb2abe7d5c3651d) --- .../kevm_pyk/kproj/evm-semantics/lemmas/bytes-simplification.k | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/bytes-simplification.k b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/bytes-simplification.k index 392a50c6e9..658be17aeb 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/bytes-simplification.k +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/bytes-simplification.k @@ -306,5 +306,5 @@ module BYTES-SIMPLIFICATION [symbolic] rule [lookup-as-asWord]: B:Bytes [ I:Int ] => #asWord ( #range ( B, I, 1 ) ) requires 0 <=Int I andBool I Date: Mon, 25 May 2026 15:06:14 +0000 Subject: [PATCH 02/25] lemmas: Round 2 Booster gap fixes bytes-simplification.k: add preserves-definedness to lengthBytes-buf and lengthBytes-range. evm-int-simplification.k: add asWord-buf-inversion-rangeUInt256. (cherry picked from commit d4dad3335e7e98d76057c9c0b07387a21a20c0b2) (cherry picked from commit c60634bc589f05a98aa30b06409df4ed478d407f) --- .../kproj/evm-semantics/lemmas/bytes-simplification.k | 4 ++-- .../kproj/evm-semantics/lemmas/evm-int-simplification.k | 8 ++++++++ 2 files changed, 10 insertions(+), 2 deletions(-) diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/bytes-simplification.k b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/bytes-simplification.k index 658be17aeb..b99732cb2d 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/bytes-simplification.k +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/bytes-simplification.k @@ -267,8 +267,8 @@ module BYTES-SIMPLIFICATION [symbolic] rule [lengthBytes-geq-zero]: 0 <=Int lengthBytes ( _ ) => true [simplification, smt-lemma] rule [lengthBytes-geq-nonPos]: X <=Int lengthBytes ( _ ) => true requires X <=Int 0 [simplification, concrete(X)] rule [lengthBytes-concat]: lengthBytes(BUF1 +Bytes BUF2) => lengthBytes(BUF1) +Int lengthBytes(BUF2) [simplification] - rule [lengthBytes-buf]: lengthBytes(#buf(S, _)) => S requires 0 <=Int S [simplification] - rule [lengthBytes-range]: lengthBytes(#range(_, S:Int, W:Int)) => maxInt(0, W) requires 0 <=Int S [simplification] + rule [lengthBytes-buf]: lengthBytes(#buf(S, _)) => S requires 0 <=Int S [simplification, preserves-definedness] + rule [lengthBytes-range]: lengthBytes(#range(_, S:Int, W:Int)) => maxInt(0, W) requires 0 <=Int S [simplification, preserves-definedness] rule [lengthBytes-prtw]: lengthBytes(#padRightToWidth(W:Int, B:Bytes)) => maxInt(lengthBytes(B), W) [simplification] rule [lengthBytes-leq-zero]: lengthBytes(B:Bytes) <=Int 0 => B ==K .Bytes [simplification] diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/evm-int-simplification.k b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/evm-int-simplification.k index 3a16df7834..f6789b90eb 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/evm-int-simplification.k +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/evm-int-simplification.k @@ -101,6 +101,14 @@ module EVM-INT-SIMPLIFICATION requires 0 <=Int WB andBool 0 <=Int X andBool X X + requires #rangeUInt ( 256, X ) + [simplification, preserves-definedness] + // Reduction: bitwise right shift in terms of `#range` rule [asWord-shr]: #asWord( BA ) >>Int N => #asWord ( #range ( BA, 0, lengthBytes( BA ) -Int ( N /Int 8 ) ) ) From e82cf130a179f546065a986557b942b36affe7f1 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Sun, 24 May 2026 14:31:53 +0000 Subject: [PATCH 03/25] lemmas/int-simplification.k: normalize ==Int commutativity concrete-on-left MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Kore's execute-fallback applies INT-KORE.eq-int-true-rigth which can swap ==Int argument order in path conditions (e.g. lengthBytes(BA) ==Int 32 → 32 ==Int lengthBytes(BA)). This makes Booster's implies check fail due to a syntactic mismatch even when the logical content is identical. The new rule [int-eq-comm-concrete] at priority 30 fires before the +Int cancellation rules and normalises concrete-on-left to concrete-on-right, restoring the form the target spec expects. Co-Authored-By: Claude Sonnet 4.6 (cherry picked from commit 1d384970bda6669b479959a31f152c0e8aedde35) (cherry picked from commit 2cf8e8c620fee897758f02f5b2b512595428fbec) --- .../kevm_pyk/kproj/evm-semantics/lemmas/int-simplification.k | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/int-simplification.k b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/int-simplification.k index 30e5663c47..90fb519861 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/int-simplification.k +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/int-simplification.k @@ -86,6 +86,10 @@ module INT-SIMPLIFICATION-HASKELL [symbolic] rule A +Int B >Int C +Int D => A -Int C >Int D -Int B [concrete(B, D), symbolic(A, C), simplification(45)] rule A +Int B >=Int C +Int D => A -Int C >=Int D -Int B [concrete(B, D), symbolic(A, C), simplification(45)] + rule [int-eq-comm-concrete]: + N:Int ==Int X:Int => X ==Int N + [simplification(30), concrete(N), symbolic(X)] + rule A +Int B ==Int A => B ==Int 0 [simplification(40)] rule A +Int B ==Int B => A ==Int 0 [simplification(40)] rule A +Int B ==Int C +Int B => A ==Int C [simplification(40)] From 13375271ff3c2dcd035e47bf97e3e237d202fbf2 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Sun, 24 May 2026 17:41:44 +0000 Subject: [PATCH 04/25] lemmas/{int-simplification,lemmas}.k: add arithmetic + Bool simplification lemmas MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Adds to INT-SIMPLIFICATION-COMMON: - A <=Int A => true (reflexivity; fixes chop-overflow-02 under --booster-only-simplify) - A <=Int A +Int B => 0 <=Int B - A +Int ((B -Int A) +Int C) => B +Int C (4-term cancellation; fixes cancellation-02) - A false (strict order contradiction; fixes b2w-03) Adds to INT-SIMPLIFICATION-HASKELL: - A false requires B <=Int C [concrete(B,C)] (range contradiction) - C <=Int A andBool A false requires B <=Int C [concrete(B,C)] (range contradiction) (requires is purely concrete, evaluated by LLVM hook — no circular self-application risk) Adds to LEMMAS-HASKELL: - B orBool notBool B => true (and commuted variant; fixes b2w-05, chop-additional-knowledge) - B andBool notBool B => false (and commuted variant) Validation: full functional test suite passes in normal mode (slot-updates-spec.k failure is pre-existing, unrelated to these changes). Under --booster-only-simplify, lemmas-spec.k drops from 22 to 18 failing claims. No loops detected (checked via kevm-analyse hot-rules). Co-Authored-By: Claude Sonnet 4.6 (cherry picked from commit 3bb01297db74cacf75fa138f0550440882df8de1) (cherry picked from commit 4c13678fdb82d593bfc495cf0418804a3e505c90) --- .../kproj/evm-semantics/lemmas/int-simplification.k | 12 ++++++++++++ .../src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k | 5 +++++ 2 files changed, 17 insertions(+) diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/int-simplification.k b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/int-simplification.k index 90fb519861..c67282123a 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/int-simplification.k +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/int-simplification.k @@ -105,6 +105,11 @@ module INT-SIMPLIFICATION-HASKELL [symbolic] rule A -Int B A A <=Int B [simplification, symbolic(A, B)] + // Mixed range contradictions: A < B /\ C <= A where B <= C (all concrete B, C) + // Requires is purely concrete (both B and C are concrete), so no circular self-application. + rule A:Int false requires B <=Int C [simplification, concrete(B, C)] + rule C:Int <=Int A:Int andBool A:Int false requires B <=Int C [simplification, concrete(B, C)] + endmodule module INT-SIMPLIFICATION-COMMON @@ -137,6 +142,7 @@ module INT-SIMPLIFICATION-COMMON rule (A +Int B) +Int (C -Int B) => A +Int C [simplification] rule (A -Int B) -Int (C -Int B) => A -Int C [simplification] rule ((A -Int B) -Int C) +Int B => A -Int C [simplification] + rule A +Int ((B -Int A) +Int C) => B +Int C [simplification] // 5 terms // NOTE: required for `tests/specs/functional/infinite-gas-spec.k.prove` (haskell) @@ -245,6 +251,12 @@ module INT-SIMPLIFICATION-COMMON rule A false requires 0 <=Int B [simplification] + rule A:Int <=Int A:Int => true [simplification] + + rule A:Int <=Int A:Int +Int B:Int => 0 <=Int B [simplification] + + rule A:Int false [simplification] + rule 0 true requires 0 <=Int A [simplification, preserves-definedness] // inequality sign normalization 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 d6ae1bb695..2498ef8349 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 @@ -259,4 +259,9 @@ module LEMMAS-HASKELL [symbolic] rule [notBool-or]: notBool ( A orBool B ) => ( notBool A ) andBool ( notBool B ) [simplification(60)] rule [notBool-and]: notBool ( A andBool B ) => ( notBool A ) orBool ( notBool B ) [simplification(60)] + rule [bool-or-not-self]: B:Bool orBool notBool B:Bool => true [simplification] + rule [bool-not-or-self]: notBool B:Bool orBool B:Bool => true [simplification] + rule [bool-and-not-self]: B:Bool andBool notBool B:Bool => false [simplification] + rule [bool-not-and-self]: notBool B:Bool andBool B:Bool => false [simplification] + endmodule From 99fd8256917c47f0f3b8ad53fe9d429d7d15f229 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Thu, 4 Jun 2026 04:48:19 +0000 Subject: [PATCH 05/25] lemmas/int-simplification.k: short-circuit A <=Int A+Int B to true when 0 <=Int B Add a higher-priority (40) variant of `A <=Int A+B => 0 <=Int B` that short-circuits directly to `true` when `0 <=Int B` is already in the path condition, fixing `chop-overflow-01` in --booster-only-simplify mode where the intermediate `0 <=Int Y` form cannot be discharged at the implies check. Co-Authored-By: Claude Opus 4.8 (cherry picked from commit bfb0225f96a28cbf42ddd520dd49773b234944e5) --- .../kevm_pyk/kproj/evm-semantics/lemmas/int-simplification.k | 2 ++ 1 file changed, 2 insertions(+) diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/int-simplification.k b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/int-simplification.k index c67282123a..817d853912 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/int-simplification.k +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/int-simplification.k @@ -253,6 +253,8 @@ module INT-SIMPLIFICATION-COMMON rule A:Int <=Int A:Int => true [simplification] + // Higher-priority: short-circuit to true directly when path condition already has 0 <=Int B. + rule A:Int <=Int A:Int +Int B:Int => true requires 0 <=Int B [simplification(40)] rule A:Int <=Int A:Int +Int B:Int => 0 <=Int B [simplification] rule A:Int false [simplification] From 9ccb90a90695610fb33c4c79fbcf7a2b8322fcab Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Mon, 25 May 2026 00:34:15 +0000 Subject: [PATCH 06/25] lemmas/bytes-simplification.k: add concrete b"" concat identity rules In K, .Bytes (the constructor) and b"" (LLVM-evaluated concrete empty bytes, a Kore domain value \dv{SortBytes}("")) are different Kore terms. The existing bytes-concat-empty-right/left rules use .Bytes and do not fire when LLVM hooks (e.g. #encodeArgs base case) return b"". New rules: [bytes-concat-empty-right-concrete]: B +Bytes b"" => B [bytes-concat-empty-left-concrete]: b"" +Bytes B => B Fixes booster-only failure for encodepacked-keccak01: the contract evaluates keccak(1 : #encodeArgs(#uint256(A0))) where the #encodeArgs base case produces b"", leaving keccak(X +Bytes b"") vs keccak(X) as the implies-check mismatch. Co-Authored-By: Claude Sonnet 4.6 (cherry picked from commit 829d293906d6efb769649002b2cea2ebf90235fc) (cherry picked from commit a4669b0942edb8c974750490affdad4e1ed1d54d) --- .../kproj/evm-semantics/lemmas/bytes-simplification.k | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/bytes-simplification.k b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/bytes-simplification.k index b99732cb2d..571f024104 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/bytes-simplification.k +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/bytes-simplification.k @@ -29,6 +29,10 @@ module BYTES-SIMPLIFICATION [symbolic] rule [bytes-concat-empty-right]: B:Bytes +Bytes .Bytes => B [simplification] rule [bytes-concat-empty-left]: .Bytes +Bytes B:Bytes => B [simplification] + // b"" is a Kore domain value (\dv{Bytes}("")) distinct from the .Bytes constructor; + // LLVM hooks (e.g. #encodeArgs base case) return b"", not .Bytes, so we need both forms. + rule [bytes-concat-empty-right-concrete]: B:Bytes +Bytes b"" => B [simplification, preserves-definedness] + rule [bytes-concat-empty-left-concrete]: b"" +Bytes B:Bytes => B [simplification, preserves-definedness] rule [bytes-concat-right-assoc-symb-l]: (B1:Bytes +Bytes B2:Bytes) +Bytes B3:Bytes => B1 +Bytes (B2 +Bytes B3) [symbolic(B1), simplification(40)] rule [bytes-concat-right-assoc-symb-r]: (B1:Bytes +Bytes B2:Bytes) +Bytes B3:Bytes => B1 +Bytes (B2 +Bytes B3) [symbolic(B2), simplification(40)] From 78df03a5502780ee6ec754b95b63d72d76ccbe8d Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Wed, 27 May 2026 06:49:00 +0000 Subject: [PATCH 07/25] buf.md, abi-spec.k: add [preserves-definedness] to 2^(8*SIZE) simplification, add coverage claim The rule `2 ^Int (8 *Int SIZE) => #powByteLen(SIZE)` was [mixed] in booster: it sometimes matched successfully but sometimes failed because booster rejected the rewrite without proof that #powByteLen(SIZE) is defined. Since #powByteLen is a function symbol with no-evaluators (always yields a defined term), adding [preserves-definedness] is safe and fixes the gap. This was the root cause of the kore-vs-booster gap in ecrecoverloop02-sig1-invalid and ecrecoverloop02-sigs-valid benchmarks specs. The new abi-spec.k claim pow-byte-len-simplify exercises this rule directly in booster-only mode and passes after the fix. Co-Authored-By: Claude Sonnet 4.6 (cherry picked from commit efa0e111609946d7c3506e3a7ae2c6d52cef16e4) (cherry picked from commit fcab3c84c70d9034bee5d6a3b3152c306b6e9d00) --- .../src/kevm_pyk/kproj/evm-semantics/buf.md | 2 +- tests/specs/functional/abi-spec.k | 22 +++++++++++-------- 2 files changed, 14 insertions(+), 10 deletions(-) diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/buf.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/buf.md index 40b09b5fa1..f9430e96d5 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/buf.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/buf.md @@ -37,7 +37,7 @@ module BUF syntax Int ::= #powByteLen ( Int ) [symbol(#powByteLen), function, no-evaluators] // --------------------------------------------------------------------------------- // rule #powByteLen(SIZE) => 2 ^Int (8 *Int SIZE) - rule 2 ^Int (8 *Int SIZE) => #powByteLen(SIZE) [symbolic(SIZE), simplification] + rule 2 ^Int (8 *Int SIZE) => #powByteLen(SIZE) [symbolic(SIZE), simplification, preserves-definedness] rule 0 true requires 0 <=Int SIZE [simplification, preserves-definedness] rule SIZE true requires 0 <=Int SIZE [simplification, preserves-definedness] diff --git a/tests/specs/functional/abi-spec.k b/tests/specs/functional/abi-spec.k index 0d27b80096..358e4a0094 100644 --- a/tests/specs/functional/abi-spec.k +++ b/tests/specs/functional/abi-spec.k @@ -3,8 +3,8 @@ requires "abi.md" module VERIFICATION imports EVM-ABI - syntax Step ::= Bool | Bytes - // ------------------------------ + syntax Step ::= Bool | Bytes | Int + // ----------------------------------- syntax KItem ::= runLemma ( Step ) [symbol(runLemma)] | doneLemma( Step ) @@ -43,22 +43,26 @@ module ABI-SPEC runLemma( #sizeOfDynamicType( #array( - #bytes(b"\x00"), - 3, + #bytes(b"\x00"), + 3, #bytes(b"\xaa"), #bytes(b"\xbb\xbb"), #bytes(b"\xcc\xcc\xcc") ) ) ==Int lengthBytes(#enc( #array( - #bytes(b"\x00"), - 3, + #bytes(b"\x00"), + 3, #bytes(b"\xaa"), #bytes(b"\xbb\xbb"), #bytes(b"\xcc\xcc\xcc") ) )) - ) - => doneLemma(true) - ... + ) + => doneLemma(true) + ... + claim [pow-byte-len-simplify]: + runLemma ( 2 ^Int (8 *Int N:Int) ) => doneLemma ( #powByteLen(N:Int) ) ... + requires 0 <=Int N + endmodule From 0d5cac1054198d33ac92d34caede9d5509f1a439 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Wed, 27 May 2026 12:58:27 +0000 Subject: [PATCH 08/25] int-simplification.k, int-simplifications-spec.k: add [preserves-definedness] to 46 comparison normalization rules, add coverage claims Co-Authored-By: Claude Sonnet 4.6 (cherry picked from commit ccce6b5dc1442f51df8939c71b3e378cf74c5894) (cherry picked from commit 2b7099cf814c7ed27e8bc5af007cd52591e7b869) --- .../evm-semantics/lemmas/int-simplification.k | 112 +++++++++--------- .../functional/int-simplifications-spec.k | 15 +++ 2 files changed, 71 insertions(+), 56 deletions(-) diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/int-simplification.k b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/int-simplification.k index 817d853912..873b9da06e 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/int-simplification.k +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/int-simplification.k @@ -31,60 +31,60 @@ module INT-SIMPLIFICATION-HASKELL [symbolic] // add, sub: comparison normalization // ########################################################################### - rule A +Int B A A <=Int C -Int B [concrete(B, C), symbolic(A), simplification(45)] - rule A +Int B >Int C => A >Int C -Int B [concrete(B, C), symbolic(A), simplification(45)] - rule A +Int B >=Int C => A >=Int C -Int B [concrete(B, C), symbolic(A), simplification(45)] - - rule A +Int B B B <=Int C -Int A [concrete(A, C), symbolic(B), simplification(45)] - rule A +Int B >Int C => B >Int C -Int A [concrete(A, C), symbolic(B), simplification(45)] - rule A +Int B >=Int C => B >=Int C -Int A [concrete(A, C), symbolic(B), simplification(45)] - - rule A -Int B A A <=Int C +Int B [concrete(B, C), symbolic(A), simplification(45)] - rule A -Int B >Int C => A >Int C +Int B [concrete(B, C), symbolic(A), simplification(45)] - rule A -Int B >=Int C => A >=Int C +Int B [concrete(B, C), symbolic(A), simplification(45)] - - rule A -Int B A -Int C A -Int C <=Int B [concrete(A, C), symbolic(B), simplification(45)] - rule A -Int B >Int C => A -Int C >Int B [concrete(A, C), symbolic(B), simplification(45)] - rule A -Int B >=Int C => A -Int C >=Int B [concrete(A, C), symbolic(B), simplification(45)] - - rule A A -Int B A -Int B <=Int C [concrete(A, B), symbolic(C), simplification(45)] - rule A >Int B +Int C => A -Int B >Int C [concrete(A, B), symbolic(C), simplification(45)] - rule A >=Int B +Int C => A -Int B >=Int C [concrete(A, B), symbolic(C), simplification(45)] - - rule A A -Int C A -Int C <=Int B [concrete(A, C), symbolic(B), simplification(45)] - rule A >Int B +Int C => A -Int C >Int B [concrete(A, C), symbolic(B), simplification(45)] - rule A >=Int B +Int C => A -Int C >=Int B [concrete(A, C), symbolic(B), simplification(45)] - - rule A C C <=Int B -Int A [concrete(A, B), symbolic(C), simplification(45)] - rule A >Int B -Int C => C >Int B -Int A [concrete(A, B), symbolic(C), simplification(45)] - rule A >=Int B -Int C => C >=Int B -Int A [concrete(A, B), symbolic(C), simplification(45)] - - rule A A +Int C A +Int C <=Int B [concrete(A, C), symbolic(B), simplification(45)] - rule A >Int B -Int C => A +Int C >Int B [concrete(A, C), symbolic(B), simplification(45)] - rule A >=Int B -Int C => A +Int C >=Int B [concrete(A, C), symbolic(B), simplification(45)] - - rule A +Int B ==Int C => A ==Int C -Int B [concrete(B, C), symbolic(A), simplification(45), comm] - rule A +Int B ==Int C => B ==Int C -Int A [concrete(A, C), symbolic(B), simplification(45), comm] - rule A -Int B ==Int C => A ==Int C +Int B [concrete(B, C), symbolic(A), simplification(45), comm] - rule A -Int B ==Int C => A -Int C ==Int B [concrete(A, C), symbolic(B), simplification(45), comm] - - rule { A +Int B #Equals C } => { A #Equals C -Int B } [concrete(B, C), symbolic(A), simplification(45), comm] - rule { A +Int B #Equals C } => { B #Equals C -Int A } [concrete(A, C), symbolic(B), simplification(45), comm] - rule { A -Int B #Equals C } => { A #Equals C +Int B } [concrete(B, C), symbolic(A), simplification(45), comm] - rule { A -Int B #Equals C } => { A -Int C #Equals B } [concrete(A, C), symbolic(B), simplification(45), comm] - - rule A +Int B A -Int C A -Int C <=Int D -Int B [concrete(B, D), symbolic(A, C), simplification(45)] - rule A +Int B >Int C +Int D => A -Int C >Int D -Int B [concrete(B, D), symbolic(A, C), simplification(45)] - rule A +Int B >=Int C +Int D => A -Int C >=Int D -Int B [concrete(B, D), symbolic(A, C), simplification(45)] + rule A +Int B A A <=Int C -Int B [concrete(B, C), symbolic(A), simplification(45), preserves-definedness] + rule A +Int B >Int C => A >Int C -Int B [concrete(B, C), symbolic(A), simplification(45), preserves-definedness] + rule A +Int B >=Int C => A >=Int C -Int B [concrete(B, C), symbolic(A), simplification(45), preserves-definedness] + + rule A +Int B B B <=Int C -Int A [concrete(A, C), symbolic(B), simplification(45), preserves-definedness] + rule A +Int B >Int C => B >Int C -Int A [concrete(A, C), symbolic(B), simplification(45), preserves-definedness] + rule A +Int B >=Int C => B >=Int C -Int A [concrete(A, C), symbolic(B), simplification(45), preserves-definedness] + + rule A -Int B A A <=Int C +Int B [concrete(B, C), symbolic(A), simplification(45), preserves-definedness] + rule A -Int B >Int C => A >Int C +Int B [concrete(B, C), symbolic(A), simplification(45), preserves-definedness] + rule A -Int B >=Int C => A >=Int C +Int B [concrete(B, C), symbolic(A), simplification(45), preserves-definedness] + + rule A -Int B A -Int C A -Int C <=Int B [concrete(A, C), symbolic(B), simplification(45), preserves-definedness] + rule A -Int B >Int C => A -Int C >Int B [concrete(A, C), symbolic(B), simplification(45), preserves-definedness] + rule A -Int B >=Int C => A -Int C >=Int B [concrete(A, C), symbolic(B), simplification(45), preserves-definedness] + + rule A A -Int B A -Int B <=Int C [concrete(A, B), symbolic(C), simplification(45), preserves-definedness] + rule A >Int B +Int C => A -Int B >Int C [concrete(A, B), symbolic(C), simplification(45), preserves-definedness] + rule A >=Int B +Int C => A -Int B >=Int C [concrete(A, B), symbolic(C), simplification(45), preserves-definedness] + + rule A A -Int C A -Int C <=Int B [concrete(A, C), symbolic(B), simplification(45), preserves-definedness] + rule A >Int B +Int C => A -Int C >Int B [concrete(A, C), symbolic(B), simplification(45), preserves-definedness] + rule A >=Int B +Int C => A -Int C >=Int B [concrete(A, C), symbolic(B), simplification(45), preserves-definedness] + + rule A C C <=Int B -Int A [concrete(A, B), symbolic(C), simplification(45), preserves-definedness] + rule A >Int B -Int C => C >Int B -Int A [concrete(A, B), symbolic(C), simplification(45), preserves-definedness] + rule A >=Int B -Int C => C >=Int B -Int A [concrete(A, B), symbolic(C), simplification(45), preserves-definedness] + + rule A A +Int C A +Int C <=Int B [concrete(A, C), symbolic(B), simplification(45), preserves-definedness] + rule A >Int B -Int C => A +Int C >Int B [concrete(A, C), symbolic(B), simplification(45), preserves-definedness] + rule A >=Int B -Int C => A +Int C >=Int B [concrete(A, C), symbolic(B), simplification(45), preserves-definedness] + + rule A +Int B ==Int C => A ==Int C -Int B [concrete(B, C), symbolic(A), simplification(45), comm, preserves-definedness] + rule A +Int B ==Int C => B ==Int C -Int A [concrete(A, C), symbolic(B), simplification(45), comm, preserves-definedness] + rule A -Int B ==Int C => A ==Int C +Int B [concrete(B, C), symbolic(A), simplification(45), comm, preserves-definedness] + rule A -Int B ==Int C => A -Int C ==Int B [concrete(A, C), symbolic(B), simplification(45), comm, preserves-definedness] + + rule { A +Int B #Equals C } => { A #Equals C -Int B } [concrete(B, C), symbolic(A), simplification(45), comm, preserves-definedness] + rule { A +Int B #Equals C } => { B #Equals C -Int A } [concrete(A, C), symbolic(B), simplification(45), comm, preserves-definedness] + rule { A -Int B #Equals C } => { A #Equals C +Int B } [concrete(B, C), symbolic(A), simplification(45), comm, preserves-definedness] + rule { A -Int B #Equals C } => { A -Int C #Equals B } [concrete(A, C), symbolic(B), simplification(45), comm, preserves-definedness] + + rule A +Int B A -Int C A -Int C <=Int D -Int B [concrete(B, D), symbolic(A, C), simplification(45), preserves-definedness] + rule A +Int B >Int C +Int D => A -Int C >Int D -Int B [concrete(B, D), symbolic(A, C), simplification(45), preserves-definedness] + rule A +Int B >=Int C +Int D => A -Int C >=Int D -Int B [concrete(B, D), symbolic(A, C), simplification(45), preserves-definedness] rule [int-eq-comm-concrete]: N:Int ==Int X:Int => X ==Int N @@ -93,12 +93,12 @@ module INT-SIMPLIFICATION-HASKELL [symbolic] rule A +Int B ==Int A => B ==Int 0 [simplification(40)] rule A +Int B ==Int B => A ==Int 0 [simplification(40)] rule A +Int B ==Int C +Int B => A ==Int C [simplification(40)] - rule A +Int B ==Int C +Int D => A -Int C ==Int D -Int B [simplification(45), symbolic(A, C), concrete(B, D)] + rule A +Int B ==Int C +Int D => A -Int C ==Int D -Int B [simplification(45), symbolic(A, C), concrete(B, D), preserves-definedness] rule { A +Int B #Equals A } => { B #Equals 0 } [simplification(40)] rule { A +Int B #Equals B } => { A #Equals 0 } [simplification(40)] rule { A +Int B #Equals C +Int B } => { A #Equals C } [simplification(40)] - rule { A +Int B #Equals C +Int D } => { A -Int C #Equals D -Int B } [simplification(45), symbolic(A, C), concrete(B, D)] + rule { A +Int B #Equals C +Int D } => { A -Int C #Equals D -Int B } [simplification(45), symbolic(A, C), concrete(B, D), preserves-definedness] rule 0 B B <=Int A [simplification, symbolic(A, B)] diff --git a/tests/specs/functional/int-simplifications-spec.k b/tests/specs/functional/int-simplifications-spec.k index 1516fad092..2f8e5e361b 100644 --- a/tests/specs/functional/int-simplifications-spec.k +++ b/tests/specs/functional/int-simplifications-spec.k @@ -127,4 +127,19 @@ module INT-SIMPLIFICATIONS-SPEC claim [le-maxuint256]: runLemma ( X <=Int maxUInt256 ) => doneLemma ( X + // Comparison normalization coverage (int-simplification.k [preserves-definedness]) + // --------------------------------------------------------------------------------- + + claim [int-comp-norm-add-lt]: + runLemma ( X:Int +Int 3 doneLemma ( X:Int + + claim [int-comp-norm-add-le]: + runLemma ( X:Int +Int 3 <=Int 10 ) => doneLemma ( X:Int <=Int 7 ) ... + + claim [int-comp-norm-sub-lt]: + runLemma ( X:Int -Int 3 doneLemma ( X:Int + + claim [int-comp-norm-rhs-add-lt]: + runLemma ( 7 doneLemma ( 4 + endmodule From 17a203fb9e5efe3a2277e2a64e9eaec5b2e09767 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Wed, 27 May 2026 13:38:15 +0000 Subject: [PATCH 09/25] lemmas.k, lemmas-no-smt-spec.k: add bool #Equals workaround rules for BOOL-KORE @-variable patterns, add coverage claim The BOOL-KORE module in K's domains.md defines 8 rules using @-prefixed "here variables" (e.g., {true #Equals notBool @B}) which booster cannot match. Add equivalent rules with regular B:Bool variables to LEMMAS-HASKELL so booster can apply the same normalizations. Add a functional spec claim exercising the notBool case, which passes in booster-only mode. Co-Authored-By: Claude Sonnet 4.6 (cherry picked from commit 80ed6938ac79faf1a98ef55ddc2a0226a3ae39b2) (cherry picked from commit c498024497ff2a65fd6cc58916db745813f5acf4) --- .../src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k | 10 ++++++++++ tests/specs/functional/lemmas-no-smt-spec.k | 4 ++++ 2 files changed, 14 insertions(+) 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 2498ef8349..995e031a97 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 @@ -264,4 +264,14 @@ module LEMMAS-HASKELL [symbolic] rule [bool-and-not-self]: B:Bool andBool notBool B:Bool => false [simplification] rule [bool-not-and-self]: notBool B:Bool andBool B:Bool => false [simplification] + rule [bool-eq-not-true-l]: {true #Equals notBool B:Bool} => {false #Equals B} [simplification, preserves-definedness] + rule [bool-eq-not-true-r]: {notBool B:Bool #Equals true } => {B #Equals false} [simplification, preserves-definedness] + rule [bool-eq-not-false-l]: {false #Equals notBool B:Bool} => {true #Equals B} [simplification, preserves-definedness] + rule [bool-eq-not-false-r]: {notBool B:Bool #Equals false} => {B #Equals true} [simplification, preserves-definedness] + + rule [bool-eq-and-true-l]: {true #Equals B1:Bool andBool B2:Bool} => {true #Equals B1} #And {true #Equals B2} [simplification, preserves-definedness] + rule [bool-eq-and-true-r]: {B1:Bool andBool B2:Bool #Equals true } => {B1 #Equals true} #And {B2 #Equals true} [simplification, preserves-definedness] + rule [bool-eq-or-false-l]: {false #Equals B1:Bool orBool B2:Bool} => {false #Equals B1} #And {false #Equals B2} [simplification, preserves-definedness] + rule [bool-eq-or-false-r]: {B1:Bool orBool B2:Bool #Equals false} => {B1 #Equals false} #And {B2 #Equals false} [simplification, preserves-definedness] + endmodule diff --git a/tests/specs/functional/lemmas-no-smt-spec.k b/tests/specs/functional/lemmas-no-smt-spec.k index dc12dc9e51..bde5e8db0f 100644 --- a/tests/specs/functional/lemmas-no-smt-spec.k +++ b/tests/specs/functional/lemmas-no-smt-spec.k @@ -43,4 +43,8 @@ module LEMMAS-NO-SMT-SPEC claim [bool-simpl-02]: runLemma ( bool2Word( B:Bool ) ==Int 1 ) => doneLemma ( B ==K true ) ... claim [bool-simpl-03]: runLemma ( 1 ==Int bool2Word( B:Bool ) ) => doneLemma ( B ==K true ) ... + claim [bool-eq-not-false]: + runLemma ( B:Bool ) => doneLemma ( false ) ... + requires notBool B + endmodule From cdfbcfd1617d0240d627cc2147830bc543a428fd Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Wed, 27 May 2026 16:46:50 +0000 Subject: [PATCH 10/25] lemmas/bytes-simplification.k, tests/functional/lemmas-no-smt-spec.k: add preserves-definedness to range-empty The range-empty rule (#range(_,S,W) => .Bytes when S<0 or W<=0) previously lacked [preserves-definedness], so booster refused to apply it during the implies check. Tag it accordingly and add two coverage claims to lemmas-no-smt-spec.k to verify it fires in booster. Co-Authored-By: Claude Sonnet 4.6 (cherry picked from commit 666ba06c5956d8b9b540446089f73b6a45fba000) (cherry picked from commit f30c2ff9ac9e7bdf0af6f10b47f716f5e0f1728e) --- .../kproj/evm-semantics/lemmas/bytes-simplification.k | 2 +- tests/specs/functional/lemmas-no-smt-spec.k | 6 ++++++ 2 files changed, 7 insertions(+), 1 deletion(-) diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/bytes-simplification.k b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/bytes-simplification.k index 571f024104..5fcf53b850 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/bytes-simplification.k +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/bytes-simplification.k @@ -103,7 +103,7 @@ module BYTES-SIMPLIFICATION [symbolic] rule [range-empty]: #range(_:Bytes, S:Int, W:Int) => .Bytes requires S B +Bytes #buf(W -Int lengthBytes(B), 0) diff --git a/tests/specs/functional/lemmas-no-smt-spec.k b/tests/specs/functional/lemmas-no-smt-spec.k index bde5e8db0f..dc71958097 100644 --- a/tests/specs/functional/lemmas-no-smt-spec.k +++ b/tests/specs/functional/lemmas-no-smt-spec.k @@ -47,4 +47,10 @@ module LEMMAS-NO-SMT-SPEC runLemma ( B:Bool ) => doneLemma ( false ) ... requires notBool B + claim [range-empty-neg-start]: + runLemma ( #range(B:Bytes, 0 -Int 1, 5) ==K .Bytes ) => doneLemma ( true ) ... + + claim [range-empty-zero-width]: + runLemma ( #range(B:Bytes, 3, 0) ==K .Bytes ) => doneLemma ( true ) ... + endmodule From ab55d49a267dc51ca493499b7195cf9aacabced6 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Wed, 27 May 2026 21:20:07 +0000 Subject: [PATCH 11/25] buf.md, lemmas-no-smt-spec.k: add powByteLen-lt-concrete concrete comparison rule After commit 5d0d8083c added [preserves-definedness] to the 2^Int(8*SIZE) => #powByteLen(SIZE) rule, booster fires it consistently even when SIZE is concrete (the rule fires before path-condition lookup makes the argument concrete). Because #powByteLen has no-evaluators, the result #powByteLen(N) cannot self-evaluate, leaving CONST (cherry picked from commit 8b4972c4cc410995c3ec2360ca6dd50c189d374b) (cherry picked from commit 11b7050dfc88d903d1e1c1cb62802b6db25b9187) --- .../src/kevm_pyk/kproj/evm-semantics/buf.md | 7 ++++ tests/specs/functional/lemmas-no-smt-spec.k | 36 +++++++++++++++++++ 2 files changed, 43 insertions(+) diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/buf.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/buf.md index f9430e96d5..1ea46865b8 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/buf.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/buf.md @@ -41,6 +41,13 @@ module BUF rule 0 true requires 0 <=Int SIZE [simplification, preserves-definedness] rule SIZE true requires 0 <=Int SIZE [simplification, preserves-definedness] + // Concrete comparison: CONST < #powByteLen(N) evaluates when both arguments are concrete. + // Needed because 2^Int(8*N) is rewritten to #powByteLen(N) even for concrete N (via the + // symbolic(N) rule firing before path-condition lookup makes N concrete), but #powByteLen + // has no-evaluators so the result can't be computed directly. + rule [powByteLen-lt-concrete]: CONST true + requires 0 <=Int N andBool CONST WM [ IDX := #buf(1, VAL) ] [simplification] rule #bufStrict(SIZE, DATA) => #buf(SIZE, DATA) diff --git a/tests/specs/functional/lemmas-no-smt-spec.k b/tests/specs/functional/lemmas-no-smt-spec.k index dc71958097..d53a57de5a 100644 --- a/tests/specs/functional/lemmas-no-smt-spec.k +++ b/tests/specs/functional/lemmas-no-smt-spec.k @@ -53,4 +53,40 @@ module LEMMAS-NO-SMT-SPEC claim [range-empty-zero-width]: runLemma ( #range(B:Bytes, 3, 0) ==K .Bytes ) => doneLemma ( true ) ... + // #asWord comparison — false cases + // --------------------------------- + + // asWord-lt-false: #asWord(B) < X => false when X <=Int #asWord(B) + // Here X=0, and 0 <=Int #asWord(B) is always true (asWord-lb), so no extra requires needed. + claim [asword-lt-false]: + runLemma ( #asWord(B:Bytes) doneLemma ( false ) ... + + // asWord-le-false: #asWord(B) <=Int X => false when X runLemma ( #asWord(B:Bytes) <=Int 0 ) => doneLemma ( false ) ... + requires 0 false when X =/=Int #asWord(B) + // X must be symbolic so asword-eq-num (requires concrete(X)) does not fire first. + claim [asword-eq-false]: + runLemma ( #asWord(B:Bytes) ==Int X:Int ) => doneLemma ( false ) ... + requires X =/=Int #asWord(B) + + // eq-false-lt + // ----------- + + // eq-false-lt: A ==Int B => false when A < B is in path conditions (B concrete). + claim [eq-false-lt]: + runLemma ( X:Int ==Int 42 ) => doneLemma ( false ) ... + requires X true when both concrete. + // Needed because 2^Int(8*N) is rewritten to #powByteLen(N) even for concrete N, + // but #powByteLen has no-evaluators, so the comparison cannot self-evaluate. + claim [powByteLen-lt-concrete]: + runLemma ( 31 doneLemma ( true ) ... + endmodule From 61c31608f171c6538a8b308d6922b60133be2490 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Sun, 31 May 2026 15:33:32 +0000 Subject: [PATCH 12/25] evm-semantics/evm-types.md: mark #asAccount as [total] MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit #asAccount is total over its Bytes domain — the two rules (lengthBytes == 0 → .Account; [owise] → #asWord(BS)) are jointly exhaustive. Marking it [total] lets booster's definedness checker clear the RHS-definedness gate on rules that contain #asAccount in their RHS — notably [call.delegatedAuthority] at evm.md:1633, where the symbolic argument #range(CODE, 3, 20) prevents concrete evaluation and previously caused booster to abort with "Uncertain about definedness of rule due to: non-total symbol Lbl#asAccount", yielding to kore for the rewrite step. The recover-mode sweep across functional + examples + erc20 + benchmarks identified 12 kore-execute handoffs (all benchmarks ecrecover variants) that traced to exactly this definedness abort. Validated locally on benchmarks/ecrecover00-siginvalid-spec.k: 2 handoffs → 0, proof still passes. Co-Authored-By: Claude Opus 4.7 (cherry picked from commit 33c04ff6558c339ffc06759dcaa49cd139222ef8) (cherry picked from commit 4ce956c09bb03a7d06fdf533f95b2cfaa40b0dc7) --- kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md | 4 ++-- 1 file changed, 2 insertions(+), 2 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 d55b737ded..e4cabe0a65 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 @@ -358,8 +358,8 @@ Bytes helper functions // ------------------------------------------------------------------------- rule #asInteger(WS) => Bytes2Int(WS, BE, Unsigned) [concrete] - syntax Account ::= #asAccount ( Bytes ) [symbol(#asAccount), function] - // ---------------------------------------------------------------------------------- + syntax Account ::= #asAccount ( Bytes ) [symbol(#asAccount), function, total] + // ----------------------------------------------------------------------------- rule #asAccount(BS) => .Account requires lengthBytes(BS) ==Int 0 rule #asAccount(BS) => #asWord(BS) [owise] From 8ad71015dbc8904e0f943788fd3692c2a04c859d Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Thu, 4 Jun 2026 20:18:45 +0000 Subject: [PATCH 13/25] lemmas/int-simplification.k: add minInt --- .../kproj/evm-semantics/lemmas/int-simplification.k | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/int-simplification.k b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/int-simplification.k index 873b9da06e..6d05de1d7d 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/int-simplification.k +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/int-simplification.k @@ -242,6 +242,18 @@ module INT-SIMPLIFICATION-COMMON rule [maxInt-factor-left]: maxInt ( A:Int +Int B:Int, A:Int +Int C:Int ) => A +Int maxInt ( B, C ) [simplification] rule [maxInt-factor-right]: maxInt ( A:Int +Int B:Int, C:Int +Int B:Int ) => maxInt ( A, C ) +Int B [simplification] + // minInt true + requires A true + requires B <=Int D + [simplification(40), preserves-definedness] + // ########################################################################### // inequality // ########################################################################### From 0f55900d881b056d29af5bfff0d71cd13cb64d30 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Thu, 4 Jun 2026 20:19:28 +0000 Subject: [PATCH 14/25] lemmas/evm-int-simplification.k: add asWord comparison-false simplifications Tier-1 subset of upstream 584462824: the asWord-{lt,le,eq}-false rules (contrapositives of path-condition facts; RHS is false, so trivially definedness-preserving). Drops that commit's slot-updates-spec.k edits (claims regressed PASS->FAIL and need investigation). Coverage claims for these rules are already in lemmas-no-smt-spec.k. Co-Authored-By: Claude Opus 4.8 --- .../evm-semantics/lemmas/evm-int-simplification.k | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/evm-int-simplification.k b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/evm-int-simplification.k index f6789b90eb..511422f9ee 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/evm-int-simplification.k +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/evm-int-simplification.k @@ -131,6 +131,18 @@ module EVM-INT-SIMPLIFICATION // Comparison: `#asWord(B)` is certainly less than or equal to something that is not less than the max number fitting into `lengthBytes(B)` bytes rule [asWord-le]: #asWord ( B ) <=Int X:Int => true requires ( 2 ^Int (8 *Int minInt(32, lengthBytes(B))) -Int 1 ) <=Int X [simplification, preserves-definedness] + // Comparison: `#asWord(B) < X` is false when the path condition says X <= #asWord(B). + // Loop-safe with asWord-le-false: requires clauses have #asWord on the RIGHT, so + // neither rule fires on the other's requires. + rule [asWord-lt-false]: #asWord ( B:Bytes ) false requires X <=Int #asWord ( B ) [simplification, preserves-definedness] + rule [asWord-le-false]: #asWord ( B:Bytes ) <=Int X:Int => false requires X false requires X =/=Int #asWord ( B ) [simplification, preserves-definedness] + // Comparison: `#asWord` of `+Bytes` when lower bytes match, with ` #asWord ( BA1 ) Date: Thu, 4 Jun 2026 20:20:07 +0000 Subject: [PATCH 15/25] lemmas/int-simplification.k: add eq-false-lt simplification Tier-1 subset of upstream d0f4bdec3: keep eq-false-lt (A ==Int B => false when A --- .../kevm_pyk/kproj/evm-semantics/lemmas/int-simplification.k | 3 +++ 1 file changed, 3 insertions(+) diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/int-simplification.k b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/int-simplification.k index 6d05de1d7d..3501a09c06 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/int-simplification.k +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/int-simplification.k @@ -286,6 +286,9 @@ module INT-SIMPLIFICATION-COMMON rule A ==Int B => false requires 0 <=Int A andBool B false requires A true requires 0 <=Int X andBool notBool (X ==Int 0) [simplification(60)] rule X <=Int maxUInt256 => X Date: Thu, 4 Jun 2026 20:21:07 +0000 Subject: [PATCH 16/25] evm.md, lemmas/lemmas.k: mark #widthOpCode [total, smtlib] and add bound + concat-lookup simplifications Consolidates the Tier-1 #widthOpCode work from upstream Rounds 2-5 (which iteratively rewrote the same lines): #widthOpCode is total (PUSH ops -> 2..33, owise -> 1) and gets an smtlib symbol; widthOpCode-lb/ub encode its 0..33 range as smt-lemmas; widthOpCode-concat-{left,right} push a concrete-prefix byte lookup through +Bytes. Drops the Round-4 asWord-range-buf and the #computeValidJumpDests preserves-definedness riders pending review. Co-Authored-By: Claude Opus 4.8 --- .../src/kevm_pyk/kproj/evm-semantics/evm.md | 2 +- .../kproj/evm-semantics/lemmas/lemmas.k | 24 +++++++++++++++++++ 2 files changed, 25 insertions(+), 1 deletion(-) diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md index aa0e14fd92..600e43c51d 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md @@ -1812,7 +1812,7 @@ System Transaction Configuration ``` ```k - syntax Int ::= #widthOpCode(Int) [symbol(#widthOpCode), function] + syntax Int ::= #widthOpCode(Int) [symbol(#widthOpCode), function, total, smtlib(widthOpCode)] // ----------------------------------------------------------------- rule #widthOpCode(W) => W -Int 94 requires W >=Int 96 andBool W <=Int 127 rule #widthOpCode(_) => 1 [owise] 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 995e031a97..ebe2ebb861 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 @@ -245,6 +245,30 @@ module LEMMAS-HASKELL [symbolic] requires notBool ( I1 ==Int I2 ) [simplification] + // ######################## + // #widthOpCode range + // ######################## + + // #widthOpCode always returns 1..33 (PUSH ops 2..33, everything else 1). + // smtlib(widthOpCode) on the declaration lets smt-lemma encode these as + // universally-quantified bounds so the solver can discharge side conditions + // containing #widthOpCode without needing to evaluate it concretely. + rule [widthOpCode-lb]: 0 <=Int #widthOpCode(_:Int) => true [simplification, smt-lemma] + rule [widthOpCode-ub]: #widthOpCode(_:Int) <=Int 33 => true [simplification, smt-lemma] + + // Booster's equation engine does not descend inside #widthOpCode(...) to + // apply bytes-concat-lookup-{left,right}. These rules compose the two + // steps so the full concrete-prefix lookup can be reduced in one go. + rule [widthOpCode-concat-left]: + #widthOpCode ( ( B1:Bytes +Bytes _B2:Bytes ) [ I:Int ] ) => #widthOpCode ( B1 [ I ] ) + requires 0 <=Int I andBool I #widthOpCode ( B2 [ I -Int lengthBytes ( B1 ) ] ) + requires lengthBytes ( B1 ) <=Int I + [simplification, preserves-definedness] + // ######################## // Boolean Logic // ######################## From dc3f8e91cf5e77396868c8996954281da64bb3bb Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Thu, 4 Jun 2026 20:49:12 +0000 Subject: [PATCH 17/25] lemmas: drop redundant [preserves-definedness] from all-total simplification rules For a [simplification] rule the booster's definedness obligation is the set of non-total, non-constructor symbols on the LHS and RHS (Internalise.hs); when that set is empty the rule is determined definedness-preserving automatically and the attribute is a no-op. Removed it from the 66 rules added here whose every symbol is total (`+Int -Int *Int` / comparisons / `minInt maxInt lengthBytes +Bytes notBool` / the `total` functions `#asWord #buf #range #widthOpCode`), i.e. the comparison-normalization block, eq-false-lt, the minInt --- .../lemmas/bytes-simplification.k | 10 +- .../lemmas/evm-int-simplification.k | 8 +- .../evm-semantics/lemmas/int-simplification.k | 118 +++++++++--------- .../kproj/evm-semantics/lemmas/lemmas.k | 28 ++--- 4 files changed, 82 insertions(+), 82 deletions(-) diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/bytes-simplification.k b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/bytes-simplification.k index 5fcf53b850..402e488e35 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/bytes-simplification.k +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/bytes-simplification.k @@ -31,8 +31,8 @@ module BYTES-SIMPLIFICATION [symbolic] rule [bytes-concat-empty-left]: .Bytes +Bytes B:Bytes => B [simplification] // b"" is a Kore domain value (\dv{Bytes}("")) distinct from the .Bytes constructor; // LLVM hooks (e.g. #encodeArgs base case) return b"", not .Bytes, so we need both forms. - rule [bytes-concat-empty-right-concrete]: B:Bytes +Bytes b"" => B [simplification, preserves-definedness] - rule [bytes-concat-empty-left-concrete]: b"" +Bytes B:Bytes => B [simplification, preserves-definedness] + rule [bytes-concat-empty-right-concrete]: B:Bytes +Bytes b"" => B [simplification] + rule [bytes-concat-empty-left-concrete]: b"" +Bytes B:Bytes => B [simplification] rule [bytes-concat-right-assoc-symb-l]: (B1:Bytes +Bytes B2:Bytes) +Bytes B3:Bytes => B1 +Bytes (B2 +Bytes B3) [symbolic(B1), simplification(40)] rule [bytes-concat-right-assoc-symb-r]: (B1:Bytes +Bytes B2:Bytes) +Bytes B3:Bytes => B1 +Bytes (B2 +Bytes B3) [symbolic(B2), simplification(40)] @@ -103,7 +103,7 @@ module BYTES-SIMPLIFICATION [symbolic] rule [range-empty]: #range(_:Bytes, S:Int, W:Int) => .Bytes requires S B +Bytes #buf(W -Int lengthBytes(B), 0) @@ -271,8 +271,8 @@ module BYTES-SIMPLIFICATION [symbolic] rule [lengthBytes-geq-zero]: 0 <=Int lengthBytes ( _ ) => true [simplification, smt-lemma] rule [lengthBytes-geq-nonPos]: X <=Int lengthBytes ( _ ) => true requires X <=Int 0 [simplification, concrete(X)] rule [lengthBytes-concat]: lengthBytes(BUF1 +Bytes BUF2) => lengthBytes(BUF1) +Int lengthBytes(BUF2) [simplification] - rule [lengthBytes-buf]: lengthBytes(#buf(S, _)) => S requires 0 <=Int S [simplification, preserves-definedness] - rule [lengthBytes-range]: lengthBytes(#range(_, S:Int, W:Int)) => maxInt(0, W) requires 0 <=Int S [simplification, preserves-definedness] + rule [lengthBytes-buf]: lengthBytes(#buf(S, _)) => S requires 0 <=Int S [simplification] + rule [lengthBytes-range]: lengthBytes(#range(_, S:Int, W:Int)) => maxInt(0, W) requires 0 <=Int S [simplification] rule [lengthBytes-prtw]: lengthBytes(#padRightToWidth(W:Int, B:Bytes)) => maxInt(lengthBytes(B), W) [simplification] rule [lengthBytes-leq-zero]: lengthBytes(B:Bytes) <=Int 0 => B ==K .Bytes [simplification] diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/evm-int-simplification.k b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/evm-int-simplification.k index 511422f9ee..f1735b4664 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/evm-int-simplification.k +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/evm-int-simplification.k @@ -107,7 +107,7 @@ module EVM-INT-SIMPLIFICATION rule [asWord-buf-inversion-rangeUInt256]: #asWord ( #buf ( 32, X:Int ) ) => X requires #rangeUInt ( 256, X ) - [simplification, preserves-definedness] + [simplification] // Reduction: bitwise right shift in terms of `#range` rule [asWord-shr]: @@ -134,14 +134,14 @@ module EVM-INT-SIMPLIFICATION // Comparison: `#asWord(B) < X` is false when the path condition says X <= #asWord(B). // Loop-safe with asWord-le-false: requires clauses have #asWord on the RIGHT, so // neither rule fires on the other's requires. - rule [asWord-lt-false]: #asWord ( B:Bytes ) false requires X <=Int #asWord ( B ) [simplification, preserves-definedness] - rule [asWord-le-false]: #asWord ( B:Bytes ) <=Int X:Int => false requires X false requires X <=Int #asWord ( B ) [simplification] + rule [asWord-le-false]: #asWord ( B:Bytes ) <=Int X:Int => false requires X false requires X =/=Int #asWord ( B ) [simplification, preserves-definedness] + rule [asWord-eq-false]: #asWord ( B:Bytes ) ==Int X:Int => false requires X =/=Int #asWord ( B ) [simplification] // Comparison: `#asWord` of `+Bytes` when lower bytes match, with ` A A <=Int C -Int B [concrete(B, C), symbolic(A), simplification(45), preserves-definedness] - rule A +Int B >Int C => A >Int C -Int B [concrete(B, C), symbolic(A), simplification(45), preserves-definedness] - rule A +Int B >=Int C => A >=Int C -Int B [concrete(B, C), symbolic(A), simplification(45), preserves-definedness] - - rule A +Int B B B <=Int C -Int A [concrete(A, C), symbolic(B), simplification(45), preserves-definedness] - rule A +Int B >Int C => B >Int C -Int A [concrete(A, C), symbolic(B), simplification(45), preserves-definedness] - rule A +Int B >=Int C => B >=Int C -Int A [concrete(A, C), symbolic(B), simplification(45), preserves-definedness] - - rule A -Int B A A <=Int C +Int B [concrete(B, C), symbolic(A), simplification(45), preserves-definedness] - rule A -Int B >Int C => A >Int C +Int B [concrete(B, C), symbolic(A), simplification(45), preserves-definedness] - rule A -Int B >=Int C => A >=Int C +Int B [concrete(B, C), symbolic(A), simplification(45), preserves-definedness] - - rule A -Int B A -Int C A -Int C <=Int B [concrete(A, C), symbolic(B), simplification(45), preserves-definedness] - rule A -Int B >Int C => A -Int C >Int B [concrete(A, C), symbolic(B), simplification(45), preserves-definedness] - rule A -Int B >=Int C => A -Int C >=Int B [concrete(A, C), symbolic(B), simplification(45), preserves-definedness] - - rule A A -Int B A -Int B <=Int C [concrete(A, B), symbolic(C), simplification(45), preserves-definedness] - rule A >Int B +Int C => A -Int B >Int C [concrete(A, B), symbolic(C), simplification(45), preserves-definedness] - rule A >=Int B +Int C => A -Int B >=Int C [concrete(A, B), symbolic(C), simplification(45), preserves-definedness] - - rule A A -Int C A -Int C <=Int B [concrete(A, C), symbolic(B), simplification(45), preserves-definedness] - rule A >Int B +Int C => A -Int C >Int B [concrete(A, C), symbolic(B), simplification(45), preserves-definedness] - rule A >=Int B +Int C => A -Int C >=Int B [concrete(A, C), symbolic(B), simplification(45), preserves-definedness] - - rule A C C <=Int B -Int A [concrete(A, B), symbolic(C), simplification(45), preserves-definedness] - rule A >Int B -Int C => C >Int B -Int A [concrete(A, B), symbolic(C), simplification(45), preserves-definedness] - rule A >=Int B -Int C => C >=Int B -Int A [concrete(A, B), symbolic(C), simplification(45), preserves-definedness] - - rule A A +Int C A +Int C <=Int B [concrete(A, C), symbolic(B), simplification(45), preserves-definedness] - rule A >Int B -Int C => A +Int C >Int B [concrete(A, C), symbolic(B), simplification(45), preserves-definedness] - rule A >=Int B -Int C => A +Int C >=Int B [concrete(A, C), symbolic(B), simplification(45), preserves-definedness] - - rule A +Int B ==Int C => A ==Int C -Int B [concrete(B, C), symbolic(A), simplification(45), comm, preserves-definedness] - rule A +Int B ==Int C => B ==Int C -Int A [concrete(A, C), symbolic(B), simplification(45), comm, preserves-definedness] - rule A -Int B ==Int C => A ==Int C +Int B [concrete(B, C), symbolic(A), simplification(45), comm, preserves-definedness] - rule A -Int B ==Int C => A -Int C ==Int B [concrete(A, C), symbolic(B), simplification(45), comm, preserves-definedness] - - rule { A +Int B #Equals C } => { A #Equals C -Int B } [concrete(B, C), symbolic(A), simplification(45), comm, preserves-definedness] - rule { A +Int B #Equals C } => { B #Equals C -Int A } [concrete(A, C), symbolic(B), simplification(45), comm, preserves-definedness] - rule { A -Int B #Equals C } => { A #Equals C +Int B } [concrete(B, C), symbolic(A), simplification(45), comm, preserves-definedness] - rule { A -Int B #Equals C } => { A -Int C #Equals B } [concrete(A, C), symbolic(B), simplification(45), comm, preserves-definedness] - - rule A +Int B A -Int C A -Int C <=Int D -Int B [concrete(B, D), symbolic(A, C), simplification(45), preserves-definedness] - rule A +Int B >Int C +Int D => A -Int C >Int D -Int B [concrete(B, D), symbolic(A, C), simplification(45), preserves-definedness] - rule A +Int B >=Int C +Int D => A -Int C >=Int D -Int B [concrete(B, D), symbolic(A, C), simplification(45), preserves-definedness] + rule A +Int B A A <=Int C -Int B [concrete(B, C), symbolic(A), simplification(45)] + rule A +Int B >Int C => A >Int C -Int B [concrete(B, C), symbolic(A), simplification(45)] + rule A +Int B >=Int C => A >=Int C -Int B [concrete(B, C), symbolic(A), simplification(45)] + + rule A +Int B B B <=Int C -Int A [concrete(A, C), symbolic(B), simplification(45)] + rule A +Int B >Int C => B >Int C -Int A [concrete(A, C), symbolic(B), simplification(45)] + rule A +Int B >=Int C => B >=Int C -Int A [concrete(A, C), symbolic(B), simplification(45)] + + rule A -Int B A A <=Int C +Int B [concrete(B, C), symbolic(A), simplification(45)] + rule A -Int B >Int C => A >Int C +Int B [concrete(B, C), symbolic(A), simplification(45)] + rule A -Int B >=Int C => A >=Int C +Int B [concrete(B, C), symbolic(A), simplification(45)] + + rule A -Int B A -Int C A -Int C <=Int B [concrete(A, C), symbolic(B), simplification(45)] + rule A -Int B >Int C => A -Int C >Int B [concrete(A, C), symbolic(B), simplification(45)] + rule A -Int B >=Int C => A -Int C >=Int B [concrete(A, C), symbolic(B), simplification(45)] + + rule A A -Int B A -Int B <=Int C [concrete(A, B), symbolic(C), simplification(45)] + rule A >Int B +Int C => A -Int B >Int C [concrete(A, B), symbolic(C), simplification(45)] + rule A >=Int B +Int C => A -Int B >=Int C [concrete(A, B), symbolic(C), simplification(45)] + + rule A A -Int C A -Int C <=Int B [concrete(A, C), symbolic(B), simplification(45)] + rule A >Int B +Int C => A -Int C >Int B [concrete(A, C), symbolic(B), simplification(45)] + rule A >=Int B +Int C => A -Int C >=Int B [concrete(A, C), symbolic(B), simplification(45)] + + rule A C C <=Int B -Int A [concrete(A, B), symbolic(C), simplification(45)] + rule A >Int B -Int C => C >Int B -Int A [concrete(A, B), symbolic(C), simplification(45)] + rule A >=Int B -Int C => C >=Int B -Int A [concrete(A, B), symbolic(C), simplification(45)] + + rule A A +Int C A +Int C <=Int B [concrete(A, C), symbolic(B), simplification(45)] + rule A >Int B -Int C => A +Int C >Int B [concrete(A, C), symbolic(B), simplification(45)] + rule A >=Int B -Int C => A +Int C >=Int B [concrete(A, C), symbolic(B), simplification(45)] + + rule A +Int B ==Int C => A ==Int C -Int B [concrete(B, C), symbolic(A), simplification(45), comm] + rule A +Int B ==Int C => B ==Int C -Int A [concrete(A, C), symbolic(B), simplification(45), comm] + rule A -Int B ==Int C => A ==Int C +Int B [concrete(B, C), symbolic(A), simplification(45), comm] + rule A -Int B ==Int C => A -Int C ==Int B [concrete(A, C), symbolic(B), simplification(45), comm] + + rule { A +Int B #Equals C } => { A #Equals C -Int B } [concrete(B, C), symbolic(A), simplification(45), comm] + rule { A +Int B #Equals C } => { B #Equals C -Int A } [concrete(A, C), symbolic(B), simplification(45), comm] + rule { A -Int B #Equals C } => { A #Equals C +Int B } [concrete(B, C), symbolic(A), simplification(45), comm] + rule { A -Int B #Equals C } => { A -Int C #Equals B } [concrete(A, C), symbolic(B), simplification(45), comm] + + rule A +Int B A -Int C A -Int C <=Int D -Int B [concrete(B, D), symbolic(A, C), simplification(45)] + rule A +Int B >Int C +Int D => A -Int C >Int D -Int B [concrete(B, D), symbolic(A, C), simplification(45)] + rule A +Int B >=Int C +Int D => A -Int C >=Int D -Int B [concrete(B, D), symbolic(A, C), simplification(45)] rule [int-eq-comm-concrete]: N:Int ==Int X:Int => X ==Int N @@ -93,12 +93,12 @@ module INT-SIMPLIFICATION-HASKELL [symbolic] rule A +Int B ==Int A => B ==Int 0 [simplification(40)] rule A +Int B ==Int B => A ==Int 0 [simplification(40)] rule A +Int B ==Int C +Int B => A ==Int C [simplification(40)] - rule A +Int B ==Int C +Int D => A -Int C ==Int D -Int B [simplification(45), symbolic(A, C), concrete(B, D), preserves-definedness] + rule A +Int B ==Int C +Int D => A -Int C ==Int D -Int B [simplification(45), symbolic(A, C), concrete(B, D)] rule { A +Int B #Equals A } => { B #Equals 0 } [simplification(40)] rule { A +Int B #Equals B } => { A #Equals 0 } [simplification(40)] rule { A +Int B #Equals C +Int B } => { A #Equals C } [simplification(40)] - rule { A +Int B #Equals C +Int D } => { A -Int C #Equals D -Int B } [simplification(45), symbolic(A, C), concrete(B, D), preserves-definedness] + rule { A +Int B #Equals C +Int D } => { A -Int C #Equals D -Int B } [simplification(45), symbolic(A, C), concrete(B, D)] rule 0 B B <=Int A [simplification, symbolic(A, B)] @@ -248,11 +248,11 @@ module INT-SIMPLIFICATION-COMMON rule [minint-lt-maxint-a]: minInt(A:Int, _B:Int) true requires A true requires B <=Int D - [simplification(40), preserves-definedness] + [simplification(40)] // ########################################################################### // inequality @@ -287,7 +287,7 @@ module INT-SIMPLIFICATION-COMMON rule A ==Int B => false requires 0 <=Int A andBool B false requires A false requires A true requires 0 <=Int X andBool notBool (X ==Int 0) [simplification(60)] 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 ebe2ebb861..5eb9ab3a8c 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 @@ -283,19 +283,19 @@ module LEMMAS-HASKELL [symbolic] rule [notBool-or]: notBool ( A orBool B ) => ( notBool A ) andBool ( notBool B ) [simplification(60)] rule [notBool-and]: notBool ( A andBool B ) => ( notBool A ) orBool ( notBool B ) [simplification(60)] - rule [bool-or-not-self]: B:Bool orBool notBool B:Bool => true [simplification] - rule [bool-not-or-self]: notBool B:Bool orBool B:Bool => true [simplification] - rule [bool-and-not-self]: B:Bool andBool notBool B:Bool => false [simplification] - rule [bool-not-and-self]: notBool B:Bool andBool B:Bool => false [simplification] - - rule [bool-eq-not-true-l]: {true #Equals notBool B:Bool} => {false #Equals B} [simplification, preserves-definedness] - rule [bool-eq-not-true-r]: {notBool B:Bool #Equals true } => {B #Equals false} [simplification, preserves-definedness] - rule [bool-eq-not-false-l]: {false #Equals notBool B:Bool} => {true #Equals B} [simplification, preserves-definedness] - rule [bool-eq-not-false-r]: {notBool B:Bool #Equals false} => {B #Equals true} [simplification, preserves-definedness] - - rule [bool-eq-and-true-l]: {true #Equals B1:Bool andBool B2:Bool} => {true #Equals B1} #And {true #Equals B2} [simplification, preserves-definedness] - rule [bool-eq-and-true-r]: {B1:Bool andBool B2:Bool #Equals true } => {B1 #Equals true} #And {B2 #Equals true} [simplification, preserves-definedness] - rule [bool-eq-or-false-l]: {false #Equals B1:Bool orBool B2:Bool} => {false #Equals B1} #And {false #Equals B2} [simplification, preserves-definedness] - rule [bool-eq-or-false-r]: {B1:Bool orBool B2:Bool #Equals false} => {B1 #Equals false} #And {B2 #Equals false} [simplification, preserves-definedness] + rule [bool-or-not-self]: B:Bool orBool notBool B:Bool => true [simplification] + rule [bool-not-or-self]: notBool B:Bool orBool B:Bool => true [simplification] + rule [bool-and-not-self]: B:Bool andBool notBool B:Bool => false [simplification] + rule [bool-not-and-self]: notBool B:Bool andBool B:Bool => false [simplification] + + rule [bool-eq-not-true-l]: { true #Equals notBool B:Bool } => { false #Equals B } [simplification] + rule [bool-eq-not-true-r]: { notBool B:Bool #Equals true } => { B #Equals false } [simplification] + rule [bool-eq-not-false-l]: { false #Equals notBool B:Bool } => { true #Equals B } [simplification] + rule [bool-eq-not-false-r]: { notBool B:Bool #Equals false } => { B #Equals true } [simplification] + + rule [bool-eq-and-true-l]: { true #Equals B1:Bool andBool B2:Bool } => { true #Equals B1 } #And { true #Equals B2 } [simplification] + rule [bool-eq-and-true-r]: { B1:Bool andBool B2:Bool #Equals true } => { B1 #Equals true } #And { B2 #Equals true } [simplification] + rule [bool-eq-or-false-l]: { false #Equals B1:Bool orBool B2:Bool } => { false #Equals B1 } #And { false #Equals B2 } [simplification] + rule [bool-eq-or-false-r]: { B1:Bool orBool B2:Bool #Equals false } => { B1 #Equals false } #And { B2 #Equals false} [simplification] endmodule From ee9a0d2f3476248f8557e44024f2ba3596c82c22 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Thu, 4 Jun 2026 20:51:51 +0000 Subject: [PATCH 18/25] evm.md: formatting --- kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md index 600e43c51d..27547a6feb 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md @@ -1813,7 +1813,7 @@ System Transaction Configuration ```k syntax Int ::= #widthOpCode(Int) [symbol(#widthOpCode), function, total, smtlib(widthOpCode)] - // ----------------------------------------------------------------- + // --------------------------------------------------------------------------------------------- rule #widthOpCode(W) => W -Int 94 requires W >=Int 96 andBool W <=Int 127 rule #widthOpCode(_) => 1 [owise] From 6cd5f0deb8cdae8efc2a9a2c744c4e8d150f8319 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Thu, 4 Jun 2026 21:09:56 +0000 Subject: [PATCH 19/25] buf.md: relax powByteLen-lt-concrete to concrete(CONST) only (review) Per review: N need not be syntactically concrete -- once N is concrete the `requires CONST --- kevm-pyk/src/kevm_pyk/kproj/evm-semantics/buf.md | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/buf.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/buf.md index 1ea46865b8..8fa8a76285 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/buf.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/buf.md @@ -41,13 +41,14 @@ module BUF rule 0 true requires 0 <=Int SIZE [simplification, preserves-definedness] rule SIZE true requires 0 <=Int SIZE [simplification, preserves-definedness] - // Concrete comparison: CONST < #powByteLen(N) evaluates when both arguments are concrete. - // Needed because 2^Int(8*N) is rewritten to #powByteLen(N) even for concrete N (via the - // symbolic(N) rule firing before path-condition lookup makes N concrete), but #powByteLen - // has no-evaluators so the result can't be computed directly. + // Concrete comparison: CONST < #powByteLen(N) when CONST < 2^(8*N). + // 2^Int(8*N) is rewritten to #powByteLen(N) even for concrete N (the symbolic(N) + // rule fires before the path condition makes N concrete), but #powByteLen has + // no-evaluators so the comparison can't self-evaluate. Only CONST need be + // concrete: once N is concrete the requires reduces to a linear inequality. rule [powByteLen-lt-concrete]: CONST true requires 0 <=Int N andBool CONST WM [ IDX := #buf(1, VAL) ] [simplification] rule #bufStrict(SIZE, DATA) => #buf(SIZE, DATA) From 761f1f30d881119a86634f2a0d857bea9646324a Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Thu, 4 Jun 2026 21:09:56 +0000 Subject: [PATCH 20/25] lemmas/lemmas.k: drop widthOpCode-concat-{left,right} (review) Per review: bytes-simplification.k already provides bytes-concat-lookup-{left, right}, so these were only a workaround for booster not descending into #widthOpCode(...) to apply them. Remove rather than duplicate per-function; if the non-descent persists it should be addressed in the backend. Co-Authored-By: Claude Opus 4.8 --- .../kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k | 13 ------------- 1 file changed, 13 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 5eb9ab3a8c..8ea4e413ad 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 @@ -256,19 +256,6 @@ module LEMMAS-HASKELL [symbolic] rule [widthOpCode-lb]: 0 <=Int #widthOpCode(_:Int) => true [simplification, smt-lemma] rule [widthOpCode-ub]: #widthOpCode(_:Int) <=Int 33 => true [simplification, smt-lemma] - // Booster's equation engine does not descend inside #widthOpCode(...) to - // apply bytes-concat-lookup-{left,right}. These rules compose the two - // steps so the full concrete-prefix lookup can be reduced in one go. - rule [widthOpCode-concat-left]: - #widthOpCode ( ( B1:Bytes +Bytes _B2:Bytes ) [ I:Int ] ) => #widthOpCode ( B1 [ I ] ) - requires 0 <=Int I andBool I #widthOpCode ( B2 [ I -Int lengthBytes ( B1 ) ] ) - requires lengthBytes ( B1 ) <=Int I - [simplification, preserves-definedness] - // ######################## // Boolean Logic // ######################## From 6c6d9dfca83246c0f98caf4821ee56a54fd11acc Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Fri, 5 Jun 2026 14:01:31 +0000 Subject: [PATCH 21/25] lemmas/lemmas.k, tests/specs/functional/lemmas-no-smt-spec.k: drop unused bool-eq #Equals rules Whole-prove-suite rule-firing measurement (booster Simplify + kore SimplifyKore logging over functional/benchmarks/erc20/examples/kontrol/mcd) shows the eight bool-eq-* ML-#Equals distribution rules are never applied by the booster: five fire in no engine at all, and three (bool-eq-not-true-l/r, bool-eq-and-true-l) fire only in the kore-rpc implies/subsumption path. Since this PR targets booster performance and these proofs already discharge those goals under kore without the rules, all eight are removed. The bool-*-self rules are kept (they fire in the booster). The bool-eq-not-false coverage claim, which was discharged by bool-eq-not-true-l rather than by the not-false rules, is removed with them. Verified: lemmas-no-smt-spec proves all 22 remaining claims under --use-booster. Co-Authored-By: Claude Opus 4.8 --- .../src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k | 10 ---------- tests/specs/functional/lemmas-no-smt-spec.k | 4 ---- 2 files changed, 14 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 8ea4e413ad..0dcf1b17a5 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 @@ -275,14 +275,4 @@ module LEMMAS-HASKELL [symbolic] rule [bool-and-not-self]: B:Bool andBool notBool B:Bool => false [simplification] rule [bool-not-and-self]: notBool B:Bool andBool B:Bool => false [simplification] - rule [bool-eq-not-true-l]: { true #Equals notBool B:Bool } => { false #Equals B } [simplification] - rule [bool-eq-not-true-r]: { notBool B:Bool #Equals true } => { B #Equals false } [simplification] - rule [bool-eq-not-false-l]: { false #Equals notBool B:Bool } => { true #Equals B } [simplification] - rule [bool-eq-not-false-r]: { notBool B:Bool #Equals false } => { B #Equals true } [simplification] - - rule [bool-eq-and-true-l]: { true #Equals B1:Bool andBool B2:Bool } => { true #Equals B1 } #And { true #Equals B2 } [simplification] - rule [bool-eq-and-true-r]: { B1:Bool andBool B2:Bool #Equals true } => { B1 #Equals true } #And { B2 #Equals true } [simplification] - rule [bool-eq-or-false-l]: { false #Equals B1:Bool orBool B2:Bool } => { false #Equals B1 } #And { false #Equals B2 } [simplification] - rule [bool-eq-or-false-r]: { B1:Bool orBool B2:Bool #Equals false } => { B1 #Equals false } #And { B2 #Equals false} [simplification] - endmodule diff --git a/tests/specs/functional/lemmas-no-smt-spec.k b/tests/specs/functional/lemmas-no-smt-spec.k index d53a57de5a..cf269ed100 100644 --- a/tests/specs/functional/lemmas-no-smt-spec.k +++ b/tests/specs/functional/lemmas-no-smt-spec.k @@ -43,10 +43,6 @@ module LEMMAS-NO-SMT-SPEC claim [bool-simpl-02]: runLemma ( bool2Word( B:Bool ) ==Int 1 ) => doneLemma ( B ==K true ) ... claim [bool-simpl-03]: runLemma ( 1 ==Int bool2Word( B:Bool ) ) => doneLemma ( B ==K true ) ... - claim [bool-eq-not-false]: - runLemma ( B:Bool ) => doneLemma ( false ) ... - requires notBool B - claim [range-empty-neg-start]: runLemma ( #range(B:Bytes, 0 -Int 1, 5) ==K .Bytes ) => doneLemma ( true ) ... From 351b480b46ea4674ea6dab03386545083fe543fb Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Fri, 5 Jun 2026 16:43:03 +0000 Subject: [PATCH 22/25] tests/specs/mcd/verification.k: mark keccak disequality [smt-lemma] to fix DSS/MCD implies failures The new tier1 simplification lemmas simplify away the keccak path-condition constraint during EVM execution, so the final subsumption check can no longer prove `keccak(_) =/=Int smallInt` from the path condition alone. Encoding the rule as an SMT lemma lets Z3 discharge it independently of the path condition. This matches the treatment already present in mcd-structured/verification.k, whose sibling proofs pass; the plain mcd suite lacked the annotation. Fixes the heal/fold/frob-diff-zero-dart DSS proofs and the mcd flopper-tick/end-pack rule proofs. Verified mcd/end-pack-pass-rough-spec.k passes with the change. Co-Authored-By: Claude Opus 4.8 --- tests/specs/mcd/verification.k | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/specs/mcd/verification.k b/tests/specs/mcd/verification.k index cf400bac8b..2bcc3e0045 100644 --- a/tests/specs/mcd/verification.k +++ b/tests/specs/mcd/verification.k @@ -139,7 +139,7 @@ module LEMMAS-MCD [symbolic] // Keccak // ######################## - rule keccak(_) ==Int I => false requires #rangeSmall(I) [simplification] + rule keccak(_) ==Int I => false requires #rangeSmall(I) [simplification, smt-lemma] rule keccak(_) +Int I1 ==Int I2 => false requires #rangeSmall(I1) andBool #rangeSmall(I2) [simplification] From 293a1a4699a6cb98f2487bf04148f1be706d98bf Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Mon, 8 Jun 2026 13:57:10 +0000 Subject: [PATCH 23/25] Revert "buf.md: relax powByteLen-lt-concrete to concrete(CONST) only (review)" This reverts commit 6cd5f0deb8cdae8efc2a9a2c744c4e8d150f8319. --- kevm-pyk/src/kevm_pyk/kproj/evm-semantics/buf.md | 11 +++++------ 1 file changed, 5 insertions(+), 6 deletions(-) diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/buf.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/buf.md index 8fa8a76285..1ea46865b8 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/buf.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/buf.md @@ -41,14 +41,13 @@ module BUF rule 0 true requires 0 <=Int SIZE [simplification, preserves-definedness] rule SIZE true requires 0 <=Int SIZE [simplification, preserves-definedness] - // Concrete comparison: CONST < #powByteLen(N) when CONST < 2^(8*N). - // 2^Int(8*N) is rewritten to #powByteLen(N) even for concrete N (the symbolic(N) - // rule fires before the path condition makes N concrete), but #powByteLen has - // no-evaluators so the comparison can't self-evaluate. Only CONST need be - // concrete: once N is concrete the requires reduces to a linear inequality. + // Concrete comparison: CONST < #powByteLen(N) evaluates when both arguments are concrete. + // Needed because 2^Int(8*N) is rewritten to #powByteLen(N) even for concrete N (via the + // symbolic(N) rule firing before path-condition lookup makes N concrete), but #powByteLen + // has no-evaluators so the result can't be computed directly. rule [powByteLen-lt-concrete]: CONST true requires 0 <=Int N andBool CONST WM [ IDX := #buf(1, VAL) ] [simplification] rule #bufStrict(SIZE, DATA) => #buf(SIZE, DATA) From 486068ce9e429fda8a06495b34805b65d690fe51 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Tue, 9 Jun 2026 14:01:26 +0000 Subject: [PATCH 24/25] tests/failing-symbolic.haskell-booster-dev: drop 5 specs now passing under booster-dev Verified by running the booster-dev binary over the full skip-list on this branch: mcd-structured/dsvalue-peek-pass-rough now passes under tier1's lemmas (failed on master), and 4 entries (functional/bitwise-{asword,simplifications}, mcd[-structured]/dsvalue-read-pass-summarize) were stale (already passing on master). bitwise-mask-shift-spec.k is intentionally kept: it regresses under booster-dev on this branch. Co-Authored-By: Claude Opus 4.8 --- tests/failing-symbolic.haskell-booster-dev | 5 ----- 1 file changed, 5 deletions(-) diff --git a/tests/failing-symbolic.haskell-booster-dev b/tests/failing-symbolic.haskell-booster-dev index 897d760720..56a94f2e18 100644 --- a/tests/failing-symbolic.haskell-booster-dev +++ b/tests/failing-symbolic.haskell-booster-dev @@ -59,9 +59,7 @@ tests/specs/examples/solidity-code-spec.md tests/specs/examples/storage-spec.md tests/specs/examples/sum-to-n-foundry-spec.k tests/specs/examples/sum-to-n-spec.k -tests/specs/functional/bitwise-asword-spec.k tests/specs/functional/bitwise-mask-shift-spec.k -tests/specs/functional/bitwise-simplifications-spec.k tests/specs/functional/bytes-range-spec.k tests/specs/functional/evm-int-simplifications-spec.k tests/specs/functional/infinite-gas-spec.k @@ -96,7 +94,6 @@ tests/specs/mcd/dai-adduu-fail-rough-spec.k tests/specs/mcd/dstoken-approve-fail-rough-spec.k tests/specs/mcd/dsvalue-peek-pass-rough-spec.k tests/specs/mcd/dsvalue-read-pass-spec.k -tests/specs/mcd/dsvalue-read-pass-summarize-spec.k tests/specs/mcd/end-cash-pass-rough-spec.k tests/specs/mcd/end-pack-pass-rough-spec.k tests/specs/mcd/end-subuu-pass-spec.k @@ -116,8 +113,6 @@ tests/specs/mcd-structured/cat-exhaustiveness-spec.k tests/specs/mcd-structured/cat-file-addr-pass-rough-spec.k tests/specs/mcd-structured/dai-adduu-fail-rough-spec.k tests/specs/mcd-structured/dstoken-approve-fail-rough-spec.k -tests/specs/mcd-structured/dsvalue-peek-pass-rough-spec.k -tests/specs/mcd-structured/dsvalue-read-pass-summarize-spec.k tests/specs/mcd-structured/end-cash-pass-rough-spec.k tests/specs/mcd-structured/end-pack-pass-rough-spec.k tests/specs/mcd-structured/end-subuu-pass-spec.k From 24484e78e2fb9e294ad439ad60f9ed67746686dd Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Tue, 9 Jun 2026 16:58:30 +0000 Subject: [PATCH 25/25] tests/failing-symbolic.haskell-booster-dev: re-add 2 dsvalue-read-pass-summarize specs failing booster-dev in CI PR #2859 CI 'Proofs: Rules (booster-dev)' failed on mcd/dsvalue-read-pass-summarize and mcd-structured/dsvalue-read-pass-summarize (SystemExit: 1); local verification diverged from CI. Re-add them; the other three drops (mcd-structured/dsvalue-peek-pass-rough and functional/bitwise-{asword,simplifications}) pass in CI and stay removed. Co-Authored-By: Claude Opus 4.8 --- tests/failing-symbolic.haskell-booster-dev | 2 ++ 1 file changed, 2 insertions(+) diff --git a/tests/failing-symbolic.haskell-booster-dev b/tests/failing-symbolic.haskell-booster-dev index 56a94f2e18..da378e008c 100644 --- a/tests/failing-symbolic.haskell-booster-dev +++ b/tests/failing-symbolic.haskell-booster-dev @@ -94,6 +94,7 @@ tests/specs/mcd/dai-adduu-fail-rough-spec.k tests/specs/mcd/dstoken-approve-fail-rough-spec.k tests/specs/mcd/dsvalue-peek-pass-rough-spec.k tests/specs/mcd/dsvalue-read-pass-spec.k +tests/specs/mcd/dsvalue-read-pass-summarize-spec.k tests/specs/mcd/end-cash-pass-rough-spec.k tests/specs/mcd/end-pack-pass-rough-spec.k tests/specs/mcd/end-subuu-pass-spec.k @@ -113,6 +114,7 @@ tests/specs/mcd-structured/cat-exhaustiveness-spec.k tests/specs/mcd-structured/cat-file-addr-pass-rough-spec.k tests/specs/mcd-structured/dai-adduu-fail-rough-spec.k tests/specs/mcd-structured/dstoken-approve-fail-rough-spec.k +tests/specs/mcd-structured/dsvalue-read-pass-summarize-spec.k tests/specs/mcd-structured/end-cash-pass-rough-spec.k tests/specs/mcd-structured/end-pack-pass-rough-spec.k tests/specs/mcd-structured/end-subuu-pass-spec.k