Simp rule 4 zkevm project's PUSH

package/version

@@ -1 +1 @@
-0.1.117
+0.1.118

pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "hatchling.build"
 
 [project]
 name = "kriscv"
-version = "0.1.117"
+version = "0.1.118"
 description = "K tooling for the RISC-V architecture"
 readme = "README.md"
 requires-python = "~=3.10"

src/kriscv/kdist/riscv-semantics/lemmas/int-simplifications.md

@@ -33,6 +33,21 @@ module INT-SIMPLIFICATIONS [symbolic]
     [simplification]
   rule [int-and-add-assoc-32]: ((X &Int 4294967295) +Int Y) &Int 4294967295 => (X +Int Y) &Int 4294967295
     [simplification]
+  rule [bytes2int-and-255]: Bytes2Int(X, LE, Unsigned) &Int 255 => Bytes2Int(X, LE, Unsigned)
+    requires lengthBytes(X) <=Int 1 [simplification]
+  rule [bytes2int-or-under-255]: Bytes2Int(b"\x00" +Bytes X, LE, Unsigned) |Int Y => Bytes2Int(Int2Bytes(Y, LE, Unsigned) +Bytes X, LE, Unsigned)
+    requires Y <Int 256 [simplification, concrete(Y)]
+```
+
+## Equality Lemmas
+
+```k
+  rule [int-eq-bytes2int]: X ==Int Bytes2Int(B0 +Bytes B1, LE, Unsigned) => 
+    (X &Int ((1 <<Int (lengthBytes(B0) *Int 8)) -Int 1)) ==Int Bytes2Int(B0, LE, Unsigned)
+    andBool
+    (X >>Int (lengthBytes(B0) *Int 8)) ==Int Bytes2Int(B1, LE, Unsigned)
+    [simplification, concrete(B0), preserves-definedness]
+    // without preserves-definedness, the rule is not applicable to B1 == substrBytes(B2, I, J)
 ```
 
 ## Inequality Lemmas

src/tests/integration/test-data/specs/zkevm-push.k

@@ -0,0 +1,14 @@
+module ZKEVM-PUSH
+  imports RISCV
+
+  claim [id]:
+    <instrs> #CHECK_HALT => #HALT </instrs>
+    <pc> 0 </pc>
+    <regs>
+     1 |-> ((Bytes2Int(OP0, LE, Unsigned) &Int 255) <<Int 8 &Int 4294967295 |Int 96 => Bytes2Int(b"`" +Bytes OP0, LE, Unsigned))
+     2 |-> (Bool2Word(239 ==Int Bytes2Int(b"`" +Bytes OP0, LE, Unsigned)) => 0)
+     3 |-> (Bool2Word(239 ==Int Bytes2Int(b"a" +Bytes substrBytes(OP1, 0, 1), LE, Unsigned)) => 0)
+    </regs>
+    <haltCond> ADDRESS(0) </haltCond>
+    requires lengthBytes(OP0) ==Int 1 andBool lengthBytes(OP1) ==Int 2
+endmodule