# Verify a proof - How the reviewer of a claimed-mechanical chain (or a single commit) consumes its proof. - The certified property and primitive contracts: `spec-reproduction-utils.md`; the chain-level contract: `spec-reproduction-cli.md`. - How the proof was produced and the folder it arrives in: `guide-construct-proof.md`. ## 0. Do not trust the PR — verify yourself - Everything the PR shows you is a **claim**, not evidence: a pasted `PASS` verdict, a pasted chain report, a green checkmark, the classification words themselves. All of it is text the author (or the author's tooling) produced and could be wrong or fabricated. - The proof is only ever the run **you** perform locally: run the chain verifier (§1) against the PR's actual base and head, with the proof folder you downloaded — never approve from the author's pasted output. - This is cheap by design: the whole point of the machinery is that re-verification is one command, so there is no excuse to trust instead of re-run. - **Sampling is not verification.** Re-running a subset of the proofs ("spot-check 8 of 43") proves nothing about the rest and must never be the basis for approval — the only acceptable run is the §1 chain verifier, which executes **every** provable commit's proof. The same holds for the manual duties: audit every `HUMAN_REVIEW` row and every PASS's authored surfaces (§2.3), not a sample of them. ## 1. Verify the whole chain - The default — and the only sufficient — entry point: do not re-run proofs one by one, and never a sample; run the chain verifier over the whole chain: ```bash python3 .claude/skills/mechanical-refactor-verify/scripts/mechanical_refactor_reproduction_cli.py \ --base --branch --proof ``` - It checks every commit declares `mechanical_provable` or `non_mechanical_provable`, runs every provable commit's proof, and prints + writes a full report (`/chain_report.md`); exit 0 iff the chain verifies. - Proofs run up to `--jobs` at a time (default 3; each proof works in its own throwaway worktree, so this is safe) — raise it to shorten a long chain's wall clock. - Re-running a long chain: add `--skip-passed` to reuse **this machine's own** earlier PASS verdicts for unchanged proofs (keyed by sha + script hash + utils hash, stored under the repo's `.git/`, never shipped with the proof folder — so §0 still holds; contract: `spec-reproduction-cli.md` §3.5). - The contract (word rule, proof resolution, PASS criterion, exit codes): `spec-reproduction-cli.md`. - The `HUMAN_REVIEW` rows in the report are your remaining manual surface — the declared non-mechanical commits, plus the §2.3 authored-surface audit of each PASS. - Each `HUMAN_REVIEW` row carries **two** review duties, and the commit is not approved until both hold. - Duty 1 — **correctness-review the diff itself**: a `non_mechanical_provable` commit is exactly the part the machine never certifies, so read its diff and confirm it does exactly what its message claims — no lost logic (a branch, a write, an early return dropped on the floor), no hidden bug, no unintended behavior change riding along. When the commit claims to be behavior-preserving, that means checking equivalence; a commit that intentionally changes behavior (a chain need not be a pure refactor) is reviewed for the correctness of that change instead. Tests passing is supporting evidence, not the review. - Duty 2 — **verify the declaration itself**: the commit asserts **nothing in it is a provable relocation** (`spec-reproduction-cli.md` §2.1), and hiding provable content there to dodge the verifier is exactly the escape this chain check exists to close. - Read the commit's diff for relocated code. Concretely, run `git show --color-moved=dimmed-zebra --color-moved-ws=allow-indentation-change` and look for moved blocks, and run `python3 .claude/skills/mechanical-refactor-verify/scripts/mechanical_refactor_proof_generator.py ` to see what a relocation recipe would cover. - A hidden provable part is not a judgement call: demand the split (`guide-split.md` §2.2) — do not approve the commit as-is. - **A `non_mechanical_provable` commit whose body is a large verbatim block relocation the primitives can express** — a cut+paste move (including one landing above an `if TYPE_CHECKING:` guard, now anchorable with `move_symbol(after=)`), a module-level constant move, or a verbatim inline-block extract (the generator now infers it as `extract_function`) — is a **FINDING**, not an acceptable label. The generator being unable to infer it, or a past tooling gap, does not license the softer label: demand it be relabelled `mechanical_provable` with a hand-written `Repro`, or the primitive enhanced (guide-split.md §2.7.6). Only a genuine non-relocation edit (signature redesign, logic rewrite, de-self restructure) justifies the label. ## 2. Verify a single commit - For diagnosing one commit (a failing proof, a suspicious script) — never a substitute for §1: approving a chain requires the full §1 run, not single-commit re-runs of a chosen subset. ### 2.1 Re-run it - From the repo root: ```bash python3 /repro_scripts/.py ``` - When the proof arrived as a gist (`guide-construct-proof.md` §1.3), download it first: ```bash gh gist clone /tmp/proof # or: git clone https://gist.github.com/.git /tmp/proof cd # the run resolves the repo from the cwd python3 /tmp/proof/.py # PASS = byte-identical to this commit ``` - The run *is* the proof — it replays the primitives from the base commit and byte-diffs against the target in a throwaway worktree. - The script prints the verdict and exits 0 only on PASS (a residual exits non-zero), so a harness can consume the exit code. - Do not trust a pasted verdict you did not re-run. ### 2.2 Read the verdict - **PASS** — byte-identical: the commit is exactly the relocations listed in the script, nothing else. - **RESIDUAL** — a non-empty diff: precisely the bundled non-move change. Review it as semantic content; a legitimate tail fixup (string-literal module path, doc reference) belongs in a postpare commit, not the move. - **UNSUPPORTED** — no recipe inferred (cases: `guide-construct-proof.md` §2.2.2). Not thereby wrong, but not machine-certified: review by hand as a prepare-style reshape, or ask the author for a hand-written `Repro`. ### 2.3 Audit the authored surfaces - A PASS certifies the relocated bytes; the small **authored** surfaces are reproduced from the target and need human eyes. - In the script, check: - the `header=` of `extract_symbols_to_new_module` — the module audits its content (imports / docstring / TYPE_CHECKING imports / logger / relocated `drop_assigns` copies only); what remains for you: should those assignments move at all? - a `leave_delegate=` on `move_symbol` — the forwarding stub is authored code in the source file; - the `signature=` / `return_text=` / `call=` of `extract_function` — the new function's interface is authored; only its body is certified; - the `drop_assigns=` list — each named constant leaves the source file. ### 2.4 Know what a PASS does and does not assert - Requalification / lowering / repath in a script is tied to symbols the same script relocates; a consumer-only call or import rewrite (no relocated definition) cannot reproduce as a move — it surfaces as a residual. - Whatever the repo's pre-commit hooks auto-fix is absorbed on both sides (`spec-reproduction-utils.md` §4) — the hook set is part of what you trust. - A PASS judges the **shape of a relocation**, not **intent**: "this commit is exactly these relocations", not "this relocation was a good idea". Confirm the commit's subject matches what the script actually moves before approving. ### 2.5 Why the mechanism is trustworthy - It runs the real formatter and compares bytes — no diff-shape heuristic to fool (`spec-reproduction-utils.md` §4). - The proof is the few primitive calls in the script; auditing them (plus §2.3) is the whole human surface. - The folder is self-contained and re-runnable by anyone — a CI step or a reviewer — without the skill installed.