From 39e969394322a8183945f106538757d2604a500e Mon Sep 17 00:00:00 2001 From: Stevengre Date: Tue, 26 May 2026 11:46:19 +0800 Subject: [PATCH] kevm-pyk: add per_depth_timeout to run_prover Adds a `per_depth_timeout: int = 0` parameter to `run_prover`. When set, each APRProof advance attempt is given a wall-clock budget of `current_depth * per_depth_timeout` seconds; on expiry, `execute_depth` is halved (floor 1) and the proof resumes from the disk-persisted KCFG state (the `advance_proof` maintenance loop calls `write_proof_data` before each callback, so on-disk state is always current). Repeats down to `depth = 1`. Default `0` keeps the prior behavior: one attempt at `max_depth`, no timeout. The timeout is enforced via a maintenance callback that raises an internal `_ProgressiveTimeout`; the unwind closes the `parallel_advance_proof` worker pool cleanly between attempts. Use case: progressive cut-point finding. A proof that stalls because `execute_depth` is too coarse to cut at the next branch can complete once the depth halves enough times. --- kevm-pyk/src/kevm_pyk/utils.py | 64 ++++++++++++++++++++++++---------- 1 file changed, 45 insertions(+), 19 deletions(-) diff --git a/kevm-pyk/src/kevm_pyk/utils.py b/kevm-pyk/src/kevm_pyk/utils.py index 80d13f453c..4f080937d9 100644 --- a/kevm-pyk/src/kevm_pyk/utils.py +++ b/kevm-pyk/src/kevm_pyk/utils.py @@ -1,6 +1,7 @@ from __future__ import annotations import logging +import time from contextlib import contextmanager from pathlib import Path from typing import TYPE_CHECKING @@ -47,6 +48,10 @@ _LOGGER: Final = logging.getLogger(__name__) +class _ProgressiveTimeout(Exception): + pass + + def claim_dependency_dict(claims: Iterable[KClaim], spec_module_name: str | None = None) -> dict[str, list[str]]: claims_by_label = {claim.label: claim for claim in claims} graph: dict[str, list[str]] = {} @@ -117,6 +122,7 @@ def run_prover( assume_defined: bool = False, extra_module: KFlatModule | None = None, optimize_kcfg: bool = False, + per_depth_timeout: int = 0, ) -> bool: prover: APRProver | ImpliesProver try: @@ -140,25 +146,45 @@ 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) - if force_sequential: - prover = create_prover() - prover.advance_proof( - proof=proof, - max_iterations=max_iterations, - fail_fast=fail_fast, - callback=update_status_bar, - maintenance_rate=maintenance_rate, - ) - else: - parallel_advance_proof( - proof=proof, - create_prover=create_prover, - max_iterations=max_iterations, - fail_fast=fail_fast, - max_workers=max_frontier_parallel, - callback=update_status_bar, - maintenance_rate=maintenance_rate, - ) + attempt_start = time.time() + budget_s: int | None = max_depth * per_depth_timeout if per_depth_timeout > 0 else None + + def maintenance_callback(_proof: Proof) -> None: + update_status_bar(_proof) + if budget_s is not None and time.time() - attempt_start > budget_s: + raise _ProgressiveTimeout() + + while True: + try: + if force_sequential: + prover = create_prover() + prover.advance_proof( + proof=proof, + max_iterations=max_iterations, + fail_fast=fail_fast, + callback=maintenance_callback, + maintenance_rate=maintenance_rate, + ) + else: + parallel_advance_proof( + proof=proof, + create_prover=create_prover, + max_iterations=max_iterations, + fail_fast=fail_fast, + max_workers=max_frontier_parallel, + callback=maintenance_callback, + maintenance_rate=maintenance_rate, + ) + break + except _ProgressiveTimeout: + _LOGGER.warning( + f'Proof {proof.id}: depth={max_depth} attempt exhausted {budget_s}s budget; halving.' + ) + if max_depth <= 1: + break + max_depth = max(1, max_depth // 2) + attempt_start = time.time() + budget_s = max_depth * per_depth_timeout elif type(proof) is EqualityProof: prover = ImpliesProver(proof, kcfg_explore=create_kcfg_explore(), assume_defined=assume_defined)