Simp rule 4 complex (X + Y & 4294967295) + Z & 4294967295 (#140)

Co-authored-by: devops <devops@runtimeverification.com>

Author: Stevengre

.gitignore

@@ -2,3 +2,5 @@
 __pycache__/
 .coverage
 tests/riscv-arch-test-compiled
+debug*/
+.DS_Store

package/version

@@ -1 +1 @@
-0.1.106
+0.1.107

pyproject.toml

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

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

@@ -43,6 +43,7 @@ module INT-SIMPLIFICATIONS [symbolic]
   rule [int-and-ineq]: 0 <=Int A &Int B => true requires 0 <=Int A andBool 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]
   rule [int-add-ineq-4294967295]: X &Int 4294967295 <Int A => 4294967295 <Int X
     requires 0 <=Int A andBool A <=Int X [simplification]
 ```

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

@@ -15,6 +15,12 @@ module WORD-SIMPLIFICATIONS
     requires NumBits ==Int lengthBytes(B) *Int 8 [simplification(45), preserves-definedness]
 ```
 
+## Bool2Word
+
+```k
+  rule [bool2word-non-neg]: 0 <=Int Bool2Word(_) => true [simplification]
+```
+
 ```k
 endmodule
 ```

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

@@ -30,10 +30,13 @@ module BYTES-INT
      23 |-> (Bool2Word(Bytes2Int(substrBytes(reverseBytes(W3), 0, 4), LE, Unsigned) +Int Bytes2Int(substrBytes(reverseBytes(W0), 0, 4), LE, Unsigned) &Int 4294967295 <Int Bytes2Int(substrBytes(reverseBytes(W3), 0, 4), LE, Unsigned)) => Bool2Word(4294967295 <Int Bytes2Int(substrBytes(reverseBytes(W3), 0, 4), LE, Unsigned) +Int Bytes2Int(substrBytes(reverseBytes(W0), 0, 4), LE, Unsigned)))
      24 |-> (Bytes2Int(b"\x00\x00\x00" +Bytes substrBytes(W0, 24, 28), LE, Unsigned) &Int 4294967295 => Bytes2Int ( b"\x00\x00\x00" +Bytes substrBytes(W0 ,24, 25), LE, Unsigned))
      25 |-> (Bytes2Int(Int2Bytes(1, (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), 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), LE, Unsigned) => ( Bytes2Int ( substrBytes ( reverseBytes ( W3:Bytes ) , 8 , 12 ) , LE , Unsigned ) +Int Bytes2Int ( substrBytes ( reverseBytes ( W0:Bytes ) , 8 , 12 ) , LE , Unsigned ) +Int Bool2Word ( 4294967295 <Int Bytes2Int ( substrBytes ( reverseBytes ( W3:Bytes ) , 4 , 8 ) , LE , Unsigned ) +Int Bytes2Int ( substrBytes ( reverseBytes ( W0:Bytes ) , 4 , 8 ) , LE , Unsigned ) +Int Bool2Word ( 4294967295 <Int Bytes2Int ( substrBytes ( reverseBytes ( W3:Bytes ) , 0 , 4 ) , LE , Unsigned ) +Int Bytes2Int ( substrBytes ( reverseBytes ( W0:Bytes ) , 0 , 4 ) , LE , Unsigned ) ) ) &Int 4294967295 ) >>Int 8 &Int 255)
+     26 |-> ((Bytes2Int(substrBytes(reverseBytes(W3), 20, 24), LE, Unsigned) +Int Bytes2Int(substrBytes(reverseBytes(W0), 20, 24), LE, Unsigned) &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 => (Bytes2Int(substrBytes(reverseBytes(W3), 20, 24), LE, Unsigned) +Int Bytes2Int(substrBytes(reverseBytes(W0), 20, 24), LE, Unsigned)) +Int Bool2Word(4294967295 <Int Bytes2Int(substrBytes(reverseBytes(W3), 16, 20), LE, Unsigned) +Int Bytes2Int(substrBytes(reverseBytes(W0), 16, 20), LE, Unsigned)) &Int 4294967295)
+     27 |-> ((X +Int Y &Int 4294967295) +Int Z &Int 4294967295 => X +Int Y +Int Z &Int 4294967295)
+     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)
     </regs>
     <haltCond> ADDRESS ( 0 ) </haltCond>
 requires lengthBytes(W0) ==Int 32
  andBool lengthBytes(W1) ==Int 4
  andBool lengthBytes(W3) ==Int 32
- andBool 0 <=Int X andBool 0 <=Int Y
+ andBool 0 <=Int X andBool 0 <=Int Y andBool 0 <=Int Z
 endmodule