General slot updates and test suite extension (#2587)

* extending test suites

* not running structured mcd tests with booster-dev

* more general slot update and division lemmas

* normalisation of *Int

* multiplication normalisation continuation

* additional lemma

* additional lemma

* functional spec passing

* correction

* mcd should not use slot updates, lemma corrections

* typo

* commutativity lemma

* lemma corrections

* correcting the double requires...

* minor corrections

* further refinements

* corrections

* refining lemmas, adding tests

* formatting error correction...

* further corrections

* more owises and test suite

* unconditional overflow trim

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

@@ -11,7 +11,7 @@ module BUF-SYNTAX
 Both `#bufStrict(SIZE, DATA)` and `#buf(SIZE, DATA)` represents a symbolic byte array of length `SIZE` bytes, left-padded with zeroes.
 Version `#bufStrict` is partial and only defined when `DATA` is in the range given by `SIZE`.
 It rewrites to `#buf` when data is in range, and is expected to immediately evaluate into `#buf` in all contexts.
-Version `#buf` is total and artificially defined `modulo 2 ^Int (SIZE *Int 8)`.
+Version `#buf` is total and artificially defined `modulo 2 ^Int (8 *Int SIZE)`.
 This division is required to facilitate symbolic reasoning in Haskell backend, because Haskell has limitations
 when dealing with partial functions.
 
@@ -36,17 +36,17 @@ module BUF
 
     syntax Int ::= #powByteLen ( Int ) [symbol(#powByteLen), function, no-evaluators]
  // ---------------------------------------------------------------------------------
- // rule #powByteLen(SIZE) => 2 ^Int (SIZE *Int 8)
-    rule 2 ^Int (SIZE *Int 8) => #powByteLen(SIZE) [symbolic(SIZE), simplification]
+ // rule #powByteLen(SIZE) => 2 ^Int (8 *Int SIZE)
+    rule 2 ^Int (8 *Int SIZE) => #powByteLen(SIZE) [symbolic(SIZE), simplification]
 
     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]
     rule #write(WM, IDX, VAL) => WM [ IDX := #buf(1, VAL) ] [simplification]
 
     rule #bufStrict(SIZE, DATA) => #buf(SIZE, DATA)
-      requires #range(0 <= DATA < (2 ^Int (SIZE *Int 8)))
+      requires #range(0 <= DATA < (2 ^Int (8 *Int SIZE)))
 
-    rule #buf(SIZE, DATA) => #padToWidth(SIZE, #asByteStack(DATA %Int (2 ^Int (SIZE *Int 8))))
+    rule #buf(SIZE, DATA) => #padToWidth(SIZE, #asByteStack(DATA %Int (2 ^Int (8 *Int SIZE))))
       requires 0 <Int SIZE
       [concrete]
     rule #buf(_SIZE, _) => .Bytes [owise, concrete] // SIZE <= 0

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

@@ -190,8 +190,8 @@ Bitwise logical operators are lifted from the integer versions.
     rule bit (N, _) => 0 requires notBool (N >=Int 0 andBool N <Int 256)
     rule byte(N, _) => 0 requires notBool (N >=Int 0 andBool N <Int  32)
 
-    rule bit (N, W) => bitRangeInt(W , (255 -Int N)        , 1) requires N >=Int 0 andBool N <Int 256
-    rule byte(N, W) => bitRangeInt(W , ( 31 -Int N) *Int 8 , 8) requires N >=Int 0 andBool N <Int  32
+    rule bit (N, W) => bitRangeInt(W , (255 -Int N)       , 1) requires N >=Int 0 andBool N <Int 256
+    rule byte(N, W) => bitRangeInt(W , 8 *Int (31 -Int N) , 8) requires N >=Int 0 andBool N <Int  32
 ```
 
 -   `#nBits` shifts in `N` ones from the right.
