Fix definedness

kmxwasm/pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kmxwasm"
-version = "0.1.70"
+version = "0.1.71"
 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

@@ -70,14 +70,21 @@ module BYTES-NORMALIZATION-LEMMAS  [symbolic]
             LE
         )
         requires 0 <=Int Start andBool Start <=Int End andBool End <=Int Size
-        [simplification]
+        [simplification, preserves-definedness]
+        // Preserving definedness:
+        // * The LHS:
+        //   - Int2Bytes is total
+        //   - substrBytesTotal is total
+        // * The RHS:
+        //   - >>Int is defined because 8 * Start >= 0
+        //   - Int2Bytes is total
 
     rule replaceAtBytesTotal(Dest:Bytes, Start:Int, Src:Bytes)
         => substrBytes(Dest, 0, Start)
           +Bytes Src
           +Bytes substrBytes(Dest, Start +Int lengthBytes(Src), lengthBytes(Dest))
         requires 0 <=Int Start andBool Start +Int lengthBytes(Src) <=Int lengthBytes(Dest)
-        [simplification]
+        [simplification, preserves-definedness]
 
     rule padRightBytesTotal (B:Bytes, Length:Int, Value:Int) => B
         requires Length <=Int lengthBytes(B)

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

@@ -106,7 +106,9 @@ module INT-INEQUALITIES-LEMMAS
       requires 0 <=Int A
           andBool 0 <=Int C
           andBool definedShlInt(A, B)
-      [simplification, concrete(B, C)]
+      [simplification, concrete(B, C), preserves-definedness]
+      // Preserving definedness: definedShlInt(A, B) requires 0 <= B, so all shifts are defined.
+
   // When c & fullMask(b) != 0:
   // a * 2^b < c
   // iff a < c / 2^b
@@ -127,7 +129,9 @@ module INT-INEQUALITIES-LEMMAS
           andBool 0 <=Int C
           andBool definedShlInt(A, B)
           andBool notBool C &Int fullMask(B) ==Int 0
-      [simplification, concrete(B, C)]
+      [simplification, concrete(B, C), preserves-definedness]
+      // Preserving definedness: definedShlInt checks that 0 <= B so all
+      // shifts are defined. fullMask is total.
 
   rule 0 <=Int A >>IntTotal B => 0 <=Int A
       requires definedShrInt(A, B)
@@ -155,7 +159,7 @@ module INT-INEQUALITIES-LEMMAS
       requires 0 <=Int A
           andBool 0 <=Int C
           andBool definedShrInt(A, B)
-      [simplification, concrete(B, C)]
+      [simplification, concrete(B, C), preserves-definedness]
   // trunc(a / 2^b) < c
   // iff a / 2^b - frac(a / 2^b) <= c
   // iff a / 2^b <= c + frac(a / 2^b)
@@ -172,7 +176,7 @@ module INT-INEQUALITIES-LEMMAS
       requires 0 <=Int A
           andBool 0 <=Int C
           andBool definedShrInt(A, B)
-      [simplification, concrete(B, C)]
+      [simplification, concrete(B, C), preserves-definedness]
 
   // Moved to proven-mx-lemmas.md
   // rule A +Int B <=Int A => B <=Int 0  [simplification]
@@ -239,19 +243,19 @@ module INT-INEQUALITIES-LEMMAS
 
   rule A *Int B <=Int C => B <=Int C /Int A
       requires 0 <Int A
-      [simplification, concrete(A, C)]
+      [simplification, concrete(A, C), preserves-definedness]
   rule A *Int B <Int C => B <=Int (C -Int 1) /Int A
       requires 0 <Int A
-      [simplification, concrete(A, C)]
+      [simplification, concrete(A, C), preserves-definedness]
   rule A <=Int B *Int C => A /Int B <=Int C
       requires 0 <Int B andBool A modInt B ==Int 0
-      [simplification, concrete(A, B)]
+      [simplification, concrete(A, B), preserves-definedness]
   rule A <=Int B *Int C => A /Int B +Int 1 <=Int C
       requires 0 <Int B andBool A modInt B =/=Int 0
-      [simplification, concrete(A, B)]
+      [simplification, concrete(A, B), preserves-definedness]
   rule A <Int B *Int C => A /Int B <Int C
       requires 0 <Int B
