corrections

runtimeverification · Sep 9, 2024 · 53238fd · 53238fd
1 parent c161d10
commit 53238fd
Showing 1 changed file with 4 additions and 4 deletions.
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
@@ -111,10 +111,10 @@ module EVM-INT-SIMPLIFICATION-COMMON
       requires #rangeUInt(256, X) andBool #rangeUInt(256, Y)
       [simplification, concrete(Y), comm]
 
-    rule [chop-no-overflow-add-l]: X:Int <=Int chop ( X +Int Y:Int ) => X +Int Y <Int pow256 requires #rangeUInt(256, X) andBool #rangeUInt(256, Y) [simplification]
-    rule [chop-no-overflow-add-r]: X:Int <=Int chop ( Y +Int X:Int ) => X +Int Y <Int pow256 requires #rangeUInt(256, X) andBool #rangeUInt(256, Y) [simplification]
-    rule [chop-no-overflow-mul-l]: X:Int <=Int chop ( X *Int Y:Int ) => X *Int Y <Int pow256 requires #rangeUInt(256, X) andBool #rangeUInt(256, Y) [simplification]
-    rule [chop-no-overflow-mul-r]: X:Int <=Int chop ( Y *Int X:Int ) => X *Int Y <Int pow256 requires #rangeUInt(256, X) andBool #rangeUInt(256, Y) [simplification]
+    rule [chop-no-overflow-add-l]: X:Int <=Int chop ( X +Int Y:Int ) => X +Int Y <Int pow256 requires #rangeUInt(256, X) andBool 0 <=Int Y [simplification]
+    rule [chop-no-overflow-add-r]: X:Int <=Int chop ( Y +Int X:Int ) => X +Int Y <Int pow256 requires #rangeUInt(256, X) andBool 0 <=Int Y [simplification]
+    rule [chop-no-overflow-mul-l]: X:Int <=Int chop ( X *Int Y:Int ) => X *Int Y <Int pow256 requires #rangeUInt(256, X) andBool 0  <Int Y [simplification]
+    rule [chop-no-overflow-mul-r]: X:Int <=Int chop ( Y *Int X:Int ) => X *Int Y <Int pow256 requires #rangeUInt(256, X) andBool 0  <Int Y [simplification]
 
     rule [chop-no-overflow-mul-eq]:        X  ==Int  chop ( X *Int Y ) /Int Y   =>                X *Int Y <Int pow256   requires #rangeUInt(256, X) andBool 0 <Int Y [simplification, comm, preserves-definedness]
     rule [chop-no-overflow-mul-eq-ml-l]: { X #Equals chop ( X *Int Y ) /Int Y } => { true #Equals X *Int Y <Int pow256 } requires #rangeUInt(256, X) andBool 0 <Int Y [simplification, preserves-definedness]