kevm-pyk: thread step_timeout through run_prover (#2867)

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).

Co-authored-by: Everett Hildenbrandt <everett.hildenbrandt@gmail.com>

Author: Stevengre

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(