^Int and /Int definedness preservation (#2425)

* ^Int and /Int definedness preservation

* Set Version: 1.0.555

---------

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

Author: PetarMax

kevm-pyk/pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kevm-pyk"
-version = "1.0.554"
+version = "1.0.555"
 description = ""
 authors = [
     "Runtime Verification, Inc. <[email protected]>",

kevm-pyk/src/kevm_pyk/__init__.py

@@ -5,4 +5,4 @@
 if TYPE_CHECKING:
     from typing import Final
 
-VERSION: Final = '1.0.554'
+VERSION: Final = '1.0.555'

kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/bitwise-simplification.k

@@ -50,15 +50,15 @@ module BITWISE-SIMPLIFICATION [symbolic]
       requires 0 <=Int X
        andBool X +Int 1 ==Int 2 ^Int log2Int(X +Int 1)
        andBool 0 <=Int Y andBool Y <Int X +Int 1
-       [concrete(X), simplification, comm]
+       [concrete(X), simplification, comm, preserves-definedness]
 
     // Generalization of: notMaxUIntXXX &Int Y => 0 requires #rangeUInt(XXX, Y)
     rule [bitwise-and-notMaxUInt-zero]:
       X &Int Y => 0
       requires #rangeUInt(256, X)
        andBool pow256 -Int X ==Int 2 ^Int ( log2Int ( pow256 -Int X ) )
        andBool 0 <=Int Y andBool Y <Int pow256 -Int X
-      [simplification, concrete(X)]
+      [simplification, concrete(X), preserves-definedness]
 
     // Generalization of: maxUIntXXX &Int #asWord ( BA )
     rule X &Int #asWord ( BA ) => #asWord ( #range(BA, 32 -Int (log2Int(X +Int 1) /Int 8), log2Int(X +Int 1) /Int 8) )
@@ -113,7 +113,7 @@ module BITWISE-SIMPLIFICATION [symbolic]
 
     rule (X <<Int Y) <Int pow256 => true
       requires 0 <=Int X andBool 0 <=Int Y andBool Y <Int 256 andBool X <Int 2 ^Int (256 -Int Y)
-      [simplification]
+      [simplification, preserves-definedness]
 
     rule 0 <=Int (X <<Int Y) => true requires 0 <=Int X andBool 0 <=Int Y [simplification]
 

kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/bytes-simplification.k

@@ -41,14 +41,14 @@ module BYTES-SIMPLIFICATION [symbolic]
       requires 0 <=Int W
        andBool 0 <=Int X andBool X <Int 2 ^Int (8 *Int W)
        andBool 0 <=Int Y andBool Y <Int 2 ^Int (8 *Int W)
-      [simplification]
+      [simplification, preserves-definedness]
 
     rule [buf-inject-ml]:
       { #buf(W:Int, X:Int) #Equals #buf(W:Int, Y:Int) } => { X #Equals Y }
       requires 0 <=Int W
        andBool 0 <=Int X andBool X <Int 2 ^Int (8 *Int W)
        andBool 0 <=Int Y andBool Y <Int 2 ^Int (8 *Int W)
-      [simplification]
+      [simplification, preserves-definedness]
 
     rule [buf-as-int]: B:Bytes ==K #buf(32, X:Int) => X ==Int #asInteger(B)
       requires lengthBytes(B) <=Int 32
@@ -68,21 +68,21 @@ module BYTES-SIMPLIFICATION [symbolic]
       #buf (W:Int , #asWord(B:Bytes)) => #range(B, lengthBytes(B) -Int W, W)
       requires 0 <=Int W andBool W <Int lengthBytes(B) andBool lengthBytes(B) <=Int 32
        andBool #asWord(B) <Int 2 ^Int (8 *Int W)
-      [simplification, concrete(W)]
+      [simplification, concrete(W), preserves-definedness]
 
     rule [buf-asWord-invert-rl]:
       #asWord ( #buf ( WB:Int, X:Int ) ) => X
       requires 0 <=Int WB andBool 0 <=Int X andBool
                ( ( WB <=Int 32 andBool X <Int 2 ^Int (WB *Int 8) ) orBool
                  ( WB  >Int 32 andBool X <Int pow256 ) )
-      [simplification, concrete(WB)]
+      [simplification, concrete(WB), preserves-definedness]
 
     rule [buf-asWord-invert-rl-range]:
       #asWord ( #range ( #buf ( WB:Int, X:Int ), S:Int, WR:Int ) ) => X
       requires 0 <=Int WB andBool 0 <=Int X andBool 0 <=Int S andBool 0 <=Int WR
        andBool S +Int WR ==Int WB
        andBool X <Int 2 ^Int (WR *Int 8)
-      [simplification, concrete(WB, S, WR)]
+      [simplification, concrete(WB, S, WR), preserves-definedness]
 
     rule [buf-zero-concat-base]:
       #buf(W1:Int, 0) +Bytes #buf(W2:Int, 0) => #buf(W1 +Int W2, 0)
@@ -189,13 +189,13 @@ module BYTES-SIMPLIFICATION [symbolic]
       B:Bytes +Bytes #buf(W:Int, X:Int) => #buf(lengthBytes(B) +Int W, X)
       requires 0 <=Int W andBool 0 <=Int X andBool X <Int 2 ^Int (W *Int 8)
        andBool #asInteger(B) ==Int 0 andBool lengthBytes(B) +Int W <=Int 32
-      [concrete(B, W), simplification]
+      [concrete(B, W), simplification, preserves-definedness]
 
     rule [range-buf-zero-concat-extend]:
       B1:Bytes +Bytes #buf(W:Int, X:Int) +Bytes B2 => #buf(lengthBytes(B1) +Int W, X) +Bytes B2
       requires 0 <=Int W andBool 0 <=Int X andBool X <Int 2 ^Int (W *Int 8)
        andBool #asInteger(B1) ==Int 0 andBool lengthBytes(B1) +Int W <=Int 32
-      [concrete(B1, W), simplification]
+      [concrete(B1, W), simplification, preserves-definedness]
 
     rule [range-memUpdate-before]:
       #range(B1:Bytes [ S1:Int := B2:Bytes ], S2:Int, W2:Int) =>
@@ -220,13 +220,13 @@ module BYTES-SIMPLIFICATION [symbolic]
       #range (#buf(W1:Int, X:Int), S2:Int, W2:Int) => #buf(W2, 0)
       requires 0 <=Int X andBool X <Int 2 ^Int (8 *Int (W1 -Int (S2 +Int W2)))
        andBool 0 <=Int S2 andBool 0 <=Int W2 andBool S2 +Int W2 <=Int W1
-      [simplification, concrete(W1, S2, W2)]
+      [simplification, concrete(W1, S2, W2), preserves-definedness]
 
     rule [range-buf-value]:
       #range (#buf(W1:Int, X:Int), S2:Int, W2:Int) => #buf(W2, X)
       requires 0 <=Int X andBool X <Int 2 ^Int (8 *Int W2)
        andBool 0 <=Int S2 andBool 0 <=Int W2 andBool W1 ==Int S2 +Int W2
-      [simplification, concrete(W1, S2, W2)]
+      [simplification, concrete(W1, S2, W2), preserves-definedness]
 
     rule [range-padRightToWidth]:
       #range(#padRightToWidth(_, BUF), 0, WIDTH) => BUF
@@ -239,7 +239,7 @@ module BYTES-SIMPLIFICATION [symbolic]
       andBool #asInteger( BZ ) ==Int 0
       andBool lengthBytes( BZ ) ==Int S
       andBool #asWord ( B ) <Int 2 ^Int ( 8 *Int W )
-      [simplification, concrete(BZ, S, W), comm]
+      [simplification, concrete(BZ, S, W), comm, preserves-definedness]
 
     rule [range-eq-check-ml]:
       { BZ +Bytes #range ( B, S, W ) #Equals B } => #Top
@@ -248,7 +248,7 @@ module BYTES-SIMPLIFICATION [symbolic]
       andBool #asInteger( BZ ) ==Int 0
       andBool lengthBytes( BZ ) ==Int S
       andBool #asWord ( B ) <Int 2 ^Int ( 8 *Int W )
-      [simplification, concrete(BZ, S, W), comm]
+      [simplification, concrete(BZ, S, W), comm, preserves-definedness]
 
     // Memory update
 
@@ -291,7 +291,9 @@ module BYTES-SIMPLIFICATION [symbolic]
 
     // #asWord
 
-    rule #asWord(WS) >>Int M => #asWord(#range(WS, 0, lengthBytes(WS) -Int (M /Int 8) ))  requires 0 <=Int M andBool M modInt 8 ==Int 0 [simplification]
+    rule #asWord(WS) >>Int M => #asWord(#range(WS, 0, lengthBytes(WS) -Int (M /Int 8) ))
+      requires 0 <=Int M andBool M modInt 8 ==Int 0
+      [simplification, preserves-definedness]
 
     // This simplification needs to be generalised properly
     rule notMaxUInt224 &Int #asWord(#padRightToWidth(32, BUF)) => #asWord(#padRightToWidth(32, BUF))

kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/evm-int-simplification.k

@@ -68,20 +68,20 @@ module EVM-INT-SIMPLIFICATION-COMMON
   rule [asWord-lt-concat]:
     #asWord ( BA1 +Bytes BA2 ) <Int X => #asWord ( BA1 ) <Int ( X -Int #asWord ( BA2 ) ) /Int ( 2 ^Int ( 8 *Int lengthBytes ( BA2 ) ) )
     requires ( X -Int #asWord ( BA2 ) ) modInt ( 2 ^Int ( 8 *Int lengthBytes ( BA2 ) ) ) ==Int 0
-    [concrete(BA2, X), simplification]
+    [concrete(BA2, X), simplification, preserves-definedness]
 
   rule [asWord-lt-range]:
     #asWord ( #range ( _:Bytes, S, W ) ) <Int X => true
     requires 0 <=Int S andBool 0 <=Int W
      andBool 2 ^Int ( 8 *Int W ) <=Int X
-    [simplification, concrete(S, W, X)]
+    [simplification, concrete(S, W, X), preserves-definedness]
 
   rule [lt-asWord-range]:
     X <Int #asWord ( #range ( B:Bytes, S, W ) ) => X <Int #asWord ( B )
     requires 0 <=Int S andBool 0 <=Int W
      andBool lengthBytes(B) ==Int S +Int W
      andBool #asWord ( B ) <Int 2 ^Int ( 8 *Int W )
-    [simplification, concrete(X, S, W)]
+    [simplification, concrete(X, S, W), preserves-definedness]
 
   // ###########################################################################
   // chop

kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k

@@ -159,10 +159,6 @@ module LEMMAS-HASKELL [symbolic]
        requires D ==Int 256 ^Int log256Int(D) andBool D >=Int 0
         andBool lengthBytes(BUF) >=Int log256Int(D) [simplification, preserves-definedness]
 
-    rule #asWord(#buf(N, BUF)) => BUF
-      requires #range(0 < N <= 32)
-       andBool #range(0 <= BUF < 2 ^Int (N *Int 8)) [simplification]
-
     rule notBool  (X ==Int 0) => X ==Int 1 requires #rangeBool(X) [simplification]
     rule notBool  (X ==Int 1) => X ==Int 0 requires #rangeBool(X) [simplification]
     rule bool2Word(X ==Int 1) => X         requires #rangeBool(X) [simplification]

package/version

@@ -1 +1 @@
-1.0.554
+1.0.555