Simplification lemmas to improve Haskell booster coverage

kevm-pyk/src/kevm_pyk/kproj/evm-semantics/buf.md

@@ -37,10 +37,17 @@ 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    <Int #powByteLen(SIZE) => true requires 0 <=Int SIZE [simplification, preserves-definedness]
     rule SIZE <Int #powByteLen(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 <Int #powByteLen(N) => true
+        requires 0 <=Int N andBool CONST <Int 2 ^Int (8 *Int N)
+        [simplification, concrete(CONST, N), preserves-definedness]
     rule #write(WM, IDX, VAL) => WM [ IDX := #buf(1, VAL) ] [simplification]
 
     rule #bufStrict(SIZE, DATA) => #buf(SIZE, DATA)

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]
 

kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md

@@ -1812,8 +1812,8 @@ 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]
 

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]
+    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)]
@@ -306,5 +310,5 @@ module BYTES-SIMPLIFICATION [symbolic]
     rule [lookup-as-asWord]:
       B:Bytes [ I:Int ] => #asWord ( #range ( B, I, 1 ) )
       requires 0 <=Int I andBool I <Int lengthBytes(B)
-      [simplification(60)]
+      [simplification(60), preserves-definedness]
 endmodule

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 <Int minInt ( 2 ^Int (8 *Int WB), pow256 )
     [simplification, concrete(WB), preserves-definedness]
 
+  // Specialisation for 32-byte buf with rangeUInt(256) side-condition: avoids
+  // the minInt(2^256, pow256) evaluation that Booster cannot match against the
+  // path condition's 2^Int 256 tree form.
+  rule [asWord-buf-inversion-rangeUInt256]:
+    #asWord ( #buf ( 32, X:Int ) ) => X
+    requires #rangeUInt ( 256, X )
+    [simplification]
+
   // 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 ) ) )
@@ -123,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 )  <Int X:Int => false requires X <=Int #asWord ( B ) [simplification]
+  rule [asWord-le-false]: #asWord ( B:Bytes ) <=Int X:Int => false requires X  <Int #asWord ( B ) [simplification]
+  // Comparison: `#asWord(B) == X` is false when the path condition says X =/= #asWord(B).
+  // The requires X =/=Int #asWord(B) expands to notBool(X ==Int #asWord(B)) via the K builtin;
+  // since ==Int is comm, this matches the path condition fact notBool(#asWord(B) ==Int X).
+  // No loop: our rule matches #asWord on the LEFT; after builtin expansion the recursive
+  // term X ==Int #asWord(B) has X on the LEFT, so this rule does not fire on it.
+  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 `<Int`
   rule [asWord-concat-lt]:
     #asWord ( BA1 +Bytes BA2 ) <Int X:Int => #asWord ( BA1 ) <Int X /Int ( 2 ^Int ( 8 *Int lengthBytes ( BA2 ) ) )

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)]
@@ -101,6 +105,11 @@ module INT-SIMPLIFICATION-HASKELL [symbolic]
     rule A -Int B  <Int 0 => A  <Int B [simplification, symbolic(A, B)]
     rule A -Int B <=Int 0 => 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  <Int B:Int andBool C:Int <=Int A:Int => false requires B <=Int C [simplification, concrete(B, C)]
+    rule C:Int <=Int A:Int andBool A:Int  <Int B:Int => false requires B <=Int C [simplification, concrete(B, C)]
+
 endmodule
 
 module INT-SIMPLIFICATION-COMMON
@@ -133,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)
@@ -232,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 <Int maxInt / minInt <=Int maxInt: priority 40 fires before the default-priority (50) expansion rules,
+    // so Booster sees `true` directly rather than a disjunction requiring path-condition reasoning.
+    // Sound: minInt(A,_) <=Int A and C <=Int maxInt(C,_), so A <Int C implies minInt(A,_) <Int maxInt(C,_).
+    rule [minint-lt-maxint-a]:
+        minInt(A:Int, _B:Int) <Int maxInt(C:Int, _D:Int) => true
+        requires A <Int C
+        [simplification(40)]
+    rule [minint-leq-maxint-b]:
+        minInt(_A:Int, B:Int) <=Int maxInt(_C:Int, D:Int) => true
+        requires B <=Int D
+        [simplification(40)]
+
   // ###########################################################################
   // inequality
   // ###########################################################################
@@ -241,6 +263,14 @@ module INT-SIMPLIFICATION-COMMON
 
     rule A <Int A -Int B => false requires 0 <=Int B [simplification]
 
