Additional lemmas for Kontrol (#2288)

* adding lemmas needed for Kontrol, removing superfluous requires

* Set Version: 1.0.448

* Update tests/specs/functional/lemmas-spec.k

Co-authored-by: Everett Hildenbrandt <everett.hildenbrandt@gmail.com>

* Set Version: 1.0.449

---------

Co-authored-by: devops <devops@runtimeverification.com>
Co-authored-by: Everett Hildenbrandt <everett.hildenbrandt@gmail.com>

kevm-pyk/pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kevm-pyk"
-version = "1.0.448"
+version = "1.0.449"
 description = ""
 authors = [
     "Runtime Verification, Inc. <contact@runtimeverification.com>",

kevm-pyk/src/kevm_pyk/__init__.py

@@ -6,4 +6,4 @@
     from typing import Final
 
 
-VERSION: Final = '1.0.448'
+VERSION: Final = '1.0.449'

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

@@ -293,6 +293,12 @@ module BYTES-SIMPLIFICATION [symbolic]
 
     rule #padToWidth(32, #asByteStack(V)) => #buf(32, V)  requires #rangeUInt(256, V) [simplification]
 
+    // #padRightToWidth
+
+    rule #padRightToWidth ( X:Int, B:Bytes ) => B +Bytes padRightBytes(.Bytes, X -Int lengthBytes(B), 0 )
+      requires lengthBytes(B) <=Int X
+      [simplification, concrete(X)]
+
     // #ecrec
 
     rule lengthBytes ( #ecrec ( _ , _ , _ , _ ) ) <=Int 32 => true

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

@@ -66,7 +66,6 @@ module EVM-INT-SIMPLIFICATION-COMMON
     #asWord ( #range ( _:Bytes, S, W ) ) <Int X => true
     requires 0 <=Int S andBool 0 <=Int W
      andBool 2 ^Int ( 8 *Int W ) <=Int X
-     andBool X ==Int 2 ^Int log2Int( X )
     [simplification, concrete(S, W, X)]
 
   rule [lt-asWord-range]:

package/version

@@ -1 +1 @@
-1.0.448
+1.0.449

tests/specs/functional/lemmas-spec.k

@@ -602,6 +602,18 @@ module LEMMAS-SPEC
         => doneLemma ( X ) ... </k>
         requires #rangeUInt ( 256 , X )
 
+ // #padRightToWidth
+ // ----------------
+
+    claim [pRTW-01]:
+      <k> runLemma (
+            notBool ( #asWord ( #padRightToWidth ( 32 , #buf ( 4 , VV0_x_114b9705:Int ) ) ) ==Int
+              #asWord ( #buf ( 4 , VV0_x_114b9705:Int ) +Bytes b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" ) )
+          ) => doneLemma(
+            false
+          ) ... </k>
+        requires #rangeUInt(32, VV0_x_114b9705)
+
  // ecrecover
  // ---------