-      [simplification, concrete(A, B)]
+      [simplification, concrete(A, B), preserves-definedness]
 
   rule A *Int B <=Int C => (0 -Int C) <=Int (0 -Int A) *Int B
       requires A <Int 0
@@ -270,44 +274,44 @@ module INT-INEQUALITIES-LEMMAS
   // Has tests
   rule A <=Int B *Int X => A /Int B <=Int X
       requires 0 <Int B andBool A %Int B ==Int 0
-      [simplification, concrete(A, B)]
+      [simplification, concrete(A, B), preserves-definedness]
   // Has tests
   rule A <=Int B *Int X => X <=Int A /Int B
       requires B <Int 0 andBool A %Int B ==Int 0
-      [simplification, concrete(A, B)]
+      [simplification, concrete(A, B), preserves-definedness]
   // Has tests
   rule A *Int X <=Int B => X <=Int B /Int A
       requires 0 <Int A andBool B %Int A ==Int 0
-      [simplification, concrete(A, B)]
+      [simplification, concrete(A, B), preserves-definedness]
   // Has tests
   rule A *Int X <=Int B => B /Int A <=Int X
       requires A <Int 0 andBool B %Int A ==Int 0
-      [simplification, concrete(A, B)]
+      [simplification, concrete(A, B), preserves-definedness]
 
   // Has tests
   rule A <Int B *Int X => A /Int B <Int X
       requires 0 <Int B andBool A %Int B ==Int 0
-      [simplification, concrete(A, B)]
+      [simplification, concrete(A, B), preserves-definedness]
   // Has tests
   rule A <Int B *Int X => X <Int A /Int B
       requires B <Int 0 andBool A %Int B ==Int 0
-      [simplification, concrete(A, B)]
+      [simplification, concrete(A, B), preserves-definedness]
   // Has tests
   rule A *Int X <Int B => X <Int B /Int A
       requires 0 <Int A andBool B %Int A ==Int 0
-      [simplification, concrete(A, B)]
+      [simplification, concrete(A, B), preserves-definedness]
   // Has tests
   rule A *Int X <Int B => B /Int A <Int X
       requires A <Int 0 andBool B %Int A ==Int 0
-      [simplification, concrete(A, B)]
+      [simplification, concrete(A, B), preserves-definedness]
 
   // a * b <= c
   // iff a <= c / b
   // iff a <= trunc(c/b)
   // Has tests
   rule B *Int A <=Int C => A <=Int C /Int B
       requires 0 <Int B andBool 0 <=Int C
-      [simplification, concrete(B, C)]
+      [simplification, concrete(B, C), preserves-definedness]
   // When c mod b is 0:
   // a * b < c
   // iff a < c / b
@@ -328,7 +332,7 @@ module INT-INEQUALITIES-LEMMAS
           #fi
       requires 0 <Int B
         andBool 0 <=Int C
-      [simplification, concrete(B, C)]
+      [simplification, concrete(B, C), preserves-definedness]
   // When a mod c is 0:
   // a <= b * c
   // iff a / c <= b
@@ -349,14 +353,14 @@ module INT-INEQUALITIES-LEMMAS
             #fi
       requires 0 <Int C
         andBool 0 <=Int A
-      [simplification, concrete(A, C)]
+      [simplification, concrete(A, C), preserves-definedness]
   // a < b * c
   // iff a / c < b
   // iff trunc(a/c) < b
   // Has tests
   rule A <Int C *Int B => A /Int C <Int B
       requires 0 <Int C andBool 0 <=Int B
-      [simplification, concrete(A, C)]
+      [simplification, concrete(A, C), preserves-definedness]
 
 
   // a * b <= c
@@ -412,7 +416,7 @@ module INT-INEQUALITIES-LEMMAS
   rule log2IntTotal(A) <Int B => A <Int 2 ^Int B
       requires 0 <Int A andBool 0 <=Int B
           andBool B <=Int 1000 // Making sure there is no OOM when computing 2^B
-      [simplification, concrete(B)]
+      [simplification, concrete(B), preserves-definedness]
   // Partly covering the case when 1000 < B
   // Has tests
   rule log2IntTotal(A) <Int B => true
@@ -426,7 +430,7 @@ module INT-INEQUALITIES-LEMMAS
   rule log2IntTotal(A) <=Int B => A <Int 2 ^Int (B +Int 1)
       requires 0 <Int A andBool 0 <=Int B
           andBool B <=Int 1000 // Making sure there is no OOM when computing 2^B
