formatting

runtimeverification · Sep 9, 2024 · c161d10 · c161d10
1 parent e15d405
commit c161d10
Showing 1 changed file with 8 additions and 19 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,24 +111,13 @@ 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-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]
-
-    rule [chop-no-overflow-mul-eq-ml-r]:
-      { chop ( X *Int Y ) /Int Y #Equals X } => { true #Equals X *Int Y <Int pow256 }
-      requires #rangeUInt(256, X) andBool 0 <Int Y
-      [simplification, preserves-definedness]
+    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-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]
+    rule [chop-no-overflow-mul-eq-ml-r]: { chop ( X *Int Y ) /Int Y #Equals X } => { true #Equals X *Int Y <Int pow256 } requires #rangeUInt(256, X) andBool 0 <Int Y [simplification, preserves-definedness]
 
 endmodule