Simp rules 4 zkevm project SLOAD

Author: Stevengre

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

@@ -80,6 +80,9 @@ module INT-SIMPLIFICATIONS [symbolic]
   rule [int-or-bytes-2]: Bytes2Int(b"\x00\x00" +Bytes X, LE, Unsigned) |Int Bytes2Int(Y, LE, Unsigned) => Bytes2Int(Y +Bytes X, LE, Unsigned)
     requires lengthBytes(Y) ==Int 2
     [simplification]
+  rule [int-or-bytes-2s]: Bytes2Int(b"\x00\x00" +Bytes X, LE, Unsigned) |Int Bytes2Int(Y +Bytes b"\x00\x00", LE, Unsigned) => Bytes2Int(Y +Bytes X, LE, Unsigned)
+    requires lengthBytes(Y) ==Int 2 andBool lengthBytes(X) ==Int 2
+    [simplification]
   rule [int-or-bytes-3]: Bytes2Int(b"\x00\x00\x00" +Bytes X, LE, Unsigned) |Int Bytes2Int(Y, LE, Unsigned) => Bytes2Int(Y +Bytes X, LE, Unsigned)
     requires lengthBytes(Y) ==Int 3
     [simplification]

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

@@ -0,0 +1,12 @@
+module ZKEVM-SLOAD
+  imports RISCV
+
+  claim [id]:
+    <instrs> #CHECK_HALT => #HALT </instrs>
+    <pc> 0 </pc>
+    <regs>
+     1 |-> ((Bytes2Int(b"\x00\x00" +Bytes reverseBytes(substrBytes(KEY, 16, 18)), LE, Unsigned) |Int Bytes2Int(reverseBytes(substrBytes(KEY, 18, 20)) +Bytes b"\x00\x00", LE, Unsigned)) &Int 4294967295 => Bytes2Int(reverseBytes(substrBytes(KEY, 16, 20)), LE, Unsigned))
+    </regs>
+    <haltCond> ADDRESS ( 0 ) </haltCond>
+    requires lengthBytes(KEY) ==Int 32
+endmodule