From 16dac735654df9593291de4bd0bceb729ebdeb02 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Wed, 7 Aug 2024 13:41:15 -0600 Subject: [PATCH] Partial evaluation of EVM optimization lemmas (#2566) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit * 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 Co-authored-by: Petar Maksimović --- kevm-pyk/pyproject.toml | 2 +- kevm-pyk/src/kevm_pyk/__init__.py | 2 +- .../kproj/evm-semantics/optimizations.md | 22 +++++++++---------- kevm-pyk/src/tests/integration/test_prove.py | 4 ++-- package/version | 2 +- 5 files changed, 16 insertions(+), 16 deletions(-) diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml index 53fd50bb00..69d267e2e7 100644 --- 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. ", diff --git a/kevm-pyk/src/kevm_pyk/__init__.py b/kevm-pyk/src/kevm_pyk/__init__.py index 96797d7217..df83a670b7 100644 --- 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 index 964d994d57..4882178349 100644 --- 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 ... 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 ... 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 ... - 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 ... - 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 ... 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 ... 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 ... 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 ... requires ( #if USEGAS #then Gverylow < SCHED > <=Gas GAVAIL #else true #fi ) - andBool ( #sizeWordStack( bool2Word( W0 requires ( #if USEGAS #then Gverylow < SCHED > <=Gas GAVAIL #else true #fi ) - andBool ( #sizeWordStack( bool2Word( W1 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 index 268959c7a6..d2c75b65da 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -1.0.672 +1.0.673