Simp rules 4 zkevm-harness project's MSTORE

package/version

@@ -1 +1 @@
-0.1.114
+0.1.115

pyproject.toml

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

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

@@ -39,6 +39,10 @@ module INT-SIMPLIFICATIONS [symbolic]
 
 ```k
   rule [int-and-ineq]: 0 <=Int A &Int B => true requires 0 <=Int A andBool 0 <=Int B [simplification]
+  rule [int-and-ineq-4294967295]: 0 <=Int _ &Int 4294967295 => true [simplification(45)]
+  rule [int-and-ineq-65535]: 0 <=Int _ &Int 65535 => true [simplification(45)]
+  rule [int-and-ineq-255]: 0 <=Int _ &Int 255 => true [simplification(45)]
+  rule [int-or-gt]: 0 <Int A |Int B => true requires 0 <Int A orBool 0 <Int B [simplification]
   rule [int-rhs-ineq]: 0 <=Int A >>Int B => true requires 0 <=Int A andBool 0 <=Int B [simplification]
   rule [int-add-ineq]: A <=Int A +Int B => true requires 0 <=Int B [simplification]
   rule [int-add-ineq-0]: 0 <=Int A +Int B => true requires 0 <=Int A andBool 0 <=Int B [simplification]

src/kriscv/kdist/riscv-semantics/lemmas/lemmas.k

@@ -2,10 +2,12 @@ requires "sparse-bytes-simplifications.md"
 requires "bytes-simplifications.md"
 requires "int-simplifications.md"
 requires "word-simplifications.md"
+requires "zkevm-harness-simplifications.md"
 
 module LEMMAS
   imports SPARSE-BYTES-SIMPLIFICATIONS
   imports BYTES-SIMPLIFICATIONS
   imports INT-SIMPLIFICATIONS
   imports WORD-SIMPLIFICATIONS
+  imports ZKEVM-HARNESS-SIMPLIFICATIONS
 endmodule

src/kriscv/kdist/riscv-semantics/lemmas/zkevm-harness-simplifications.md

@@ -0,0 +1,47 @@
+# ZKEVM Harness Simplifications
+
+This file contains simplification rules for the [zkevm-harness](https://github.com/runtimeverification/zkevm-harness). Although these simplification rules are not specific to this project, they are rules that were discovered to be needed within this project. However, we currently do not want to perform a comprehensive organization of rules, so we place these rules here for quick addition of simplification rules.
+
+Why not put them in the zkevm-harness repository?
+1. We currently do not have an out-of-the-box simplification rule testing framework, so we would need to spend additional time creating a new testing framework in the zkevm-harness repository;
+2. These rules actually have some general applicability, but considering performance, we may not need to adopt these rules for all verification targets.
+
+```k
+requires "../word.md"
+module ZKEVM-HARNESS-SIMPLIFICATIONS [symbolic]
+  imports INT
+  imports BYTES
+  imports K-EQUAL
+  imports BOOL
+  imports WORD
+```
+
+## MSTORE
+
+The following rules are required to prove the claim in `tests/integration/test-data/specs/zkevm-mstore.k`:
+
+```k
+rule 0 <Int (0 -Int Bool2Word(4294967295 <Int X)) &Int 4294967295 |Int X &Int 4294967295 => true requires 0 <Int X [simplification(45)]
+
+rule 0 <Int A +Int B => true requires 0 <=Int A andBool 0 <Int B [simplification(45)]
+rule 0 <Int A +Int B => true requires 0 <Int A andBool 0 <=Int B [simplification]
+
+rule Bytes2Int (B:Bytes +Bytes b"\x00\x00\x00" , LE , Unsigned ) => Bytes2Int (B, LE, Unsigned) [simplification(45)]
+```
+
+The following additional rules would be needed to handle the 5th register in the zkevm-mstore claim, but they interfere with the targeted rewriting of the 4th register. Therefore, they are not included in the module above:
+```
+rule X <Int Bytes2Int(B, _, Unsigned) => false requires 2 ^Int (lengthBytes(B) *Int 8) -Int 1 <=Int X [simplification]
+rule A <Int B +Int C => A -Int C <Int B [simplification, concrete(A,C), symbolic(B)]
+rule 0 |Int X => X [simplification]
+```
+
+To handle the 6-th and 7-th registers in the zkevm-mstore claim, we need the following rules:
+```k
+rule Bool2Word(B) ==Int 0 => notBool B [simplification]
+rule Bool2Word(B) ==Int 1 => B [simplification]
+```
+
+```k
+endmodule
+```

src/tests/integration/test-data/specs/zkevm-mstore-0.k

@@ -0,0 +1,21 @@
+module ZKEVM-MSTORE-0
+  imports RISCV
+
+  claim [id]:
+    <instrs> #CHECK_HALT => #HALT </instrs>
+    <pc> 0 </pc>
+    <regs>
+     1  |-> (Bool2Word(0 <Int (0 -Int Bool2Word(4294967295 <Int X)) &Int 4294967295 |Int X &Int 4294967295) => 1)
+     2  |-> (Bool2Word(0 <=Int Bytes2Int ( OFFSET:Bytes +Bytes b"\x00\x00\x00" , LE , Unsigned )) => 1)
+     3  |-> (Bool2Word(0 <Int Bytes2Int ( OFFSET:Bytes +Bytes b"\x00\x00\x00" , LE , Unsigned ) +Int 32) => 1)
+     4  |-> (Bool2Word(0 <Int 0 -Int Bool2Word ( 4294967295 <Int Bytes2Int ( OFFSET:Bytes +Bytes b"\x00\x00\x00" , LE , Unsigned ) +Int 32 ) &Int 4294967295 |Int Bytes2Int ( OFFSET:Bytes +Bytes b"\x00\x00\x00" , LE , Unsigned ) +Int 32 &Int 4294967295) => 1)
+     // 5  |-> (Bool2Word(4294967295 <Int Bytes2Int ( OFFSET:Bytes +Bytes b"\x00\x00\x00" , LE , Unsigned ) +Int 32) => 0)
+     6  |-> (Bool2Word(Y <=Int Z) => 0)
+     7  |-> (Bool2Word(Z <=Int 4294967295) => 1)
+    </regs>
+    <haltCond> ADDRESS ( 0 ) </haltCond>
+    requires 0 <Int X 
+     andBool lengthBytes(OFFSET) ==Int 1
+     andBool notBool (Y <=Int Z)
+     andBool notBool (Bool2Word(Z <=Int 4294967295) ==Int 0)
+endmodule