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.

```bash
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.

```bash
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)

- [x] verify_certs.py (re-verify guard)
- [x] 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.