feat: add --per-depth-timeout option for progressive depth-halving prove

[Stevengre]

Summary

Adds a new --per-depth-timeout SECONDS option to kontrol prove. When set, each prove attempt gets a wall-clock budget of max_depth * per_depth_timeout seconds; on timeout, max_depth is halved and the proof resumes from disk-persisted KCFG state, repeating down to depth = 1. Default 0 disables the behavior — existing runs are unaffected.

Example: --max-depth 1000 --per-depth-timeout 10 runs 1000 @ 10000s → 500 @ 5000s → ... → 1 @ 10s.

Why

A proof can get stuck when execute_depth is too coarse to cut at the next branch / 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, since the saved KCFG carries over between attempts.

Implementation

• New --per-depth-timeout flag in cli.py and ProveOptions.per_depth_timeout (default 0).
• init_and_run_proof is restructured so each prove attempt opens its own with select_server(). Server-independent prep (cut_point_rules, lemmas_module, terminal_rules) is computed once outside any server; first-time method_to_apr_proof uses a short-lived initial server.
• A nested attempt(depth, callback) mirrors run_prover's sequential / parallel dispatch but lets us inject our own callback. The progressive path installs a timed_callback that raises _ProgressiveTimeout once time.time() - attempt_start > budget_s.
• Because advance_proof / parallel_advance_proof invoke the callback immediately after proof.write_proof_data(), on-disk state is current at the moment of abort. The unwind closes parallel_advance_proof's _ProverPool (terminates worker threads) and the with select_server() (terminates the KoreServer subprocess), so each halving starts from a clean slate.
• The run_prover import from kevm-pyk is dropped; the local dispatch is the sole path for both progressive and non-progressive runs.

Test plan

• kontrol prove --help lists --per-depth-timeout with documented behavior.
• Default-off: an existing proof finishes with the same status as before (smoke against an existing test suite).
• Progressive enabled on a contrived slow proof: logs show Proof <id>: depth=N attempt exhausted Ms budget; halving. lines and the depth halves monotonically.
• No orphan processes between attempts: pgrep kore-rpc count returns to baseline between halvings under both --workers 1 and --workers >1 (with parallel_advance_proof).
• Resumption: after a forced timeout, the next attempt's KCFG starts from where the previous one left off (no full restart).

Follow-up

• Upstream a callback parameter to kevm-pyk's run_prover so we can drop the mirrored dispatch in attempt() and call run_prover directly again.
• The timeout fires at maintenance-callback boundaries (after one committed step), so a single very long step can overshoot the budget by up to one step. If this becomes problematic, escalate to subprocess-and-kill enforcement.

🤖 Generated with Claude Code