diff --git a/kevm-pyk/src/kevm_pyk/summarizer.py b/kevm-pyk/src/kevm_pyk/summarizer.py index 3240a4e4c7..468827a749 100644 --- a/kevm-pyk/src/kevm_pyk/summarizer.py +++ b/kevm-pyk/src/kevm_pyk/summarizer.py @@ -2,10 +2,10 @@ import logging import time -from pathlib import Path +from typing import TYPE_CHECKING from pyk.cterm import CSubst, CTerm, CTermSymbolic, cterm_build_claim -from pyk.kast.inner import KApply, KSequence, KVariable, Subst +from pyk.kast.inner import KApply, KInner, KSequence, KVariable, Subst from pyk.kast.outer import KSort from pyk.kcfg import KCFGExplore from pyk.kdist import kdist @@ -16,6 +16,9 @@ from kevm_pyk.kevm import KEVM, KEVMSemantics, kevm_node_printer from kevm_pyk.utils import initialize_apr_proof, legacy_explore, run_prover +if TYPE_CHECKING: + from pathlib import Path + _LOGGER = logging.getLogger(__name__) @@ -50,12 +53,12 @@ def build_spec( # construct the initial substitution opcode = KVariable('OP_CODE', KSort('OpCode')) next_opcode = KApply('#next[_]_EVM_InternalOp_MaybeOpCode', opcode) - _init_subst = {'K_CELL': KSequence([next_opcode, KVariable('K_CELL')])} + _init_subst: dict[str, KInner] = {'K_CELL': KSequence([next_opcode, KVariable('K_CELL')])} _init_subst['PROGRAM_CELL'] = self.kevm.bytes_empty() init_subst = CSubst(Subst(_init_subst), ()) - + # construct the final substitution - _final_subst = {vname: KVariable('FINAL_' + vname) for vname in cterm.free_vars} + _final_subst: dict[str, KInner] = {vname: KVariable('FINAL_' + vname) for vname in cterm.free_vars} _final_subst['K_CELL'] = KVariable('K_CELL') _final_subst['PROGRAM_CELL'] = self.kevm.bytes_empty() final_subst = CSubst(Subst(_final_subst), ()) @@ -135,7 +138,7 @@ def create_kcfg_explore() -> KCFGExplore: max_frontier_parallel=8, force_sequential=False, assume_defined=False, - optimize_kcfg=True, + optimize_kcfg=False, ) end_time = time.time() print(f'Proof timing {proof.id}: {end_time - start_time}s')