Simp rulle 4 >> 0 (#142)

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

Author: 3 people

package/version

@@ -1 +1 @@
-0.1.107
+0.1.108

pyproject.toml

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

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

@@ -19,6 +19,7 @@ module INT-SIMPLIFICATIONS [symbolic]
     [simplification, preserves-definedness]
   rule [int-lsh-non-negative]: 0 <=Int (X <<Int Y) => true
     requires 0 <=Int X andBool 0 <=Int Y [simplification]
+  rule [rsh-0]: X >>Int 0 => X [simplification, preserves-definedness]
 ```
 
 ## &Int Lemmas
@@ -27,13 +28,10 @@ module INT-SIMPLIFICATIONS [symbolic]
   rule [chop-32bits]: X &Int 4294967295 => X requires 0 <=Int X andBool X <Int 4294967296 [simplification]
   rule [int-and-assoc]: (X &Int Y) &Int Z => X &Int (Y &Int Z) [simplification, symbolic(X), concrete(Y,Z)]
   rule [int-and-add-assoc-8]: ((X &Int 255) +Int Y) &Int 255 => (X +Int Y) &Int 255
-    requires 0 <=Int X andBool 0 <=Int Y
     [simplification]
   rule [int-and-add-assoc-16]: ((X &Int 65535) +Int Y) &Int 65535 => (X +Int Y) &Int 65535
-    requires 0 <=Int X andBool 0 <=Int Y
     [simplification]
   rule [int-and-add-assoc-32]: ((X &Int 4294967295) +Int Y) &Int 4294967295 => (X +Int Y) &Int 4294967295
-    requires 0 <=Int X andBool 0 <=Int Y
     [simplification]
 ```
 

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

@@ -33,6 +33,8 @@ module BYTES-INT
      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)
+     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)
     </regs>
     <haltCond> ADDRESS ( 0 ) </haltCond>
 requires lengthBytes(W0) ==Int 32