Partial evaluation of EVM optimization lemmas (#2566)

* kevm-pyk/tests/integration/test_prove: add cut-rule, longer proof runs, for optimizations * kevm-pyk/kproj/optimizations: partial evaluation of sizeWordStack expressions * Set Version: 1.0.673 * Set Version: 1.0.673 --------- Co-authored-by: devops <[email protected]> Co-authored-by: Petar Maksimović <[email protected]>
runtimeverification · Aug 7, 2024 · 16dac73 · 16dac73
1 parent 6e916f3
commit 16dac73
Show file tree

Hide file tree

Showing 5 changed files with 16 additions and 16 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.672"
+version = "1.0.673"
 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
@@ -5,4 +5,4 @@
 if TYPE_CHECKING:
     from typing import Final
 
-VERSION: Final = '1.0.672'
+VERSION: Final = '1.0.673'
diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/optimizations.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/optimizations.md
@@ -42,7 +42,7 @@ module EVM-OPTIMIZATIONS
       ...
     </kevm>
     requires ( #if USEGAS #then Gbase < SCHED > <=Gas GAVAIL #else true #fi )
-     andBool ( #sizeWordStack( 0 : WS ) <=Int 1024 )
+     andBool ( #sizeWordStack( WS ) <=Int 1023 )
      [priority(40)]
 
   rule
@@ -81,7 +81,7 @@ module EVM-OPTIMIZATIONS
       ...
     </kevm>
     requires ( #if USEGAS #then Gverylow < SCHED > <=Gas GAVAIL #else true #fi )
-     andBool ( #sizeWordStack( #asWord( #range(PGM, PCOUNT +Int 1, N) ) : WS ) <=Int 1024 )
+     andBool ( #sizeWordStack( WS ) <=Int 1023 )
      [priority(40)]
 
   rule
@@ -116,9 +116,9 @@ module EVM-OPTIMIZATIONS
       </ethereum>
       ...
     </kevm>
-    requires #stackNeeded(DUP(N)) <=Int #sizeWordStack(WS)
+    requires N <=Int #sizeWordStack(WS)
      andBool ( #if USEGAS #then Gverylow < SCHED > <=Gas GAVAIL #else true #fi )
-     andBool ( #sizeWordStack( WS [ ( N +Int -1 ) ] : WS ) <=Int 1024 )
+     andBool ( #sizeWordStack( WS ) <=Int 1023 )
      [priority(40)]
 
   rule
@@ -153,9 +153,9 @@ module EVM-OPTIMIZATIONS
       </ethereum>
       ...
     </kevm>
-    requires #stackNeeded(SWAP(N)) <=Int #sizeWordStack(W0 : WS)
+    requires N <=Int #sizeWordStack(WS)
      andBool ( #if USEGAS #then Gverylow < SCHED > <=Gas GAVAIL #else true #fi )
-     andBool ( #sizeWordStack( WS [ ( N +Int -1 ) ] : ( WS [ ( N +Int -1 ) := W0 ] ) ) <=Int 1024 )
+     andBool ( #sizeWordStack( WS ) <=Int 1023 )
      [priority(40)]
 
   rule
@@ -191,7 +191,7 @@ module EVM-OPTIMIZATIONS
       ...
     </kevm>
     requires ( #if USEGAS #then Gverylow < SCHED > <=Gas GAVAIL #else true #fi )
-     andBool ( #sizeWordStack( chop( ( W0 +Int W1 ) ) : WS ) <=Int 1024 )
+     andBool ( #sizeWordStack( WS ) <=Int 1023 )
      [priority(40)]
 
   rule
@@ -227,7 +227,7 @@ module EVM-OPTIMIZATIONS
       ...
     </kevm>
     requires ( #if USEGAS #then Gverylow < SCHED > <=Gas GAVAIL #else true #fi )
-     andBool ( #sizeWordStack( chop( ( W0 -Int W1 ) ) : WS ) <=Int 1024 )
+     andBool ( #sizeWordStack( WS ) <=Int 1023 )
      [priority(40)]
 
   rule
@@ -263,7 +263,7 @@ module EVM-OPTIMIZATIONS
       ...
     </kevm>
     requires ( #if USEGAS #then Gverylow < SCHED > <=Gas GAVAIL #else true #fi )
-     andBool ( #sizeWordStack( W0 &Int W1 : WS ) <=Int 1024 )
+     andBool ( #sizeWordStack( WS ) <=Int 1023 )
      [priority(40)]
 
   rule
@@ -299,7 +299,7 @@ module EVM-OPTIMIZATIONS
       ...
     </kevm>
     requires ( #if USEGAS #then Gverylow < SCHED > <=Gas GAVAIL #else true #fi )
-     andBool ( #sizeWordStack( bool2Word( W0 <Int W1 ) : WS ) <=Int 1024 )
+     andBool ( #sizeWordStack( WS ) <=Int 1023 )
      [priority(40)]
 
   rule
@@ -335,7 +335,7 @@ module EVM-OPTIMIZATIONS
       ...
     </kevm>
     requires ( #if USEGAS #then Gverylow < SCHED > <=Gas GAVAIL #else true #fi )
-     andBool ( #sizeWordStack( bool2Word( W1 <Int W0 ) : WS ) <=Int 1024 )
+     andBool ( #sizeWordStack( WS ) <=Int 1023 )
      [priority(40)]
 
 

diff --git a/kevm-pyk/src/tests/integration/test_prove.py b/kevm-pyk/src/tests/integration/test_prove.py
@@ -425,14 +425,14 @@ def _get_optimization_proofs() -> list[APRProof]:
             kcfg_explore,
             execute_depth=20,
             terminal_rules=[],
-            cut_point_rules=['EVM.pc.inc'],
+            cut_point_rules=['EVM.pc.inc', 'EVM.end-basic-block'],
             counterexample_info=False,
             always_check_subsumption=True,
             fast_check_subsumption=True,
         )
         for proof in _get_optimization_proofs():
             initialize_apr_proof(kcfg_explore.cterm_symbolic, proof)
-            prover.advance_proof(proof, max_iterations=10)
+            prover.advance_proof(proof, max_iterations=20)
             node_printer = kevm_node_printer(kevm, proof)
             proof_show = APRProofShow(kevm, node_printer=node_printer)
             proof_display = '\n'.join('    ' + line for line in proof_show.show(proof))

diff --git a/package/version b/package/version
@@ -1 +1 @@
-1.0.672
+1.0.673