+    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 <Int B:Int andBool B:Int <Int A:Int => false [simplification]
+
     rule 0 <Int 1 <<Int A => true requires 0 <=Int A [simplification, preserves-definedness]
 
     // inequality sign normalization
@@ -256,6 +286,9 @@ module INT-SIMPLIFICATION-COMMON
 
     rule A ==Int B => false requires 0 <=Int A andBool B <Int 0 [simplification, concrete(B)]
 
+    // A ==Int B is false when A < B is a known path-condition fact (B concrete).
+    rule [eq-false-lt]: A:Int ==Int B:Int => false requires A <Int B [simplification, concrete(B)]
+
     rule 0 <Int X => true requires 0 <=Int X andBool notBool (X ==Int 0) [simplification(60)]
 
     rule X <=Int maxUInt256 => X <Int pow256 [simplification]

kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k

@@ -245,6 +245,17 @@ 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]
+
   // ########################
   // Boolean Logic
   // ########################
@@ -259,4 +270,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

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
@@ -116,7 +114,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/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
       <k> 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)
+      ...
       </k>
 
+    claim [pow-byte-len-simplify]:
+      <k> runLemma ( 2 ^Int (8 *Int N:Int) ) => doneLemma ( #powByteLen(N:Int) ) ... </k>
+      requires 0 <=Int N
+
 endmodule

tests/specs/functional/int-simplifications-spec.k

@@ -127,4 +127,19 @@ module INT-SIMPLIFICATIONS-SPEC
 
     claim [le-maxuint256]: <k> runLemma ( X <=Int maxUInt256 ) => doneLemma ( X <Int pow256 ) ... </k>
 
+ // Comparison normalization coverage (int-simplification.k [preserves-definedness])
+ // ---------------------------------------------------------------------------------
+
+    claim [int-comp-norm-add-lt]:
+      <k> runLemma ( X:Int +Int 3 <Int 10 ) => doneLemma ( X:Int <Int 7 ) ... </k>
+
+    claim [int-comp-norm-add-le]:
+      <k> runLemma ( X:Int +Int 3 <=Int 10 ) => doneLemma ( X:Int <=Int 7 ) ... </k>
+
+    claim [int-comp-norm-sub-lt]:
+      <k> runLemma ( X:Int -Int 3 <Int 10 ) => doneLemma ( X:Int <Int 13 ) ... </k>
+
+    claim [int-comp-norm-rhs-add-lt]:
+      <k> runLemma ( 7 <Int X:Int +Int 3 ) => doneLemma ( 4 <Int X:Int ) ... </k>
+
 endmodule

tests/specs/functional/lemmas-no-smt-spec.k

@@ -43,4 +43,46 @@ module LEMMAS-NO-SMT-SPEC
     claim [bool-simpl-02]: <k> runLemma ( bool2Word( B:Bool ) ==Int 1 )   => doneLemma ( B ==K true ) ... </k>
     claim [bool-simpl-03]: <k> runLemma ( 1 ==Int bool2Word( B:Bool ) )   => doneLemma ( B ==K true ) ... </k>
 
+    claim [range-empty-neg-start]:
+      <k> runLemma ( #range(B:Bytes, 0 -Int 1, 5) ==K .Bytes ) => doneLemma ( true ) ... </k>
+
+    claim [range-empty-zero-width]:
+      <k> runLemma ( #range(B:Bytes, 3, 0) ==K .Bytes ) => doneLemma ( true ) ... </k>
+
+ // #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]:
+      <k> runLemma ( #asWord(B:Bytes) <Int 0 ) => doneLemma ( false ) ... </k>
+
+    // asWord-le-false: #asWord(B) <=Int X => false when X <Int #asWord(B)
+    claim [asword-le-false]:
+      <k> runLemma ( #asWord(B:Bytes) <=Int 0 ) => doneLemma ( false ) ... </k>
+      requires 0 <Int #asWord(B)
+
+    // asword-eq-false: #asWord(B) ==Int X => 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]:
+      <k> runLemma ( #asWord(B:Bytes) ==Int X:Int ) => doneLemma ( false ) ... </k>
+      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]:
+      <k> runLemma ( X:Int ==Int 42 ) => doneLemma ( false ) ... </k>
+      requires X <Int 42
+
+ // #powByteLen concrete comparison
+ // --------------------------------
+
+    // powByteLen-lt-concrete: CONST <Int #powByteLen(N) => 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]:
+      <k> runLemma ( 31 <Int #powByteLen(32) ) => doneLemma ( true ) ... </k>
+
 endmodule

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]