Add rules for handling 6th and 7th registers in zkevm-mstore claim and update requirements in test specification.

Author: Stevengre

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

@@ -36,6 +36,12 @@ rule A <Int B +Int C => A -Int C <Int B [simplification, concrete(A,C), symbolic
 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

@@ -10,8 +10,12 @@ module ZKEVM-MSTORE-0
      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 0 <=Int Y andBool 0 <Int Z
+    requires 0 <Int X 
      andBool lengthBytes(OFFSET) ==Int 1
+     andBool notBool (Y <=Int Z)
+     andBool notBool (Bool2Word(Z <=Int 4294967295) ==Int 0)
 endmodule