hjsang/crisp_reasoning_compression/mechanical-refactor-verify

Mechanical Refactor — Machine-Checkable Verification

1. Overview

• The correctness of a mechanical change (file split, function move, module extraction,

rename) must be machine-checkable, not eyeballed — the proof is something anyone can re-run, whoever made the change and whenever.

• One property: a commit is a pure relocation. One proof: reproduce —

regenerate the move from the base commit with faithful primitives, run the formatter, byte-diff against the target.

• Empty diff = the proof. Any residual = a bundled non-move change, surfaced for review.
• A reshape must not ride along: split into optional prepare + certified move +

optional postpare (guide-split.md).

2. Commands — what do you want to do?

The skill takes an argument naming one of three commands; invoked without one, pick the row matching your task.

• `split <base>..<tip>` — author a compliant refactor branch: split it into commits,

satisfy the contract (extract, move, file split) → guide-split.md: §1 splits the PR into classified pieces (the chain contract: classification format, correct labeling, proofs PASS, non-mechanical commits correctness-reviewed); §2 splits one piece into prepare + move + postpare (the case recipes and the anti-patterns). The argument is the chain to author (or a single commit / a description of the change to split).

• `construct <base>..<tip> [--match REGEX] [--out DIR]` — construct the proof, for

the chain or one commit → guide-construct-proof.md: §1 generates + publishes the whole chain's proof folder (the flags are the generator's: scripts/mechanical_refactor_proof_generator.py <base>..<tip> --match REGEX --out DIR); §2 proves a single commit — pass just <commit> (the generator, or a hand-written Repro when it reports UNSUPPORTED).

• `verify --base <base> --branch <branch> --proof <folder> [--jobs N] [--skip-passed]`

— verify someone's proof: a whole chain / PR branch → guide-verify-proof.md: run the chain verifier with exactly these flags (scripts/mechanical_refactor_reproduction_cli.py) — it checks every commit declares mechanical_provable or non_mechanical_provable, runs every provable commit's proof (never a sample), and writes one full report; then audit the authored surfaces and the HUMAN_REVIEW rows. Re-running one commit's script is for diagnosis only.

• Decide whether a change counts as a clean move → spec-reproduction-utils.md: the

property, the whole whitelist / not-allowed list, and each primitive's contract. The source of truth for the reproduction module; if any other file disagrees, it wins.

• Change this skill itself (edit the engine, the generator, or the spec) →

guide-modify-skill.md: the spec-leads rule, the faithfulness invariant, and the testing bar a change must clear before it is trusted.

3. Files

• `guide-split.md` — split the PR into classified pieces (§1, the

chain contract) and each piece into prepare + move + postpare (§2: case recipes, what stays mechanical, anti-patterns).

• `guide-construct-proof.md` — produce the proof: the whole

chain's proof folder + publishing (§1), and a single commit's proof — generator or hand-written Repro (§2).

• `guide-verify-proof.md` — consume the proof: the whole-chain

verifier, single-commit re-runs, verdicts, and the audit checklist for authored surfaces.

• `spec-reproduction-utils.md` — the normative spec of the

clean-move property and the reproduction primitives.

• `spec-reproduction-cli.md` — the normative spec of the

verified-chain property: the classification word rule, the proof obligation, the report, and the exit codes.

• `guide-modify-skill.md` — change the engine, the generator, or

the spec: the spec-leads rule, the byte-faithfulness invariant, and the testing bar.

• `scripts/mechanical_refactor_proof_generator.py` —

the generator: infers a reproduce recipe from a commit's diff and emits/runs a standalone, auditable script per commit, with a PASS / RESIDUAL / UNSUPPORTED verdict.

• `scripts/mechanical_refactor_reproduction_utils.py` — the

proof engine: the Repro builder's faithful relocation primitives plus the worktree + pre-commit + byte-diff scaffold. Self-contained — only git and the standard library.

• `scripts/mechanical_refactor_reproduction_cli.py` — the

chain verifier: classifies every commit in base..branch, runs every provable commit's proof from the proof folder, and emits the full chain report.

• `scripts/tests/` — pytest suites, one folder per module:

reproduction_utils/ for the proof engine, proof_generator/ for the generator, reproduction_cli/ for the chain verifier.