From 2fe7317f478dae099e2a811c9d862481d335ce9b Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Tue, 12 Nov 2024 06:01:47 +0000 Subject: [PATCH 1/2] kevm-pyk/utils: thread through option `extra_module` to run_prover --- kevm-pyk/src/kevm_pyk/utils.py | 2 ++ 1 file changed, 2 insertions(+) diff --git a/kevm-pyk/src/kevm_pyk/utils.py b/kevm-pyk/src/kevm_pyk/utils.py index 4aeebc356a..4e476ff8a7 100644 --- a/kevm-pyk/src/kevm_pyk/utils.py +++ b/kevm-pyk/src/kevm_pyk/utils.py @@ -114,6 +114,7 @@ def run_prover( task_id: TaskID | None = None, maintenance_rate: int = 1, assume_defined: bool = False, + extra_module: KFlatModule | None = None, ) -> bool: prover: APRProver | ImpliesProver try: @@ -129,6 +130,7 @@ def create_prover() -> APRProver: fast_check_subsumption=fast_check_subsumption, direct_subproof_rules=direct_subproof_rules, assume_defined=assume_defined, + extra_module=extra_module, ) def update_status_bar(_proof: Proof) -> None: From 6555fc746a16a58e2c7449f08a5f3f427b7a7ca8 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Tue, 26 Nov 2024 10:17:38 +0000 Subject: [PATCH 2/2] kevm-pyk/utils: add import of KFlatModule --- kevm-pyk/src/kevm_pyk/utils.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kevm-pyk/src/kevm_pyk/utils.py b/kevm-pyk/src/kevm_pyk/utils.py index 4e476ff8a7..26bcf540b4 100644 --- a/kevm-pyk/src/kevm_pyk/utils.py +++ b/kevm-pyk/src/kevm_pyk/utils.py @@ -30,7 +30,7 @@ from collections.abc import Callable, Collection, Iterable, Iterator from typing import Final, TypeVar - from pyk.kast.outer import KClaim, KDefinition + from pyk.kast.outer import KClaim, KDefinition, KFlatModule from pyk.kcfg import KCFG from pyk.kcfg.semantics import KCFGSemantics from pyk.kore.rpc import FallbackReason