Remove evm-int-simplifications.k module (#2255)

* Remove evm-int-simplifications.k module

All rules in `evm-int-simplifications.k` are duplicated in `int-simplifications.k`
at the time of writing. Therefore the file can be deleted without losing any
simplifications, all proofs should have the simplifications available as before.

* Set Version: 1.0.415

* Set Version: 1.0.416

* Restore evm-int-simplifications.k module, remove rules from int-simplifications.k

int-simplifications should be decoupled from evm-semantics so it
cannot import any of its modules. The evm-int-simplifications.k
equations continue to be tested in separate lemmas.

This reverts commit da94a9f.

---------

Co-authored-by: devops <[email protected]>

kevm-pyk/pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kevm-pyk"
-version = "1.0.415"
+version = "1.0.416"
 description = ""
 authors = [
     "Runtime Verification, Inc. <[email protected]>",

kevm-pyk/src/kevm_pyk/__init__.py

@@ -6,4 +6,4 @@
     from typing import Final
 
 
-VERSION: Final = '1.0.415'
+VERSION: Final = '1.0.416'

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

@@ -1,5 +1,3 @@
-requires "evm-types.md"
-
 module INT-SIMPLIFICATION
     imports INT-SIMPLIFICATION-HASKELL
 endmodule
@@ -90,7 +88,6 @@ endmodule
 module INT-SIMPLIFICATION-COMMON
     imports INT
     imports BOOL
-    imports EVM-TYPES
 
   // ###########################################################################
   // add, sub
@@ -204,43 +201,4 @@ module INT-SIMPLIFICATION-COMMON
 
     rule A -Int B +Int C <=Int D => false requires D <Int A -Int B andBool 0 <=Int C [simplification]
 
-  // ###########################################################################
-  // up/Int
-  // ###########################################################################
-
-    rule [upInt-lt-true]:
-      ((X up/Int Y) *Int Y) <Int Z => true
-      requires X +Int Y <=Int Z andBool 0 <Int Y
-      [simplification]
-
-    rule [upInt-lt-false]:
-      ((X up/Int Y) *Int Y) <Int Z => false
-      requires Z <=Int X andBool 0 <Int Y
-      [simplification]
-
-    rule [upInt-refl-leq]:
-      ((X up/Int Y) *Int Y) <=Int X => X modInt Y ==Int 0
-      requires 0 <Int Y
-      [simplification]
-
-    rule [upInt-refl-gt]:
-      X <Int ((X up/Int Y) *Int Y) => X modInt Y =/=Int 0
-      requires 0 <Int Y
-      [simplification]
-
-    rule [upInt-refl-geq]:
-      X <=Int ((X up/Int Y) *Int Y) => true
-      requires 0 <Int Y
-      [simplification]
-
-    rule [upInt-ref-eq]:
-      X ==Int ((X up/Int Y) *Int Y) => X modInt Y ==Int 0
-      requires 0 <Int Y
-      [simplification, comm]
-
-    rule [upInt-refl-neq]:
-      X =/=Int ((X up/Int Y) *Int Y) => X modInt Y =/=Int 0
-      requires 0 <Int Y
-      [simplification, comm]
-
 endmodule

package/version

@@ -1 +1 @@
-1.0.415
+1.0.416