autosetup: preprocessing watchdog — cancel cloud jobs stuck in prover preprocessing

[shellygr]

Problem

A cloud job whose prover-side preprocessing (scene construction, storage/pointer analyses, CVL typechecking) blows up never produces rule results: it sits in RUNNING until the prover's global timeout (~2h). Autosetup's wait loop only polls the coarse job status, so it cannot distinguish this from a healthy long run and burns its entire 150-minute per-job budget — per job, several times per contract.

Approach

The prover's treeViewStatus.json carries an empty rules list for the whole preprocessing phase; rules appear in it only once rule checking begins (verified against a live production job — note that the file itself is served early, so mere existence is not the signal). The new PreprocessingWatchdog (certora_autosetup/utils/preprocessing_watchdog.py) piggy-backs on the existing 10s status poll:

• queue time never starts the clock; the first RUNNING observation does;
• it probes the treeview via POU get_treeview_status at a bounded cadence (default 90s), the first probe one interval into RUNNING (a job that just started running is still fetching the jar and booting the JVM);
• non-empty rules ⇒ dormant forever (zero further overhead);
• JobNotFoundError = "not served yet", not an error — verified live: the endpoint presigns the S3 object without an existence check and a missing object answers 404; 3 consecutive transport errors self-disable the watchdog, restoring the old behavior byte-for-byte, and any answered probe resets that count;
• budget exceeded (default 30 min of RUNNING with no rules) ⇒ cancel the job, return PREPROCESSING_TIMEOUT.

The result is classified as a new distinct JobStatus.PREPROCESSING_TIMEOUT:

• on_job_problem skips conf workarounds for it (a preprocessing stall is not conf-fixable), so no identical job is resubmitted; the submission-cache entry is dropped so a deliberate future run submits fresh;
• sanity_summary.md gets a dedicated row instead of crashing on the missing job report of a cancelled job (the get_job_report call is now also generally hardened).

Env knobs: AUTOSETUP_PREPROCESSING_BUDGET_SECONDS (default 1800; 0 disables), AUTOSETUP_PREPROCESSING_PROBE_SECONDS (90). No CLI-surface change, no new dependencies.

Testing

• tests/test_preprocessing_watchdog.py — 16 tests: state machine (queue-time free, first probe one interval in, probe cadence, dormancy, empty-rules-is-still-preprocessing, not-found vs error, self-disable only on consecutive errors, answered probe resets the count), wait-loop integration with mocked POU (stuck ⇒ cancel+classify; rules appear ⇒ never cancelled; zero-budget ⇒ watchdog off), retry suppression, serialization round-trip, reporter rows.
• Live end-to-end: driver ran the real wait loop against a production job stuck in preprocessing — watchdog fired ~5.5 min after the budget window opened, the job shows CANCELED on the cloud, and PREPROCESSING_TIMEOUT was returned (vs ~90 min of doomed polling before).
• pyright: 0 errors on all changed files.

🤖 Generated with Claude Code

[shellygr]

to Claude: why do we need grace seconds? what if preprocessing is super quick? we're introducing a 5 minute delay with this

[shellygr]

Claude answers: You're right that the knob shouldn't exist — removed it. But the reasoning is worth stating, because "5 minute delay" isn't quite what it was doing.

It delayed nothing. The grace only suppressed treeview probes. The job, the 10s status poll, and the returned result were untouched, and nothing downstream consumes PREPROCESSING_DONE — it just makes the watchdog dormant. If preprocessing was super quick, the job finished on its normal schedule and the watchdog never mattered. If anything, removing the grace makes stuck-job cancellation slightly later, not sooner: the budget check only fires on a probe tick, so with grace=300/interval=90 the first cancel-eligible probe was at 1830s, and at a bare 0+90k grid it is 1890s.

What it actually bought was probe-saving. Measured over 702 real cloud jobs in our fleet logs, p50 whole-job RUNNING time is 124s and ~70% finish under 300s, so most jobs never issued a single probe. Per-contract fastest successful run (an upper bound on that contract's preprocessing) is p50 39s, p95 282s.

But that doesn't justify a second time knob, and it had a real footgun: grace and budget were independently env-tunable with no ordering check, so AUTOSETUP_PREPROCESSING_BUDGET_SECONDS=120 (the obvious way to test the watchdog) would have silently disabled it. So the grace period, the class constant and AUTOSETUP_PREPROCESSING_GRACE_SECONDS are gone. Instead the last-probe timestamp is seeded when the clock starts, which puts the first probe one probe_interval (90s) into RUNNING — the existing knob expressing the same "a job that just entered RUNNING is still pulling the jar and booting the JVM" fact, with no way to misconfigure it into a no-op.

Two things that came out of digging into this:

1. Fixed a real bug the grace was masking. _consecutive_probe_errors was only reset in the JobNotFoundError branch, never after a probe that succeeded with rules: []. So "consecutive" was a lie — three unrelated blips over a long run would permanently self-disable the watchdog. It now resets after any probe the endpoint answers. Probing earlier makes more probes per job, so this had to be fixed alongside. New regression test test_answered_probe_resets_the_error_count; I confirmed it fails against the previous logic.

2. Verified the one thing that could have made early probing unsafe. Only HTTP 404 maps to the benign JobNotFoundError; anything else counts as a strike. The tree-view endpoint presigns the S3 object without an existence check (data-processors controllers.py:799-810), so a not-yet-uploaded treeViewStatus.json returns whatever S3 says — and S3 answers 403 rather than 404 when the signer lacks s3:ListBucket. I tested it live against a job that resolves fine (real treeview → 200) and requested a bogus path on the same job: 404 → JobNotFoundError. Benign, so no special handling needed.

16 tests pass, pyright clean. Note the branch is 40 commits behind master — say the word and I'll rebase before merge.