Thread through option to add modules to prover context (#2654)

* kevm-pyk/utils: thread through option `extra_module` to run_prover

* kevm-pyk/utils: add import of KFlatModule

---------

Co-authored-by: Andrei Văcaru <16517508+anvacaru@users.noreply.github.com>

Author: ehildenb

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
@@ -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: