kevm-pyk: add per_depth_timeout to run_prover for progressive depth halving

[Stevengre]

Summary

Adds a new 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. If the budget is exhausted, execute_depth is halved (floor 1) and the proof resumes from the disk-persisted KCFG state, repeating down to depth = 1. Default 0 keeps the prior behavior — a single attempt at max_depth, no timeout.

Example: run_prover(proof, ..., max_depth=1000, per_depth_timeout=10) runs 1000 @ 10000s → 500 @ 5000s → ... → 1 @ 10s.

Why

A proof can stall when execute_depth is too coarse to cut at the next branch or terminal point. Halving the depth makes each step shorter and more interruptible, giving the prover more chances to find branch points without changing proof semantics — the saved KCFG carries over between attempts.

Downstream tools (kontrol, kasmer, kmir, etc.) all wrap run_prover; centralizing the policy here means every caller gets it via one option.

Implementation

• New per_depth_timeout keyword argument (default 0, off — fully backward-compatible).
• The APRProof branch is wrapped in a while True: retry loop. Each iteration:
  • Computes budget_s = current_depth * per_depth_timeout (or None when disabled).
  • Defines maintenance_callback(_proof, _start, _budget) (defaults bound to avoid late-binding) which calls the existing status-bar update and raises _ProgressiveTimeout when wall-clock exceeds _budget. With _budget = None the callback is a no-op beyond the status update — single-attempt semantics for per_depth_timeout=0.
  • Builds APRProver / parallel_advance_proof with that callback. advance_proof and parallel_advance_proof both invoke the callback after proof.write_proof_data(), so on-disk KCFG state is always current when the callback fires.
  • On _ProgressiveTimeout: logs the halving (depth=N attempt exhausted Ms budget; halving.), halves current_depth (floor 1), continues. On depth=1 timeout we break out.
  • On any other exception: propagates to the outer try/except Exception and stored in proof.error_info as before.
• The unwind on timeout exits parallel_advance_proof cleanly: its internal with _ProverPool(...) runs shutdown(wait=True) so worker threads drain, no orphan workers.
• EqualityProof path is unchanged (no max_depth notion there).

Test plan

• make check clean (flake8, mypy, autoflake, isort, black).
• make test-unit — 21/21 pass.
• Downstream smoke: kontrol with per_depth_timeout=0 (default) must produce identical results to today.
• Downstream behavior: kontrol with --per-depth-timeout 10 on a contrived stalling proof exhibits halving logs and eventual completion at a smaller depth.

Downstream

A kontrol PR (runtimeverification/kontrol#1141) consumes this parameter to add a --per-depth-timeout CLI option to kontrol prove. That PR currently inlines a copy of the retry logic; once this lands and kontrol bumps deps/kevm_release, the inlined logic will be replaced by a single kwarg passed to run_prover.

[Stevengre]

Superseded by kontrol#1141, which switched to a subprocess + SIGKILL design at the kontrol layer. The callback-based maintenance hook here only fires at iteration boundaries, so a single long-running step could overshoot the per-attempt budget arbitrarily — the kontrol use case requires a hard wall-clock cutoff. The hard-kill design lives entirely in kontrol; no upstream changes needed.