@@ -202,7 +202,7 @@ Bitwise logical operators are lifted from the integer versions.
                  | #nBytes ( Int )  [symbol(#nBytes), function]
  // -----------------------------------------------------------
     rule #nBits(N)  => (1 <<Int N) -Int 1 requires N >=Int 0
-    rule #nBytes(N) => #nBits(N *Int 8)   requires N >=Int 0
+    rule #nBytes(N) => #nBits(8 *Int N)   requires N >=Int 0
 ```
 
 -   `signextend(N, W)` sign-extends from byte `N` of `W` (0 being MSB).

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

@@ -75,17 +75,27 @@ module BYTES-SIMPLIFICATION [symbolic]
     rule [buf-asWord-invert-rl]:
       #asWord ( #buf ( WB:Int, X:Int ) ) => X
       requires 0 <=Int WB andBool 0 <=Int X andBool
-               ( ( WB <=Int 32 andBool X <Int 2 ^Int (WB *Int 8) ) orBool
+               ( ( WB <=Int 32 andBool X <Int 2 ^Int (8 *Int WB) ) orBool
                  ( WB  >Int 32 andBool X <Int pow256 ) )
       [simplification, concrete(WB), preserves-definedness]
 
     rule [buf-asWord-invert-rl-range]:
       #asWord ( #range ( #buf ( WB:Int, X:Int ), S:Int, WR:Int ) ) => X
       requires 0 <=Int WB andBool 0 <=Int X andBool 0 <=Int S andBool 0 <=Int WR
        andBool S +Int WR ==Int WB
-       andBool X <Int 2 ^Int (WR *Int 8)
+       andBool X <Int 2 ^Int (8 *Int WR)
       [simplification, concrete(WB, S, WR), preserves-definedness]
 
+    rule [asWord-trim-leading-zeros-concat]:
+      #asWord ( BZ +Bytes B ) => #asWord ( B )
+      requires #asInteger ( BZ ) ==Int 0
+      [simplification, concrete(BZ)]
+
+    rule [asWord-trim-overflowing-zeros]:
+      #asWord ( B ) => #asWord ( #range(B, lengthBytes(B) -Int 32, 32) )
+      requires 32 <Int lengthBytes(B)
+      [simplification]
+
     rule [buf-zero-concat-base]:
       #buf(W1:Int, 0) +Bytes #buf(W2:Int, 0) => #buf(W1 +Int W2, 0)
       requires 0 <=Int W1 andBool 0 <=Int W2
@@ -189,13 +199,13 @@ module BYTES-SIMPLIFICATION [symbolic]
 
     rule [range-buf-zero-concat]:
       B:Bytes +Bytes #buf(W:Int, X:Int) => #buf(lengthBytes(B) +Int W, X)
-      requires 0 <=Int W andBool 0 <=Int X andBool X <Int 2 ^Int (W *Int 8)
+      requires 0 <=Int W andBool 0 <=Int X andBool X <Int 2 ^Int (8 *Int W)
        andBool #asInteger(B) ==Int 0 andBool lengthBytes(B) +Int W <=Int 32
       [concrete(B, W), simplification, preserves-definedness]
 
     rule [range-buf-zero-concat-extend]:
       B1:Bytes +Bytes #buf(W:Int, X:Int) +Bytes B2 => #buf(lengthBytes(B1) +Int W, X) +Bytes B2
-      requires 0 <=Int W andBool 0 <=Int X andBool X <Int 2 ^Int (W *Int 8)
+      requires 0 <=Int W andBool 0 <=Int X andBool X <Int 2 ^Int (8 *Int W)
        andBool #asInteger(B1) ==Int 0 andBool lengthBytes(B1) +Int W <=Int 32
       [concrete(B1, W), simplification, preserves-definedness]
 

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

@@ -62,7 +62,7 @@ module EVM-INT-SIMPLIFICATION-COMMON
 
   rule [asWord-lt]:
     #asWord ( BA ) <Int X => true
-    requires 2 ^Int ( lengthBytes(BA) *Int 8) <=Int X
+    requires 2 ^Int ( 8 *Int lengthBytes(BA) ) <=Int X
     [concrete(X), simplification]
 
   rule [asWord-lt-concat]:

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

@@ -6,11 +6,9 @@ module INT-SIMPLIFICATION-HASKELL [symbolic]
     imports INT-SIMPLIFICATION-COMMON
 
   // ###########################################################################
-  // add, sub
+  // add, sub: associativity normalization
   // ###########################################################################
 
-    // associativity normalization
-
     rule A +Int (B +Int C) => (A +Int B) +Int C [symbolic(A, B), concrete(C), simplification(40)]
     rule A +Int (B -Int C) => (A +Int B) -Int C [symbolic(A, B), concrete(C), simplification(40)]
     rule A -Int (B +Int C) => (A -Int B) -Int C [symbolic(A, B), concrete(C), simplification(40)]
@@ -30,7 +28,7 @@ module INT-SIMPLIFICATION-HASKELL [symbolic]
     rule (A -Int B) -Int C => A -Int (B +Int C) [concrete(B, C), symbolic(A), simplification(40)]
 
   // ###########################################################################
-  // comparison normalization
+  // add, sub: comparison normalization
   // ###########################################################################
 
     rule A +Int B   <Int C => A  <Int C -Int B [concrete(B, C), symbolic(A), simplification(45)]
@@ -88,9 +86,15 @@ 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 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 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 #Equals C +Int D } => { A -Int C #Equals D -Int B } [concrete(B, D), symbolic(A, C), simplification(45)]
+    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)]
 
 endmodule
 
@@ -134,10 +138,10 @@ module INT-SIMPLIFICATION-COMMON
   // mul
   // ###########################################################################
 
+    rule A *Int B => B *Int A [simplification, symbolic(A), concrete(B)]
+
     rule 1 *Int A => A [simplification]
-    rule A *Int 1 => A [simplification]
     rule 0 *Int _ => 0 [simplification]
-    rule _ *Int 0 => 0 [simplification]
 
     rule (A *Int C) +Int (B *Int C) => (A +Int B) *Int C [simplification]
     rule (A *Int C) -Int (B *Int C) => (A -Int B) *Int C [simplification]
@@ -151,11 +155,15 @@ module INT-SIMPLIFICATION-COMMON
     rule A /Int 1 => A  [simplification, preserves-definedness]
 
     // safeMath mul check c / a == b where c == a * b
-    rule (A *Int B) /Int A => B requires A =/=Int 0 [simplification, preserves-definedness]
+    rule (A *Int B) /Int A => B requires notBool A ==Int 0 [simplification, preserves-definedness]
+    rule (B *Int A) /Int A => B requires notBool A ==Int 0 [simplification, preserves-definedness]
 
-    rule ((A *Int B) /Int C) /Int B => A /Int C requires B =/=Int 0 andBool C =/=Int 0 [simplification, preserves-definedness]
+    rule ((A *Int B) /Int C) /Int B => A /Int C requires 0 <Int B andBool 0 <Int C [simplification, preserves-definedness]
+    rule ((A *Int B) /Int C) /Int A => B /Int C requires 0 <Int A andBool 0 <Int C [simplification, preserves-definedness]
 
-    rule (A /Int 32) *Int 32 => A requires A modInt 32 ==Int 0 [simplification, preserves-definedness]
+    rule (A *Int B) /Int C => B *Int (A /Int C)
+      requires notBool C ==Int 0 andBool A modInt C ==Int 0
+      [simplification, concrete(A, C), preserves-definedness]
 
     rule (A *Int B) /Int C <=Int D => true
       requires 0 <=Int A andBool 0 <=Int B andBool 0 <Int C andBool A <=Int D andBool B <=Int C

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

@@ -4,10 +4,14 @@ requires "bitwise-simplification.k"
 requires "bytes-simplification.k"
 requires "evm-int-simplification.k"
 requires "int-simplification.k"
-
-
+requires "slot-updates.k"
 
 module LEMMAS [symbolic]
+    imports LEMMAS-WITHOUT-SLOT-UPDATES
+    imports SLOT-UPDATES
+endmodule
+
+module LEMMAS-WITHOUT-SLOT-UPDATES [symbolic]
     imports BITWISE-SIMPLIFICATION
     imports BYTES-SIMPLIFICATION
     imports INT-SIMPLIFICATION
@@ -22,15 +26,18 @@ module LEMMAS [symbolic]
     rule 0 <=Int #ceil32(I)        => true requires 0 <=Int I [simplification, smt-lemma]
     rule 0 <=Int #ceil32(I) -Int I => true requires 0 <=Int I [simplification]
 
-    rule X *Int Y <Int pow256 => true requires Y <=Int maxUInt256 /Int X [simplification]
+    rule X *Int Y <Int pow256 => true
+      requires (0 <=Int X orBool 0 <=Int Y) andBool Y <=Int maxUInt256 /Int X
+      [simplification]
+
     rule #if B #then C +Int C1 #else C +Int C2 #fi => C +Int #if B #then C1 #else C2 #fi [simplification]
 
   // ########################
   // Set Reasoning
   // ########################
 
-    rule X in (SetItem(Y) _   ) => true      requires X  ==Int Y [simplification]
-    rule X in (SetItem(Y) REST) => X in REST requires X =/=Int Y [simplification]
+    rule X in (SetItem(Y) _   ) => true      requires           X ==Int Y   [simplification]
+    rule X in (SetItem(Y) REST) => X in REST requires notBool ( X ==Int Y ) [simplification]
 
     rule   ( S:Set |Set SetItem ( X )                      ) |Set SetItem( X ) =>   ( S:Set |Set SetItem ( X )                      ) [simplification]
     rule ( ( S:Set |Set SetItem ( X ) ) |Set SetItem ( Y ) ) |Set SetItem( X ) => ( ( S:Set |Set SetItem ( X ) ) |Set SetItem ( Y ) ) [simplification]
@@ -51,9 +58,6 @@ module LEMMAS [symbolic]
     rule 1 |Int bool2Word(_B) => 1            [simplification]
     rule 1 &Int bool2Word( B) => bool2Word(B) [simplification]
 
-    rule bool2Word(_B) |Int 1 => 1            [simplification]
-    rule bool2Word( B) &Int 1 => bool2Word(B) [simplification]
-
     // #newAddr range
     rule 0 <=Int #newAddr(_,_)             => true   [simplification]
     rule         #newAddr(_,_) <Int pow160 => true   [simplification]
@@ -77,11 +81,11 @@ module LEMMAS [symbolic]
     rule         #lookup( _M:Map , _ ) <Int pow256 => true [simplification, smt-lemma]
 
     rule #lookup ( _M:Map [ K1 <- V1 ] , K2 )    => #lookup ( K1 |-> V1 , K1 ) requires K1 ==Int  K2 [simplification]
-    rule #lookup (  M:Map [ K1 <- _  ] , K2 )    => #lookup ( M         , K2 ) requires K1 =/=Int K2 [simplification]
-    rule #lookup ( (K1:Int |-> _) M:Map, K2:Int) => #lookup ( M         , K2 ) requires K1 =/=Int K2 [simplification]
+    rule #lookup (  M:Map [ K1 <- _  ] , K2 )    => #lookup ( M         , K2 ) requires notBool ( K1 ==Int K2 ) [simplification]
+    rule #lookup ( (K1:Int |-> _) M:Map, K2:Int) => #lookup ( M         , K2 ) requires notBool ( K1 ==Int K2 ) [simplification]
 
     rule M:Map [ I1:Int <- V1:Int ] [ I2:Int <- V2:Int ] ==K M:Map [ I2 <- V2 ] [ I1 <- V1 ] => true
-      requires I1 =/=Int I2
+      requires notBool ( I1 ==Int I2 )
       [simplification]
 
  // Hardcoded #addrFromPrivateKey simplifications, see: https://github.com/runtimeverification/haskell-backend/issues/3573
@@ -91,18 +95,16 @@ module LEMMAS [symbolic]
   // Memory
   // ########################
 
-    rule #memoryUsageUpdate(MU, _, WIDTH) => MU requires WIDTH <=Int 0 [simplification]
+    rule #memoryUsageUpdate(MU, _, WIDTH) => MU requires 0 <=Int MU andBool WIDTH <=Int 0 [simplification]
 
-    rule 0 <=Int #memoryUsageUpdate(MU, START, WIDTH) => true requires 0 <=Int MU andBool 0 <=Int START andBool 0 <=Int WIDTH [simplification]
+    rule 0 <=Int #memoryUsageUpdate(MU, START, WIDTH) => true requires 0 <=Int MU orBool ( 0 <=Int START andBool 0 <=Int WIDTH ) [simplification]
 
     rule #memoryUsageUpdate(#memoryUsageUpdate(MU, START1, WIDTH1), START2, WIDTH2) => #memoryUsageUpdate(MU, START1, WIDTH1)
-      requires #rangeUInt(256, MU) andBool 0 <Int WIDTH1 andBool 0 <Int WIDTH2
-       andBool START2 +Int WIDTH2 <=Int START1 +Int WIDTH1
+      requires 0 <Int WIDTH1 andBool 0 <Int WIDTH2 andBool START2 +Int WIDTH2 <=Int START1 +Int WIDTH1
       [simplification]
 
     rule #memoryUsageUpdate(#memoryUsageUpdate(MU, START1, WIDTH1), START2, WIDTH2) => #memoryUsageUpdate(MU, START2, WIDTH2)
-      requires #rangeUInt(256, MU) andBool 0 <Int WIDTH1 andBool 0 <Int WIDTH2
-       andBool START1 +Int WIDTH1 <Int START2 +Int WIDTH2
+      requires 0 <Int WIDTH1 andBool 0 <Int WIDTH2 andBool START1 +Int WIDTH1 <Int START2 +Int WIDTH2
       [simplification]
 
   // ########################
@@ -156,8 +158,8 @@ module LEMMAS-HASKELL [symbolic]
   // ########################
 
     rule #asWord(BUF) /Int D => #asWord(#range(BUF, 0, lengthBytes(BUF) -Int log256Int(D)))
-       requires D ==Int 256 ^Int log256Int(D) andBool D >=Int 0
-        andBool lengthBytes(BUF) >=Int log256Int(D) [simplification, preserves-definedness]
+       requires 0 <Int D andBool D <Int pow256 andBool D ==Int 256 ^Int log256Int(D)
+        andBool log256Int(D) <=Int lengthBytes(BUF) [simplification, preserves-definedness]
 
     rule notBool  (X ==Int 0) => X ==Int 1 requires #rangeBool(X) [simplification]
     rule notBool  (X ==Int 1) => X ==Int 0 requires #rangeBool(X) [simplification]
@@ -171,8 +173,6 @@ module LEMMAS-HASKELL [symbolic]
   // Arithmetic
   // ########################
 
-    rule N modInt pow160   => N  requires #rangeUInt(160, N) [simplification]
-
     // ; Z3 version 4.8.12
     // (set-option :smt.mbqi true)
     //
@@ -200,7 +200,7 @@ module LEMMAS-HASKELL [symbolic]
   // ########################
 
     rule { M:Map [ I1:Int <- V1:Int ] [ I2:Int <- V2:Int ] #Equals M:Map [ I2 <- V2 ] [ I1 <- V1 ] } => #Top
-      requires I1 =/=Int I2
+      requires notBool ( I1 ==Int I2 )
       [simplification]
 
   // ########################