Remove redundant requirement for substr o int2bytes (#145)

Co-authored-by: Tamás Tóth <tothtamas28@users.noreply.github.com>
Co-authored-by: devops <devops@runtimeverification.com>

Author: 3 people

package/version

@@ -1 +1 @@
-0.1.108
+0.1.109

pyproject.toml

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

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

@@ -97,7 +97,7 @@ module BYTES-SIMPLIFICATIONS [symbolic]
     requires lengthBytes(A) <=Int I
     [simplification, preserves-definedness]
   rule [substr-int2bytes]: substrBytes(Int2Bytes(Num, V, LE), SI, EI) => Int2Bytes(EI -Int SI, V >>Int (SI *Int 8), LE)
-    requires 0 <=Int SI andBool SI <=Int EI andBool EI <=Int Num andBool 0 <=Int V
+    requires 0 <=Int SI andBool SI <=Int EI andBool EI <=Int Num
     [simplification, preserves-definedness]
   
   rule [substr-reverse-concat-0]: substrBytes(B, I1, I2) +Bytes substrBytes(B, I0, I1) => reverseBytes(substrBytes(B, I0, I2))

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

@@ -35,6 +35,7 @@ module BYTES-INT
      28 |-> ((X +Int Y &Int 4294967295) +Int Bool2Word(4294967295 <Int Bytes2Int(substrBytes(reverseBytes(W3), 16, 20), LE, Unsigned) +Int Bytes2Int(substrBytes(reverseBytes(W0), 16, 20), LE, Unsigned)) &Int 4294967295 => X +Int Y +Int Bool2Word(4294967295 <Int Bytes2Int(substrBytes(reverseBytes(W3), 16, 20), LE, Unsigned) +Int Bytes2Int(substrBytes(reverseBytes(W0), 16, 20), LE, Unsigned)) &Int 4294967295)
      29 |-> ((Bytes2Int(substrBytes(reverseBytes(W3), 0, 4), LE, Unsigned) +Int Bytes2Int(substrBytes(reverseBytes(W0), 0, 4), LE, Unsigned) &Int 4294967295) >>Int 0 => (Bytes2Int(substrBytes(reverseBytes(W3), 0, 4), LE, Unsigned) +Int Bytes2Int(substrBytes(reverseBytes(W0), 0, 4), LE, Unsigned) &Int 4294967295))
      30 |-> (((Bytes2Int(substrBytes(reverseBytes(W3), 16, 20), LE, Unsigned) +Int Bytes2Int(substrBytes(reverseBytes(W0), 16, 20), LE, Unsigned) &Int 4294967295) +Int (Bool2Word(4294967295 <Int Bytes2Int(substrBytes(reverseBytes(W3), 8, 12), LE, Unsigned) +Int Bytes2Int(substrBytes(reverseBytes(W0), 8, 12), LE, Unsigned)) |Int Bool2Word(Bytes2Int(substrBytes(reverseBytes(W3), 8, 12), LE, Unsigned) +Int Bytes2Int(substrBytes(reverseBytes(W0), 8, 12), LE, Unsigned) +Int Bool2Word(4294967295 <Int Bytes2Int(substrBytes(reverseBytes(W3), 0, 4), LE, Unsigned) +Int Bytes2Int(substrBytes(reverseBytes(W0), 0, 4), LE, Unsigned)) &Int 4294967295 <Int Bytes2Int(substrBytes(reverseBytes(W3), 8, 12), LE, Unsigned) +Int Bytes2Int(substrBytes(reverseBytes(W0), 8, 12), LE, Unsigned) &Int 4294967295) &Int Bool2Word(Bytes2Int(substrBytes(reverseBytes(W3), 12, 16), LE, Unsigned) +Int Bytes2Int(substrBytes(reverseBytes(W0), 12, 16), LE, Unsigned) +Int Bool2Word(4294967295 <Int Bytes2Int(substrBytes(reverseBytes(W3), 8, 12), LE, Unsigned) +Int Bytes2Int(substrBytes(reverseBytes(W0), 8, 12), LE, Unsigned)) +Int Bool2Word(Bytes2Int(substrBytes(reverseBytes(W3), 8, 12), LE, Unsigned) +Int Bytes2Int(substrBytes(reverseBytes(W0), 8, 12), LE, Unsigned) +Int Bool2Word(4294967295 <Int Bytes2Int(substrBytes(reverseBytes(W3), 0, 4), LE, Unsigned) +Int Bytes2Int(substrBytes(reverseBytes(W0), 0, 4), LE, Unsigned)) &Int 4294967295 <Int Bytes2Int(substrBytes(reverseBytes(W3), 8, 12), LE, Unsigned) +Int Bytes2Int(substrBytes(reverseBytes(W0), 8, 12), LE, Unsigned) &Int 4294967295) &Int 4294967295 <Int Bytes2Int(substrBytes(reverseBytes(W3), 12, 16), LE, Unsigned) +Int Bytes2Int(substrBytes(reverseBytes(W0), 12, 16), LE, Unsigned) +Int Bool2Word(4294967295 <Int Bytes2Int(substrBytes(reverseBytes(W3), 8, 12), LE, Unsigned) +Int Bytes2Int(substrBytes(reverseBytes(W0), 8, 12), LE, Unsigned)) &Int 4294967295))) &Int 4294967295 => Bytes2Int(substrBytes(reverseBytes(W3), 16, 20), LE, Unsigned) +Int Bytes2Int(substrBytes(reverseBytes(W0), 16, 20), LE, Unsigned) +Int (Bool2Word(4294967295 <Int Bytes2Int(substrBytes(reverseBytes(W3), 8, 12), LE, Unsigned) +Int Bytes2Int(substrBytes(reverseBytes(W0), 8, 12), LE, Unsigned)) |Int Bool2Word(Bytes2Int(substrBytes(reverseBytes(W3), 8, 12), LE, Unsigned) +Int Bytes2Int(substrBytes(reverseBytes(W0), 8, 12), LE, Unsigned) +Int Bool2Word(4294967295 <Int Bytes2Int(substrBytes(reverseBytes(W3), 0, 4), LE, Unsigned) +Int Bytes2Int(substrBytes(reverseBytes(W0), 0, 4), LE, Unsigned)) &Int 4294967295 <Int Bytes2Int(substrBytes(reverseBytes(W3), 8, 12), LE, Unsigned) +Int Bytes2Int(substrBytes(reverseBytes(W0), 8, 12), LE, Unsigned) &Int 4294967295) &Int Bool2Word(Bytes2Int(substrBytes(reverseBytes(W3), 12, 16), LE, Unsigned) +Int Bytes2Int(substrBytes(reverseBytes(W0), 12, 16), LE, Unsigned) +Int Bool2Word(4294967295 <Int Bytes2Int(substrBytes(reverseBytes(W3), 8, 12), LE, Unsigned) +Int Bytes2Int(substrBytes(reverseBytes(W0), 8, 12), LE, Unsigned)) +Int Bool2Word(Bytes2Int(substrBytes(reverseBytes(W3), 8, 12), LE, Unsigned) +Int Bytes2Int(substrBytes(reverseBytes(W0), 8, 12), LE, Unsigned) +Int Bool2Word(4294967295 <Int Bytes2Int(substrBytes(reverseBytes(W3), 0, 4), LE, Unsigned) +Int Bytes2Int(substrBytes(reverseBytes(W0), 0, 4), LE, Unsigned)) &Int 4294967295 <Int Bytes2Int(substrBytes(reverseBytes(W3), 8, 12), LE, Unsigned) +Int Bytes2Int(substrBytes(reverseBytes(W0), 8, 12), LE, Unsigned) &Int 4294967295) &Int 4294967295 <Int Bytes2Int(substrBytes(reverseBytes(W3), 12, 16), LE, Unsigned) +Int Bytes2Int(substrBytes(reverseBytes(W0), 12, 16), LE, Unsigned) +Int Bool2Word(4294967295 <Int Bytes2Int(substrBytes(reverseBytes(W3), 8, 12), LE, Unsigned) +Int Bytes2Int(substrBytes(reverseBytes(W0), 8, 12), LE, Unsigned)) &Int 4294967295)) &Int 4294967295)
+     31 |-> (Bytes2Int(substrBytes(Int2Bytes(3, (Bytes2Int(substrBytes(reverseBytes(W3), 4, 8), LE, Unsigned) +Int Bytes2Int(substrBytes(reverseBytes(W0), 4, 8), LE, Unsigned) +Int Bool2Word(4294967295 <Int Bytes2Int(substrBytes(reverseBytes(W3), 0, 4), LE, Unsigned) +Int Bytes2Int(substrBytes(reverseBytes(W0), 0, 4), LE, Unsigned)) &Int 4294967295) >>Int 8, LE), 0, 1), LE, Unsigned) => (Bytes2Int(substrBytes(reverseBytes(W3), 4, 8), LE, Unsigned) +Int Bytes2Int(substrBytes(reverseBytes(W0), 4, 8), LE, Unsigned) +Int Bool2Word(4294967295 <Int Bytes2Int(substrBytes(reverseBytes(W3), 0, 4), LE, Unsigned) +Int Bytes2Int(substrBytes(reverseBytes(W0), 0, 4), LE, Unsigned)) &Int 4294967295) >>Int 8 &Int 255)
     </regs>
     <haltCond> ADDRESS ( 0 ) </haltCond>
 requires lengthBytes(W0) ==Int 32