-      [simplification, concrete(B)]
+      [simplification, concrete(B), preserves-definedness]
   // Partly covering the case when 1000 < B
   // Has tests
   rule log2IntTotal(A) <=Int B => true
@@ -440,7 +444,7 @@ module INT-INEQUALITIES-LEMMAS
   rule B <=Int log2IntTotal(A) => 2 ^Int B <=Int A
       requires 0 <Int A andBool 0 <=Int B
           andBool B <=Int 1000 // Making sure there is no OOM when computing 2^B
-      [simplification, concrete(B)]
+      [simplification, concrete(B), preserves-definedness]
   // Partly covering the case when 1000 < B
   // Has tests
   rule B <=Int log2IntTotal(A) => false
@@ -455,7 +459,7 @@ module INT-INEQUALITIES-LEMMAS
   rule B <Int log2IntTotal(A) => 2 ^Int (B +Int 1) <=Int A
       requires 0 <Int A andBool 0 <=Int B
           andBool B <=Int 1000 // Making sure there is no OOM when computing 2^B
-      [simplification, concrete(B)]
+      [simplification, concrete(B), preserves-definedness]
   // Partly covering the case when 1000 < B
   // Has tests
   rule B <Int log2IntTotal(A) => false

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

@@ -176,11 +176,11 @@ module BINARY-SEARCH [symbolic]
       => findLowerUnknown(B, R, Min, (Min +Int Max) /Int 2)
       requires Min <Int Max -Int 1
         andBool evaluate(B, (Min +Int Max) /Int 2)
-      [simplification(50)]
+      [simplification(50), preserves-definedness]
   rule findLowerUnknown(B:BinSearchBeforeLambda, R:BinSearchResultLambda, Min, Max)
       => findLowerUnknown(B, R, (Min +Int Max) /Int 2, Max)
       requires Min <Int Max -Int 1
-      [simplification(51)]
+      [simplification(51), preserves-definedness]
 
   rule evaluate(GeqThan(A), _:Int, Max:Int) => true
       requires A <=Int Max

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

@@ -110,7 +110,7 @@ module INT-BIT-NORMALIZATION-LEMMAS  [symbolic]
         => (A &Int (M >>Int B)) <<IntTotal B
       requires 0 <=Int B
           andBool 1 <<Int B <=Int M +Int 1
-      [simplification, concrete(M, B)]
+      [simplification, concrete(M, B), preserves-definedness]
   rule (_A <<IntTotal B) &Int M => 0
       requires 0 <=Int M
           andBool 0 <=Int B
@@ -119,7 +119,7 @@ module INT-BIT-NORMALIZATION-LEMMAS  [symbolic]
   rule (A >>IntTotal B) &Int M
         => (A &Int (M <<Int B)) >>IntTotal B
       requires 0 <=Int B
-      [simplification, concrete(M, B)]
+      [simplification, concrete(M, B), preserves-definedness]
 
   rule (A <<IntTotal 0) => A
       [simplification]
@@ -395,7 +395,7 @@ module INT-ARITHMETIC-NORMALIZATION-LEMMAS
 
   rule (X +Int Y) modIntTotal Z => (X +Int (Y modInt Z)) modIntTotal Z
       requires Z =/=Int 0 andBool Y >=Int Z
-      [simplification, concrete(Y, Z)]
+      [simplification, concrete(Y, Z), preserves-definedness]
   rule {((X +Int Y) modIntTotal M) #Equals ((X +Int Z) modIntTotal M)}
       => {(Y modIntTotal M) #Equals (Z modIntTotal M)}
       [simplification]

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

@@ -174,7 +174,7 @@ module PROVEN-MX-LEMMAS
       requires ( notBool (Z:Int ==Int 0)
        andBool ( Y:Int >=Int Z:Int
                ))
-      [concrete(Y,Z), simplification()]
+      [concrete(Y,Z), preserves-definedness(), simplification()]
 
     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()]

kmxwasm/src/kmxwasm/kdist/mxwasm-semantics/lemmas/sparse-bytes/handle-sparse-bytes-lemmas.md

@@ -352,7 +352,7 @@ clause that is more restrictive for `canSplitSparseBytes` ensures that
             , 0
             )
         requires 0 <Int Addr andBool Addr <Int lengthBytes(A)
