From ca4b1334a1906e019eba8ff856c44aa69e494b3f Mon Sep 17 00:00:00 2001 From: Stevengre Date: Wed, 19 Mar 2025 16:50:54 +0000 Subject: [PATCH 1/2] Support gas cost summarization for all supported opcode. - Updated the handling of `GAS_CELL` to ensure it uses infinite gas for SLOAD and SSTORE operations. - Adjusted the initialization of `STATIC_CELL` for the `SSTORE` opcode to improve clarity. - Increased the `max_iterations` parameter in the summarization process to 300 to simplify the analysis of error cases. - Simplified the `#accessStorage` rule in the EVM semantics to avoid unexpected (nd)branches during gas consumption summarization. --- kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md | 10 +++------- kevm-pyk/src/kevm_pyk/summarizer.py | 8 +++++--- 2 files changed, 8 insertions(+), 10 deletions(-) diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md index 6c46c79dc9..6572057604 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md @@ -1597,16 +1597,11 @@ The various `CALL*` (and other inter-contract control flow) operations will be d syntax KItem ::= "#accessStorage" Account Int // --------------------------------------------- rule #accessStorage ACCT INDEX => .K ... - ... ACCT |-> (TS:Set => TS |Set SetItem(INDEX)) ... + TS => TS[ACCT <- {TS[ACCT] orDefault .Set}:>Set |Set SetItem(INDEX)] SCHED requires Ghasaccesslist << SCHED >> [preserves-definedness] - rule #accessStorage ACCT INDEX => .K ... - TS => TS[ACCT <- SetItem(INDEX)] - SCHED - requires Ghasaccesslist << SCHED >> andBool notBool ACCT in_keys(TS) - rule #accessStorage _ _ => .K ... SCHED requires notBool Ghasaccesslist << SCHED >> @@ -2310,7 +2305,8 @@ Access List Gas SCHED requires Ghasaccesslist << SCHED >> andBool #usesAccessList(OP) - rule #access [ _ , _ ] => .K ... _ [owise] + rule #access [ OP , _ ] => .K ... SCHED + requires notBool (Ghasaccesslist << SCHED >> andBool #usesAccessList(OP)) syntax InternalOp ::= #gasAccess ( Schedule, OpCode ) [symbol(#gasAccess)] // -------------------------------------------------------------------------- diff --git a/kevm-pyk/src/kevm_pyk/summarizer.py b/kevm-pyk/src/kevm_pyk/summarizer.py index bbf3e25dfc..9532cb7636 100644 --- a/kevm-pyk/src/kevm_pyk/summarizer.py +++ b/kevm-pyk/src/kevm_pyk/summarizer.py @@ -433,8 +433,7 @@ def _build_spec( # This is because #push doesn't handle `.Account`. And it's okay to be Int for other opcodes. _init_subst['CALLER_CELL'] = KVariable('CALLER_CELL', KSort('Int')) # CALLER_CELL should be Int for CALLER. _init_subst['ORIGIN_CELL'] = KVariable('ORIGIN_CELL', KSort('Int')) # ORIGIN_CELL should be Int for ORIGIN. - inf_gas_cell = KEVM.inf_gas(KVariable('GAS_CELL', KSort('Gas'))) - _init_subst['GAS_CELL'] = inf_gas_cell # inf_gas to reduce the computation cost. + _init_subst['GAS_CELL'] = KEVM.inf_gas(KVariable('GAS_CELL', 'Gas')) # SLOAD & SSTORE must use infinite gas. _init_subst.update(init_map) init_subst = CSubst(Subst(_init_subst), init_constraints) @@ -466,6 +465,9 @@ def _le(a: KInner, b: KInner) -> KInner: specs: list[tuple[KApply, dict[str, KInner], list[KInner], dict[str, KInner], list[KInner], str]] = [] init_subst: dict[str, KInner] = {} final_subst: dict[str, KInner] = {} + + if opcode_symbol == 'SSTORE': + init_subst['STATIC_CELL'] = KToken('false', KSort('Bool')) if opcode_symbol in NOT_USEGAS_OPCODES: # TODO: Should allow infGas to calculate gas. Skip for now. @@ -572,7 +574,7 @@ def create_kcfg_explore() -> KCFGExplore: proof, create_kcfg_explore=create_kcfg_explore, max_depth=1, - max_iterations=None, + max_iterations=300, cut_point_rules=KEVMSemantics.cut_point_rules( break_on_jumpi=False, break_on_jump=False, From c267123acddb2829d410d63255975b3cd0a43dab Mon Sep 17 00:00:00 2001 From: Stevengre Date: Fri, 21 Mar 2025 10:15:47 +0000 Subject: [PATCH 2/2] make format --- kevm-pyk/src/kevm_pyk/summarizer.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kevm-pyk/src/kevm_pyk/summarizer.py b/kevm-pyk/src/kevm_pyk/summarizer.py index 9532cb7636..5f35f7c8d1 100644 --- a/kevm-pyk/src/kevm_pyk/summarizer.py +++ b/kevm-pyk/src/kevm_pyk/summarizer.py @@ -465,7 +465,7 @@ def _le(a: KInner, b: KInner) -> KInner: specs: list[tuple[KApply, dict[str, KInner], list[KInner], dict[str, KInner], list[KInner], str]] = [] init_subst: dict[str, KInner] = {} final_subst: dict[str, KInner] = {} - + if opcode_symbol == 'SSTORE': init_subst['STATIC_CELL'] = KToken('false', KSort('Bool'))