Upstream first batch of lemmas from Lido engagement

Author: lucasmt

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

@@ -79,4 +79,29 @@ module BITWISE-SIMPLIFICATION [symbolic]
 
     rule 0 <=Int (X <<Int Y) => true requires 0 <=Int X andBool 0 <=Int Y [simplification]
 
+  // ###########################################################################
+  // bit-xor
+  // ###########################################################################
+
+    // Simplifications for the OpenZeppelin ternary operator function
+
+    rule [xorInt-ge-zero]:
+      0 <=Int X xorInt Y => true
+      requires 0 <=Int X andBool 0 <=Int Y
+      [simplification]
+
+    rule [xorInt-lt]:
+      X xorInt Y <Int Z => true
+      requires X <Int ( 2 ^Int log2Int ( Z ) ) andBool Y <Int ( 2 ^Int log2Int ( Z ) )
+      [simplification, concrete(Z)]
+
+    rule [b2w-lt]:
+      bool2Word ( B:Bool ) *Int X <Int Y =>
+        ( ( notBool B ) andBool 0 <Int Y ) orBool ( B andBool X <Int Y )
+      [simplification, concrete(Y)]
+
+    rule [xorInt-to-if]:
+      X xorInt ( bool2Word ( B ) *Int ( X xorInt Y ) ) => #if B #then Y #else X #fi
+      [simplification]
+
 endmodule

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

@@ -34,6 +34,12 @@ module BYTES-SIMPLIFICATION [symbolic]
     rule [bytes-concat-right-assoc-symb-r]: (B1:Bytes +Bytes B2:Bytes) +Bytes B3:Bytes => B1 +Bytes (B2 +Bytes B3) [symbolic(B2), simplification(40)]
     rule [bytes-concat-left-assoc-conc]:    B1:Bytes +Bytes (B2:Bytes +Bytes B3:Bytes) => (B1 +Bytes B2) +Bytes B3 [concrete(B1, B2), symbolic(B3), simplification(40)]
 
+    // Can ignore lower bytes for <Int if the corresponding bytes in X are 0 (note this does not apply to <=Int)
+    rule [asWord-lt-concat-left]:
+      #asWord ( B1 +Bytes B2 ) <Int X => #asWord ( B1 ) <Int X /Int ( 2 ^Int ( 8 *Int lengthBytes ( B2 ) ) )
+      requires X modInt ( 2 ^Int ( 8 *Int lengthBytes ( B2 ) ) ) ==Int 0
+      [simplification, preserves-definedness]
+
     // #buf
 
     rule [buf-empty]: #buf(N:Int, _) => b"" requires N ==Int 0 [simplification]

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

@@ -96,6 +96,11 @@ module INT-SIMPLIFICATION-HASKELL [symbolic]
     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 0  <Int A -Int B => B  <Int A [simplification, symbolic(A, B)]
+    rule 0 <=Int A -Int B => B <=Int A [simplification, symbolic(A, B)]
+    rule 0  >Int A -Int B => B  >Int A [simplification, symbolic(A, B)]
+    rule 0 >=Int A -Int B => B >=Int A [simplification, symbolic(A, B)]
+
 endmodule
 
 module INT-SIMPLIFICATION-COMMON
@@ -148,6 +153,24 @@ module INT-SIMPLIFICATION-COMMON
 
     rule (E *Int A) +Int B +Int C +Int D +Int (F *Int A) => ((E +Int F) *Int A) +Int B +Int C +Int D [simplification]
 
+    // Simplification of concrete multiplication
+
+    rule A *Int B <Int C => B <Int C /Int A
+      requires 0 <Int A andBool 0 <=Int C andBool C modInt A ==Int 0
+      [simplification(40), concrete(A, C), preserves-definedness]
+
+    rule A *Int B <=Int C => B <=Int C /Int A
+      requires 0 <Int A andBool 0 <=Int C andBool C modInt A ==Int 0
+      [simplification(40), concrete(A, C), preserves-definedness]
+
+    rule C <=Int A *Int B => C /Int A <=Int B
+      requires 0 <Int A andBool 0 <=Int C andBool C modInt A ==Int 0
+      [simplification(40), concrete(A, C), preserves-definedness]
+
+    rule C <Int A *Int B => C /Int A <Int B
+      requires 0 <Int A andBool 0 <=Int C andBool C modInt A ==Int 0
+      [simplification(40), concrete(A, C), preserves-definedness]
+
   // ###########################################################################
   // div
   // ###########################################################################
@@ -169,6 +192,13 @@ module INT-SIMPLIFICATION-COMMON
       requires 0 <=Int A andBool 0 <=Int B andBool 0 <Int C andBool A <=Int D andBool B <=Int C
       [simplification, preserves-definedness]
 
+    rule ( A /Int B ) /Int C => 0
+        requires 0 <=Int A
+         andBool 0 <Int B
+         andBool 0 <Int C
+         andBool A <Int ( C *Int B )
+        [simplification, symbolic(A, B), concrete(C), preserves-definedness]
+
   // ###########################################################################
   // mod
   // ###########################################################################
@@ -223,4 +253,10 @@ module INT-SIMPLIFICATION-COMMON
 
     rule A -Int B +Int C <=Int D => false requires D <Int A -Int B andBool 0 <=Int C [simplification]
 
+    rule A ==Int B => false requires 0 <=Int A andBool B <Int 0 [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]
+
 endmodule

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

@@ -252,4 +252,7 @@ module LEMMAS-HASKELL [symbolic]
 
     rule (notBool (A andBool B)) andBool A => (notBool B) andBool A [simplification]
 
+    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)]
+
 endmodule