Additional constraints for simplifications of PR #2307 (#2311)

* non-negativity and concrete arguments for simplifications * Set Version: 1.0.462 --------- Co-authored-by: devops <[email protected]>
runtimeverification · Feb 22, 2024 · adfe3a0 · adfe3a0
1 parent f0a032b
commit adfe3a0
Show file tree

Hide file tree

Showing 4 changed files with 6 additions and 6 deletions.
diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml
@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kevm-pyk"
-version = "1.0.461"
+version = "1.0.462"
 description = ""
 authors = [
     "Runtime Verification, Inc. <[email protected]>",

diff --git a/kevm-pyk/src/kevm_pyk/__init__.py b/kevm-pyk/src/kevm_pyk/__init__.py
@@ -6,4 +6,4 @@
     from typing import Final
 
 
-VERSION: Final = '1.0.461'
+VERSION: Final = '1.0.462'
diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/bytes-simplification.k b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/bytes-simplification.k
@@ -62,13 +62,13 @@ module BYTES-SIMPLIFICATION [symbolic]
     rule [buf-asWord-invert-lr-len-leq]:
       #buf (W:Int , #asWord(B:Bytes)) => #buf(W -Int lengthBytes(B), 0) +Bytes B
       requires lengthBytes(B) <=Int W andBool W <=Int 32
-      [simplification]
+      [simplification, concrete(W)]
 
     rule [buf-asWord-invert-lr-len-gt]:
       #buf (W:Int , #asWord(B:Bytes)) => #range(B, lengthBytes(B) -Int W, W)
-      requires W <Int lengthBytes(B) andBool lengthBytes(B) <=Int 32
+      requires 0 <=Int W andBool W <Int lengthBytes(B) andBool lengthBytes(B) <=Int 32
        andBool #asWord(B) <Int 2 ^Int (8 *Int W)
-      [simplification]
+      [simplification, concrete(W)]
 
     rule [buf-asWord-invert-rl]:
       #asWord ( #buf ( WB:Int, X:Int ) ) => X

diff --git a/package/version b/package/version
@@ -1 +1 @@
-1.0.461
+1.0.462
Original file line number	Diff line number	Diff line change
Expand Up		@@ -6,4 +6,4 @@
		from typing import Final


		VERSION: Final = '1.0.461'
		VERSION: Final = '1.0.462'