release_tools/README.md

release_tools — flagship release / verification kit (owner: leaner)

Guardrails for the run-up to freeze (~08-25). Both tools are self-contained (only the judge repo + Python stdlib — no cebench, no pysat) so any collaborator can run them.

verify_certs.py — re-verify a bundle before posting

One bad certificate invalidates a whole result on the eval space. Run this on any certs.json or eq2 manifest.json before posting — it re-runs every claimed certificate through the official judge exactly as the eval space will.

source <repo>/.env.judge
python3 verify_certs.py <repo> <bundle.json> [--jobs N] [--ids a,b,c]

• Accepts a certs map {"id": {"verdict","code"}} or a manifest with results:[{id,verdict,code,solved}] (auto-detected; only solved rows checked).
• Prints [PASS]/[FAIL] per problem (FAIL shows the judge error), a summary, and exits 1 if anything is rejected — so it gates a post / CI step.
• --jobs N verifies in parallel (independent Lean processes).

Replaces the merge_shards.py spot-check with a full re-verify.

diff_solved.py — regression diff between flagship versions

Catches the silent-drop failure mode (a refactor or orchestrator cap starving a stage). Run on every new flagship version before it becomes the submission.

python3 diff_solved.py <old.json> <new.json>

• Each input is a coverage file (solved_ids:[...]) or a manifest (results:[{id,solved}]).
• Prints per-tier old/new/gained/lost + net delta.
• Exits 1 if any id regressed (solved by old, not by new) — gates a release.

Roadmap (this kit)

• verify_certs.py (re-verify guard)
• diff_solved.py (regression diff)
• order-5 OOD FALSE risk table + static structural-hints JSON (constancy + top-k h-instantiations for the open hard2/hard3 trues) — in progress.