Merge remote-tracking branch 'origin/master' into release

rv-auditor · rv-auditor · commit b060078b9db0 · 2025-08-19T20:27:57.000Z
diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/bitwise-simplification.k b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/bitwise-simplification.k
@@ -79,4 +79,25 @@ 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 0 <=Int X andBool 0 <=Int Y andBool 0 <Int Z
+       andBool X <Int ( 2 ^Int log2Int ( Z ) ) andBool Y <Int ( 2 ^Int log2Int ( Z ) )
+      [simplification, concrete(Z)]
+
+    rule [xorInt-to-if]:
+      X xorInt ( bool2Word ( B ) *Int ( X xorInt Y ) ) => #if B #then Y #else X #fi
+      [simplification]
+
 endmodule
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
@@ -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]
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
@@ -96,11 +96,17 @@ 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 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)]
+
 endmodule
 
 module INT-SIMPLIFICATION-COMMON
     imports INT
     imports BOOL
+    imports WORD
 
   // ###########################################################################
   // add, sub
@@ -148,6 +154,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 +193,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 +254,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
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
@@ -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
diff --git a/tests/specs/functional/lemmas-spec.k b/tests/specs/functional/lemmas-spec.k
@@ -90,6 +90,27 @@ module LEMMAS-SPEC
           ) ... </k>
           requires 0 <=Int X andBool X <Int 2 ^Int 144
 
+    claim [div-div]: <k> runLemma ( ( A /Int B ) /Int 1024 ) => doneLemma ( 0 ) ... </k>
+        requires 0 <=Int A andBool 0 <Int B andBool A <Int ( 1024 *Int B )
+
+ // Booleans
+ // ---------
+
+    claim [notBool-or]:
+      <k> runLemma (
+            notBool ( ( X <Int LOWER ) orBool ( UPPER <=Int X ) )
+          ) => doneLemma (
+            ( notBool ( X <Int LOWER ) ) andBool ( notBool ( UPPER <=Int X ) )
+          ) ...
+      </k>
+
+    claim [notBool-and]:
+      <k> runLemma (
+            notBool ( ( LOWER <=Int X ) andBool ( X <Int UPPER ) )
+          ) => doneLemma (
+            ( notBool ( LOWER <=Int X ) ) orBool ( notBool ( X <Int UPPER ) )
+          ) ...
+      </k>
 
  // Comparisons
  // -----------
@@ -130,6 +151,34 @@ module LEMMAS-SPEC
           ) ...
       </k>
 
+    claim [zero-lt-sub]: <k> runLemma ( 0  <Int A -Int B ) => doneLemma ( B  <Int A ) ... </k>
+    claim [zero-le-sub]: <k> runLemma ( 0 <=Int A -Int B ) => doneLemma ( B <=Int A ) ... </k>
+    claim [zero-gt-sub]: <k> runLemma ( 0  >Int A -Int B ) => doneLemma ( B  >Int A ) ... </k>
+    claim [zero-ge-sub]: <k> runLemma ( 0 >=Int A -Int B ) => doneLemma ( B >=Int A ) ... </k>
+
+    claim [sub-gt-zero]: <k> runLemma ( A -Int B  >Int 0 ) => doneLemma ( A  >Int B ) ... </k>
+    claim [sub-ge-zero]: <k> runLemma ( A -Int B >=Int 0 ) => doneLemma ( A >=Int B ) ... </k>
+    claim [sub-lt-zero]: <k> runLemma ( A -Int B  <Int 0 ) => doneLemma ( A  <Int B ) ... </k>
+    claim [sub-le-zero]: <k> runLemma ( A -Int B <=Int 0 ) => doneLemma ( A <=Int B ) ... </k>
+
+    claim [mul-lt-const]: <k> runLemma ( 36 *Int B  <Int 1728 ) => doneLemma ( B  <Int 48 ) ... </k>
+    claim [mul-le-const]: <k> runLemma ( 36 *Int B <=Int 1728 ) => doneLemma ( B <=Int 48 ) ... </k>
+    claim [mul-gt-const]: <k> runLemma ( 36 *Int B  >Int 1728 ) => doneLemma ( B  >Int 48 ) ... </k>
+    claim [mul-ge-const]: <k> runLemma ( 36 *Int B >=Int 1728 ) => doneLemma ( B >=Int 48 ) ... </k>
+
+    claim [const-gt-mul]: <k> runLemma ( 1728  >Int 36 *Int B ) => doneLemma ( 48  >Int B ) ... </k>
+    claim [const-ge-mul]: <k> runLemma ( 1728 >=Int 36 *Int B ) => doneLemma ( 48 >=Int B ) ... </k>
+    claim [const-lt-mul]: <k> runLemma ( 1728  <Int 36 *Int B ) => doneLemma ( 48  <Int B ) ... </k>
+    claim [const-le-mul]: <k> runLemma ( 1728 <=Int 36 *Int B ) => doneLemma ( 48 <=Int B ) ... </k>
+
+    claim [eq-neg]: <k> runLemma ( A ==Int -1 ) => doneLemma ( false ) ... </k>
+        requires 0 <=Int A
+
+    claim [nonneg-and-nonzero]: <k> runLemma ( 0 <Int X ) => doneLemma ( true ) ... </k>
+        requires 0 <=Int X andBool notBool ( X ==Int 0 )
+
+    claim [le-maxuint256]: <k> runLemma ( X <=Int maxUInt256 ) => doneLemma ( X <Int pow256 ) ... </k>
+
 
  // Sets
  // ----
@@ -657,6 +706,12 @@ module LEMMAS-SPEC
     claim [shift-range]: <k> runLemma ( #rangeUInt ( 256 , X <<Int 16 ) ) => doneLemma ( true ) ... </k> requires #rangeUInt ( 16 , X )
     claim [shift-mod]: <k> runLemma ( ( X <<Int 16 ) modInt pow256 ) => doneLemma ( X <<Int 16 ) ... </k> requires #rangeUInt ( 16 , X )
 
+ // xor
+ // -----
+
+    claim [xorInt-range]: <k> runLemma ( #rangeUInt ( 256 , X xorInt Y ) ) => doneLemma ( true ) ... </k> requires #rangeUInt ( 256 , X ) andBool #rangeUInt ( 256 , Y )
+    claim [xorInt-to-if]: <k> runLemma ( A xorInt ( bool2Word ( A <=Int B ) *Int ( A xorInt B )  ) ) => doneLemma ( #if ( A <=Int B ) #then B #else A #fi ) ... </k>
+
  // concat
  // ------
 
@@ -769,6 +824,13 @@ module LEMMAS-SPEC
         requires #asWord ( BA3 ) ==Int X modInt ( 2 ^Int ( 8 *Int lengthBytes ( BA3 ) ) )
          andBool 0 <Int lengthBytes(BA1) andBool lengthBytes(BA2 +Bytes BA3) ==Int 32
 
+    claim [asWord-lt-concat-left]:
+      <k> runLemma (
+            #asWord ( B1 +Bytes b"\xde\xad\xbe\xef" ) <Int #asWord ( b"\xfa\xca\xde\x00\x00\x00\x00" )
+          ) => doneLemma (
+            #asWord ( B1 ) <Int #asWord ( b"\xfa\xca\xde")
+          ) ... </k>
+
  // bool2Word
  // ---------
 
