Bound the prover subprocesses, and kill the tree when one wedges

[shellygr]

What happened

A codegen run stopped making progress and sat in that state for three days, having consumed one second of CPU. The process tree:

PID	Process	Blocked in
1	console-codegen	epoll_wait — awaiting the subprocess
1545	certoraRunWrapper.py	pipe_read — reading the JVM's stderr
1570	java Typechecker.jar	futex, all 18 threads parked (GC and VM threads included)

The JVM's last log line was writing .certora_verify.json, and every file in the build directory shared one timestamp. Its stdout went to /dev/null, so this was not a pipe-buffer deadlock — the JVM itself had stopped.

Nothing could end it. All three create_subprocess_exec calls in composer/prover/core.py awaited their child with no bound, so a local phase that stops responding without exiting takes the run with it. The --global_timeout 7200 visible in the command line is the cloud prover's budget, passed through to certoraRun; it bounds nothing locally, and this process never reached the point of submitting a job.

The change

A _bounded_subprocess context manager wraps all three sites:

• the run path uses prover_opts.global_timeout + 5 * 60 — the same bound the result poller already uses at step 7
• the two build-and-typecheck helpers behind rule listing use a shorter fixed bound

On the run path a timeout returns an error string rather than raising, so the agent reads it as a tool result and can retry, instead of the pipeline stalling. The message says explicitly that this is infrastructure and not a problem with the spec — otherwise the author burns turns rewriting CVL that was fine.

The part that is easy to get wrong

Killing the direct child is not enough. certoraRun is a python front end that shells out to a JVM. Signal only the child and the JVM survives, still holding the pipe its parent was read-waiting on — so the caller hangs exactly as it did before. Children are therefore spawned as process-group leaders (process_group=0) and killed by group.

This is not theoretical: with the group kill removed, the helper hangs rather than failing, reproducing the original bug in a unit test.

Tests

tests/test_prover_subprocess_timeout.py — a hung child raises promptly, a grandchild standing in for the JVM is killed too, a healthy child is left alone, and the child genuinely leads its own process group.

Every test bounds itself with asyncio.timeout, because a regression here hangs instead of failing and a test guarding against a hang must not hang CI. Verified both ways:

	result
with the fix	4 passed
group kill removed	2 failed in 30s (not hung)

Full suite: 1045 passed, 49 skipped (test_rag_db.py deselected — it needs a Docker socket to spin up its own Postgres, unavailable when running inside the container).

fake_exec in tests/test_rules_striping.py gains **kwargs plus an assertion on the new argument, so the double keeps matching the real call signature rather than silently drifting from it.

Not in scope

The bound on the run path is deliberately generous — it is a backstop against a wedged process, not a budget, and a healthy cloud submit finishes in minutes. A tighter bound specifically for the cloud submit phase (which does not wait on the remote job at all) would catch this class of failure much sooner, but wants its own change.