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;
• after a grace period (default 5 min) it probes the treeview at a bounded cadence (default 90s) via POU get_treeview_status;
• non-empty rules ⇒ dormant forever (zero further overhead);
• JobNotFoundError = "not served yet", not an error; 3 consecutive transport errors self-disable the watchdog, restoring the old behavior byte-for-byte;
• 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_GRACE_SECONDS (300), AUTOSETUP_PREPROCESSING_PROBE_SECONDS (90). No CLI-surface change, no new dependencies.

Testing

• tests/test_preprocessing_watchdog.py — 15 tests: state machine (queue-time free, grace, probe cadence, dormancy, empty-rules-is-still-preprocessing, not-found vs error, self-disable), 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