Simplify pattern Bytes2Int o substrBytes &Int 65280 (#105)

Co-authored-by: devops <[email protected]>

Author: Stevengre

package/version

@@ -1 +1 @@
-0.1.77
+0.1.78

pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kriscv"
-version = "0.1.77"
+version = "0.1.78"
 description = "K tooling for the RISC-V architecture"
 authors = [
     "Runtime Verification, Inc. <[email protected]>",

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

@@ -83,6 +83,17 @@ module BYTES-SIMPLIFICATIONS
   [simplification, preserves-definedness]
 ```
 
+## Bytes2Int Lemmas
+
+```k
+  rule [bytes2int-substr-ff00-0]: Bytes2Int (substrBytes(B, I, J), LE, Unsigned) &Int 65280 => 0
+    requires 0 <=Int I andBool I <=Int J andBool J <=Int I +Int 1 andBool J <=Int lengthBytes(B)
+    [simplification, preserves-definedness]
+  rule [bytes2int-substr-ff00-1]: Bytes2Int (substrBytes(B, I, J), LE, Unsigned) &Int 65280 => B[I +Int 1] <<Int 8
+    requires 0 <=Int I andBool I +Int 1 <Int J andBool J <=Int lengthBytes(B)
+    [simplification, preserves-definedness]
+```
+
 ```k
 endmodule
 ```

src/tests/integration/test-data/specs/bytes-int.k

@@ -0,0 +1,20 @@
+requires "riscv-semantics/riscv.md"
+
+module BYTES-INT
+  imports RISCV
+
+  claim [id]:
+    <instrs> #CHECK_HALT => #HALT </instrs>
+    <pc> W ( 0 ) </pc>
+    <regs>
+     1 |-> (W(Bytes2Int (b"\x12\x34\x56\x78", LE, Unsigned) &Int 65280) => W(13312))
+     2 |-> (W(b"\x12\x34\x56\x78" [ 1 ] <<Int 8) => W(13312))
+     3 |-> (W(Bytes2Int (substrBytes(W0, 0, 4), LE, Unsigned ) &Int 65280) => W(W0 [ 1 ] <<Int 8))
+     4 |-> (W(Bytes2Int(substrBytes(b"\x01\x02", 0, 1), LE, Unsigned) &Int 65280) => W(0))
+     5 |-> (W(Bytes2Int(substrBytes(W0, 0, 1), LE, Unsigned) &Int 65280) => W(0))
+    </regs>
+    <test>
+      <haltCond> ADDRESS ( W ( 0 ) ) </haltCond>
+    </test>
+requires lengthBytes(W0) ==Int 32
+endmodule