From 4b7fef4f26d3290d0d17be5eb83aa5a34688ec2f Mon Sep 17 00:00:00 2001 From: Stevengre Date: Thu, 18 Jun 2026 22:22:45 +0800 Subject: [PATCH] kevm-pyk: thread step_timeout through run_prover Adds a `step_timeout: int | None = None` parameter to `run_prover` and forwards it to the `APRProver` constructor, which enforces the per-step wall-clock budget (interrupt + halve `execute_depth` + retry). `step_timeout` is only honored on the sequential `advance_proof` path; `parallel_advance_proof` does not wrap steps with the timeout budget. So when `step_timeout` is set, `run_prover` runs sequentially regardless of `force_sequential`, warning if `max_frontier_parallel > 1` that frontier parallelism is being dropped. Default `None` keeps the prior behavior (no per-step timeout, parallel path unchanged). --- kevm-pyk/src/kevm_pyk/utils.py | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/kevm-pyk/src/kevm_pyk/utils.py b/kevm-pyk/src/kevm_pyk/utils.py index d7dbfe65c5..39ea0f0cfd 100644 --- a/kevm-pyk/src/kevm_pyk/utils.py +++ b/kevm-pyk/src/kevm_pyk/utils.py @@ -117,6 +117,7 @@ def run_prover( assume_defined: bool = False, extra_module: KFlatModule | None = None, optimize_kcfg: bool = False, + step_timeout: int | None = None, ) -> bool: prover: APRProver | ImpliesProver try: @@ -134,12 +135,23 @@ def create_prover() -> APRProver: assume_defined=assume_defined, extra_module=extra_module, optimize_kcfg=optimize_kcfg, + step_timeout=step_timeout, ) def update_status_bar(_proof: Proof) -> None: if progress is not None and task_id is not None: progress.update(task_id, summary=_proof.one_line_summary) + # step_timeout is only enforced on the sequential `advance_proof` path; + # `parallel_advance_proof` does not wrap steps with the timeout budget. + if step_timeout is not None and not force_sequential: + if max_frontier_parallel > 1: + _LOGGER.warning( + f'Proof {proof.id}: step_timeout is only enforced when running sequentially; ' + f'ignoring max_frontier_parallel={max_frontier_parallel} and running sequentially.' + ) + force_sequential = True + if force_sequential: prover = create_prover() prover.advance_proof(