Enhance integer simplifications with definedness preservation and update ZKEVM-PUSH test specification to include length condition for OP1.

Author: Stevengre

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

@@ -46,7 +46,8 @@ module INT-SIMPLIFICATIONS [symbolic]
     (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)]
+    [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

@@ -7,7 +7,8 @@ module ZKEVM-PUSH
     <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
+    requires lengthBytes(OP0) ==Int 1 andBool lengthBytes(OP1) ==Int 2
 endmodule