-        [simplification, concrete(A, Addr)]
+        [simplification, concrete(A, Addr), preserves-definedness]
     rule splitSparseBytes(SBChunk(#empty(A)) SB:SparseBytes, Prefix:SparseBytes, Addr:Int)
         => splitSparseBytes
             ( SBChunk(#empty(A -Int Addr))
@@ -506,7 +506,7 @@ module UPDATE-SPARSE-BYTES-LEMMAS
             andBool functionCommutesAtStart(F)
             andBool Start <Int lengthBytes(A)
             andBool 0 <Int Start
-        [simplification, concrete(A, Start)]
+        [simplification, concrete(A, Start), preserves-definedness]
     rule updateSparseBytes(
               F:SBSetFunction,
               SBChunk(#empty(A)) SB:SparseBytes,
@@ -630,7 +630,7 @@ module UPDATE-SPARSE-BYTES-LEMMAS
             andBool 0 <Int Start
             andBool Start <Int lengthBytes(A)
             andBool lengthBytes(A) <Int Start +Int Width
-        [simplification, concrete(A, Start)]
+        [simplification, concrete(A, Start), preserves-definedness]
     rule updateSparseBytes(
               F:SBSetFunction,
               SBChunk(#bytes(A)),
@@ -643,7 +643,7 @@ module UPDATE-SPARSE-BYTES-LEMMAS
             andBool functionCommutesAtStart(F)
             andBool 0 <Int Start
             andBool Start <Int lengthBytes(A)
-        [simplification, concrete(A, Start)]
+        [simplification, concrete(A, Start), preserves-definedness]
     rule updateSparseBytes(
               F:SBSetFunction,
               SBChunk(#bytes(A)),
@@ -654,8 +654,9 @@ module UPDATE-SPARSE-BYTES-LEMMAS
           )
         requires functionSparseBytesWellDefined(F, 0, Width)
             andBool functionCommutesAtStart(F)
+            andBool 0 <=Int Width
             andBool Width <Int lengthBytes(A)
-        [simplification, concrete(A)]
+        [simplification, concrete(A), preserves-definedness]
     // TODO: Make this work
     // rule updateSparseBytes(
     //           F:SBSetFunction,
@@ -981,7 +982,7 @@ module EXTRACT-SPARSE-BYTES-LEMMAS
             andBool 0 <Int Start
             andBool Start <Int lengthBytes(A)
             andBool lengthBytes(A) <Int Start +Int Width
-        [simplification, concrete(A, Start)]
+        [simplification, concrete(A, Start), preserves-definedness]
     rule extractSparseBytes(
               F:SBGetFunction,
               SBChunk(#bytes(_)) #as SBI:SBItemChunk,

kmxwasm/src/kmxwasm/kdist/mxwasm-semantics/lemmas/sparse-bytes/set-range-lemmas.md

@@ -38,7 +38,7 @@ module SET-RANGE-LEMMAS
         => SBChunk(#bytes(replaceAtBytes(A, Start, Int2Bytes(Width, Value, LE))))
         requires functionSparseBytesWellDefined(setRange(Value), Start, Width)
             andBool Start +Int Width <=Int lengthBytes(A)
-        [simplification, concrete(A)]
+        [simplification, concrete(A), preserves-definedness]
 
     rule updateSparseBytes(setRange(Value:Int), SBChunk(#empty(A)), Start:Int, Width:Int)
         => SBChunk(#empty(Start))

kmxwasm/src/kmxwasm/kdist/mxwasm-semantics/lemmas/sparse-bytes/substr-sparse-bytes-lemmas.md

@@ -79,7 +79,7 @@ module SUBSTR-SPARSE-BYTES-LEMMAS
             0, Width
         )
         requires 0 <Int Start andBool Start <Int Size
-        [simplification]
+        [simplification, preserves-definedness]
     rule extractSparseBytes(
             substr, SBChunk(#bytes(Int2Bytes(Size:Int, Val:Int, LE))),
             0, Width:Int
@@ -89,7 +89,7 @@ module SUBSTR-SPARSE-BYTES-LEMMAS
             0, Width
         )
         requires 0 <Int Width andBool Width <Int Size
-        [simplification]
+        [simplification, preserves-definedness]
 
 endmodule