Improve some simplifications for booster (#172)

* add lemmas without #Equals to int-normalisation

* add lemmas without #Equals to bytes-normalisation and proven-mx lemma files

* add a trivial lemma for int64encoding of boolToInt values

* Constrain simplifications for ^IntTotal to have positive exponent

* Set Version: 0.1.75

---------

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

kmxwasm/pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kmxwasm"
-version = "0.1.74"
+version = "0.1.75"
 description = "Symbolic execution for the MultiversX blockchain with the Wasm semantics, using pyk."
 authors = [
     "Runtime Verification, Inc. <[email protected]>",

kmxwasm/src/kmxwasm/kdist/mxwasm-semantics/lemmas/bytes-normalization-lemmas.md

@@ -135,6 +135,19 @@ module BYTES-NORMALIZATION-LEMMAS  [symbolic]
         requires lengthBytes(A) >Int 0
         [simplification(100)]
 
+    rule b"" ==K Int2Bytes(Len:Int, _Value:Int, _E:Endianness)
+        => 0 ==Int Len
+        [simplification]
+    rule b"" ==K Int2Bytes(Value:Int, _E:Endianness, _S:Signedness)
+        => 0 ==Int Value
+        [simplification]
+    rule b"" ==K substrBytesTotal(B:Bytes, Start:Int, End:Int)
+        => 0 ==Int End -Int Start
+        requires definedSubstrBytes(B, Start, End)
+        [simplification]
+    rule b"" ==K A => false
+        requires lengthBytes(A) >Int 0
+        [simplification(100)]
 
 endmodule
 ```

kmxwasm/src/kmxwasm/kdist/mxwasm-semantics/lemmas/int-encoding-lemmas.md

@@ -74,6 +74,9 @@ of the bytes corresponding to `B<N>` values that are `>= 0`, placed on the
       requires 0 <=Int B1 andBool B1 <=Int 7
       [simplification, concrete, preserves-definedness]  // All <<Int and >>Int arguments are >= 0
 
+  rule int64encoding(boolToInt(_), -1, -1, -1, -1, -1, -1, -1, 0) ==Int A => false
+      requires 1 <Int A
+      [simplification] // boolToInt is 0,1-valued
 ```
 int64BytesAre0
 --------------

kmxwasm/src/kmxwasm/kdist/mxwasm-semantics/lemmas/int-normalization-lemmas.md

@@ -257,6 +257,24 @@ module INT-BIT-NORMALIZATION-LEMMAS  [symbolic]
       => {true #Equals A <=Int fullMask(8) }
       requires 0 <=Int A andBool A <=Int fullMask(16)
       [simplification]
+
+  // versions of the above rules that avoid #Equals:
+  rule 0  ==Int (A &Int B) >>IntTotal C
+       => 0 ==Int A &Int B
+      requires B &Int fullMask(C) ==Int 0
+      [simplification, concrete(B, C)]
+  rule 0 ==Int A &Int 4278190080
+       => A <=Int fullMask(24)
+      requires 0 <=Int A andBool A <=Int fullMask(32)
+      [simplification]
+  rule 0 ==Int A &Int 16711680
+      => A <=Int fullMask(16)
+      requires 0 <=Int A andBool A <=Int fullMask(24)
+      [simplification]
+  rule 0 ==Int A &Int 65280
+      => A <=Int fullMask(8)
+      requires 0 <=Int A andBool A <=Int fullMask(16)
+      [simplification]
 endmodule
 
 module INT-ARITHMETIC-NORMALIZATION-LEMMAS
@@ -399,30 +417,62 @@ module INT-ARITHMETIC-NORMALIZATION-LEMMAS
   rule {((X +Int Y) modIntTotal M) #Equals ((X +Int Z) modIntTotal M)}
       => {(Y modIntTotal M) #Equals (Z modIntTotal M)}
       [simplification]
+  rule ((X +Int Y) modIntTotal M) ==Int ((X +Int Z) modIntTotal M)
+      => (Y modIntTotal M) ==Int (Z modIntTotal M)
+      [simplification]
+
   rule X modIntTotal Y => X requires 0 <=Int X andBool X <Int Y
 
   rule {(A modIntTotal C) #Equals (B modIntTotal C)} => #Top
       requires A ==Int B
       [simplification]
+  rule (A modIntTotal C) ==Int (B modIntTotal C) => true
+      requires A ==Int B
+      [simplification]
 
 
-  rule {0 #Equals A ^IntTotal _B} => #Bottom
+  rule {0 #Equals A ^IntTotal B} => #Bottom
       requires A =/=Int 0
+       andBool B >=Int 0
       [simplification(40)]
-  rule {A ^IntTotal _B #Equals 0} => #Bottom
+  rule {A ^IntTotal B #Equals 0} => #Bottom
       requires A =/=Int 0
+       andBool B >=Int 0
       [simplification(40)]
   rule {0 #Equals A ^IntTotal B} => {0 #Equals A}
-      requires B =/=Int 0
+      requires B >Int 0
+      [simplification(50)]
+
+  // ==Int versions of the above rules
+  rule 0 ==Int A ^IntTotal B => false
+      requires A =/=Int 0
+       andBool B >=Int 0
+      [simplification(40)]
+  rule A ^IntTotal B ==Int 0 => false
+      requires A =/=Int 0
+       andBool B >=Int 0
+      [simplification(40)]
+  rule 0 ==Int A ^IntTotal B => 0 ==Int A
+      requires B >Int 0
       [simplification(50)]
 
+  // complementing the above, ^IntTotal is positive if its 1st argument is
+  rule 0 <Int A ^IntTotal B => 0 <Int A
+       requires B >Int 0
+      [simplification]
+
   rule {0 #Equals A divIntTotal B} => {true #Equals A <Int B}
       requires 0 <=Int A andBool 0 <Int B
       [simplification]
   rule {A divIntTotal B #Equals 0} => {true #Equals A <Int B}
       requires 0 <=Int A andBool 0 <Int B
       [simplification]
 
+  // rule similar to the above but using Int domain operations
+  rule A divIntTotal B ==Int 0 => A <Int B
+      requires 0 <=Int A andBool 0 <Int B
+      [simplification]
+
   // log2IntTotal(X) is the index of the highest bit. This means that
   // X < 2^(log2IntTotal(X) + 1) since the highest bit of the right term
   // has a higher index.

kmxwasm/src/kmxwasm/kdist/mxwasm-semantics/lemmas/proven-mx-lemmas.md

@@ -21,6 +21,12 @@ module PROVEN-MX-LEMMAS
     rule  ( { 1 #Equals #bool ( B:Bool ) }:Bool => { true #Equals B:Bool }:Bool )
       [simplification()]
 
+    rule  0 ==Int #bool ( B:Bool )  => notBool B
+      [simplification()]
+
+    rule  1 ==Int #bool ( B:Bool )  => B:Bool
+      [simplification()]
+
     rule  ( size ( _L:List ) >=Int 0 => true )
       [smt-lemma, simplification()]
 
@@ -179,6 +185,10 @@ module PROVEN-MX-LEMMAS
     rule  ( { ((X:Int) +Int (Y:Int)) modIntTotal (M:Int) #Equals ((X:Int) +Int (Z:Int)) modIntTotal (M:Int) }:Bool => { (Y:Int) modIntTotal (M:Int) #Equals (Z:Int) modIntTotal (M:Int) }:Bool )
       [simplification()]
 
+    rule  (X +Int Y) modIntTotal M ==Int (X +Int Z) modIntTotal M
+          => Y modIntTotal M ==Int Z modIntTotal M
+      [simplification()]
+
     rule  ( (X:Int) modIntTotal (Y:Int) => X:Int )
       requires ( 0 <=Int X:Int
        andBool ( X:Int <Int Y:Int

package/version

@@ -1 +1 @@
-0.1.74
+0.1.75