feat: add --per-depth-timeout option for kontrol prove

[Stevengre]

Summary

Adds --per-depth-timeout SECONDS to kontrol prove. Each prove attempt runs in a forked subprocess with current_depth * per_depth_timeout seconds as a stall window: as long as the proof keeps writing to disk (any file under proofs_dir/<test.id> gets a new mtime), the window resets. When a full window passes with no writes, the whole session is SIGKILL'd, current_depth is halved (floor 1), and the next attempt resumes from the disk-persisted KCFG. Default 0 disables the wrapper.

Example: --max-depth 1000 --per-depth-timeout 0.5 → 500s window at depth 1000, halving to 250s @ 500, … 0.5s @ 1.

Why this shape

• Stall window, not total budget — progressive halving exists to detect when execute_depth is too coarse to break out of a stuck step. As long as new nodes appear, we leave the proof alone.
• Subprocess + session SIGKILL, not in-process callback — advance_proof's maintenance callback only fires after step_proof returns. A single long step (deep symbolic execution, expensive SMT) is uninterruptible from inside the prover. Killing the session is the only way to enforce wall-clock regardless of what the prover is doing.

Implementation

• cli.py / options.py: new --per-depth-timeout flag and ProveOptions.per_depth_timeout field (default 0).
• prove.py: when per_depth_timeout > 0, init_and_run_proof dispatches to _init_and_run_proof_progressive, which loops over halving depths via _run_attempt_under_timeout:
  • mp.get_context('fork').Process → child inherits everything via CoW; child os.setsid() so the parent's killpg reaps Python + KoreServer + worker threads.
  • Parent calls proc.join(timeout=budget_s) then compares max mtime under proofs_dir/<test.id> against the previous snapshot. Changed → another window. Unchanged → SIGKILL, halve, retry.

Test plan

• kontrol prove --help lists --per-depth-timeout with documented behavior.
• Default-off: kontrol prove --match-test TokenValueLibProofs.init --max-depth 100 (no --per-depth-timeout) passed in 28s; process tree showed a single python + one kore-rpc-booster (no fork), confirming the run_prover path is unchanged.
• Stall detection on a real stuck proof (vault-contracts-aave-v4 test_amountToValueDown, --per-depth-timeout 0.5 --max-depth 1000): observed 10 halvings 1000→1, KCFG advanced 1437 steps in the first attempt then stayed pinned at the deepest unresolvable node — proof stopped exactly where it should.
• No false positives on a productive proof (steady progress completes without being killed).
• Cleanup: after the 10-cycle halving run above, pgrep kore-rpc-booster returned 0 — session-group SIGKILL reaped every kore-rpc subprocess across all kill cycles.

Caveats

• POSIX-only (already a kontrol requirement).
• Each halving spawns a fresh KoreServer (a few seconds startup overhead per attempt).
• proof.write_proof_data() is assumed atomic (temp + rename); a SIGKILL mid-write would at worst lose one step.
• Kill latency ≤ one extra budget_s window beyond actual stall onset.

[ehildenb]

This seems like something we can probably build into Prover.advance_proof, and have a generic solution rather than duplicating a bunch of code here. At the very least, do we need a new _init_and_run_proof_progressive, or can it be integrated into the existing _init_and_run_proof?

[Stevengre]

@ehildenb Instead of providing this feature through a long dependency, I'd like to have a pr here to prove the concept and use it earlier.

1. inlined _init_and_run_proof_progressive into _init_and_run_proof.
2. introduce an issue in k repo Support progressive depth halving as a generic policy in Prover.advance_proof k#4924, and may provide this feature in k later.