diff --git a/.claude/skills/mechanical-refactor-verify/SKILL.md b/.claude/skills/mechanical-refactor-verify/SKILL.md index 786339771..079d80db6 100644 --- a/.claude/skills/mechanical-refactor-verify/SKILL.md +++ b/.claude/skills/mechanical-refactor-verify/SKILL.md @@ -1,6 +1,8 @@ --- name: mechanical-refactor-verify description: Make mechanical refactoring (file splits, function moves, module extractions, renames) machine-checkable instead of eyeballed. Reproduce a relocation commit byte-for-byte from faithful primitives, and split an extraction into a verifiable prepare + move + postpare. Use when doing or reviewing such changes. +user_invocable: true +argument: "split .. | construct .. [--match REGEX] [--out DIR] | verify --base --branch --proof [--jobs N] [--skip-passed]" --- # Mechanical Refactor — Machine-Checkable Verification @@ -17,34 +19,64 @@ description: Make mechanical refactoring (file splits, function moves, module ex - A reshape must not ride along: split into optional **prepare** + certified **move** + optional **postpare** (`guide-split.md`). -## 2. What do you want to do? +## 2. Commands — what do you want to do? -- **Split a change into commits** (extract, move, file split) → `guide-split.md`: the - prepare + move + postpare rule, the case recipes, and the anti-patterns. -- **Construct the proof for a move commit** → `guide-construct-proof.md`: run - `scripts/mechanical_refactor_proof_generator.py`, or hand-write a `Repro` when the - generator reports `UNSUPPORTED`. -- **Verify someone's proof** → `guide-verify-proof.md`: re-run it, read the verdict, audit - the authored surfaces. +The skill takes an argument naming one of three commands; invoked without one, pick the +row matching your task. + +- **`split ..`** — 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 .. [--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 .. --match REGEX --out DIR`); + §2 proves a single commit — pass just `` (the generator, or a hand-written + `Repro` when it reports `UNSUPPORTED`). +- **`verify --base --branch --proof [--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`](guide-split.md) — split a change into prepare + move + postpare: the - case recipes, what stays mechanical, and the anti-patterns. -- [`guide-construct-proof.md`](guide-construct-proof.md) — produce the proof: the - generator, the hand-written `Repro`, and publishing the proof with the PR. -- [`guide-verify-proof.md`](guide-verify-proof.md) — consume the proof: re-run, verdicts, - and the audit checklist for authored surfaces. +- [`guide-split.md`](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`](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`](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`](spec-reproduction-utils.md) — the normative spec of the clean-move property and the reproduction primitives. +- [`spec-reproduction-cli.md`](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`](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`](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`](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`](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/`](scripts/tests/) — pytest suites, one folder per module: - `reproduction_utils/` for the proof engine, `proof_generator/` for the generator. + `reproduction_utils/` for the proof engine, `proof_generator/` for the generator, + `reproduction_cli/` for the chain verifier. diff --git a/.claude/skills/mechanical-refactor-verify/guide-construct-proof.md b/.claude/skills/mechanical-refactor-verify/guide-construct-proof.md index 8c773fb8f..683e75fe6 100644 --- a/.claude/skills/mechanical-refactor-verify/guide-construct-proof.md +++ b/.claude/skills/mechanical-refactor-verify/guide-construct-proof.md @@ -1,30 +1,26 @@ -# Construct a proof for a move commit +# Construct a proof -## 1. What a proof is - -- A runnable script that regenerates the commit from its base with the faithful relocation - primitives and byte-diffs the result against it. +- Two levels, one chapter each: §1 constructs the **proof folder for a whole chain** (and + publishes it with the PR); §2 constructs the proof for a **single commit** (the + generator, the hand-written `Repro`, the hand-written transform). - The property and primitive contracts: `spec-reproduction-utils.md`. Splitting the change so the move is provable: `guide-split.md`. Consuming the proof: `guide-verify-proof.md`. -## 2. Auto-generate the script (primary path) +## 1. Construct proofs for a whole chain -- `mechanical_refactor_proof_generator.py` infers the recipe from a commit's diff and - before-state AST. -- It emits and runs a standalone, auditable script — no one hand-writes it. - -### 2.1 Commands +### 1.1 Generate the proof folder ```bash -# one commit: print the inferred script and run it (non-zero exit unless PASS) -python3 .claude/skills/mechanical-refactor-verify/scripts/mechanical_refactor_proof_generator.py - -# a range: write a self-contained folder +# a range: write a self-contained folder for every mechanical_provable commit python3 .claude/skills/mechanical-refactor-verify/scripts/mechanical_refactor_proof_generator.py \ - .. --match -move: --out repro_out + .. --match '(?/ -- put it in the PR description +``` + +- `gh gist create` flattens paths — fine per §1.3.1. +- Alternatives: a PR attachment (zip the `--out` folder) or a branch holding it. +- Put the reviewer's download-and-re-run commands (`guide-verify-proof.md` §2.1) in the + PR description under a "Mechanical move — reproducible" heading. + +#### 1.3.3 Keep the classification honest — in both directions + +- A `mechanical_provable` commit (and a PR made only of such commits) contains **only** + mechanical changes (moves, splits, renames, import fixes, formatting). Semantic changes + go in their own `non_mechanical_provable` commits — a chain, and therefore a PR, need + not be purely mechanical, but a single commit never mixes the two. +- The dual holds too: a semantic (`non_mechanical_provable`) commit must not swallow a + provable relocation to skip the proof — split it out and prove it + (`guide-split.md` §2.2; property: `spec-reproduction-cli.md` §2.1). + +## 2. Construct the proof for a single commit + +### 2.1 What a proof is + +- A runnable script that regenerates the commit from its base with the faithful relocation + primitives and byte-diffs the result against it. + +### 2.2 Auto-generate the script (primary path) + +```bash +# one commit: print the inferred script and run it (non-zero exit unless PASS) +python3 .claude/skills/mechanical-refactor-verify/scripts/mechanical_refactor_proof_generator.py +``` + +#### 2.2.1 What the inference covers - **Method → existing class**: call sites lowered (`Owner.m(recv, …)` → `recv.m(…)`), the orphaned local import removed. @@ -43,31 +91,46 @@ Self-contained, auditable without the skill installed: - **New-module extract of scattered defs**: `extract_symbols_to_new_module` under the audited header; a constant that relocated into the header is dropped from the source. A contiguous-tail source still uses `extract_to_new_module`. +- **Inline-block extract-function** (intra-file): a new helper whose verbatim body is a + block cut from a sibling function, that function's block replaced by a call — inferred as + `extract_function`, authoring only the signature, the call, and (when the block ends in + `lhs = expr` returned by the helper) a `return lhs`. A body edited on the way out (a + de-self / restructure) does not infer — the residual surfaces it. +- **A move landing just above an `if TYPE_CHECKING:` guard**: anchored with + `move_symbol(after=)` rather than a `before=` that would overshoot past + the guard. - **A source file the commit deletes** once its defs relocated: `delete_file`. - **The module-level import diff**, realised directly from the target: gained names added - (a wholly new module's statement verbatim, wrapping kept), lost names removed with + (a wholly new module's statement verbatim, wrapping kept, or one name folded into an + existing `from module import …` with `add_imported_name`), lost names removed with `remove_imported_name`. - Non-Python files in the commit do not block inference; their diff is noted and left to the residual. -### 2.4 What it reports `UNSUPPORTED` +#### 2.2.2 What it reports `UNSUPPORTED` - Single-commit mode prints the verdict with notes and exits non-zero; range mode records it in the outputs. -- Review such a commit as prepare, or hand-write the `Repro` (§3). +- Review such a commit as prepare, or hand-write the `Repro` (§2.3). - The cases: - **no definition relocated** — a rename (even a privacy flip `_foo` → `foo`) or a statement-level reorder; reshapes belong in prepare; - **a new-module extract whose symbols are not all top-level in the source** — a method still inside a class; prepare must de-self it out first; - - **an extract drawing from more than one source file**, and an **inline-block - extract-function** — compose `extract_function` by hand (the body must be unchanged; - a de-self / restructure is a separate semantic commit). + - **an extract drawing from more than one source file** — compose `extract_function` by + hand. An inline-block extract-function within one file is inferred (§2.2.1), but only + when the body is a verbatim cut; a de-self / restructure on the way out is a separate + semantic commit and does not infer. -## 3. Hand-write the `Repro` when inference falls short +### 2.3 Hand-write the `Repro` when inference falls short - Compose the transform from the same primitives (`spec-reproduction-utils.md` §3). - The same byte-diff then certifies it. +- **`UNSUPPORTED`, or a primitive that cannot express the exact edit, is never a reason to + relabel a relocation as `non_mechanical_provable`.** If the change is a relocation, it + gets a proof: hand-write the `Repro` here, or (when a primitive genuinely lacks the needed + form, e.g. an insertion anchor) enhance the primitive first, then prove it. See + guide-split.md §2.7.6. ```python import sys @@ -86,7 +149,7 @@ r.add_import("dst.py", "import gc") r.run() # PASS = byte-identical; otherwise prints the residual ``` -## 4. A hand-written transform for a non-relocation mechanical change +### 2.4 A hand-written transform for a non-relocation mechanical change - For a whole-file split or rename — no single symbol relocates — write a `transform()` and call `verify_mechanical_refactor`. @@ -116,42 +179,3 @@ def transform(dir_root: Path) -> None: if __name__ == "__main__": verify_mechanical_refactor(BASE_COMMIT, TARGET_COMMIT, transform) ``` - -## 5. Publish the proof with the PR - -### 5.1 What to share - -- Share the scripts **plus** the copied `mechanical_refactor_reproduction_utils.py` — the - scripts import it, so a lone raw file is not runnable. -- Never a `python3 <(curl ...)` one-liner: process substitution gives the script no real - directory, so the import breaks. -- Flat layouts work: Python puts the script's own directory on `sys.path`, so the utils - module can sit either next to the script or one level up (the `--out` layout). - -### 5.2 Author: create a gist - -```bash -cd repro_out -gh gist create --desc "mechanical-move proof for PR #NNNN" \ - repro_scripts/*.py mechanical_refactor_reproduction_utils.py output.log -# prints https://gist.github.com// -- put it in the PR description -``` - -- `gh gist create` flattens paths — fine per §5.1. -- Alternatives: a PR attachment (zip the `--out` folder) or a branch holding it. - -### 5.3 Reviewer: download and re-run - -```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 -``` - -- Include exactly these commands in the PR description under a - "Mechanical move — reproducible" heading. - -### 5.4 Keep the PR mechanical - -- A mechanical PR contains **only** mechanical changes (moves, splits, renames, import - fixes, formatting). Semantic changes go in a separate PR. diff --git a/.claude/skills/mechanical-refactor-verify/guide-modify-skill.md b/.claude/skills/mechanical-refactor-verify/guide-modify-skill.md new file mode 100644 index 000000000..4cc11ddb0 --- /dev/null +++ b/.claude/skills/mechanical-refactor-verify/guide-modify-skill.md @@ -0,0 +1,100 @@ +# Modify this skill: the engine, the generator, or the spec + +- How to change `scripts/mechanical_refactor_reproduction_utils.py` (the proof engine), + `scripts/mechanical_refactor_proof_generator.py` (the generator), + `scripts/mechanical_refactor_reproduction_cli.py` (the chain verifier), or the specs — + without silently weakening the proof. +- Read this **before** editing any file under this skill. The engine is trusted: a wrong + primitive certifies a non-mechanical commit as clean, and every downstream reviewer + believes it. Changes here carry a higher bar than ordinary code. + +## 1. What has which bar + +| File | Role | Bar | +|---|---|---| +| `spec-reproduction-utils.md` | **normative** source of truth (SKILL.md §2): the clean-move property, the whitelist / not-allowed lists, each primitive's contract, the arbiter | any behavior change lands here first | +| `spec-reproduction-cli.md` | **normative** source of truth for the chain verifier: the word rule, the proof obligation, the report, the exit codes | any behavior change lands here first | +| `mechanical_refactor_reproduction_utils.py` | **trusted engine**: the relocation primitives + the arbiter | highest — byte-faithfulness proven by tests | +| `mechanical_refactor_proof_generator.py` | **convenience**: infers a recipe from a diff | lower — may report `RESIDUAL`/`UNSUPPORTED` without compromising trust, but still tested | +| `mechanical_refactor_reproduction_cli.py` | **gatekeeper**: walks a chain, runs the proofs, reports | high — a false chain PASS certifies an unproven commit; classification, resolution, and PASS-criterion behavior proven by tests | +| `guide-*.md`, `SKILL.md` | workflow + file map | kept in sync, never describe behavior the code lacks | + +## 2. Cardinal rule — the spec leads, code follows + +- `spec-reproduction-utils.md` wins over every other file (SKILL.md §2). Code serves the + spec, not the reverse. +- A behavior change to a primitive, to §2.1/§2.2 (what counts as a clean move), or to the + §4 arbiter **must edit the spec in the same commit as the code**. Code and spec never + diverge across commits. + - New primitive → add its contract to §3. + - Changed clean-move boundary → edit §2.1 (allowed) / §2.2 (not allowed). + - Changed reproduce/diff behavior → edit §4. +- If you discover code and spec already disagree, the spec is authoritative: fix the code + to match — or, if the spec itself is wrong, change it **deliberately** in one commit with + the reasoning, not as a silent side effect. + +## 3. The faithfulness invariant — never break this + +- Every primitive relocates **original source bytes**: AST-located, spliced as the source + text that was there, **never regenerated**. A byte match after the formatter is the + *entire* proof — the moment a primitive regenerates instead of splicing, the proof is + worthless (it can no longer distinguish "moved" from "rewritten to look moved"). +- A new or changed primitive **must**: + - locate its target through the AST, not by string search over source; + - splice the original bytes (interiors of multi-line strings, comments, a magic + trailing comma, semicolon-joined statements all survive verbatim); + - preserve the file's newline style (CRLF round-trips) and UTF-8-byte-accurate columns. +- Do **not** add a primitive that normalizes, reflows, or reformats. Formatting belongs to + the pre-commit pass in the §4 arbiter, applied to **both** sides; primitives do + relocation only. +- When the generator cannot infer a move, the answer is a hand-written `Repro` + (guide-construct-proof §2.3) — **not** loosening a primitive to make it fit. + +## 4. Testing rules — the hard bar + +- The engine is trusted, so an untested change to it is not acceptable. "It ran once" is + not a test. +- Run the **full** suite and keep it green: + + ```bash + cd scripts && uv run --with pytest --python 3.12 python -m pytest tests/ -q + ``` + + Baseline at the time of writing: **188 passed**. Your change must leave the count at or + above baseline — never delete a case to make the suite pass. +- Layout mirrors the modules; put your test where it belongs: + - `tests/reproduction_utils/` — one `test_.py` per engine primitive. + - `tests/proof_generator/` — the inference layer (`test_infer_*`, `test_script_and_diff`). + - `tests/reproduction_cli/` — the chain verifier (classification, proof discovery, + chain walking, the report). +- A new or changed **primitive** requires, in its `test_.py`: + - a **byte-exact** assertion on the resulting file (compare full bytes, not "contains"); + - at least one **adversarial** case where a regenerating implementation would differ + from splicing — a comment mid-body, a magic trailing comma, odd indentation, a + semicolon-joined import, non-ASCII text, or a CRLF file — asserting the original + bytes survive; + - the **raise paths** the spec promises: ambiguous anchor raises, missing anchor + raises, wrong/absent `from_class` raises. +- A change to the **generator** requires a `tests/proof_generator/` case that runs it on a + synthetic commit and asserts `PASS`, plus one non-move / bundled-change case that asserts + `RESIDUAL` or `UNSUPPORTED` — so a future regression that makes it "pass" a dirty commit + is caught. +- A change to the **chain verifier** requires a `tests/reproduction_cli/` case asserting a + verified chain passes, plus one asserting the broken shape it guards (an unclassified + commit, a missing proof, a failing proof) still fails — so a regression cannot silently + green a dirty chain. +- The engine stays **self-contained**: `mechanical_refactor_reproduction_utils.py` imports + only `git` (via subprocess) and the standard library. Do not add a third-party dependency + to it. + +## 5. Before you commit — checklist + +- [ ] `spec-reproduction-utils.md` / `spec-reproduction-cli.md` edited in this same + commit (if any behavior changed). +- [ ] Full pytest suite green; case count ≥ prior baseline. +- [ ] New/changed primitive has: byte-exact test + ≥1 adversarial (regeneration-would-differ) + case + the raise-path tests. +- [ ] Generator change has a `PASS` test **and** a `RESIDUAL`/`UNSUPPORTED` test. +- [ ] `SKILL.md` §3 file map and the relevant `guide-*.md` updated for any new file or + workflow change. +- [ ] `mechanical_refactor_reproduction_utils.py` still imports only git + stdlib. diff --git a/.claude/skills/mechanical-refactor-verify/guide-split.md b/.claude/skills/mechanical-refactor-verify/guide-split.md index 3d60925be..014b6a094 100644 --- a/.claude/skills/mechanical-refactor-verify/guide-split.md +++ b/.claude/skills/mechanical-refactor-verify/guide-split.md @@ -1,6 +1,60 @@ -# Split a mechanical change: prepare, move, postpare +# Split a mechanical refactor -## 1. Why split +- Two levels of splitting, one chapter each: §1 splits the **PR/branch** into small + classified pieces (the chain contract); §2 splits **one piece** into prepare + move + + postpare so its move is provable. + +## 1. Split the PR into small verifiable pieces + +### 1.1 The chain contract — what a compliant branch satisfies + +When asked to make (or fix) a refactor branch so it "satisfies this skill", ALL of the +following must hold over `base..branch`; run the chain verifier +(`guide-verify-proof.md` §1) to check the machine-checkable part in one command. + +1. **Every commit is classified, in the required subject format:** + + ```text + (,): + ``` + + with `` exactly `mechanical_provable` or `non_mechanical_provable`, and + `` / `` kebab-case (contiguous same-`` commits form one + future PR). The verifier machine-checks the standalone-word rule + (`spec-reproduction-cli.md` §2.1); the full format is required on top of it so the + chain can be grouped into PRs. +2. **Classification is correct — mechanical work is labeled mechanical.** Every operation + expressible as the whitelisted relocations (an extract-function, a bulk move, a file + split, an import repoint, …) is its own `mechanical_provable` commit. Hiding provable + content inside a `non_mechanical_provable` commit — dodging the verifier — is + forbidden (§2.2 maximality); catching it is the reviewer's duty + (`guide-verify-proof.md` §1). How to split so this holds: §2. +3. **Every `mechanical_provable` commit has a proof that PASSes.** Produce the proofs + with the generator (`guide-construct-proof.md` §1); the chain verifier re-runs every + one of them against the proof folder. +4. **Every `non_mechanical_provable` commit is correctness-reviewed by eyes.** Its diff + must be confirmed to do exactly what its message claims: no lost logic, no hidden bug, + no unintended behavior change riding along (`guide-verify-proof.md` §1). When the + commit claims to be behavior-preserving that means checking equivalence — but a chain + need not be a pure refactor, and a commit that intentionally changes behavior is + reviewed for the correctness of that change instead. The machine never certifies + these — that is exactly why they must stay minimal (item 2). + +### 1.2 Commit naming and classification + +- The subject format is exactly §1.1 item 1 — no reserved phase suffixes are required. + The `` is free (naming it after the phase, e.g. `foo-prepare` / `foo-move`, + is fine but optional). +- The phases map onto the classification word directly: **move** commits declare + `mechanical_provable`; **prepare**, **postpare**, and standalone semantic commits + declare `non_mechanical_provable`. +- The generator's range command selects the provable commits by the word itself: + `--match '(? --color-moved=dimmed-zebra --color-moved-ws=allow-indentation-change` marks the whole block as moved. -### 3.2 Case 2: method → method on a class +### 2.4 Case 2: method → method on a class - For pulling **several methods and the fields they touch** into a new (or existing) class. - Prep does **not** de-self — it builds the class and retypes `self`, body untouched. -#### 3.2.1 Commit 1 — prep: build the class, retype `self` +#### 2.4.1 Commit 1 — prep: build the class, retype `self` 1. Create the target class with the fields the moved methods touch (a frozen dataclass is simplest; drop `frozen` only if they mutate). @@ -143,7 +221,7 @@ Boundaries: **Check:** lint + tests pass; body unchanged; types check (`self: Target` matches the instance the caller passes). -#### 3.2.2 Commit 2 — move: relocate into the class +#### 2.4.2 Commit 2 — move: relocate into the class - Cut `foo` into the target class; drop `@staticmethod` — body **unchanged, line for line**. @@ -154,7 +232,7 @@ instance the caller passes). **Check:** `mechanical_refactor_proof_generator.py ` reports `PASS`. The split paid off: prep left the body untouched, so the move is a clean cut/paste. -### 3.3 Case 3: extract to a new module — one move commit, no prep +### 2.5 Case 3: extract to a new module — one move commit, no prep - The move gathers the defs **from wherever they sit** — no prep staging at the source tail. Replayed by `extract_symbols_to_new_module`. @@ -166,9 +244,9 @@ paid off: prep left the body untouched, so the move is a clean cut/paste. - The only work outside the move: a non-mechanical reference the move cannot derive (a string-literal module path) — a one-line **postpare**. - A symbol **not top-level** in the source (a method still in a class): prepare de-selfs - it out first (§3.1); the proof reports `UNSUPPORTED` until then. + it out first (§2.3); the proof reports `UNSUPPORTED` until then. -### 3.4 Case 4: extract-function — the bulk goes in the move +### 2.6 Case 4: extract-function — the bulk goes in the move - The relocated body belongs in a certified move, not buried in a prep: the `extract_function` primitive cuts the inline block **verbatim** and authors only the @@ -179,9 +257,9 @@ paid off: prep left the body untouched, so the move is a clean cut/paste. - An extraction that rewrites the body *as* it extracts is a semantic commit, not a certifiable move — do not dress it up as one. -## 4. Remarks +### 2.7 Remarks -### 4.1 A move never renames +#### 2.7.1 A move never renames - The moved symbol keeps the **same name on both sides**. - A rename — even a privacy flip `_foo` → `foo` — is its own single-purpose commit @@ -189,7 +267,7 @@ paid off: prep left the body untouched, so the move is a clean cut/paste. - A move that also renames cannot be machine-certified: split it — rename first, then move. -### 4.2 Anti-pattern: prep adds the body, move deletes it +#### 2.7.2 Anti-pattern: prep adds the body, move deletes it - Symptom: prep **adds** a large block to the target; the move **deletes** the same block from the source. The order is reversed. @@ -198,14 +276,32 @@ paid off: prep left the body untouched, so the move is a clean cut/paste. - The body appears and disappears exactly once — on the move side. Fix by pushing the "add the body" work out of prep into the move. -### 4.3 When NOT to split (single commit) +#### 2.7.3 Anti-pattern: the giant prep (relocating inside the source to stage the move) + +- Symptom: the prep's diff is **hundreds of lines** for a single function — because it + also moved the function to the source file's tail, rewrote it as a free function next + to a staged import/constant block, or reordered its neighbors so the move can cut one + contiguous block. +- All of that staging is unnecessary: `extract_symbols_to_new_module` gathers symbols + **from wherever they sit** (§2.5) — the move needs no contiguity and no tail parking. +- A prep's legitimate diff is the handful of lines the primitives cannot derive: the + `@staticmethod` decorator, the kwargs signature, `self.x` → parameter reads, an added + `return`, the class-qualified call site. For one function that is **tens of lines, not + hundreds** — a prep in the hundreds is the signal the relocation leaked into it. +- Why it matters: every relocated-but-not-certified line in a prep is a line the machine + never checks and a reviewer must eyeball; parking blocks mid-file also leaves broken or + duplicated intermediate states (a staged import for a module that does not exist yet). +- Fix: strip the prep back to the interface edits above, leave the body **in place**, + and let the certified move do all relocation. + +#### 2.7.4 When NOT to split (single commit) - Moving an **already** module-level free function. - Pure file rename / whole-file move. - Trivial field deletion, or `getattr(obj, "x", ...)` → direct attribute access. - A class-internal helper relocated next to another helper in the same module. -### 4.4 Which actions are mechanical vs not +#### 2.7.5 Which actions are mechanical vs not - Boundary: building the component correctly the first time is mechanical; reshaping it *after* it exists is not. @@ -213,6 +309,7 @@ paid off: prep left the body untouched, so the move is a clean cut/paste. | Action | Bucket | |---|---| | target class skeleton + ctor + fields | mechanical (prep) | +| destination module scaffolding (a `logger`, a module-level constant) the moved symbol needs, when moving into an **existing** module | mechanical (prep) | | `@dataclass(frozen=True, slots=True, kw_only=True)` decoration | mechanical (prep) | | composition wiring (`self.component = Target(...)`) | mechanical (prep) | | `Callable` getter injection for runtime-mutable state | mechanical (prep) | @@ -230,14 +327,31 @@ paid off: prep left the body untouched, so the move is a clean cut/paste. change. - Review order = commit order: prep → move → non-mechanical follow-ups. -### 4.5 Naming +#### 2.7.6 Anti-pattern: the non-mechanical label as an escape hatch -- Consecutive commits with reserved suffixes; short kebab ``: - -``` --prepare: # optional: minimal in-place reshape (de-self, or retype-self) --move: # pure relocation, certified by the reproduce proof --postpare: # optional: minimal tail fixup (e.g. a string-literal path) -``` - -- The `:` form is what the range command's `--match -move:` regex keys on. +- Symptom: a commit whose body is a **pure relocation** (a cut+paste move, a module-level + constant move, a verbatim inline-block extract) is labelled `non_mechanical_provable` and + ships with no proof — because the generator reported `UNSUPPORTED` or a primitive could + not express the exact insertion point, so the author reached for the softer label instead + of a proof. +- Real example from this repo's history: `kvc-move-lazy-compaction-gate` relocated the + module-level `_should_enable_lazy_compaction` unchanged into `kv_cache_configurator.py` but + was labelled `non_mechanical_provable`, because it had to land *above* an + `if TYPE_CHECKING:` guard and `move_symbol` only anchored with `before=`, which overshot + past the guard. The relocation was fully mechanical; only the tool's insertion-anchor was + missing — so the fix was to add a `move_symbol(after=)` anchor and prove it, not to keep + the softer label. (A sibling commit that moves a *contiguous block* of constants plus their + leading comment needs a block-move primitive the toolkit does not yet have — that one is + still awaiting an enhancement, which is the correct disposition, not a relabel.) +- The rule, in order: + 1. A pure relocation **must** be `mechanical_provable` and carry a proof. The label is + a claim about the change, not about how easy the tooling made it. + 2. Generator says `UNSUPPORTED` but the change *is* a relocation → **hand-write the + `Repro`** from the same primitives (guide-construct-proof.md §2.3). Inference falling + short is not a licence to drop the proof. + 3. A primitive genuinely cannot express the faithful edit (the missing `after=` anchor + above) → **enhance the primitive first**, then prove it. The fix for a tooling gap is + to close the gap, not to relabel the commit as unprovable. +- Only a change that is genuinely *not* a relocation (a signature redesign, a logic rewrite, + a de-self restructure) earns `non_mechanical_provable`. If you cannot say which + non-relocation edit justifies the label, the label is wrong. diff --git a/.claude/skills/mechanical-refactor-verify/guide-verify-proof.md b/.claude/skills/mechanical-refactor-verify/guide-verify-proof.md index ced8160f2..054841400 100644 --- a/.claude/skills/mechanical-refactor-verify/guide-verify-proof.md +++ b/.claude/skills/mechanical-refactor-verify/guide-verify-proof.md @@ -1,10 +1,86 @@ -# Verify a proof for a move commit +# Verify a proof -- How the reviewer of a claimed-mechanical commit consumes its proof. -- The certified property and primitive contracts: `spec-reproduction-utils.md`. +- 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`. -## 1. Re-run it +## 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: @@ -12,22 +88,32 @@ 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. Read the verdict +### 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.4). Not +- **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`. -## 3. Audit the authored surfaces +### 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. @@ -41,7 +127,7 @@ function's interface is authored; only its body is certified; - the `drop_assigns=` list — each named constant leaves the source file. -## 4. Know what a PASS does and does not assert +### 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 @@ -52,11 +138,11 @@ these relocations", not "this relocation was a good idea". Confirm the commit's subject matches what the script actually moves before approving. -## 5. Why the mechanism is trustworthy +### 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 §3) is the +- 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. diff --git a/.claude/skills/mechanical-refactor-verify/scripts/mechanical_refactor_proof_generator.py b/.claude/skills/mechanical-refactor-verify/scripts/mechanical_refactor_proof_generator.py index ad36d561e..598ac7a82 100644 --- a/.claude/skills/mechanical-refactor-verify/scripts/mechanical_refactor_proof_generator.py +++ b/.claude/skills/mechanical-refactor-verify/scripts/mechanical_refactor_proof_generator.py @@ -8,18 +8,22 @@ imports were repathed, and the symmetric module-level import diff each file gain (realised directly with add_import / remove_imported_name, since an import diff is always whitelisted). ``recipe_to_script`` emits a standalone ``repro_scripts/.py`` (importing only the -reproduce util); running it reproduces the commit and diffs it byte-for-byte. +reproduce util); running it reproduces the commit, diffs it byte-for-byte, and exits +non-zero unless the diff is empty (PASS). ``generate_range`` writes a whole folder (scripts + output.log + output.html) for a range. Handles a method moved onto an existing class (call sites lowered), a method moved to a module-level free function (call sites requalified), a free-function-source move to an -existing module (callers repath their import), and a new-file extract -- where the prep +existing module (callers repath their import), a new-file extract -- where the prep commit staged the whole module body (scaffolding plus def) as a trailing block in the -source, so the move cuts that tail into the new file (extract_to_new_module). A rename or a -statement-level reorder relocates no def and is reported unsupported. Runnable directly: +source, so the move cuts that tail into the new file (extract_to_new_module) -- and an +intra-file inline-block extract-function (a new helper whose verbatim body is a block carved +from a sibling function, that block replaced by a call). A rename or a statement-level +reorder relocates no def and is reported unsupported. Runnable directly: python3 mechanical_refactor_proof_generator.py - python3 mechanical_refactor_proof_generator.py .. --match -move: --out DIR + python3 mechanical_refactor_proof_generator.py .. \ + --match '(? str | None: return None +def _delegate_stub_attr(tree: ast.AST, name: str) -> tuple[str, str] | None: + """The component attribute a forwarding stub ``def name``: ``return self..(...)`` + delegates through, with the forwarded method name -- None when no such stub exists. + """ + for node in ast.walk(tree): + if not ( + isinstance(node, (ast.FunctionDef, ast.AsyncFunctionDef)) + and node.name == name + ): + continue + if ( + len(node.body) == 1 + and isinstance(node.body[0], ast.Return) + and isinstance(node.body[0].value, ast.Call) + and isinstance(node.body[0].value.func, ast.Attribute) + and isinstance(node.body[0].value.func.value, ast.Attribute) + and isinstance(node.body[0].value.func.value.value, ast.Name) + and node.body[0].value.func.value.value.id == "self" + ): + return (node.body[0].value.func.value.attr, node.body[0].value.func.attr) + return None + return None + + def _nested_in_function(tree: ast.AST, name: str) -> bool: target = rr._find_def(tree, name) if target is None: @@ -270,7 +298,9 @@ class Recipe: target: str supported: bool = True moves: list = field(default_factory=list) + assign_moves: list = field(default_factory=list) extracts: list = field(default_factory=list) + extract_functions: list = field(default_factory=list) scatter_extracts: list = field(default_factory=list) lowerings: list = field(default_factory=list) repaths: list = field(default_factory=list) @@ -420,6 +450,83 @@ def _next_sibling_def_name( return None +def _next_sibling_assign_or_def(dst_tree: ast.AST, name: str) -> str | None: + """The name of the top-level statement (def/class/single-Name assign) that immediately + follows the assignment ``name`` in the destination, or None when it is last.""" + + def stmt_name(node: ast.AST) -> str | None: + if isinstance(node, (ast.FunctionDef, ast.AsyncFunctionDef, ast.ClassDef)): + return node.name + if ( + isinstance(node, ast.Assign) + and len(node.targets) == 1 + and isinstance(node.targets[0], ast.Name) + ): + return node.targets[0].id + if isinstance(node, ast.AnnAssign) and isinstance(node.target, ast.Name): + return node.target.id + return None + + named = [(stmt_name(n), n) for n in getattr(dst_tree, "body", []) if stmt_name(n)] + for i, (nm, _) in enumerate(named): + if nm == name: + return named[i + 1][0] if i + 1 < len(named) else None + return None + + +def _stmt_symbol_name(node: ast.AST) -> str | None: + """The name a top-level statement defines -- a def/class name, or a single-Name + assignment target -- else None (an ``if TYPE_CHECKING:`` guard, a tuple assign, ...). + """ + if isinstance(node, (ast.FunctionDef, ast.AsyncFunctionDef, ast.ClassDef)): + return node.name + if ( + isinstance(node, ast.Assign) + and len(node.targets) == 1 + and isinstance(node.targets[0], ast.Name) + ): + return node.targets[0].id + if isinstance(node, ast.AnnAssign) and isinstance(node.target, ast.Name): + return node.target.id + return None + + +def _module_move_anchor( + dst_tree: ast.AST, name: str, into_class: str | None +) -> tuple[str | None, str | None]: + """The ``(before, after)`` anchor for reinserting the moved def ``name``. Normally + ``before=``. But when a module-level def lands immediately above an + unnameable statement (e.g. an ``if TYPE_CHECKING:`` guard) with a nameable statement + immediately above it, a ``before`` anchor would resolve to the next def *past* that block + and overshoot, so anchor with ``after=`` instead.""" + before = _next_sibling_def_name(dst_tree, name, into_class) + if into_class is not None: + return before, None + body = list(getattr(dst_tree, "body", [])) + idx = next( + ( + i + for i, n in enumerate(body) + if isinstance(n, (ast.FunctionDef, ast.AsyncFunctionDef, ast.ClassDef)) + and n.name == name + ), + None, + ) + if idx is None: + return before, None + following = body[idx + 1] if idx + 1 < len(body) else None + next_is_named_def = isinstance( + following, (ast.FunctionDef, ast.AsyncFunctionDef, ast.ClassDef) + ) + if following is None or next_is_named_def: + return before, None + preceding = body[idx - 1] if idx > 0 else None + prev_name = _stmt_symbol_name(preceding) if preceding is not None else None + if prev_name is None: + return before, None + return None, prev_name + + def _symbols_form_tail(src_text: str, symbols: list[str]) -> bool: """Whether ``symbols`` sit at the end of the source as a contiguous block of defs/classes and the scaffolding leading into them -- the trailing block a prep commit stages for a @@ -484,6 +591,183 @@ def _scatter_extract_layout(dst_after: str, symbols: list[str]) -> dict | None: return {"header": header, "order": [node.name for node in sym_nodes]} +def _iter_defs_with_container( + tree: ast.AST, +) -> list[tuple[str | None, ast.AST]]: + """(container_class_name_or_None, def_node) for every module-level function and every + method one class deep -- the two nesting depths an extract_function helper can land at. + """ + out: list[tuple[str | None, ast.AST]] = [] + for node in getattr(tree, "body", []): + if isinstance(node, (ast.FunctionDef, ast.AsyncFunctionDef)): + out.append((None, node)) + elif isinstance(node, ast.ClassDef): + for child in node.body: + if isinstance(child, (ast.FunctionDef, ast.AsyncFunctionDef)): + out.append((node.name, child)) + return out + + +def _statements_parse(lines: list[str]) -> bool: + """Whether ``lines`` (dedented to their own minimum indent) parse as complete Python + statements -- used to keep a prefix/suffix split from cutting through the middle of a + multi-line statement.""" + text = "".join(lines) + if not text.strip(): + return True + indents = [len(ln) - len(ln.lstrip(" ")) for ln in lines if ln.strip()] + dedented = rr.dedent(text, min(indents)) if indents else text + try: + ast.parse(dedented) + return True + except SyntaxError: + return False + + +def _common_prefix_suffix(a: list[str], b: list[str]) -> tuple[int, int]: + """Longest common leading and trailing run of identical lines between two line lists, + kept non-overlapping -- isolates the single contiguous region where they differ. The + greedy match is then shrunk (suffix first, then prefix) until the differing middle of + *both* lists parses as complete statements, so a boundary line the removed block and its + replacement happen to share (e.g. a lone ``)``) is not absorbed mid-statement.""" + prefix = 0 + while prefix < len(a) and prefix < len(b) and a[prefix] == b[prefix]: + prefix += 1 + suffix = 0 + while ( + suffix < len(a) - prefix + and suffix < len(b) - prefix + and a[-1 - suffix] == b[-1 - suffix] + ): + suffix += 1 + while suffix > 0 and not ( + _statements_parse(a[prefix : len(a) - suffix]) + and _statements_parse(b[prefix : len(b) - suffix]) + ): + suffix -= 1 + while prefix > 0 and not ( + _statements_parse(a[prefix : len(a) - suffix]) + and _statements_parse(b[prefix : len(b) - suffix]) + ): + prefix -= 1 + return prefix, suffix + + +def _call_names_in(node: ast.AST) -> set[str]: + """Names invoked as ``self.(...)`` or ``(...)`` anywhere under ``node``.""" + names: set[str] = set() + for sub in ast.walk(node): + if isinstance(sub, ast.Call): + if isinstance(sub.func, ast.Attribute): + names.add(sub.func.attr) + elif isinstance(sub.func, ast.Name): + names.add(sub.func.id) + return names + + +def _infer_extract_functions( + recipe: Recipe, files: dict[str, dict], commit: str, root: str +) -> None: + """Infer intra-file extract_function ops: a new helper ``H`` whose body is a verbatim block + cut from another function ``F`` of the same file, with ``F``'s block replaced by a call to + ``H`` (optionally an ``lhs = self.H(...)`` assignment mirrored by a ``return lhs`` the helper + appends). The relocated body is byte-checked; only the header/call/return are authored. A + body whose reindent does not reconstruct the helper (a bundled edit) yields no op, so the + residual surfaces it instead of a false pass.""" + for path, f in files.items(): + if f.get("new") or f.get("deleted"): + continue + before_text = _git_output(["show", f"{commit}^:{path}"], root) + after_text = _git_output(["show", f"{commit}:{path}"], root) + try: + before_tree = ast.parse(before_text) + after_tree = ast.parse(after_text) + except SyntaxError: + continue + before_lines = rr._split_keepends(before_text) + after_lines = rr._split_keepends(after_text) + before_defs = _iter_defs_with_container(before_tree) + before_keys = {(c, n.name) for c, n in before_defs} + for container, helper in _iter_defs_with_container(after_tree): + if (container, helper.name) in before_keys: + continue + if not helper.body: + continue + # The signature is the def header only (through its colon), not everything up to + # the first statement -- a leading comment sits between them and belongs to the + # extracted body, not the authored signature. + helper_text = "".join(after_lines[helper.lineno - 1 : helper.end_lineno]) + header_len = rr._def_header_end(helper_text) + header_text = "".join( + after_lines[helper.lineno - 1 : helper.lineno - 1 + header_len] + ) + # F is the one sibling function that changed and now calls the helper. + candidates = [] + for cont, node in before_defs: + after_node = next( + ( + n + for c, n in _iter_defs_with_container(after_tree) + if c == cont and n.name == node.name + ), + None, + ) + if after_node is None or node.name == helper.name: + continue + b_lines = before_lines[node.lineno - 1 : node.end_lineno] + a_lines = after_lines[after_node.lineno - 1 : after_node.end_lineno] + if b_lines == a_lines: + continue + if helper.name not in _call_names_in(after_node): + continue + candidates.append((b_lines, a_lines)) + if len(candidates) != 1: + continue + f_before, f_after = candidates[0] + prefix, suffix = _common_prefix_suffix(f_before, f_after) + block = f_before[prefix : len(f_before) - suffix] + call_lines = f_after[prefix : len(f_after) - suffix] + if not block or not call_lines: + continue + body_indent = len(block[0]) - len(block[0].lstrip(" ")) + body_text = "".join(block) + # Detect the authored `return ` structurally, by statement count -- the + # formatter reflows lines differently at the helper's shallower indent, so a + # byte comparison of the reindented body would spuriously fail; the repro's + # byte-diff (which runs the formatter) is the real arbiter. + try: + block_stmts = ast.parse(rr.dedent(body_text, body_indent)).body + except SyntaxError: + continue + helper_stmts = helper.body + return_text: str | None = None + if len(helper_stmts) == len(block_stmts) + 1 and isinstance( + helper_stmts[-1], ast.Return + ): + ret = helper_stmts[-1] + return_text = "".join( + after_lines[ret.lineno - 1 : ret.end_lineno] + ).strip("\n") + elif len(helper_stmts) != len(block_stmts): + continue + recipe.extract_functions.append( + { + "src": path, + "dst": path, + "name": helper.name, + "signature": header_text, + "body": body_text, + "body_indent": body_indent, + "call": "".join(call_lines), + "return_text": return_text, + "into_class": container, + "before": _next_sibling_def_name( + after_tree, helper.name, container + ), + } + ) + + def infer_recipe(commit: str, root: str) -> Recipe: """Infer a faithful relocation recipe for a move commit from its diff + before-state. @@ -508,6 +792,9 @@ def infer_recipe(commit: str, root: str) -> Recipe: if (m := re.match(r"\s*(?:async\s+)?def\s+(\w+)", ln)) } + def class_names(lines: list[str]) -> set[str]: + return {m.group(1) for ln in lines if (m := re.match(r"class\s+(\w+)", ln))} + new_files = {p for p, f in files.items() if f["new"]} # A new file is a staged module body cut from one source: its top-level defs and classes @@ -595,28 +882,106 @@ def infer_recipe(commit: str, root: str) -> Recipe: } ) - # A move whose destination already exists becomes a move_symbol (the def relocated in - # order); a moved class to an existing file is left unsupported (move_symbol moves defs). all_removed = [ln for f in files.values() for ln in f["removed"]] all_added = [ln for f in files.values() for ln in f["added"]] + + # A top-level class relocated between existing files moves as one block: move_symbol + # cuts the ClassDef; its methods are excluded from the per-def loop below. + moved_classes: set[str] = set() + for cname in sorted(class_names(all_removed) & class_names(all_added)): + csrc = next( + (p for p, f in files.items() if cname in class_names(f["removed"])), None + ) + cdst = next( + (p for p, f in files.items() if cname in class_names(f["added"])), None + ) + if csrc is None or cdst is None or csrc == cdst or cdst in new_files: + continue + cdst_tree = ast.parse(_git_output(["show", f"{commit}:{cdst}"], root)) + cdst_def = rr._find_def(cdst_tree, cname) or next( + ( + n + for n in ast.walk(cdst_tree) + if isinstance(n, ast.ClassDef) and n.name == cname + ), + None, + ) + moved_classes.add(cname) + recipe.moves.append( + { + "name": cname, + "src": csrc, + "dst": cdst, + "into_class": None, + "from_class": None, + "dedent": 0, + "dst_order": cdst_def.lineno if cdst_def else 0, + "before": _next_sibling_def_name(cdst_tree, cname, None), + "drop_self_annotation": False, + } + ) + + # A move whose destination already exists becomes a move_symbol (the def relocated in + # order). for name in sorted(def_names(all_removed) & def_names(all_added)): src = next( (p for p, f in files.items() if name in def_names(f["removed"])), None ) - dst = next((p for p, f in files.items() if name in def_names(f["added"])), None) - if src is None or dst is None or src == dst or dst in new_files: + dst = next( + (p for p, f in files.items() if name in def_names(f["added"]) and p != src), + None, + ) + # A def cut and re-added within the same file (no other file gained it) is an + # in-file reorder -- a move_symbol whose src and dst are that file. A signature or + # body edit that happens to touch the def line is not a faithful move, but the + # reproduction's byte-diff surfaces it as a residual, so this never false-passes. + if dst is None and src is not None and name in def_names(files[src]["added"]): + dst = src + if src is None or dst is None or dst in new_files: continue src_before = _git_output(["show", f"{commit}^:{src}"], root) if _nested_in_function(ast.parse(src_before), name): recipe.notes.append(f"skip {name}: nested function (moves with parent)") continue src_tree = ast.parse(src_before) - src_class = _enclosing_class_of_def(src_tree, name) dst_tree = ast.parse(_git_output(["show", f"{commit}:{dst}"], root)) - into_class = _enclosing_class_of_def(dst_tree, name) - dst_def = rr._find_def(dst_tree, name) - src_indent = _def_indent(files[src]["removed"], name) or 0 - dst_indent = _def_indent(files[dst]["added"], name) or 0 + src_indent = _def_indent(files[src]["removed"], name) + dst_indent = _def_indent(files[dst]["added"], name) + # The diff's def-line indentation says which same-named def actually moved: a + # column-0 cut is the module-level def even when a class method shares its name. + src_class = None if src_indent == 0 else _enclosing_class_of_def(src_tree, name) + if src_class in moved_classes: + recipe.notes.append(f"skip {name}: method of relocated class {src_class}") + continue + into_class = ( + None if dst_indent == 0 else _enclosing_class_of_def(dst_tree, name) + ) + try: + src_def = rr._find_unique_def( + src_tree, name, from_class=src_class, where=src + ) + dst_def = rr._find_unique_def( + dst_tree, name, from_class=into_class, where=dst + ) + except AssertionError as exc: + recipe.supported = False + recipe.notes.append(f"{name}: cannot disambiguate moved def ({exc})") + continue + src_indent = src_indent or 0 + dst_indent = dst_indent or 0 + # A same-named def re-added to the source is a forwarding delegate the move + # leaves behind: a body of exactly `return self..(...)` names the + # component attribute move_symbol authors the stub through. + leave_delegate = None + delegate_name = None + if name in def_names(files[src]["added"]): + src_after_tree = ast.parse(_git_output(["show", f"{commit}:{src}"], root)) + stub = _delegate_stub_attr(src_after_tree, name) + if stub is not None: + leave_delegate, forwarded = stub + if forwarded != name: + delegate_name = forwarded + move_before, move_after = _module_move_anchor(dst_tree, name, into_class) recipe.moves.append( { "name": name, @@ -626,10 +991,11 @@ def infer_recipe(commit: str, root: str) -> Recipe: "from_class": src_class, "dedent": src_indent - dst_indent, "dst_order": dst_def.lineno if dst_def else 0, - "before": _next_sibling_def_name(dst_tree, name, into_class), - "drop_self_annotation": _self_annotation_dropped( - rr._find_def(src_tree, name), dst_def - ), + "before": move_before, + "after": move_after, + "drop_self_annotation": _self_annotation_dropped(src_def, dst_def), + "leave_delegate": leave_delegate, + "delegate_name": delegate_name, } ) if src_class is not None: @@ -648,6 +1014,110 @@ def infer_recipe(commit: str, root: str) -> Recipe: recipe, files, name=name, src=src, dst=dst, commit=commit, root=root ) + # A method whose signature line never changed leaves no def-line in the removed set: + # the body was replaced by a forwarding stub in place while the full body landed in + # another file. Detect it from the destination's added def + the source's after-state + # delegate stub. + for name in sorted(def_names(all_added) - def_names(all_removed)): + dst = next((p for p, f in files.items() if name in def_names(f["added"])), None) + if dst is None or dst in new_files: + continue + src = None + stub_info = None + for p in files: + if p == dst: + continue + try: + after_tree = ast.parse(_git_output(["show", f"{commit}:{p}"], root)) + before_tree = ast.parse(_git_output(["show", f"{commit}^:{p}"], root)) + except Exception: + continue + stub = _delegate_stub_attr(after_tree, name) + if stub is None: + continue + full_before = rr._find_def(before_tree, name) + if full_before is None or _delegate_stub_attr(before_tree, name): + continue + src, stub_info = p, stub + break + if src is None: + continue + src_before = _git_output(["show", f"{commit}^:{src}"], root) + src_tree = ast.parse(src_before) + dst_tree = ast.parse(_git_output(["show", f"{commit}:{dst}"], root)) + src_class = _enclosing_class_of_def(src_tree, name) + dst_indent = _def_indent(files[dst]["added"], name) + into_class = ( + None if dst_indent == 0 else _enclosing_class_of_def(dst_tree, name) + ) + try: + src_def = rr._find_unique_def( + src_tree, name, from_class=src_class, where=src + ) + dst_def = rr._find_unique_def( + dst_tree, name, from_class=into_class, where=dst + ) + except AssertionError as exc: + recipe.supported = False + recipe.notes.append(f"{name}: cannot disambiguate moved def ({exc})") + continue + leave_delegate, forwarded = stub_info + move_before, move_after = _module_move_anchor(dst_tree, name, into_class) + recipe.moves.append( + { + "name": name, + "src": src, + "dst": dst, + "into_class": into_class, + "from_class": src_class, + "dedent": (src_def.col_offset or 0) - (dst_indent or 0), + "dst_order": dst_def.lineno if dst_def else 0, + "before": move_before, + "after": move_after, + "drop_self_annotation": _self_annotation_dropped(src_def, dst_def), + "leave_delegate": leave_delegate, + "delegate_name": forwarded if forwarded != name else None, + } + ) + + # A module-level constant that vanished from one changed file and appeared in another + # relocated with the moved code: realise it as a move_assign. + changed_paths = [p for p in files if p.endswith(".py")] + texts_before: dict = {} + texts_after: dict = {} + for p in changed_paths: + try: + texts_before[p] = ( + "" if files[p]["new"] else _git_output(["show", f"{commit}^:{p}"], root) + ) + texts_after[p] = _git_output(["show", f"{commit}:{p}"], root) + except Exception: + continue + for p_src in changed_paths: + if p_src not in texts_before: + continue + lost = _module_assign_names(texts_before[p_src]) - _module_assign_names( + texts_after.get(p_src, "") + ) + if not lost: + continue + for p_dst in changed_paths: + if p_dst == p_src or p_dst in new_files or p_dst not in texts_after: + continue + gained = _module_assign_names(texts_after[p_dst]) - _module_assign_names( + texts_before.get(p_dst, "") + ) + for cname in sorted(lost & gained): + dst_tree = ast.parse(texts_after[p_dst]) + recipe.assign_moves.append( + { + "name": cname, + "src": p_src, + "dst": p_dst, + "before": _next_sibling_assign_or_def(dst_tree, cname), + } + ) + # Module-level imports a file gained or lost are realised directly from the symmetric # base<->target diff: a gained name is added (the destination needs the moved code's # imports, or a caller of a moved free function gains one), a lost name is removed. An @@ -677,6 +1147,11 @@ def infer_recipe(commit: str, root: str) -> Recipe: if key not in before_tc: recipe.typechecking_additions.append({"path": path, "text": stmt}) + # An intra-file helper carved out of a sibling function's body (its block replaced by a + # call) is an extract_function -- inferred only when no cross-file move already explains it. + if not recipe.moves: + _infer_extract_functions(recipe, files, commit, root) + # A move source the commit deletes (its defs all relocated, leaving only scaffolding) is # removed after the moves; move_symbol only cuts defs, it does not delete the emptied file. move_srcs = {mv["src"] for mv in recipe.moves} @@ -684,7 +1159,12 @@ def infer_recipe(commit: str, root: str) -> Recipe: if f.get("deleted") and path in move_srcs: recipe.deletes.append(path) - if not recipe.moves and not recipe.extracts and not recipe.scatter_extracts: + if ( + not recipe.moves + and not recipe.extracts + and not recipe.scatter_extracts + and not recipe.extract_functions + ): recipe.supported = False if not recipe.notes: recipe.notes.append( @@ -745,6 +1225,34 @@ def _recipe_ops(recipe: Recipe) -> list: "dedent": mv["dedent"], "drop_self_annotation": mv["drop_self_annotation"], "before": mv.get("before"), + "after": mv.get("after"), + "leave_delegate": mv.get("leave_delegate"), + "delegate_name": mv.get("delegate_name"), + }, + ) + ) + for am in recipe.assign_moves: + ops.append( + ( + "move_assign", + (am["name"],), + {"src": am["src"], "dst": am["dst"], "before": am.get("before")}, + ) + ) + for ex in recipe.extract_functions: + ops.append( + ( + "extract_function", + (ex["src"], ex["dst"]), + { + "name": ex["name"], + "signature": ex["signature"], + "body": ex["body"], + "body_indent": ex["body_indent"], + "call": ex["call"], + "return_text": ex["return_text"], + "into_class": ex["into_class"], + "before": ex["before"], }, ) ) @@ -817,7 +1325,7 @@ def recipe_to_script(recipe: Recipe, subject: str) -> str: for method, args, kwargs in _recipe_ops(recipe): rendered = [repr(a) for a in args] + [f"{k}={v!r}" for k, v in kwargs.items()] lines.append(f"r.{method}(" + ", ".join(rendered) + ")") - lines += ["r.run()", ""] + lines += ["residual = r.run()", "sys.exit(1 if residual else 0)", ""] return "\n".join(lines) @@ -863,7 +1371,12 @@ def generate_range( recipe = infer_recipe(commit, root) script = recipe_to_script(recipe, subject) (scripts_dir / f"{commit[:9]}.py").write_text(script) - relocates = bool(recipe.moves or recipe.extracts or recipe.scatter_extracts) + relocates = bool( + recipe.moves + or recipe.extracts + or recipe.scatter_extracts + or recipe.extract_functions + ) supported = recipe.supported and relocates notes = recipe.notes if supported: @@ -1022,7 +1535,12 @@ def _main(argv: list[str]) -> int: recipe, _git_output(["log", "-1", "--format=%s", target], root) ) ) - relocates = bool(recipe.moves or recipe.extracts or recipe.scatter_extracts) + relocates = bool( + recipe.moves + or recipe.extracts + or recipe.scatter_extracts + or recipe.extract_functions + ) if not (recipe.supported and relocates): print("UNSUPPORTED: " + "; ".join(recipe.notes), file=sys.stderr) return 1 diff --git a/.claude/skills/mechanical-refactor-verify/scripts/mechanical_refactor_reproduction_cli.py b/.claude/skills/mechanical-refactor-verify/scripts/mechanical_refactor_reproduction_cli.py new file mode 100644 index 000000000..899561d42 --- /dev/null +++ b/.claude/skills/mechanical-refactor-verify/scripts/mechanical_refactor_reproduction_cli.py @@ -0,0 +1,537 @@ +"""Verify a whole mechanical-refactor chain: classification, proofs, and a full report. + +Every commit in ``base..branch`` must classify itself by carrying exactly one of the two +words ``mechanical_provable`` or ``non_mechanical_provable`` anywhere in its message (the +rest of the message format is free). Every ``mechanical_provable`` commit must ship a +proof script in the proof folder (``/repro_scripts/.py`` or a flat +``/.py``), and running the proof must PASS -- reproduce the commit +byte-for-byte. A ``non_mechanical_provable`` commit carries no machine proof and is left +to human review. + +The run prints a markdown report, writes it into the proof folder (``chain_report.md``), +and exits 0 iff the whole chain verifies. Normative contract: spec-reproduction-cli.md. + + python3 mechanical_refactor_reproduction_cli.py \ + --base --branch --proof path/to/proof/folder +""" + +import argparse +import hashlib +import json +import re +import subprocess +import sys +from concurrent.futures import ThreadPoolExecutor +from dataclasses import dataclass, field +from pathlib import Path + +_DEFAULT_JOBS = 3 +_PASSED_CACHE_FILENAME = "mechanical_refactor_passed_proofs.json" +_CACHED_PASS_DETAIL = "reused this machine's earlier PASS (--skip-passed)" + +KIND_MECHANICAL = "mechanical_provable" +KIND_NON_MECHANICAL = "non_mechanical_provable" + +VERDICT_PASS = "PASS" +VERDICT_FAIL = "FAIL" +VERDICT_MISSING_PROOF = "MISSING_PROOF" +VERDICT_AMBIGUOUS_PROOF = "AMBIGUOUS_PROOF" +VERDICT_HUMAN_REVIEW = "HUMAN_REVIEW" +VERDICT_UNCLASSIFIED = "UNCLASSIFIED" +VERDICT_AMBIGUOUS_KIND = "AMBIGUOUS_KIND" + +_OK_VERDICTS = (VERDICT_PASS, VERDICT_HUMAN_REVIEW) + +# The words are matched standalone: delimited by any non-[0-9A-Za-z_] character or the +# string boundary, so `non_mechanical_provable` never also counts as the bare word. +_KIND_WORD_RE = re.compile( + r"(? bool: + return self.verdict in _OK_VERDICTS + + +@dataclass(frozen=True) +class _PendingProof: + sha: str + subject: str + kind: str + script: Path + + +@dataclass(frozen=True) +class ChainResult: + base: str + branch: str + base_sha: str + branch_sha: str + proof_dir: Path + verdicts: "list[CommitVerdict]" = field(default_factory=list) + + @property + def passed(self) -> bool: + return bool(self.verdicts) and all(v.ok for v in self.verdicts) + + +def main(argv: "list[str]") -> int: + parser = argparse.ArgumentParser( + description="Verify a whole mechanical-refactor chain against its proof folder." + ) + parser.add_argument("--base", required=True, help="base commit of the chain") + parser.add_argument("--branch", required=True, help="PR branch name (chain tip)") + parser.add_argument("--proof", required=True, help="proof folder path") + parser.add_argument("--repo-root", default=None, help="repo root (default: cwd's)") + parser.add_argument( + "--report", + default=None, + help=f"report file path (default: /{_REPORT_FILENAME})", + ) + parser.add_argument( + "--jobs", + type=int, + default=_DEFAULT_JOBS, + help=f"max concurrent proof runs (default {_DEFAULT_JOBS})", + ) + parser.add_argument( + "--skip-passed", + action="store_true", + help="reuse this machine's earlier PASS verdicts for unchanged proofs", + ) + args = parser.parse_args(argv) + + try: + result = verify_chain( + base=args.base, + branch=args.branch, + proof=Path(args.proof), + repo_root=args.repo_root, + jobs=args.jobs, + skip_passed=args.skip_passed, + ) + except ChainVerificationError as exc: + print(f"error: {exc}", file=sys.stderr) + return 2 + + report = render_report(result) + report_path = ( + Path(args.report) if args.report else result.proof_dir / _REPORT_FILENAME + ) + report_path.write_text(report) + print(report) + print(f"report written to: {report_path}") + return 0 if result.passed else 1 + + +def verify_chain( + *, + base: str, + branch: str, + proof: Path, + repo_root: "str | None" = None, + jobs: int = _DEFAULT_JOBS, + skip_passed: bool = False, +) -> ChainResult: + """Classify every commit in ``base..branch`` and run every provable commit's proof. + + Classification and proof resolution are sequential (cheap); the proof runs execute + concurrently, up to ``jobs`` at a time — safe because each proof works in its own + throwaway worktree. The verdict list keeps chain order. With ``skip_passed``, a + pending proof whose (sha, script hash, utils hash) triple this machine already ran to + a PASS is reused instead of re-executed; every fresh PASS is recorded either way.""" + root = repo_root or _repo_root() + if not proof.is_dir(): + raise ChainVerificationError(f"proof folder does not exist: {proof}") + base_sha = _rev_parse(base, root) + branch_sha = _rev_parse(branch, root) + commits = _linear_commits(base_sha=base_sha, branch_sha=branch_sha, root=root) + + resolved: "list[CommitVerdict | _PendingProof]" = [] + for sha in commits: + subject = _git_output(["log", "-1", "--format=%s", sha], root).strip() + message = _git_output(["log", "-1", "--format=%B", sha], root) + resolved.append( + _resolve_commit(sha=sha, subject=subject, message=message, proof=proof) + ) + + cache_path = _passed_cache_path(root) + cache = _load_passed_cache(cache_path) + if skip_passed: + resolved = [_reuse_cached_pass(item, cache=cache) for item in resolved] + + pending_by_sha = { + item.sha: item for item in resolved if isinstance(item, _PendingProof) + } + verdicts: "list[CommitVerdict]" = _run_pending_proofs( + resolved=resolved, root=root, jobs=jobs + ) + _record_passes( + cache=cache, + cache_path=cache_path, + verdicts=verdicts, + pending_by_sha=pending_by_sha, + ) + return ChainResult( + base=base, + branch=branch, + base_sha=base_sha, + branch_sha=branch_sha, + proof_dir=proof, + verdicts=verdicts, + ) + + +def render_report(result: ChainResult) -> str: + """The full chain report as markdown: header, per-commit table, failure details.""" + n_mech = sum(1 for v in result.verdicts if v.kind == KIND_MECHANICAL) + n_non_mech = sum(1 for v in result.verdicts if v.kind == KIND_NON_MECHANICAL) + n_unclassified = sum(1 for v in result.verdicts if v.kind is None) + n_pass = sum(1 for v in result.verdicts if v.verdict == VERDICT_PASS) + n_cached = sum(1 for v in result.verdicts if v.cached) + + lines = [ + "# Mechanical refactor chain report", + "", + f"- base: `{result.base}` (`{result.base_sha[:12]}`)", + f"- branch: `{result.branch}` (`{result.branch_sha[:12]}`)", + f"- proof folder: `{result.proof_dir}`", + f"- chain verdict: **{'PASS' if result.passed else 'FAIL'}**", + f"- commits: {len(result.verdicts)} total — {n_mech} {KIND_MECHANICAL}, " + f"{n_non_mech} {KIND_NON_MECHANICAL}, {n_unclassified} classification error(s)", + f"- proofs: {n_pass}/{n_mech} PASS", + *( + [f"- reused from the passed-proof cache (--skip-passed): {n_cached}"] + if n_cached + else [] + ), + "", + "| # | commit | kind | verdict | subject |", + "|---|--------|------|---------|---------|", + ] + for i, v in enumerate(result.verdicts, start=1): + kind = v.kind or "?" + subject = v.subject.replace("|", "\\|") + lines.append(f"| {i} | `{v.sha[:9]}` | {kind} | {v.verdict} | {subject} |") + + failures = [v for v in result.verdicts if not v.ok] + if failures: + lines += ["", "## Failure details"] + for v in failures: + lines += [ + "", + f"### `{v.sha[:9]}` — {v.verdict}", + "", + v.detail or "(no detail)", + ] + return "\n".join(lines) + "\n" + + +def _reuse_cached_pass( + item: "CommitVerdict | _PendingProof", *, cache: dict +) -> "CommitVerdict | _PendingProof": + """Turn a pending proof into a cached PASS verdict on an exact cache-key match.""" + if not isinstance(item, _PendingProof): + return item + if cache.get("passed", {}).get(item.sha) != _proof_cache_key(item.script): + return item + print(f"proof {item.sha[:9]} {VERDICT_PASS} (cached)", flush=True) + return CommitVerdict( + sha=item.sha, + subject=item.subject, + kind=item.kind, + verdict=VERDICT_PASS, + detail=_CACHED_PASS_DETAIL, + cached=True, + ) + + +def _record_passes( + *, + cache: dict, + cache_path: Path, + verdicts: "list[CommitVerdict]", + pending_by_sha: "dict[str, _PendingProof]", +) -> None: + """Record every freshly-run PASS into the cache (a FAIL is never recorded).""" + fresh = [ + v + for v in verdicts + if v.verdict == VERDICT_PASS and not v.cached and v.sha in pending_by_sha + ] + if not fresh: + return + for v in fresh: + cache.setdefault("passed", {})[v.sha] = _proof_cache_key( + pending_by_sha[v.sha].script + ) + try: + cache_path.write_text(json.dumps(cache, indent=2, sort_keys=True) + "\n") + except OSError as exc: + print(f"note: could not write passed-proof cache {cache_path}: {exc}") + + +def _proof_cache_key(script: Path) -> "dict[str, str]": + """The cache key parts beyond the sha: hashes of the script and its utils module.""" + utils_sha256 = "" + for directory in (script.parent, script.parent.parent): + utils = directory / "mechanical_refactor_reproduction_utils.py" + if utils.is_file(): + utils_sha256 = hashlib.sha256(utils.read_bytes()).hexdigest() + break + return { + "script_sha256": hashlib.sha256(script.read_bytes()).hexdigest(), + "utils_sha256": utils_sha256, + } + + +def _passed_cache_path(root: str) -> Path: + common_dir = _git_output(["rev-parse", "--git-common-dir"], root).strip() + common = Path(common_dir) + if not common.is_absolute(): + common = Path(root) / common + return common / _PASSED_CACHE_FILENAME + + +def _load_passed_cache(path: Path) -> dict: + """The cache is best-effort: missing, corrupt, or unreadable means empty.""" + try: + data = json.loads(path.read_text()) + except (OSError, ValueError): + return {"passed": {}} + if not isinstance(data, dict) or not isinstance(data.get("passed"), dict): + return {"passed": {}} + return data + + +def _run_pending_proofs( + *, resolved: "list[CommitVerdict | _PendingProof]", root: str, jobs: int +) -> "list[CommitVerdict]": + """Execute the pending proofs on a bounded thread pool; keep chain order.""" + pending = [ + (i, item) for i, item in enumerate(resolved) if isinstance(item, _PendingProof) + ] + finished: "dict[int, CommitVerdict]" = {} + if pending: + with ThreadPoolExecutor(max_workers=max(1, jobs)) as pool: + futures = { + i: pool.submit(_proof_verdict, item, root=root) for i, item in pending + } + for i, future in futures.items(): + finished[i] = future.result() + return [ + finished[i] if isinstance(item, _PendingProof) else item + for i, item in enumerate(resolved) + ] + + +def _proof_verdict(pending: _PendingProof, *, root: str) -> CommitVerdict: + passed, output = _run_proof(script=pending.script, root=root) + if passed: + verdict = CommitVerdict( + sha=pending.sha, + subject=pending.subject, + kind=pending.kind, + verdict=VERDICT_PASS, + detail="", + ) + else: + tail = "\n".join(output.splitlines()[-_FAIL_OUTPUT_TAIL_LINES:]) + verdict = CommitVerdict( + sha=pending.sha, + subject=pending.subject, + kind=pending.kind, + verdict=VERDICT_FAIL, + detail=( + f"proof `{pending.script}` did not PASS; output tail:\n\n" + f"```\n{tail}\n```" + ), + ) + print(f"proof {pending.sha[:9]} {verdict.verdict}", flush=True) + return verdict + + +def _resolve_commit( + *, sha: str, subject: str, message: str, proof: Path +) -> "CommitVerdict | _PendingProof": + kind, classification_error = _classify(message) + if kind is None: + return CommitVerdict( + sha=sha, + subject=subject, + kind=None, + verdict=classification_error, + detail=( + f"the commit message must contain exactly one of the words " + f"`{KIND_MECHANICAL}` or `{KIND_NON_MECHANICAL}`" + ), + ) + if kind == KIND_NON_MECHANICAL: + return CommitVerdict( + sha=sha, + subject=subject, + kind=kind, + verdict=VERDICT_HUMAN_REVIEW, + detail="declared non_mechanical_provable: no machine proof, review by hand", + ) + + scripts = _find_proof_scripts(proof=proof, sha=sha) + if not scripts: + return CommitVerdict( + sha=sha, + subject=subject, + kind=kind, + verdict=VERDICT_MISSING_PROOF, + detail=( + f"no proof script found; searched `{proof / 'repro_scripts'}` and " + f"`{proof}` for `.py` (>= {_MIN_PROOF_STEM_LEN} hex chars)" + ), + ) + if len(scripts) > 1: + listing = ", ".join(f"`{p}`" for p in scripts) + return CommitVerdict( + sha=sha, + subject=subject, + kind=kind, + verdict=VERDICT_AMBIGUOUS_PROOF, + detail=f"multiple proof scripts match this commit: {listing}", + ) + + return _PendingProof(sha=sha, subject=subject, kind=kind, script=scripts[0]) + + +def _classify(message: str) -> "tuple[str | None, str]": + """The commit's declared kind, or (None, error-verdict) when the word rule is broken. + + Exactly one of the two words must appear (any number of times, but only one of the + two): zero occurrences is UNCLASSIFIED, both words present is AMBIGUOUS_KIND.""" + kinds = { + KIND_NON_MECHANICAL if match.group(1) else KIND_MECHANICAL + for match in _KIND_WORD_RE.finditer(message) + } + if not kinds: + return None, VERDICT_UNCLASSIFIED + if len(kinds) > 1: + return None, VERDICT_AMBIGUOUS_KIND + return kinds.pop(), "" + + +def _find_proof_scripts(*, proof: Path, sha: str) -> "list[Path]": + """Proof scripts naming this commit: a ``.py`` (lowercase hex, >= 7 chars) + under ``/repro_scripts/`` or flat in ``/``.""" + found: "list[Path]" = [] + for directory in (proof / "repro_scripts", proof): + if not directory.is_dir(): + continue + for path in sorted(directory.glob("*.py")): + stem = path.stem + is_sha_prefix = ( + len(stem) >= _MIN_PROOF_STEM_LEN + and all(c in "0123456789abcdef" for c in stem) + and sha.startswith(stem) + ) + if is_sha_prefix: + found.append(path) + return found + + +def _run_proof(*, script: Path, root: str) -> "tuple[bool, str]": + """Run one proof script from the repo root. A PASS is exit code 0 AND the arbiter's + ``PASS:`` verdict line on stdout (an old-style script that exits 0 with a residual is + therefore still a FAIL).""" + result = subprocess.run( + [sys.executable, str(script.resolve())], + cwd=root, + capture_output=True, + text=True, + ) + output = result.stdout + result.stderr + passed = result.returncode == 0 and bool(_PASS_LINE_RE.search(result.stdout)) + return passed, output + + +def _linear_commits(*, base_sha: str, branch_sha: str, root: str) -> "list[str]": + if not _is_ancestor(base_sha=base_sha, branch_sha=branch_sha, root=root): + raise ChainVerificationError( + f"base {base_sha[:12]} is not an ancestor of branch {branch_sha[:12]}" + ) + commits = _git_output( + ["rev-list", "--reverse", f"{base_sha}..{branch_sha}"], root + ).split() + if not commits: + raise ChainVerificationError( + f"no commits in {base_sha[:12]}..{branch_sha[:12]}" + ) + merges = [ + sha + for sha in commits + if len(_git_output(["rev-list", "--parents", "-n", "1", sha], root).split()) > 2 + ] + if merges: + listing = ", ".join(sha[:9] for sha in merges) + raise ChainVerificationError( + f"the chain must be linear, but it contains merge commit(s): {listing}" + ) + return commits + + +def _is_ancestor(*, base_sha: str, branch_sha: str, root: str) -> bool: + result = subprocess.run( + ["git", "merge-base", "--is-ancestor", base_sha, branch_sha], + cwd=root, + capture_output=True, + ) + return result.returncode == 0 + + +def _rev_parse(ref: str, root: str) -> str: + result = subprocess.run( + ["git", "rev-parse", "--verify", f"{ref}^{{commit}}"], + cwd=root, + capture_output=True, + text=True, + ) + if result.returncode != 0: + raise ChainVerificationError(f"cannot resolve {ref!r}: {result.stderr.strip()}") + return result.stdout.strip() + + +def _git_output(args: "list[str]", root: str) -> str: + result = subprocess.run( + ["git", *args], cwd=root, capture_output=True, text=True, check=True + ) + return result.stdout + + +def _repo_root() -> str: + return subprocess.run( + ["git", "rev-parse", "--show-toplevel"], + capture_output=True, + text=True, + check=True, + ).stdout.strip() + + +if __name__ == "__main__": + sys.exit(main(sys.argv[1:])) diff --git a/.claude/skills/mechanical-refactor-verify/scripts/mechanical_refactor_reproduction_utils.py b/.claude/skills/mechanical-refactor-verify/scripts/mechanical_refactor_reproduction_utils.py index 972d1c968..fb0284dba 100644 --- a/.claude/skills/mechanical-refactor-verify/scripts/mechanical_refactor_reproduction_utils.py +++ b/.claude/skills/mechanical-refactor-verify/scripts/mechanical_refactor_reproduction_utils.py @@ -150,9 +150,10 @@ def _find_def(tree: ast.AST, name: str) -> ast.AST | None: def _find_unique_def( tree: ast.AST, name: str, *, from_class: str | None = None, where: str ) -> ast.AST: - """Resolve ``def name`` and refuse ambiguity: with same-named defs in scope the - first-match lookup could silently cut the wrong body, so the caller must scope the - search with ``from_class``.""" + """Resolve ``def name`` (or ``class name``) and refuse ambiguity: with same-named defs in + scope the first-match lookup could silently cut the wrong body, so the caller must scope + the search with ``from_class``.""" + definition = (ast.FunctionDef, ast.AsyncFunctionDef, ast.ClassDef) root: ast.AST = tree if from_class is not None: cls = _find_class(tree, from_class) @@ -162,16 +163,14 @@ def _find_unique_def( top_level = [ node for node in tree.body - if isinstance(node, (ast.FunctionDef, ast.AsyncFunctionDef)) - and node.name == name + if isinstance(node, definition) and node.name == name ] if len(top_level) == 1: return top_level[0] matches = [ node for node in ast.walk(root) - if isinstance(node, (ast.FunctionDef, ast.AsyncFunctionDef)) - and node.name == name + if isinstance(node, definition) and node.name == name ] assert matches, f"{name} not found in {where}" assert ( @@ -209,6 +208,19 @@ def _def_span(node: ast.AST) -> tuple[int, int]: return start, node.end_lineno +def _symbol_named(node: ast.AST, name: str) -> bool: + """Whether a top-level statement defines the symbol ``name`` -- a def/class by its name, + or a module-level assignment by one of its target names (so ``_is_hip = is_hip()`` is + found by ``_is_hip``).""" + if isinstance(node, (ast.FunctionDef, ast.AsyncFunctionDef, ast.ClassDef)): + return node.name == name + if isinstance(node, ast.AnnAssign): + return isinstance(node.target, ast.Name) and node.target.id == name + if isinstance(node, ast.Assign): + return any(isinstance(t, ast.Name) and t.id == name for t in node.targets) + return False + + def _byte_slice(line: str, start: int | None, end: int | None) -> str: """Slice a line by UTF-8 byte offsets -- ast col_offsets count bytes, not characters.""" return line.encode("utf-8")[start:end].decode("utf-8") @@ -340,13 +352,20 @@ def _multiline_string_interior_lines(top_level_text: str) -> set[int]: def _audit_extract_header( - header: str, removed_assigns: dict[str, str | None], where: str + header: str, + removed_assigns: dict[str, str | None], + where: str, + rederivable: dict[str, str | None] | None = None, ) -> None: """Refuse header content the extraction cannot vouch for. The header of a scattered extraction is authored text reproduced from the target commit, so anything beyond - imports, a TYPE_CHECKING import block, a logger, or a byte-equivalent copy of an - assignment deleted from the source would let arbitrary new code ride into the new + imports, a TYPE_CHECKING import block, a logger, a byte-equivalent copy of an + assignment deleted from the source (``removed_assigns``), or a byte-equivalent copy of + a module constant that *survives* in the source (``rederivable`` -- re-derived + boilerplate such as ``_is_hip = is_hip()``, provably not fiction because the same + statement still exists in the source) would let arbitrary new code ride into the new module under a PASS verdict.""" + rederivable = rederivable or {} header_assigned: set[str] = set() for stmt in ast.parse(header).body: if isinstance(stmt, (ast.Import, ast.ImportFrom)): @@ -374,6 +393,10 @@ def _audit_extract_header( ): header_assigned.update(names) continue + if names and all( + n in rederivable and rederivable[n] == value_src for n in names + ): + continue raise AssertionError( f"unverifiable header statement in {where}: {ast.unparse(stmt)!r} is " f"neither scaffolding nor a relocated source assignment" @@ -455,6 +478,44 @@ class Repro: self.ops.append(op) return self + def route_call_sites_through_field( + self, name: str, *, field: str, paths: list[str], owner: str | None = None + ) -> "Repro": + """Rewrite ``.name(args)`` to ``.field.name(args)`` -- the method moved + onto a collaborator reached through ``self.field``, so its callers route through that + field. With ``owner`` given, only calls whose receiver text equals ``owner`` are + rewritten. A call already routed through ``field`` is skipped, so the pass converges. + """ + + def op(root: Path) -> None: + for rel in paths: + path = root / rel + + def predicate(node: ast.Call) -> bool: + return ( + isinstance(node.func, ast.Attribute) + and node.func.attr == name + and not ( + isinstance(node.func.value, ast.Attribute) + and node.func.value.attr == field + ) + and (owner is None or ast.unparse(node.func.value) == owner) + ) + + def rewrite(text: str, node: ast.Call) -> str: + call_src = _node_slice(text, node) + func_src = _node_slice(text, node.func) + receiver_src = _node_slice(text, node.func.value) + return receiver_src + f".{field}.{name}" + call_src[len(func_src) :] + + _write_source( + path, + _rewrite_matching_calls(_read_source(path), predicate, rewrite), + ) + + self.ops.append(op) + return self + def remove_import( self, rel: str, import_text: str, *, in_function: str | None = None ) -> "Repro": @@ -546,7 +607,13 @@ class Repro: return self def remove_imported_name( - self, rel: str, *, module: str | None, name: str, asname: str | None = None + self, + rel: str, + *, + module: str | None, + name: str, + asname: str | None = None, + keep_exploded: bool = False, ) -> "Repro": """Drop a single imported ``name`` from a module-level import: from a ``from module import a, b`` keep the rest and drop only ``name``; when it was the sole name -- or for @@ -554,6 +621,12 @@ class Repro: home changed, so an importer that no longer references it loses exactly that name; the import sorter rewrites the surviving line. An import diff is always whitelisted, so this realises a lost name directly instead of relying on the formatter to prune it. + + Removing down to a single surviving name collapses the import to one line by default + (the common case). Pass ``keep_exploded`` when the target kept the sole survivor + exploded (its magic trailing comma preserved): the alias line is then merely deleted + so the surviving name keeps its comma and the formatter leaves the import multi-line. + The choice is the commit author's and cannot be inferred from the source. """ def alias_text(alias: ast.alias) -> str: @@ -584,16 +657,26 @@ class Repro: edits.append((node.lineno, node.end_lineno, None)) continue stmt_lines = lines[node.lineno - 1 : node.end_lineno] - if any("#" in ln for ln in stmt_lines): - own = dropped_alias.lineno - own_line = lines[own - 1] - assert own_line.strip().rstrip(",").strip() == alias_text( - dropped_alias - ), ( + own = dropped_alias.lineno + own_line = lines[own - 1] + on_own_line = own_line.strip().rstrip(",").strip() == alias_text( + dropped_alias + ) + has_comments = any("#" in ln for ln in stmt_lines) + # Preserve the exploded form -- delete just this alias's line -- when the + # import stays multi-line: 2+ surviving names keep the magic trailing comma + # exploded, and an import carrying comments must not be rebuilt (a rebuild + # would drop them). Both match how the target was edited (a flat rebuild + # would drop the magic comma and collapse an import the target left + # multi-line). A lone surviving name collapses to one line by default, unless + # keep_exploded says the target preserved the magic comma for it too. + if on_own_line and (len(kept) >= 2 or has_comments or keep_exploded): + edits.append((own, own, None)) + elif has_comments and not on_own_line: + raise AssertionError( f"cannot drop {name!r}: it shares a line with other text and " f"the import holds comments that a rebuild would delete" ) - edits.append((own, own, None)) else: keyword = "import " if module is None else f"from {module} import " rebuilt = keyword + ", ".join(alias_text(a) for a in kept) + nl @@ -609,15 +692,81 @@ class Repro: self.ops.append(op) return self - def add_import(self, rel: str, import_stmt: str) -> "Repro": + def add_imported_name( + self, rel: str, *, module: str, name: str, asname: str | None = None + ) -> "Repro": + """Add a single ``name`` to an existing module-level ``from module import a, b`` -- + the dual of ``remove_imported_name``. A relocated symbol gains a new importer that + already imports other names from the same module, so the target extends that line + rather than adding a fresh statement (which the sorter would not merge across an + intervening non-import statement). The import sorter rewrites the surviving line; an + import carrying comments is refused, since a rebuild would drop them.""" + + def alias_text(target_name: str, target_asname: str | None) -> str: + return target_name + (f" as {target_asname}" if target_asname else "") + + def op(root: Path) -> None: + path = root / rel + lines = _split_keepends(_read_source(path)) + nl = _newline_style("".join(lines)) + for node in ast.parse("".join(lines)).body: + if not isinstance(node, ast.ImportFrom): + continue + if "." * node.level + (node.module or "") != module: + continue + stmt_lines = lines[node.lineno - 1 : node.end_lineno] + if any("#" in ln for ln in stmt_lines): + raise AssertionError( + f"cannot add {name!r} to the import from {module!r} in {rel}: " + f"it holds comments that a rebuild would delete" + ) + existing = [alias_text(a.name, a.asname) for a in node.names] + added = alias_text(name, asname) + assert ( + added not in existing + ), f"{name!r} already imported from {module!r} in {rel}" + rebuilt = f"from {module} import " + ", ".join(existing + [added]) + nl + lines[node.lineno - 1 : node.end_lineno] = [rebuilt] + _write_source(path, "".join(lines)) + return + raise AssertionError(f"no `from {module} import` statement in {rel}") + + self.ops.append(op) + return self + + def add_import( + self, rel: str, import_stmt: str, *, after: str | None = None + ) -> "Repro": """Append an import after the last top-level import; the formatter's import sorter - places it (so the exact insertion point does not matter).""" + places it (so the exact insertion point does not matter). When ``after`` is given, + insert immediately after the top-level import statement whose source text contains + that substring instead -- needed for a file whose imports are split into separate + isort sections by an intervening statement (e.g. ``_is_hip = is_hip()``), where the + sorter will not carry the new import across the boundary into the intended block. + """ def op(root: Path) -> None: path = root / rel lines = _split_keepends(_read_source(path)) nl = _newline_style("".join(lines)) body = ast.parse("".join(lines)).body + if after is not None: + anchor = None + for node in body: + if isinstance( + node, (ast.Import, ast.ImportFrom) + ) and after in "".join(lines[node.lineno - 1 : node.end_lineno]): + anchor = node + break + if anchor is None: + raise AssertionError( + f"no top-level import containing {after!r} in {rel}" + ) + at = anchor.end_lineno + _write_source( + path, "".join(lines[:at] + [import_stmt + nl] + lines[at:]) + ) + return last = 0 if ( body @@ -639,24 +788,53 @@ class Repro: def add_typechecking_import(self, rel: str, import_stmt: str) -> "Repro": """Append ``import_stmt`` inside the file's ``if TYPE_CHECKING:`` block -- a moved definition whose annotations reference a type needs that type imported there. The - import sorter orders the block, so the exact insertion point does not matter.""" + import sorter orders the block, so the exact insertion point does not matter. A lone + ``pass`` placeholder (the block's only statement) is dropped: populating an empty + ``TYPE_CHECKING`` block makes its placeholder redundant, so the target removes it. + With no existing block, one is created after the trailing module import -- the + destination gains the guard together with its first import. + """ def op(root: Path) -> None: path = root / rel lines = _split_keepends(_read_source(path)) + nl = _newline_style("".join(lines)) for node in ast.parse("".join(lines)).body: if isinstance(node, ast.If) and ast.unparse(node.test) in ( "TYPE_CHECKING", "typing.TYPE_CHECKING", ): indent = " " * node.body[0].col_offset - at = node.body[-1].end_lineno - lines.insert( - at, indent + import_stmt + _newline_style("".join(lines)) + lone_pass = len(node.body) == 1 and isinstance( + node.body[0], ast.Pass ) + if lone_pass: + placeholder = node.body[0] + lines[placeholder.lineno - 1 : placeholder.end_lineno] = [ + indent + import_stmt + nl + ] + else: + lines.insert( + node.body[-1].end_lineno, indent + import_stmt + nl + ) _write_source(path, "".join(lines)) return - raise AssertionError(f"no `if TYPE_CHECKING:` block in {rel}") + tree = ast.parse("".join(lines)) + imports = [ + node + for node in tree.body + if isinstance(node, (ast.Import, ast.ImportFrom)) + ] + assert ( + imports + ), f"no imports to anchor a new `if TYPE_CHECKING:` block in {rel}" + insert_at = imports[-1].end_lineno + lines[insert_at:insert_at] = [ + nl, + "if TYPE_CHECKING:" + nl, + " " + import_stmt + nl, + ] + _write_source(path, "".join(lines)) self.ops.append(op) return self @@ -697,6 +875,80 @@ class Repro: self.ops.append(op) return self + def move_assign( + self, + name: str, + *, + src: str, + dst: str, + before: str | None = None, + ) -> "Repro": + """Cut the module-level assignment binding ``name`` from ``src`` and paste it verbatim + into ``dst`` at module level -- a module constant relocated together with the code + that reads it. Pasted immediately above the top-level statement named ``before`` + when given, else after the last top-level import.""" + + def op(root: Path) -> None: + src_path = root / src + dst_path = root / dst + src_lines = _split_keepends(_read_source(src_path)) + node = None + for cand in ast.parse("".join(src_lines)).body: + if ( + isinstance(cand, ast.Assign) + and len(cand.targets) == 1 + and isinstance(cand.targets[0], ast.Name) + and cand.targets[0].id == name + ) or ( + isinstance(cand, ast.AnnAssign) + and isinstance(cand.target, ast.Name) + and cand.target.id == name + ): + node = cand + assert node is not None, f"module assignment {name} not found in {src}" + block = "".join(src_lines[node.lineno - 1 : node.end_lineno]) + _write_source( + src_path, + "".join(src_lines[: node.lineno - 1] + src_lines[node.end_lineno :]), + ) + + dst_lines = _split_keepends(_read_source(dst_path)) + dst_nl = _newline_style("".join(dst_lines)) + dst_tree = ast.parse("".join(dst_lines)) + at = None + if before is not None: + for cand in dst_tree.body: + cand_name = getattr(cand, "name", None) or ( + cand.targets[0].id + if isinstance(cand, ast.Assign) + and len(cand.targets) == 1 + and isinstance(cand.targets[0], ast.Name) + else None + ) + if cand_name == before: + at = ( + min( + [d.lineno for d in getattr(cand, "decorator_list", [])], + default=cand.lineno, + ) + - 1 + ) + break + assert at is not None, f"before={before!r} not found in {dst}" + dst_lines[at:at] = [block, dst_nl] + else: + imports = [ + n + for n in dst_tree.body + if isinstance(n, (ast.Import, ast.ImportFrom)) + ] + at = imports[-1].end_lineno if imports else 0 + dst_lines[at:at] = [dst_nl, block] + _write_source(dst_path, "".join(dst_lines)) + + self.ops.append(op) + return self + def move_symbol( self, name: str, @@ -708,16 +960,23 @@ class Repro: dedent: int = 0, drop_self_annotation: bool = False, before: str | None = None, + after: str | None = None, leave_delegate: str | None = None, delegate_name: str | None = None, ) -> "Repro": """Cut ``def name`` (with decorators) from ``src`` and paste it into ``dst`` -- immediately above the sibling def ``before`` when given (so the relocated def lands in - the chain's order), else at the end of ``into_class`` (or module level when None) -- - dropping a move decorator and dedenting by ``dedent``. When ``drop_self_annotation``, - the moved method's ``self: Target`` annotation is dropped (redundant inside the class). - The body is moved verbatim; the formatter normalises the surrounding blank lines. + the chain's order), immediately below the top-level symbol ``after`` when given (a + sibling def/class or a module-level assignment target -- used to land the def just + before a following ``if TYPE_CHECKING:`` guard, which is not a nameable anchor), else + at the end of ``into_class`` (or module level when None) -- dropping a move decorator + and dedenting by ``dedent``. When ``drop_self_annotation``, the moved method's + ``self: Target`` annotation is dropped (redundant inside the class). The body is moved + verbatim; the formatter normalises the surrounding blank lines. """ + assert ( + before is None or after is None + ), "move_symbol: before and after are mutually exclusive" def op(root: Path) -> None: src_path = root / src @@ -731,10 +990,20 @@ class Repro: block = src_lines[start - 1 : end] decorator_lines = node.lineno - start if leave_delegate is not None: - assert not any( - ln.strip() in _MOVE_DECORATORS for ln in block[:decorator_lines] - ), f"leave_delegate on a {_MOVE_DECORATORS} method has no self to forward" args = node.args + has_move_decorator = any( + ln.strip() in _MOVE_DECORATORS for ln in block[:decorator_lines] + ) + arg_list = args.posonlyargs + args.args + self_annotated = ( + bool(arg_list) + and arg_list[0].arg == "self" + and arg_list[0].annotation is not None + ) + assert not has_move_decorator or self_annotated, ( + f"leave_delegate on a {_MOVE_DECORATORS} method has no self to " + "forward (a de-self'd staticmethod must annotate its self param)" + ) parts = [p.arg for p in args.posonlyargs + args.args if p.arg != "self"] if args.vararg is not None: parts.append(f"*{args.vararg.arg}") @@ -750,7 +1019,27 @@ class Repro: - 1 + _def_header_end("".join(src_lines[node.lineno - 1 : end])) ) - signature = src_lines[start - 1 : header_end] + sig_start = node.lineno - 1 if has_move_decorator else start - 1 + signature_text = "".join(src_lines[sig_start:header_end]) + # The stub drops the self annotation only when it names the class the + # def moved into (now redundant); an unrelated annotation (a mixin's + # `self: ModelRunner`) is part of the surviving header and stays. + ann = arg_list[0].annotation if self_annotated else None + ann_name = None + if isinstance(ann, ast.Name): + ann_name = ann.id + elif isinstance(ann, ast.Constant) and isinstance(ann.value, str): + ann_name = ann.value.split(".")[-1] + elif isinstance(ann, ast.Attribute): + ann_name = ann.attr + if self_annotated and ann_name == into_class: + sig_indent = len(signature_text) - len(signature_text.lstrip(" ")) + parsable = signature_text + " " * sig_indent + " pass" + src_nl + stripped = _drop_self_annotation(parsable, name) + assert stripped.endswith(" " * sig_indent + " pass" + src_nl) + signature_text = stripped[ + : -len(" " * sig_indent + " pass" + src_nl) + ] body_indent = " " * node.body[0].col_offset returning = ( "return await" @@ -761,7 +1050,7 @@ class Repro: f"{body_indent}{returning} self.{leave_delegate}." f"{delegate_name or name}({', '.join(parts)})" + src_nl ) - delegate = "".join(signature) + forward + delegate = signature_text + forward _write_source( src_path, "".join(src_lines[: start - 1] + [delegate] + src_lines[end:]), @@ -810,7 +1099,18 @@ class Repro: None, ) assert target is not None, f"before={before!r} not found in {dst}" - if target is not None: + if after is not None: + anchor = next( + (n for n in container if _symbol_named(n, after)), + None, + ) + assert anchor is not None, f"after={after!r} not found in {dst}" + at = anchor.end_lineno + _write_source( + dst_path, + "".join(dst_lines[:at] + [dst_nl, method_text] + dst_lines[at:]), + ) + elif target is not None: at = _def_span(target)[0] - 1 _write_source( dst_path, @@ -992,8 +1292,23 @@ class Repro: assert ( found_assigns == dropped ), f"{dropped - found_assigns} not assigned in {src}" + rederivable: dict[str, str | None] = {} + for node in tree.body: + targets = ( + node.targets + if isinstance(node, ast.Assign) + else [node.target] if isinstance(node, ast.AnnAssign) else [] + ) + names = [t.id for t in targets if isinstance(t, ast.Name)] + if not names or set(names) & dropped: + continue + value_src = ast.unparse(node.value) if node.value is not None else None + for kept_name in names: + rederivable[kept_name] = value_src if header.strip() or removed_assigns: - _audit_extract_header(header, removed_assigns, where=dst) + _audit_extract_header( + header, removed_assigns, where=dst, rederivable=rederivable + ) cuts = [(start, end, None) for start, end in spans.values()] cuts += [(start, end, None) for start, end in assign_spans] cuts += assign_rewrites @@ -1130,8 +1445,15 @@ class Repro: def delete_file(self, path: str) -> "Repro": """Delete a source module that its symbols' relocation left empty (the chain deletes the leftover scaffolding-only file). Run after the moves that empty it. Refuses a - file that still holds anything beyond a docstring, imports, or a TYPE_CHECKING - block -- deleting live code is not a relocation.""" + file that still holds anything beyond a docstring, imports, a TYPE_CHECKING block, or + a bare module ``logger`` -- deleting live code is not a relocation.""" + + def is_module_logger(stmt: ast.stmt) -> bool: + return ( + isinstance(stmt, ast.Assign) + and stmt.value is not None + and ast.unparse(stmt.value) == "logging.getLogger(__name__)" + ) def op(root: Path) -> None: target = root / path @@ -1152,6 +1474,7 @@ class Repro: and ast.unparse(stmt.test) in ("TYPE_CHECKING", "typing.TYPE_CHECKING") ) + or is_module_logger(stmt) ) ] assert not leftover, ( diff --git a/.claude/skills/mechanical-refactor-verify/scripts/tests/proof_generator/test_infer_extract_functions.py b/.claude/skills/mechanical-refactor-verify/scripts/tests/proof_generator/test_infer_extract_functions.py new file mode 100644 index 000000000..1ab6889d1 --- /dev/null +++ b/.claude/skills/mechanical-refactor-verify/scripts/tests/proof_generator/test_infer_extract_functions.py @@ -0,0 +1,322 @@ +import subprocess +import sys +from pathlib import Path + +import pytest + +sys.path.insert(0, str(Path(__file__).resolve().parents[2])) + +from generator_testlib import _commit, _git, _write # noqa: F401 +from mechanical_refactor_proof_generator import ( + build_repro, + infer_recipe, + recipe_to_script, +) + + +def test_infer_extract_function_with_returned_local(repo: Path) -> None: + """A block ending in ``pool = make(...)`` carved into a helper that returns ``pool`` infers + an extract_function whose body is the verbatim block and whose return_text is authored. + """ + _write( + repo, + **{ + "kv.py": ( + "class C:\n" + " def dispatch(self, n):\n" + " base = self.setup()\n" + " if self.flag:\n" + " x = self.a\n" + " y = x + n\n" + " pool = make(\n" + " a=x,\n" + " b=y,\n" + " )\n" + " return pool\n" + "\n" + " def keep(self):\n" + " return 0\n" + ) + }, + ) + _commit(repo, "base") + _write( + repo, + **{ + "kv.py": ( + "class C:\n" + " def dispatch(self, n):\n" + " base = self.setup()\n" + " if self.flag:\n" + " pool = self._build_pool(n=n)\n" + " return pool\n" + "\n" + " def _build_pool(self, *, n):\n" + " x = self.a\n" + " y = x + n\n" + " pool = make(\n" + " a=x,\n" + " b=y,\n" + " )\n" + " return pool\n" + "\n" + " def keep(self):\n" + " return 0\n" + ) + }, + ) + _commit(repo, "extract _build_pool from dispatch") + recipe = infer_recipe("HEAD", str(repo)) + assert recipe.supported + assert recipe.moves == [] + assert len(recipe.extract_functions) == 1 + ex = recipe.extract_functions[0] + assert ex["name"] == "_build_pool" + assert ex["src"] == "kv.py" and ex["dst"] == "kv.py" + assert ex["into_class"] == "C" + assert ex["before"] == "keep" + assert ex["body_indent"] == 12 + assert ex["body"] == ( + " x = self.a\n" + " y = x + n\n" + " pool = make(\n" + " a=x,\n" + " b=y,\n" + " )\n" + ) + assert ex["call"] == " pool = self._build_pool(n=n)\n" + assert ex["return_text"] == " return pool" + assert ex["signature"] == " def _build_pool(self, *, n):\n" + + +def test_infer_extract_function_keeps_leading_comment_in_body(repo: Path) -> None: + """A block whose first line is a comment extracts with that comment in the body, not + absorbed into the authored signature (which is the def header through its colon only). + """ + _write( + repo, + **{ + "kv.py": ( + "class C:\n" + " def dispatch(self, n):\n" + " if self.flag:\n" + " # pick the pool class for this backend\n" + " cls = PoolA\n" + " pool = cls(n)\n" + " return pool\n" + ) + }, + ) + _commit(repo, "base") + _write( + repo, + **{ + "kv.py": ( + "class C:\n" + " def dispatch(self, n):\n" + " if self.flag:\n" + " pool = self._build_pool(n=n)\n" + " return pool\n" + "\n" + " def _build_pool(self, *, n):\n" + " # pick the pool class for this backend\n" + " cls = PoolA\n" + " pool = cls(n)\n" + " return pool\n" + ) + }, + ) + commit = _commit(repo, "extract _build_pool with a leading comment") + recipe = infer_recipe(commit, str(repo)) + assert len(recipe.extract_functions) == 1 + ex = recipe.extract_functions[0] + assert ex["signature"] == " def _build_pool(self, *, n):\n" + assert ex["body"].lstrip().startswith("# pick the pool class") + assert build_repro(recipe, repo_root=str(repo)).run() == "" + + +def test_infer_extract_function_no_return_text_when_body_is_whole_helper( + repo: Path, +) -> None: + """When the helper body reproduces the source block with no trailing return, return_text + is None (the block is a side-effecting statement sequence, not a value producer).""" + _write( + repo, + **{ + "kv.py": ( + "class C:\n" + " def run(self):\n" + " self.pre()\n" + " self.log(1)\n" + " self.log(2)\n" + " self.post()\n" + ) + }, + ) + _commit(repo, "base") + _write( + repo, + **{ + "kv.py": ( + "class C:\n" + " def run(self):\n" + " self.pre()\n" + " self._emit()\n" + " self.post()\n" + "\n" + " def _emit(self):\n" + " self.log(1)\n" + " self.log(2)\n" + ) + }, + ) + _commit(repo, "extract _emit from run") + recipe = infer_recipe("HEAD", str(repo)) + assert recipe.supported + assert len(recipe.extract_functions) == 1 + ex = recipe.extract_functions[0] + assert ex["name"] == "_emit" + assert ex["return_text"] is None + assert ex["call"] == " self._emit()\n" + + +def test_infer_extract_function_edited_body_does_not_pass(repo: Path) -> None: + """A helper whose body was edited (not a verbatim cut) never yields a false pass: the + reproduction's byte-diff surfaces the bundled change as a non-empty residual.""" + _write( + repo, + **{ + "kv.py": ( + "class C:\n" + " def run(self):\n" + " self.pre()\n" + " self.log(1)\n" + " self.post()\n" + ) + }, + ) + _commit(repo, "base") + _write( + repo, + **{ + "kv.py": ( + "class C:\n" + " def run(self):\n" + " self.pre()\n" + " self._emit()\n" + " self.post()\n" + "\n" + " def _emit(self):\n" + " self.log(2)\n" + ) + }, + ) + commit = _commit(repo, "extract _emit but change the arg") + recipe = infer_recipe(commit, str(repo)) + residual = build_repro(recipe, repo_root=str(repo)).run() + assert residual != "" + + +def test_infer_extract_function_when_block_and_call_share_closing_paren( + repo: Path, +) -> None: + """The removed block and its replacement call both end in a lone ``)``; the prefix/suffix + split must not absorb that shared line, or the extracted body loses its final line. + """ + _write( + repo, + **{ + "kv.py": ( + "class C:\n" + " def dispatch(self, n):\n" + " if self.flag:\n" + " pool = make_pool(\n" + " a=n,\n" + " b=self.b,\n" + " )\n" + " return pool\n" + ) + }, + ) + _commit(repo, "base") + _write( + repo, + **{ + "kv.py": ( + "class C:\n" + " def dispatch(self, n):\n" + " if self.flag:\n" + " pool = self._build_pool(\n" + " n=n,\n" + " )\n" + " return pool\n" + "\n" + " def _build_pool(self, *, n):\n" + " pool = make_pool(\n" + " a=n,\n" + " b=self.b,\n" + " )\n" + " return pool\n" + ) + }, + ) + commit = _commit(repo, "extract _build_pool") + recipe = infer_recipe(commit, str(repo)) + assert len(recipe.extract_functions) == 1 + ex = recipe.extract_functions[0] + assert ex["body"].rstrip().endswith(")") + assert ex["return_text"] == " return pool" + assert build_repro(recipe, repo_root=str(repo)).run() == "" + + +def test_emitted_script_passes_on_extract_function(repo: Path, tmp_path: Path) -> None: + """The recipe for an extract_function reproduces the commit byte-for-byte (bare repo, no + formatter) so build_repro returns an empty residual.""" + _write( + repo, + **{ + "kv.py": ( + "class C:\n" + " def dispatch(self, n):\n" + " base = self.setup()\n" + " if self.flag:\n" + " x = self.a\n" + " pool = make(\n" + " a=x,\n" + " )\n" + " return pool\n" + "\n" + " def keep(self):\n" + " return 0\n" + ) + }, + ) + _commit(repo, "base") + _write( + repo, + **{ + "kv.py": ( + "class C:\n" + " def dispatch(self, n):\n" + " base = self.setup()\n" + " if self.flag:\n" + " pool = self._build_pool(n=n)\n" + " return pool\n" + "\n" + " def _build_pool(self, *, n):\n" + " x = self.a\n" + " pool = make(\n" + " a=x,\n" + " )\n" + " return pool\n" + "\n" + " def keep(self):\n" + " return 0\n" + ) + }, + ) + commit = _commit(repo, "extract _build_pool from dispatch") + recipe = infer_recipe(commit, str(repo)) + residual = build_repro(recipe, repo_root=str(repo)).run() + assert residual == "", residual + assert "extract_function" in recipe_to_script(recipe, "extract") diff --git a/.claude/skills/mechanical-refactor-verify/scripts/tests/proof_generator/test_infer_moves.py b/.claude/skills/mechanical-refactor-verify/scripts/tests/proof_generator/test_infer_moves.py index ada63842b..0b9e5ead4 100644 --- a/.claude/skills/mechanical-refactor-verify/scripts/tests/proof_generator/test_infer_moves.py +++ b/.claude/skills/mechanical-refactor-verify/scripts/tests/proof_generator/test_infer_moves.py @@ -38,6 +38,56 @@ def test_infer_recipe_method_onto_class(repo: Path) -> None: assert recipe.import_additions == [] +def test_infer_recipe_move_before_typechecking_uses_after_anchor(repo: Path) -> None: + """A module-level def relocated to land just above an ``if TYPE_CHECKING:`` guard cannot + be anchored with before= (the next def sits past the guard), so the recipe anchors it with + after=.""" + _write( + repo, + **{ + "model.py": ( + "def keep():\n return 0\n\n\ndef helper(x):\n return x + 1\n" + ), + "util.py": ( + "from u import is_hip\n" + "\n" + "_is_hip = is_hip()\n" + "\n" + "if TYPE_CHECKING:\n" + " from m import Thing\n" + ), + }, + ) + _commit(repo, "base") + _write( + repo, + **{ + "model.py": "def keep():\n return 0\n", + "util.py": ( + "from u import is_hip\n" + "\n" + "_is_hip = is_hip()\n" + "\n" + "\n" + "def helper(x):\n" + " return x + 1\n" + "\n" + "\n" + "if TYPE_CHECKING:\n" + " from m import Thing\n" + ), + }, + ) + _commit(repo, "move helper above the TYPE_CHECKING guard") + recipe = infer_recipe("HEAD", str(repo)) + assert recipe.supported + assert len(recipe.moves) == 1 + move = recipe.moves[0] + assert move["name"] == "helper" and move["dst"] == "util.py" + assert move["before"] is None + assert move["after"] == "_is_hip" + + def test_infer_recipe_free_function_move_uses_requalify(repo: Path) -> None: """A move to a module-level free function dedents and requalifies the call site (drops the qualifier), rather than lowering a receiver.""" @@ -288,3 +338,233 @@ def test_infer_recipe_records_the_source_class_for_disambiguation(repo: Path) -> assert [mv["from_class"] for mv in recipe.moves] == ["M"] script = recipe_to_script(recipe, "move M.foo onto C") assert "from_class='M'" in script + + +def test_infer_recipe_module_level_def_shadowed_by_method_name(repo: Path) -> None: + """A column-0 cut resolves to the module-level def even when a method shares its name.""" + _write( + repo, + **{ + "model.py": ( + "def foo(*, x):\n" + " return x + 1\n" + "\n" + "\n" + "class M:\n" + " def foo(self):\n" + " return foo(x=self.x)\n" + ), + "util.py": "def keep():\n return 1\n", + }, + ) + _commit(repo, "base") + _write( + repo, + **{ + "model.py": ( + "from util import foo\n" + "\n" + "\n" + "class M:\n" + " def foo(self):\n" + " return foo(x=self.x)\n" + ), + "util.py": ( + "def keep():\n" + " return 1\n" + "\n" + "\n" + "def foo(*, x):\n" + " return x + 1\n" + ), + }, + ) + commit = _commit(repo, "move module-level foo to util") + + recipe = infer_recipe(commit, str(repo)) + + assert recipe.supported + assert [mv["name"] for mv in recipe.moves] == ["foo"] + assert recipe.moves[0]["from_class"] is None + assert recipe.moves[0]["into_class"] is None + + +def test_infer_recipe_class_move_between_existing_files(repo: Path) -> None: + """A top-level class relocated to an existing module moves whole; its methods do not.""" + _write( + repo, + **{ + "model.py": ( + "class Payload:\n" + " def get(self):\n" + " return 1\n" + "\n" + "\n" + "def stay():\n" + " return 2\n" + ), + "comp.py": "def keep():\n return 3\n", + }, + ) + _commit(repo, "base") + _write( + repo, + **{ + "model.py": "def stay():\n return 2\n", + "comp.py": ( + "def keep():\n" + " return 3\n" + "\n" + "\n" + "class Payload:\n" + " def get(self):\n" + " return 1\n" + ), + }, + ) + commit = _commit(repo, "move Payload to comp") + + recipe = infer_recipe(commit, str(repo)) + + assert recipe.supported + assert [mv["name"] for mv in recipe.moves] == ["Payload"] + assert recipe.moves[0]["from_class"] is None + assert recipe.moves[0]["into_class"] is None + + +def test_infer_recipe_move_leaving_a_forwarding_delegate(repo: Path) -> None: + """A same-named stub re-added to the source infers leave_delegate on the move.""" + _write( + repo, + **{ + "model.py": ( + "class M:\n" " def work(self, x):\n" " return x + 1\n" + ), + "comp.py": "class C:\n def keep(self):\n return 1\n", + }, + ) + _commit(repo, "base") + _write( + repo, + **{ + "model.py": ( + "class M:\n" + " def work(self, x):\n" + " return self.comp.work(x)\n" + ), + "comp.py": ( + "class C:\n" + " def keep(self):\n" + " return 1\n" + "\n" + " def work(self, x):\n" + " return x + 1\n" + ), + }, + ) + commit = _commit(repo, "move M.work onto C, leaving a delegate") + + recipe = infer_recipe(commit, str(repo)) + + assert recipe.supported + assert [mv["name"] for mv in recipe.moves] == ["work"] + assert recipe.moves[0]["dst"] == "comp.py" + assert recipe.moves[0]["leave_delegate"] == "comp" + assert recipe.moves[0]["delegate_name"] is None + script = recipe_to_script(recipe, "move with delegate") + assert "leave_delegate='comp'" in script + + +def test_infer_recipe_constant_relocated_with_the_move(repo: Path) -> None: + """A module constant that vanished from the source and appeared in the existing + destination becomes a move_assign.""" + _write( + repo, + **{ + "model.py": ( + "RATIO = 3\n" + "\n" + "\n" + "def work(x):\n" + " return x * RATIO\n" + "\n" + "\n" + "def stay():\n" + " return 1\n" + ), + "comp.py": "import os\n\n\ndef keep():\n return 2\n", + }, + ) + _commit(repo, "base") + _write( + repo, + **{ + "model.py": "def stay():\n return 1\n", + "comp.py": ( + "import os\n" + "\n" + "RATIO = 3\n" + "\n" + "\n" + "def keep():\n" + " return 2\n" + "\n" + "\n" + "def work(x):\n" + " return x * RATIO\n" + ), + }, + ) + commit = _commit(repo, "move work + RATIO to comp") + + recipe = infer_recipe(commit, str(repo)) + + assert recipe.supported + assert [am["name"] for am in recipe.assign_moves] == ["RATIO"] + script = recipe_to_script(recipe, "move with constant") + assert "move_assign" in script + + +def test_infer_recipe_in_file_method_reorder(repo: Path) -> None: + """A method cut and re-inserted elsewhere in the same class (no other file gains it) infers + an in-file move_symbol (src == dst) anchored above its new next sibling.""" + _write( + repo, + **{ + "m.py": ( + "class C:\n" + " def a(self):\n" + " return 1\n" + "\n" + " def b(self):\n" + " return 2\n" + "\n" + " def c(self):\n" + " return 3\n" + ) + }, + ) + _commit(repo, "base") + _write( + repo, + **{ + "m.py": ( + "class C:\n" + " def c(self):\n" + " return 3\n" + "\n" + " def a(self):\n" + " return 1\n" + "\n" + " def b(self):\n" + " return 2\n" + ) + }, + ) + commit = _commit(repo, "move c above a") + recipe = infer_recipe(commit, str(repo)) + assert recipe.supported + assert len(recipe.moves) == 1 + mv = recipe.moves[0] + assert mv["name"] == "c" and mv["src"] == "m.py" and mv["dst"] == "m.py" + assert mv["into_class"] == "C" and mv["before"] == "a" diff --git a/.claude/skills/mechanical-refactor-verify/scripts/tests/proof_generator/test_main_single_commit.py b/.claude/skills/mechanical-refactor-verify/scripts/tests/proof_generator/test_main_single_commit.py new file mode 100644 index 000000000..505089574 --- /dev/null +++ b/.claude/skills/mechanical-refactor-verify/scripts/tests/proof_generator/test_main_single_commit.py @@ -0,0 +1,71 @@ +import sys +from pathlib import Path + +import pytest + +sys.path.insert(0, str(Path(__file__).resolve().parents[2])) + +from generator_testlib import _commit, _write # noqa: F401 +from mechanical_refactor_proof_generator import _main + + +def _extract_function_commit(repo: Path) -> str: + _write( + repo, + **{ + "kv.py": ( + "class C:\n" + " def dispatch(self, n):\n" + " x = self.a\n" + " y = x + n\n" + " return y\n" + "\n" + " def keep(self):\n" + " return 0\n" + ) + }, + ) + _commit(repo, "base") + _write( + repo, + **{ + "kv.py": ( + "class C:\n" + " def dispatch(self, n):\n" + " y = self._combine(n=n)\n" + " return y\n" + "\n" + " def _combine(self, *, n):\n" + " x = self.a\n" + " y = x + n\n" + " return y\n" + "\n" + " def keep(self):\n" + " return 0\n" + ) + }, + ) + return _commit(repo, "extract _combine from dispatch") + + +def test_single_commit_extract_function_reproduces_instead_of_unsupported( + repo: Path, monkeypatch: pytest.MonkeyPatch +) -> None: + """A pure intra-file extract_function commit run in single-commit mode reproduces (exit 0), + not UNSUPPORTED -- the relocates check must count extract_functions like the range path. + """ + sha = _extract_function_commit(repo) + monkeypatch.chdir(repo) + assert _main([sha]) == 0 + + +def test_single_commit_pure_rename_is_unsupported( + repo: Path, monkeypatch: pytest.MonkeyPatch +) -> None: + """A commit that relocates no definition (a bare rename) stays UNSUPPORTED with exit 1.""" + _write(repo, **{"m.py": "def foo():\n return 1\n"}) + _commit(repo, "base") + _write(repo, **{"m.py": "def bar():\n return 1\n"}) + sha = _commit(repo, "rename foo to bar") + monkeypatch.chdir(repo) + assert _main([sha]) == 1 diff --git a/.claude/skills/mechanical-refactor-verify/scripts/tests/proof_generator/test_script_and_diff.py b/.claude/skills/mechanical-refactor-verify/scripts/tests/proof_generator/test_script_and_diff.py index 113d8a214..0ca8c735b 100644 --- a/.claude/skills/mechanical-refactor-verify/scripts/tests/proof_generator/test_script_and_diff.py +++ b/.claude/skills/mechanical-refactor-verify/scripts/tests/proof_generator/test_script_and_diff.py @@ -25,7 +25,8 @@ def test_recipe_to_script_is_self_contained_and_ordered(repo: Path) -> None: script = recipe_to_script(infer_recipe("HEAD", str(repo)), "move foo onto C") assert "from mechanical_refactor_reproduction_utils import Repro" in script assert script.index("lower_call_sites") < script.index("move_symbol") - assert "r.run()" in script + assert "residual = r.run()" in script + assert "sys.exit(1 if residual else 0)" in script # importing nothing else from the skill keeps the script auditable in isolation assert "mechanical_refactor_verify_utils" not in script assert "mechanical_refactor_proof_generator" not in script @@ -40,6 +41,144 @@ def test_recipe_to_script_orders_import_ops_after_moves(repo: Path) -> None: assert script.index("move_symbol") < script.index("add_import") +def _emit_runnable_script(repo: Path, out: Path, commit: str, subject: str) -> Path: + """Write the emitted script plus its util dependency into a proof-folder layout.""" + scripts_dir = out / "repro_scripts" + scripts_dir.mkdir(parents=True, exist_ok=True) + utils_src = Path(__file__).resolve().parents[2] / ( + "mechanical_refactor_reproduction_utils.py" + ) + (out / "mechanical_refactor_reproduction_utils.py").write_text( + utils_src.read_text() + ) + script = recipe_to_script(infer_recipe(commit, str(repo)), subject) + script_path = scripts_dir / f"{commit[:9]}.py" + script_path.write_text(script) + return script_path + + +def test_emitted_script_exits_zero_on_faithful_commit( + repo: Path, tmp_path: Path +) -> None: + """Running the emitted script on a clean move exits 0 and prints the PASS verdict.""" + _write( + repo, + **{ + "model.py": "def keep():\n return 0\n\n\ndef resolve(m):\n return m\n", + "util.py": "import os\n", + "caller.py": ( + "from model import resolve\n\n\ndef run(m):\n return resolve(m)\n" + ), + }, + ) + _commit(repo, "base") + # The after-state is the primitives' exact output (this bare repo has no formatter + # to absorb the cut's leftover blank lines, unlike a pre-commit-clean real repo). + _write( + repo, + **{ + "model.py": "def keep():\n return 0\n\n\n", + "util.py": "import os\n\ndef resolve(m):\n return m\n", + "caller.py": ( + "from util import resolve\n\n\ndef run(m):\n return resolve(m)\n" + ), + }, + ) + commit = _commit(repo, "move resolve to util") + script_path = _emit_runnable_script(repo, tmp_path / "out", commit, "move") + + result = subprocess.run( + [sys.executable, str(script_path)], cwd=repo, capture_output=True, text=True + ) + + assert result.returncode == 0, result.stdout + result.stderr + assert "PASS" in result.stdout + + +def test_emitted_script_exits_nonzero_on_bundled_change( + repo: Path, tmp_path: Path +) -> None: + """A commit bundling a non-move change makes the emitted script exit non-zero.""" + _write( + repo, + **{ + "model.py": "def keep():\n return 0\n\n\ndef resolve(m):\n return m\n", + "util.py": "import os\n", + }, + ) + _commit(repo, "base") + _write( + repo, + **{ + "model.py": "def keep():\n return 99\n", + "util.py": "import os\n\n\ndef resolve(m):\n return m\n", + }, + ) + commit = _commit(repo, "move resolve AND change keep") + script_path = _emit_runnable_script(repo, tmp_path / "out", commit, "dirty move") + + result = subprocess.run( + [sys.executable, str(script_path)], cwd=repo, capture_output=True, text=True + ) + + assert result.returncode == 1, result.stdout + result.stderr + assert "RESIDUAL" in result.stdout + + +def test_emitted_script_passes_on_move_above_typechecking_guard( + repo: Path, tmp_path: Path +) -> None: + """A module-level def relocated to just above an ``if TYPE_CHECKING:`` guard reproduces + via an inferred after= anchor and the emitted script exits 0.""" + _write( + repo, + **{ + "model.py": ( + "def keep():\n return 0\n\n\ndef helper(x):\n return x + 1\n" + ), + "util.py": ( + "from u import is_hip\n" + "\n" + "_is_hip = is_hip()\n" + "\n" + "if TYPE_CHECKING:\n" + " from m import Thing\n" + ), + }, + ) + _commit(repo, "base") + # After-state = the primitive's exact output (bare repo, no formatter to absorb blanks). + _write( + repo, + **{ + "model.py": "def keep():\n return 0\n\n\n", + "util.py": ( + "from u import is_hip\n" + "\n" + "_is_hip = is_hip()\n" + "\n" + "def helper(x):\n" + " return x + 1\n" + "\n" + "if TYPE_CHECKING:\n" + " from m import Thing\n" + ), + }, + ) + commit = _commit(repo, "move helper above the TYPE_CHECKING guard") + script_path = _emit_runnable_script( + repo, tmp_path / "out", commit, "after-anchor move" + ) + + result = subprocess.run( + [sys.executable, str(script_path)], cwd=repo, capture_output=True, text=True + ) + + assert result.returncode == 0, result.stdout + result.stderr + assert "PASS" in result.stdout + assert "after='_is_hip'" in script_path.read_text() + + def test_per_file_diff_keeps_content_lines_starting_with_plus_signs(repo: Path) -> None: """An added content line beginning with '++' is collected, not mistaken for a header.""" from mechanical_refactor_proof_generator import _per_file_diff diff --git a/.claude/skills/mechanical-refactor-verify/scripts/tests/reproduction_cli/cli_testlib.py b/.claude/skills/mechanical-refactor-verify/scripts/tests/reproduction_cli/cli_testlib.py new file mode 100644 index 000000000..fb1eef19b --- /dev/null +++ b/.claude/skills/mechanical-refactor-verify/scripts/tests/reproduction_cli/cli_testlib.py @@ -0,0 +1,62 @@ +import subprocess +from pathlib import Path + +_PASSING_PROOF = ( + "import sys\n" + 'print("PASS: reproduces the commit byte-for-byte.")\n' + "sys.exit(0)\n" +) +_FAILING_PROOF = ( + "import sys\n" 'print("RESIDUAL (2 lines):\\n+x\\n-y")\n' "sys.exit(1)\n" +) + + +def _git(repo: Path, *args: str) -> str: + return subprocess.run( + ["git", *args], cwd=repo, check=True, capture_output=True, text=True + ).stdout.strip() + + +def _write(repo: Path, **files: "str | None") -> None: + for name, content in files.items(): + path = repo / name.replace("__", "/") + if content is None: + path.unlink() + else: + path.parent.mkdir(parents=True, exist_ok=True) + path.write_text(content) + + +def _commit(repo: Path, message: str) -> str: + _git(repo, "add", "-A") + _git(repo, "commit", "-q", "-m", message) + return _git(repo, "rev-parse", "HEAD") + + +def _chain(repo: Path, messages: "list[str]") -> "tuple[str, list[str]]": + """A base commit plus one single-file commit per message, on a `chain` branch. + Returns (base_sha, commit_shas).""" + _write(repo, **{"seed.py": "SEED = 0\n"}) + base = _commit(repo, "base") + _git(repo, "switch", "-q", "-c", "chain") + shas: "list[str]" = [] + for i, message in enumerate(messages): + _write(repo, **{f"file_{i}.py": f"VALUE = {i}\n"}) + shas.append(_commit(repo, message)) + return base, shas + + +def _write_stub_proof( + proof_dir: Path, + sha: str, + *, + passing: bool = True, + flat: bool = False, + stem_len: int = 9, +) -> Path: + """A stand-in proof script printing the arbiter's verdict line and exiting to match.""" + directory = proof_dir if flat else proof_dir / "repro_scripts" + directory.mkdir(parents=True, exist_ok=True) + path = directory / f"{sha[:stem_len]}.py" + path.write_text(_PASSING_PROOF if passing else _FAILING_PROOF) + return path diff --git a/.claude/skills/mechanical-refactor-verify/scripts/tests/reproduction_cli/conftest.py b/.claude/skills/mechanical-refactor-verify/scripts/tests/reproduction_cli/conftest.py new file mode 100644 index 000000000..e2a378785 --- /dev/null +++ b/.claude/skills/mechanical-refactor-verify/scripts/tests/reproduction_cli/conftest.py @@ -0,0 +1,20 @@ +import sys +from pathlib import Path + +import pytest + +sys.path.insert(0, str(Path(__file__).resolve().parents[2])) +sys.path.insert(0, str(Path(__file__).resolve().parent)) + +from cli_testlib import _git + + +@pytest.fixture +def repo(tmp_path: Path) -> Path: + root = tmp_path / "repo" + root.mkdir() + _git(root, "init", "-q", "-b", "main") + _git(root, "config", "user.email", "test@example.com") + _git(root, "config", "user.name", "test") + _git(root, "config", "commit.gpgsign", "false") + return root diff --git a/.claude/skills/mechanical-refactor-verify/scripts/tests/reproduction_cli/test_classification.py b/.claude/skills/mechanical-refactor-verify/scripts/tests/reproduction_cli/test_classification.py new file mode 100644 index 000000000..1d067d81b --- /dev/null +++ b/.claude/skills/mechanical-refactor-verify/scripts/tests/reproduction_cli/test_classification.py @@ -0,0 +1,123 @@ +import sys +from pathlib import Path + +import pytest + +sys.path.insert(0, str(Path(__file__).resolve().parents[2])) + +from cli_testlib import _chain, _write_stub_proof +from mechanical_refactor_reproduction_cli import ( + KIND_MECHANICAL, + KIND_NON_MECHANICAL, + VERDICT_AMBIGUOUS_KIND, + VERDICT_HUMAN_REVIEW, + VERDICT_PASS, + VERDICT_UNCLASSIFIED, + verify_chain, +) + + +def _single_verdict(repo: Path, tmp_path: Path, message: str, *, with_proof: bool): + proof = tmp_path / "proof" + proof.mkdir(exist_ok=True) + base, shas = _chain(repo, [message]) + if with_proof: + _write_stub_proof(proof, shas[0]) + result = verify_chain(base=base, branch="chain", proof=proof, repo_root=str(repo)) + return result.verdicts[0] + + +def test_mechanical_provable_word_classifies_the_commit_as_mechanical( + repo: Path, tmp_path: Path +) -> None: + """A message carrying mechanical_provable is classified mechanical and needs a proof.""" + verdict = _single_verdict( + repo, tmp_path, "grp(step,mechanical_provable): move foo", with_proof=True + ) + assert verdict.kind == KIND_MECHANICAL + assert verdict.verdict == VERDICT_PASS + + +def test_non_mechanical_provable_word_is_not_double_counted_as_the_bare_word( + repo: Path, tmp_path: Path +) -> None: + """non_mechanical_provable classifies as non-mechanical, not as both words at once.""" + verdict = _single_verdict( + repo, + tmp_path, + "grp(step,non_mechanical_provable): rework foo", + with_proof=False, + ) + assert verdict.kind == KIND_NON_MECHANICAL + assert verdict.verdict == VERDICT_HUMAN_REVIEW + + +def test_message_without_either_word_is_unclassified_and_fails_the_chain( + repo: Path, tmp_path: Path +) -> None: + """A commit missing both words gets UNCLASSIFIED and the chain does not pass.""" + proof = tmp_path / "proof" + proof.mkdir() + base, _ = _chain(repo, ["plain subject with no kind word"]) + result = verify_chain(base=base, branch="chain", proof=proof, repo_root=str(repo)) + assert result.verdicts[0].verdict == VERDICT_UNCLASSIFIED + assert result.verdicts[0].kind is None + assert not result.passed + + +def test_message_with_both_words_is_ambiguous(repo: Path, tmp_path: Path) -> None: + """A commit declaring both kinds gets AMBIGUOUS_KIND and fails the chain.""" + verdict = _single_verdict( + repo, + tmp_path, + "subject mechanical_provable\n\nbody also says non_mechanical_provable", + with_proof=True, + ) + assert verdict.verdict == VERDICT_AMBIGUOUS_KIND + assert verdict.kind is None + + +def test_kind_word_must_stand_alone_not_as_a_substring( + repo: Path, tmp_path: Path +) -> None: + """xmechanical_provable / mechanical_provable_x do not count as the standalone word.""" + verdict = _single_verdict( + repo, + tmp_path, + "xmechanical_provable and mechanical_provable_x only", + with_proof=False, + ) + assert verdict.verdict == VERDICT_UNCLASSIFIED + + +def test_kind_word_delimited_by_punctuation_counts(repo: Path, tmp_path: Path) -> None: + """The word inside punctuation, e.g. (step,mechanical_provable), is a valid match.""" + verdict = _single_verdict( + repo, tmp_path, "grp(step,mechanical_provable): move", with_proof=True + ) + assert verdict.kind == KIND_MECHANICAL + + +def test_repeating_the_same_kind_word_is_accepted(repo: Path, tmp_path: Path) -> None: + """Multiple occurrences of one kind word still classify unambiguously.""" + verdict = _single_verdict( + repo, + tmp_path, + "mechanical_provable move\n\nthis commit is mechanical_provable", + with_proof=True, + ) + assert verdict.kind == KIND_MECHANICAL + assert verdict.verdict == VERDICT_PASS + + +def test_kind_word_in_the_body_counts_when_subject_is_free_form( + repo: Path, tmp_path: Path +) -> None: + """Classification scans the whole message, so a body-only word is enough.""" + verdict = _single_verdict( + repo, + tmp_path, + "Move resolve to util\n\nKind: non_mechanical_provable", + with_proof=False, + ) + assert verdict.kind == KIND_NON_MECHANICAL diff --git a/.claude/skills/mechanical-refactor-verify/scripts/tests/reproduction_cli/test_proof_discovery.py b/.claude/skills/mechanical-refactor-verify/scripts/tests/reproduction_cli/test_proof_discovery.py new file mode 100644 index 000000000..e40292f4c --- /dev/null +++ b/.claude/skills/mechanical-refactor-verify/scripts/tests/reproduction_cli/test_proof_discovery.py @@ -0,0 +1,89 @@ +import sys +from pathlib import Path + +sys.path.insert(0, str(Path(__file__).resolve().parents[2])) + +from cli_testlib import _chain, _write_stub_proof +from mechanical_refactor_reproduction_cli import ( + VERDICT_AMBIGUOUS_PROOF, + VERDICT_MISSING_PROOF, + VERDICT_PASS, + verify_chain, +) + +_MSG = "mechanical_provable: move foo" + + +def _run_single(repo: Path, proof: Path): + base, shas = _chain(repo, [_MSG]) + return shas[0], verify_chain( + base=base, branch="chain", proof=proof, repo_root=str(repo) + ) + + +def test_proof_is_found_under_repro_scripts_by_sha_prefix( + repo: Path, tmp_path: Path +) -> None: + """The generator layout repro_scripts/.py resolves to the commit's proof.""" + proof = tmp_path / "proof" + base, shas = _chain(repo, [_MSG]) + _write_stub_proof(proof, shas[0], stem_len=9) + result = verify_chain(base=base, branch="chain", proof=proof, repo_root=str(repo)) + assert result.verdicts[0].verdict == VERDICT_PASS + + +def test_proof_is_found_flat_in_the_proof_folder_by_full_sha( + repo: Path, tmp_path: Path +) -> None: + """A flat /.py layout is also accepted.""" + proof = tmp_path / "proof" + base, shas = _chain(repo, [_MSG]) + _write_stub_proof(proof, shas[0], flat=True, stem_len=40) + result = verify_chain(base=base, branch="chain", proof=proof, repo_root=str(repo)) + assert result.verdicts[0].verdict == VERDICT_PASS + + +def test_provable_commit_without_a_proof_script_is_missing_proof( + repo: Path, tmp_path: Path +) -> None: + """A mechanical_provable commit with no matching script fails as MISSING_PROOF.""" + proof = tmp_path / "proof" + proof.mkdir() + sha, result = _run_single(repo, proof) + assert result.verdicts[0].verdict == VERDICT_MISSING_PROOF + assert not result.passed + + +def test_unrelated_and_non_hex_scripts_do_not_match(repo: Path, tmp_path: Path) -> None: + """Scripts named for another sha or with a non-hex stem are not this commit's proof.""" + proof = tmp_path / "proof" + scripts = proof / "repro_scripts" + scripts.mkdir(parents=True) + (scripts / "0123456789abcdef.py").write_text("raise SystemExit(1)\n") + (scripts / "not_a_sha.py").write_text("raise SystemExit(1)\n") + sha, result = _run_single(repo, proof) + assert result.verdicts[0].verdict == VERDICT_MISSING_PROOF + + +def test_two_scripts_matching_one_commit_are_ambiguous( + repo: Path, tmp_path: Path +) -> None: + """A commit matched by both a nested and a flat script fails as AMBIGUOUS_PROOF.""" + proof = tmp_path / "proof" + base, shas = _chain(repo, [_MSG]) + _write_stub_proof(proof, shas[0], stem_len=9) + _write_stub_proof(proof, shas[0], flat=True, stem_len=12) + result = verify_chain(base=base, branch="chain", proof=proof, repo_root=str(repo)) + assert result.verdicts[0].verdict == VERDICT_AMBIGUOUS_PROOF + assert not result.passed + + +def test_short_hex_stem_below_minimum_length_is_ignored( + repo: Path, tmp_path: Path +) -> None: + """A 6-char hex stem is too short to name a commit and is not treated as a proof.""" + proof = tmp_path / "proof" + base, shas = _chain(repo, [_MSG]) + _write_stub_proof(proof, shas[0], stem_len=6) + result = verify_chain(base=base, branch="chain", proof=proof, repo_root=str(repo)) + assert result.verdicts[0].verdict == VERDICT_MISSING_PROOF diff --git a/.claude/skills/mechanical-refactor-verify/scripts/tests/reproduction_cli/test_report.py b/.claude/skills/mechanical-refactor-verify/scripts/tests/reproduction_cli/test_report.py new file mode 100644 index 000000000..8f827b11f --- /dev/null +++ b/.claude/skills/mechanical-refactor-verify/scripts/tests/reproduction_cli/test_report.py @@ -0,0 +1,95 @@ +import sys +from pathlib import Path + +sys.path.insert(0, str(Path(__file__).resolve().parents[2])) + +from cli_testlib import _chain, _write_stub_proof +from mechanical_refactor_reproduction_cli import main, render_report, verify_chain + + +def _mixed_chain_result(repo: Path, tmp_path: Path): + proof = tmp_path / "proof" + base, shas = _chain( + repo, + [ + "mechanical_provable: move foo", + "non_mechanical_provable: rework bar", + "mechanical_provable: move baz", + ], + ) + _write_stub_proof(proof, shas[0]) + result = verify_chain(base=base, branch="chain", proof=proof, repo_root=str(repo)) + return proof, base, shas, result + + +def test_report_has_header_table_row_per_commit_and_chain_verdict( + repo: Path, tmp_path: Path +) -> None: + """The report carries base/branch/proof, one table row per commit, and the verdict.""" + proof, base, shas, result = _mixed_chain_result(repo, tmp_path) + report = render_report(result) + + assert "# Mechanical refactor chain report" in report + assert f"`{base[:12]}`" in report + assert "chain verdict: **FAIL**" in report + assert "3 total — 2 mechanical_provable, 1 non_mechanical_provable" in report + for sha in shas: + assert f"`{sha[:9]}`" in report + assert "| mechanical_provable | PASS |" in report + assert "| non_mechanical_provable | HUMAN_REVIEW |" in report + assert "| mechanical_provable | MISSING_PROOF |" in report + + +def test_report_lists_failure_details_for_each_non_ok_commit( + repo: Path, tmp_path: Path +) -> None: + """Every non-ok commit gets a failure-details section with its explanation.""" + proof, base, shas, result = _mixed_chain_result(repo, tmp_path) + report = render_report(result) + + assert "## Failure details" in report + assert f"### `{shas[2][:9]}` — MISSING_PROOF" in report + assert "no proof script found" in report + + +def test_passing_report_has_no_failure_details_section( + repo: Path, tmp_path: Path +) -> None: + """A fully verified chain renders a PASS report without a failure section.""" + proof = tmp_path / "proof" + base, shas = _chain(repo, ["mechanical_provable: move foo"]) + _write_stub_proof(proof, shas[0]) + result = verify_chain(base=base, branch="chain", proof=proof, repo_root=str(repo)) + report = render_report(result) + + assert "chain verdict: **PASS**" in report + assert "proofs: 1/1 PASS" in report + assert "## Failure details" not in report + + +def test_main_writes_the_report_into_the_proof_folder_by_default( + repo: Path, tmp_path: Path, capsys +) -> None: + """main prints the report and writes /chain_report.md (or --report PATH).""" + proof = tmp_path / "proof" + base, shas = _chain(repo, ["mechanical_provable: move foo"]) + _write_stub_proof(proof, shas[0]) + args = [ + "--base", + base, + "--branch", + "chain", + "--proof", + str(proof), + "--repo-root", + str(repo), + ] + + assert main(args) == 0 + default_report = proof / "chain_report.md" + assert "chain verdict: **PASS**" in default_report.read_text() + assert "chain verdict: **PASS**" in capsys.readouterr().out + + custom = tmp_path / "custom_report.md" + assert main([*args, "--report", str(custom)]) == 0 + assert "chain verdict: **PASS**" in custom.read_text() diff --git a/.claude/skills/mechanical-refactor-verify/scripts/tests/reproduction_cli/test_skip_passed.py b/.claude/skills/mechanical-refactor-verify/scripts/tests/reproduction_cli/test_skip_passed.py new file mode 100644 index 000000000..972d98820 --- /dev/null +++ b/.claude/skills/mechanical-refactor-verify/scripts/tests/reproduction_cli/test_skip_passed.py @@ -0,0 +1,179 @@ +import json +import sys +from pathlib import Path + +sys.path.insert(0, str(Path(__file__).resolve().parents[2])) + +from cli_testlib import _chain, _write_stub_proof +from mechanical_refactor_reproduction_cli import ( + VERDICT_FAIL, + VERDICT_PASS, + main, + render_report, + verify_chain, +) + +_MSG = "mechanical_provable: move foo" + + +def _counting_proof(script: Path, counter: Path, *, passing: bool = True) -> None: + """Make the stub proof bump a run counter so re-execution is observable.""" + verdict = ( + 'print("PASS: reproduces the commit byte-for-byte.")\nsys.exit(0)\n' + if passing + else 'print("RESIDUAL (1 lines):\\n+x")\nsys.exit(1)\n' + ) + script.write_text( + "import sys\n" + f"counter = __import__('pathlib').Path({str(counter)!r})\n" + "runs = int(counter.read_text()) if counter.exists() else 0\n" + "counter.write_text(str(runs + 1))\n" + verdict + ) + + +def _cache_file(repo: Path) -> Path: + return repo / ".git" / "mechanical_refactor_passed_proofs.json" + + +def test_skip_passed_reuses_an_unchanged_pass_without_rerunning( + repo: Path, tmp_path: Path +) -> None: + """A PASS recorded on the first run is reused: the proof does not execute again.""" + proof = tmp_path / "proof" + counter = tmp_path / "runs" + base, shas = _chain(repo, [_MSG]) + _counting_proof(_write_stub_proof(proof, shas[0]), counter) + args = dict(base=base, branch="chain", proof=proof, repo_root=str(repo)) + + first = verify_chain(**args) + assert first.verdicts[0].verdict == VERDICT_PASS + assert counter.read_text() == "1" + + second = verify_chain(**args, skip_passed=True) + assert second.verdicts[0].verdict == VERDICT_PASS + assert second.verdicts[0].cached + assert counter.read_text() == "1" + assert second.passed + + +def test_without_the_flag_the_proof_always_reruns(repo: Path, tmp_path: Path) -> None: + """The cache is recorded on every run but consulted only under skip_passed.""" + proof = tmp_path / "proof" + counter = tmp_path / "runs" + base, shas = _chain(repo, [_MSG]) + _counting_proof(_write_stub_proof(proof, shas[0]), counter) + args = dict(base=base, branch="chain", proof=proof, repo_root=str(repo)) + + verify_chain(**args) + result = verify_chain(**args) + + assert counter.read_text() == "2" + assert not result.verdicts[0].cached + + +def test_editing_the_proof_script_invalidates_the_cache( + repo: Path, tmp_path: Path +) -> None: + """A changed script hash misses the cache, so the edited (failing) proof reruns.""" + proof = tmp_path / "proof" + base, shas = _chain(repo, [_MSG]) + script = _write_stub_proof(proof, shas[0]) + + verify_chain(base=base, branch="chain", proof=proof, repo_root=str(repo)) + script.write_text('print("RESIDUAL (1 lines):\\n+x")\nraise SystemExit(1)\n') + result = verify_chain( + base=base, branch="chain", proof=proof, repo_root=str(repo), skip_passed=True + ) + + assert result.verdicts[0].verdict == VERDICT_FAIL + + +def test_editing_the_utils_copy_invalidates_the_cache( + repo: Path, tmp_path: Path +) -> None: + """The utils module next to the scripts is part of the key: editing it forces a rerun.""" + proof = tmp_path / "proof" + counter = tmp_path / "runs" + utils = proof / "mechanical_refactor_reproduction_utils.py" + base, shas = _chain(repo, [_MSG]) + _counting_proof(_write_stub_proof(proof, shas[0]), counter) + utils.parent.mkdir(parents=True, exist_ok=True) + utils.write_text("ENGINE = 1\n") + args = dict(base=base, branch="chain", proof=proof, repo_root=str(repo)) + + verify_chain(**args) + utils.write_text("ENGINE = 2\n") + result = verify_chain(**args, skip_passed=True) + + assert counter.read_text() == "2" + assert not result.verdicts[0].cached + + +def test_a_fail_is_never_recorded_in_the_cache(repo: Path, tmp_path: Path) -> None: + """Only PASS verdicts enter the cache; a failing proof leaves no entry for its sha.""" + proof = tmp_path / "proof" + base, shas = _chain(repo, [_MSG]) + _write_stub_proof(proof, shas[0], passing=False) + + verify_chain(base=base, branch="chain", proof=proof, repo_root=str(repo)) + + cache = _cache_file(repo) + assert not cache.exists() or shas[0] not in json.loads(cache.read_text())["passed"] + + +def test_corrupt_cache_file_is_treated_as_empty(repo: Path, tmp_path: Path) -> None: + """A garbage cache file never crashes the walk; the proof simply runs.""" + proof = tmp_path / "proof" + base, shas = _chain(repo, [_MSG]) + _write_stub_proof(proof, shas[0]) + _cache_file(repo).write_text("{not json") + + result = verify_chain( + base=base, branch="chain", proof=proof, repo_root=str(repo), skip_passed=True + ) + + assert result.verdicts[0].verdict == VERDICT_PASS + assert not result.verdicts[0].cached + + +def test_cache_lives_in_the_git_common_dir_and_records_the_pass( + repo: Path, tmp_path: Path +) -> None: + """A PASS writes the (sha, script hash, utils hash) entry under .git/.""" + proof = tmp_path / "proof" + base, shas = _chain(repo, [_MSG]) + _write_stub_proof(proof, shas[0]) + + verify_chain(base=base, branch="chain", proof=proof, repo_root=str(repo)) + + entry = json.loads(_cache_file(repo).read_text())["passed"][shas[0]] + assert set(entry) == {"script_sha256", "utils_sha256"} + assert len(entry["script_sha256"]) == 64 + + +def test_report_counts_reused_proofs_and_main_accepts_the_flag( + repo: Path, tmp_path: Path +) -> None: + """The report carries the reused count and --skip-passed works through main.""" + proof = tmp_path / "proof" + base, shas = _chain(repo, [_MSG]) + _write_stub_proof(proof, shas[0]) + cli_args = [ + "--base", + base, + "--branch", + "chain", + "--proof", + str(proof), + "--repo-root", + str(repo), + ] + + assert main(cli_args) == 0 + result = verify_chain( + base=base, branch="chain", proof=proof, repo_root=str(repo), skip_passed=True + ) + report = render_report(result) + + assert "reused from the passed-proof cache (--skip-passed): 1" in report + assert main([*cli_args, "--skip-passed"]) == 0 diff --git a/.claude/skills/mechanical-refactor-verify/scripts/tests/reproduction_cli/test_verify_chain.py b/.claude/skills/mechanical-refactor-verify/scripts/tests/reproduction_cli/test_verify_chain.py new file mode 100644 index 000000000..6bd7bd58c --- /dev/null +++ b/.claude/skills/mechanical-refactor-verify/scripts/tests/reproduction_cli/test_verify_chain.py @@ -0,0 +1,219 @@ +import sys +from pathlib import Path + +import pytest + +sys.path.insert(0, str(Path(__file__).resolve().parents[2])) + +from cli_testlib import _chain, _commit, _git, _write, _write_stub_proof +from mechanical_refactor_proof_generator import generate_range +from mechanical_refactor_reproduction_cli import ( + VERDICT_FAIL, + VERDICT_HUMAN_REVIEW, + VERDICT_PASS, + ChainVerificationError, + main, + verify_chain, +) + + +def test_chain_of_proved_and_declared_commits_passes( + repo: Path, tmp_path: Path +) -> None: + """A proved mechanical commit plus a declared non-mechanical one verifies as PASS.""" + proof = tmp_path / "proof" + base, shas = _chain( + repo, + ["mechanical_provable: move foo", "non_mechanical_provable: rework bar"], + ) + _write_stub_proof(proof, shas[0]) + + result = verify_chain(base=base, branch="chain", proof=proof, repo_root=str(repo)) + + assert [v.verdict for v in result.verdicts] == [VERDICT_PASS, VERDICT_HUMAN_REVIEW] + assert result.passed + + +def test_failing_proof_fails_the_commit_and_the_chain( + repo: Path, tmp_path: Path +) -> None: + """A proof that exits non-zero yields FAIL with the output tail in the detail.""" + proof = tmp_path / "proof" + base, shas = _chain(repo, ["mechanical_provable: move foo"]) + _write_stub_proof(proof, shas[0], passing=False) + + result = verify_chain(base=base, branch="chain", proof=proof, repo_root=str(repo)) + + assert result.verdicts[0].verdict == VERDICT_FAIL + assert "RESIDUAL" in result.verdicts[0].detail + assert not result.passed + + +def test_proof_exiting_zero_without_a_pass_line_is_a_fail( + repo: Path, tmp_path: Path +) -> None: + """PASS needs exit 0 AND the PASS: verdict line, so a residual under exit 0 fails.""" + proof = tmp_path / "proof" + base, shas = _chain(repo, ["mechanical_provable: move foo"]) + script = _write_stub_proof(proof, shas[0]) + script.write_text('print("RESIDUAL (1 lines):\\n+x")\n') + + result = verify_chain(base=base, branch="chain", proof=proof, repo_root=str(repo)) + + assert result.verdicts[0].verdict == VERDICT_FAIL + + +def test_main_exit_codes_reflect_the_chain_verdict(repo: Path, tmp_path: Path) -> None: + """main returns 0 for a verified chain and 1 once an unverifiable commit appears.""" + proof = tmp_path / "proof" + base, shas = _chain(repo, ["mechanical_provable: move"]) + _write_stub_proof(proof, shas[0]) + args = [ + "--base", + base, + "--branch", + "chain", + "--proof", + str(proof), + "--repo-root", + str(repo), + ] + + assert main(args) == 0 + + _git(repo, "commit", "-q", "--allow-empty", "-m", "plain subject with no kind word") + assert main(args) == 1 + + +def test_unresolvable_refs_and_missing_proof_folder_are_setup_errors( + repo: Path, tmp_path: Path +) -> None: + """Bad --base/--branch/--proof inputs raise ChainVerificationError (exit code 2).""" + proof = tmp_path / "proof" + proof.mkdir() + base, _ = _chain(repo, ["mechanical_provable: move"]) + + with pytest.raises(ChainVerificationError): + verify_chain( + base=base, branch="no-such-branch", proof=proof, repo_root=str(repo) + ) + with pytest.raises(ChainVerificationError): + verify_chain( + base=base, + branch="chain", + proof=tmp_path / "missing", + repo_root=str(repo), + ) + assert ( + main( + [ + "--base", + base, + "--branch", + "no-such-branch", + "--proof", + str(proof), + "--repo-root", + str(repo), + ] + ) + == 2 + ) + + +def test_non_ancestor_base_and_empty_range_are_setup_errors( + repo: Path, tmp_path: Path +) -> None: + """A base off the branch or an empty base..branch range refuses to verify.""" + proof = tmp_path / "proof" + proof.mkdir() + base, shas = _chain(repo, ["mechanical_provable: move"]) + _git(repo, "switch", "-q", "main") + _write(repo, **{"other.py": "OTHER = 1\n"}) + off_branch = _commit(repo, "unrelated main-side commit") + + with pytest.raises(ChainVerificationError): + verify_chain(base=off_branch, branch="chain", proof=proof, repo_root=str(repo)) + with pytest.raises(ChainVerificationError): + verify_chain(base=shas[0], branch=shas[0], proof=proof, repo_root=str(repo)) + + +def test_merge_commit_in_the_chain_is_a_setup_error(repo: Path, tmp_path: Path) -> None: + """A non-linear chain (contains a merge commit) refuses to verify.""" + proof = tmp_path / "proof" + proof.mkdir() + base, _ = _chain(repo, ["mechanical_provable: move"]) + _git(repo, "switch", "-q", "main") + _write(repo, **{"other.py": "OTHER = 1\n"}) + _commit(repo, "mechanical_provable: main-side") + _git(repo, "switch", "-q", "chain") + _git(repo, "merge", "-q", "--no-ff", "-m", "non_mechanical_provable: merge", "main") + + with pytest.raises(ChainVerificationError): + verify_chain(base=base, branch="chain", proof=proof, repo_root=str(repo)) + + +def test_proofs_run_concurrently_up_to_jobs(repo: Path, tmp_path: Path) -> None: + """With jobs>=2 a proof that waits on a sibling proof's sentinel still completes.""" + proof = tmp_path / "proof" + sentinel = tmp_path / "sentinel" + base, shas = _chain( + repo, ["mechanical_provable: move a", "mechanical_provable: move b"] + ) + waiter = _write_stub_proof(proof, shas[0]) + waiter.write_text( + "import sys, time\n" + f"deadline = time.monotonic() + 30\n" + f"while not __import__('pathlib').Path({str(sentinel)!r}).exists():\n" + " if time.monotonic() > deadline:\n" + " sys.exit(1)\n" + " time.sleep(0.05)\n" + 'print("PASS: reproduces the commit byte-for-byte.")\n' + "sys.exit(0)\n" + ) + creator = _write_stub_proof(proof, shas[1]) + creator.write_text( + "import sys\n" + f"__import__('pathlib').Path({str(sentinel)!r}).write_text('go')\n" + 'print("PASS: reproduces the commit byte-for-byte.")\n' + "sys.exit(0)\n" + ) + + result = verify_chain( + base=base, branch="chain", proof=proof, repo_root=str(repo), jobs=2 + ) + + assert [v.verdict for v in result.verdicts] == [VERDICT_PASS, VERDICT_PASS] + assert [v.sha for v in result.verdicts] == shas + assert result.passed + + +def test_end_to_end_with_a_generated_proof_folder(repo: Path, tmp_path: Path) -> None: + """A real move commit proved by generate_range verifies through the CLI end-to-end.""" + _write( + repo, + **{ + "model.py": "def keep():\n return 0\n\n\ndef resolve(m):\n return m\n", + "util.py": "import os\n", + }, + ) + base = _commit(repo, "base") + _git(repo, "switch", "-q", "-c", "chain") + # The after-state is the primitives' exact output (this bare repo has no formatter + # to absorb the cut's leftover blank lines, unlike a pre-commit-clean real repo). + _write( + repo, + **{ + "model.py": "def keep():\n return 0\n\n\n", + "util.py": "import os\n\ndef resolve(m):\n return m\n", + }, + ) + move_sha = _commit(repo, "mechanical_provable: move resolve to util") + + proof = tmp_path / "proof" + generate_range(f"{base}..chain", out_dir=str(proof), repo_root=str(repo)) + result = verify_chain(base=base, branch="chain", proof=proof, repo_root=str(repo)) + + assert result.verdicts[0].sha == move_sha + assert result.verdicts[0].verdict == VERDICT_PASS + assert result.passed diff --git a/.claude/skills/mechanical-refactor-verify/scripts/tests/reproduction_utils/test_add_imports.py b/.claude/skills/mechanical-refactor-verify/scripts/tests/reproduction_utils/test_add_imports.py index 172ed4905..0cf0bd58e 100644 --- a/.claude/skills/mechanical-refactor-verify/scripts/tests/reproduction_utils/test_add_imports.py +++ b/.claude/skills/mechanical-refactor-verify/scripts/tests/reproduction_utils/test_add_imports.py @@ -34,6 +34,49 @@ def test_add_import_appends_after_last_top_level_import(tmp_path: Path) -> None: ).read_text() == "import os\nimport sys\nfrom pkg import Thing\n\nx = 1\n" +# --- add_imported_name --------------------------------------------------------- + + +def test_add_imported_name_extends_a_single_line_import(tmp_path: Path) -> None: + """A new name is appended to an existing from-import on the same statement.""" + (tmp_path / "m.py").write_text("from pkg import a\n\nx = 1\n") + r = Repro("b", "t").add_imported_name("m.py", module="pkg", name="b") + _apply(r, tmp_path) + assert (tmp_path / "m.py").read_text() == "from pkg import a, b\n\nx = 1\n" + + +def test_add_imported_name_carries_an_asname(tmp_path: Path) -> None: + """The added name keeps its `as` alias.""" + (tmp_path / "m.py").write_text("from pkg import a\n") + r = Repro("b", "t").add_imported_name("m.py", module="pkg", name="b", asname="c") + _apply(r, tmp_path) + assert (tmp_path / "m.py").read_text() == "from pkg import a, b as c\n" + + +def test_add_imported_name_refuses_a_commented_import(tmp_path: Path) -> None: + """An import carrying comments is refused, since a rebuild would drop them.""" + (tmp_path / "m.py").write_text("from pkg import (\n a, # keep\n)\n") + r = Repro("b", "t").add_imported_name("m.py", module="pkg", name="b") + with pytest.raises(AssertionError): + _apply(r, tmp_path) + + +def test_add_imported_name_rejects_a_name_already_present(tmp_path: Path) -> None: + """Adding a name the import already has fails loudly.""" + (tmp_path / "m.py").write_text("from pkg import a, b\n") + r = Repro("b", "t").add_imported_name("m.py", module="pkg", name="b") + with pytest.raises(AssertionError): + _apply(r, tmp_path) + + +def test_add_imported_name_raises_without_a_matching_import(tmp_path: Path) -> None: + """A file lacking a `from module import` for the module fails loudly.""" + (tmp_path / "m.py").write_text("from other import a\n") + r = Repro("b", "t").add_imported_name("m.py", module="pkg", name="b") + with pytest.raises(AssertionError): + _apply(r, tmp_path) + + # --- repath_import / add_typechecking_import ----------------------------------- @@ -64,6 +107,33 @@ def test_add_typechecking_import_inserts_in_block(tmp_path: Path) -> None: ) +def test_add_typechecking_import_creates_missing_block(tmp_path: Path) -> None: + """With no TYPE_CHECKING block, one is created after the trailing module import.""" + (tmp_path / "m.py").write_text( + "from typing import TYPE_CHECKING\n" + "\n" + "from a import X\n" + "\n" + "\n" + "def f():\n" + " pass\n" + ) + r = Repro("b", "t").add_typechecking_import("m.py", "from b import Y") + _apply(r, tmp_path) + assert (tmp_path / "m.py").read_text() == ( + "from typing import TYPE_CHECKING\n" + "\n" + "from a import X\n" + "\n" + "if TYPE_CHECKING:\n" + " from b import Y\n" + "\n" + "\n" + "def f():\n" + " pass\n" + ) + + def test_add_import_into_an_empty_file(tmp_path: Path) -> None: """Adding an import to an empty file writes just the statement.""" (tmp_path / "m.py").write_text("") @@ -134,9 +204,81 @@ def test_add_typechecking_import_after_a_multiline_final_import(tmp_path: Path) ) -def test_add_typechecking_import_raises_without_a_block(tmp_path: Path) -> None: - """A file lacking a TYPE_CHECKING block fails loudly.""" - (tmp_path / "m.py").write_text("import os\n\nx = 1\n") +def test_add_typechecking_import_raises_without_imports(tmp_path: Path) -> None: + """A file with no imports cannot anchor a new TYPE_CHECKING block and fails loudly.""" + (tmp_path / "m.py").write_text("x = 1\n") r = Repro("b", "t").add_typechecking_import("m.py", "from b import Y") with pytest.raises(AssertionError): _apply(r, tmp_path) + + +def test_add_typechecking_import_drops_a_lone_pass_placeholder(tmp_path: Path) -> None: + """Populating a `pass`-only TYPE_CHECKING block replaces the placeholder.""" + (tmp_path / "m.py").write_text( + "from typing import TYPE_CHECKING\n" + "\n" + "if TYPE_CHECKING:\n" + " pass\n" + "\n" + "x = 1\n" + ) + r = Repro("b", "t").add_typechecking_import("m.py", "from b import Y") + _apply(r, tmp_path) + assert (tmp_path / "m.py").read_text() == ( + "from typing import TYPE_CHECKING\n" + "\n" + "if TYPE_CHECKING:\n" + " from b import Y\n" + "\n" + "x = 1\n" + ) + + +def test_add_typechecking_import_keeps_a_pass_that_is_not_alone(tmp_path: Path) -> None: + """A `pass` beside a real import is left untouched; only the new import is appended.""" + (tmp_path / "m.py").write_text( + "from typing import TYPE_CHECKING\n" + "\n" + "if TYPE_CHECKING:\n" + " from a import X\n" + " pass\n" + "\n" + "x = 1\n" + ) + r = Repro("b", "t").add_typechecking_import("m.py", "from b import Y") + _apply(r, tmp_path) + assert (tmp_path / "m.py").read_text() == ( + "from typing import TYPE_CHECKING\n" + "\n" + "if TYPE_CHECKING:\n" + " from a import X\n" + " pass\n" + " from b import Y\n" + "\n" + "x = 1\n" + ) + + +# --- add_import(after=...) ----------------------------------------------------- + + +def test_add_import_after_anchors_into_a_split_import_block(tmp_path: Path) -> None: + """With `after`, the import lands right after the named import -- needed when a + statement splits the imports into separate blocks and the default (after the last + import) would land in the wrong block.""" + (tmp_path / "m.py").write_text( + "import os\n\n_flag = os.getpid()\n\nfrom pkg import a\n\nx = 1\n" + ) + r = Repro("b", "t").add_import("m.py", "from new import Thing", after="import os") + _apply(r, tmp_path) + assert (tmp_path / "m.py").read_text() == ( + "import os\nfrom new import Thing\n\n_flag = os.getpid()\n\nfrom pkg import a\n\nx = 1\n" + ) + + +def test_add_import_after_raises_when_anchor_absent(tmp_path: Path) -> None: + """An `after` substring that matches no top-level import raises.""" + (tmp_path / "m.py").write_text("import os\n\nx = 1\n") + r = Repro("b", "t").add_import("m.py", "from new import Thing", after="import nope") + with pytest.raises(AssertionError): + _apply(r, tmp_path) diff --git a/.claude/skills/mechanical-refactor-verify/scripts/tests/reproduction_utils/test_call_sites.py b/.claude/skills/mechanical-refactor-verify/scripts/tests/reproduction_utils/test_call_sites.py index 83d8cfa5f..87ced0522 100644 --- a/.claude/skills/mechanical-refactor-verify/scripts/tests/reproduction_utils/test_call_sites.py +++ b/.claude/skills/mechanical-refactor-verify/scripts/tests/reproduction_utils/test_call_sites.py @@ -79,6 +79,38 @@ def test_requalify_call_sites_drops_the_qualifier(tmp_path: Path) -> None: assert (tmp_path / "m.py").read_text() == "y = bar(a, b)\n" +def test_route_call_sites_through_field_inserts_the_field(tmp_path: Path) -> None: + """recv.bar(a) becomes recv.updater.bar(a) when bar moves onto a collaborator field.""" + (tmp_path / "m.py").write_text("y = self.worker.runner.bar(a)\n") + r = Repro("b", "t").route_call_sites_through_field( + "bar", field="updater", paths=["m.py"] + ) + _apply(r, tmp_path) + assert (tmp_path / "m.py").read_text() == "y = self.worker.runner.updater.bar(a)\n" + + +def test_route_call_sites_through_field_skips_an_already_routed_call( + tmp_path: Path, +) -> None: + """A call already going through the field is left alone, so the pass converges.""" + (tmp_path / "m.py").write_text("y = self.runner.updater.bar(a)\n") + r = Repro("b", "t").route_call_sites_through_field( + "bar", field="updater", paths=["m.py"] + ) + _apply(r, tmp_path) + assert (tmp_path / "m.py").read_text() == "y = self.runner.updater.bar(a)\n" + + +def test_route_call_sites_through_field_honors_owner_filter(tmp_path: Path) -> None: + """With owner set, only calls on that exact receiver are routed through the field.""" + (tmp_path / "m.py").write_text("a = x.bar(1)\nb = y.bar(2)\n") + r = Repro("b", "t").route_call_sites_through_field( + "bar", field="updater", paths=["m.py"], owner="x" + ) + _apply(r, tmp_path) + assert (tmp_path / "m.py").read_text() == "a = x.updater.bar(1)\nb = y.bar(2)\n" + + # --- adversarial audit: call-site rewrites --------------------------------------- diff --git a/.claude/skills/mechanical-refactor-verify/scripts/tests/reproduction_utils/test_delete_file.py b/.claude/skills/mechanical-refactor-verify/scripts/tests/reproduction_utils/test_delete_file.py index 5d874c88c..8347def97 100644 --- a/.claude/skills/mechanical-refactor-verify/scripts/tests/reproduction_utils/test_delete_file.py +++ b/.claude/skills/mechanical-refactor-verify/scripts/tests/reproduction_utils/test_delete_file.py @@ -46,4 +46,23 @@ def test_delete_file_on_a_missing_path_is_a_no_op(tmp_path: Path) -> None: assert not (tmp_path / "nope.py").exists() +def test_delete_file_allows_a_bare_module_logger(tmp_path: Path) -> None: + """A leftover module holding only imports and a `logger` is deletable scaffolding.""" + (tmp_path / "gone.py").write_text( + "import logging\n\nlogger = logging.getLogger(__name__)\n" + ) + r = Repro("b", "t").delete_file("gone.py") + _apply(r, tmp_path) + assert not (tmp_path / "gone.py").exists() + + +def test_delete_file_still_refuses_a_non_logger_assignment(tmp_path: Path) -> None: + """A leftover module-level assignment other than a logger blocks deletion.""" + (tmp_path / "live.py").write_text("CONFIG = {'a': 1}\n") + r = Repro("b", "t").delete_file("live.py") + with pytest.raises(AssertionError): + _apply(r, tmp_path) + assert (tmp_path / "live.py").exists() + + # --- adversarial audit: extract_function ----------------------------------------- diff --git a/.claude/skills/mechanical-refactor-verify/scripts/tests/reproduction_utils/test_extract_symbols_to_new_module.py b/.claude/skills/mechanical-refactor-verify/scripts/tests/reproduction_utils/test_extract_symbols_to_new_module.py index ed12fbb20..26d9fae2f 100644 --- a/.claude/skills/mechanical-refactor-verify/scripts/tests/reproduction_utils/test_extract_symbols_to_new_module.py +++ b/.claude/skills/mechanical-refactor-verify/scripts/tests/reproduction_utils/test_extract_symbols_to_new_module.py @@ -144,6 +144,30 @@ def test_extract_symbols_to_new_module_asserts_unknown_drop_assign( _apply(r, tmp_path) +def test_extract_symbols_to_new_module_header_accepts_a_typechecking_block( + tmp_path: Path, +) -> None: + """An authored header may carry an `if TYPE_CHECKING:` import block; the audit accepts it + and the block is reproduced verbatim in the new module.""" + (tmp_path / "src.py").write_text("def moved(x):\n return x\n") + header = ( + "from __future__ import annotations\n" + "\n" + "from typing import TYPE_CHECKING\n" + "\n" + "if TYPE_CHECKING:\n" + " from other import Thing\n" + "\n" + ) + r = Repro("b", "t").extract_symbols_to_new_module( + "src.py", "new.py", symbols=["moved"], header=header, order=["moved"] + ) + _apply(r, tmp_path) + new_out = (tmp_path / "new.py").read_text() + assert "if TYPE_CHECKING:\n from other import Thing\n" in new_out + assert "def moved(x):\n return x\n" in new_out + + # --- extract_function ---------------------------------------------------------- @@ -197,3 +221,44 @@ def test_extract_symbols_drop_assigns_preserves_other_targets_of_chained_assign( ) _apply(r, tmp_path) assert "B" in (tmp_path / "src.py").read_text() + + +def test_extract_symbols_to_new_module_allows_a_rederived_surviving_constant( + tmp_path: Path, +) -> None: + """A header constant that also survives verbatim in the source (re-derived boilerplate, + e.g. `_is_hip = is_hip()`) is allowed: it is provably not fiction because the same + statement remains in the source.""" + (tmp_path / "src.py").write_text( + "from pkg import is_hip\n" + "\n" + "_is_hip = is_hip()\n" + "\n" + "\n" + "def moved():\n" + " return _is_hip\n" + ) + header = "from pkg import is_hip\n\n_is_hip = is_hip()\n" + r = Repro("b", "t").extract_symbols_to_new_module( + "src.py", "new.py", symbols=["moved"], header=header, order=["moved"] + ) + _apply(r, tmp_path) + assert "_is_hip = is_hip()" in (tmp_path / "src.py").read_text() + assert "_is_hip = is_hip()" in (tmp_path / "new.py").read_text() + + +def test_extract_symbols_to_new_module_rejects_a_fictional_header_constant( + tmp_path: Path, +) -> None: + """A header constant that is neither dropped from nor surviving in the source is fiction + and raises: the audit refuses code the extraction cannot vouch for.""" + (tmp_path / "src.py").write_text("def moved():\n return 1\n") + r = Repro("b", "t").extract_symbols_to_new_module( + "src.py", + "new.py", + symbols=["moved"], + header="_fake = evil()\n", + order=["moved"], + ) + with pytest.raises(AssertionError): + _apply(r, tmp_path) diff --git a/.claude/skills/mechanical-refactor-verify/scripts/tests/reproduction_utils/test_move_assign.py b/.claude/skills/mechanical-refactor-verify/scripts/tests/reproduction_utils/test_move_assign.py new file mode 100644 index 000000000..762eab97f --- /dev/null +++ b/.claude/skills/mechanical-refactor-verify/scripts/tests/reproduction_utils/test_move_assign.py @@ -0,0 +1,69 @@ +import sys +from pathlib import Path + +import pytest + +sys.path.insert(0, str(Path(__file__).resolve().parents[2])) + +from mechanical_refactor_reproduction_utils import Repro +from reproduction_testlib import _apply # noqa: F401 + + +def test_move_assign_relocates_a_module_constant(tmp_path: Path) -> None: + """The assignment is cut verbatim from the source and lands after the destination's imports.""" + (tmp_path / "src.py").write_text( + "import os\n\nLIMIT = 480 # seconds\n\n\ndef stay():\n return LIMIT\n" + ) + (tmp_path / "dst.py").write_text("import sys\n\n\ndef keep():\n return 1\n") + r = Repro("b", "t").move_assign("LIMIT", src="src.py", dst="dst.py") + _apply(r, tmp_path) + assert "LIMIT" not in (tmp_path / "src.py").read_text().split("def stay")[0] + assert (tmp_path / "dst.py").read_text() == ( + "import sys\n" + "\n" + "LIMIT = 480 # seconds\n" + "\n" + "\n" + "def keep():\n" + " return 1\n" + ) + + +def test_move_assign_pastes_above_the_named_sibling(tmp_path: Path) -> None: + """With before=, the constant lands immediately above the named top-level statement.""" + (tmp_path / "src.py").write_text("RATIO = 3\n") + (tmp_path / "dst.py").write_text("def first():\n return 1\n") + r = Repro("b", "t").move_assign("RATIO", src="src.py", dst="dst.py", before="first") + _apply(r, tmp_path) + assert (tmp_path / "dst.py").read_text() == ( + "RATIO = 3\n\ndef first():\n return 1\n" + ) + + +def test_move_assign_relocates_an_annotated_constant(tmp_path: Path) -> None: + """An annotated module constant (AnnAssign) is cut verbatim with its annotation intact.""" + (tmp_path / "src.py").write_text( + "import os\n\nLIMIT: int = 480\n\n\ndef stay():\n return LIMIT\n" + ) + (tmp_path / "dst.py").write_text("import sys\n\n\ndef keep():\n return 1\n") + r = Repro("b", "t").move_assign("LIMIT", src="src.py", dst="dst.py") + _apply(r, tmp_path) + assert "LIMIT" not in (tmp_path / "src.py").read_text().split("def stay")[0] + assert (tmp_path / "dst.py").read_text() == ( + "import sys\n" + "\n" + "LIMIT: int = 480\n" + "\n" + "\n" + "def keep():\n" + " return 1\n" + ) + + +def test_move_assign_missing_source_raises(tmp_path: Path) -> None: + """A name with no module-level assignment in the source fails loudly.""" + (tmp_path / "src.py").write_text("x = 1\n") + (tmp_path / "dst.py").write_text("import os\n") + r = Repro("b", "t").move_assign("MISSING", src="src.py", dst="dst.py") + with pytest.raises(AssertionError): + _apply(r, tmp_path) diff --git a/.claude/skills/mechanical-refactor-verify/scripts/tests/reproduction_utils/test_move_symbol.py b/.claude/skills/mechanical-refactor-verify/scripts/tests/reproduction_utils/test_move_symbol.py index cf6863ef7..a5f74a687 100644 --- a/.claude/skills/mechanical-refactor-verify/scripts/tests/reproduction_utils/test_move_symbol.py +++ b/.claude/skills/mechanical-refactor-verify/scripts/tests/reproduction_utils/test_move_symbol.py @@ -321,6 +321,76 @@ def test_move_symbol_rejects_ambiguous_duplicate_names(tmp_path: Path) -> None: _apply(r, tmp_path) +def test_move_symbol_after_inserts_below_named_function(tmp_path: Path) -> None: + """With after=, the relocated def lands immediately below that sibling def.""" + (tmp_path / "src.py").write_text("def moved():\n return 1\n") + (tmp_path / "dst.py").write_text( + "def first():\n return 0\n\n\ndef last():\n return 2\n" + ) + r = Repro("b", "t").move_symbol( + "moved", src="src.py", dst="dst.py", into_class=None, after="first" + ) + _apply(r, tmp_path) + dst_out = (tmp_path / "dst.py").read_text() + assert ( + dst_out.index("def first") + < dst_out.index("def moved") + < dst_out.index("def last") + ) + + +def test_move_symbol_after_assign_lands_before_typechecking_guard( + tmp_path: Path, +) -> None: + """after= anchors on a module-level assignment target, landing the def just below it and + above a following ``if TYPE_CHECKING:`` guard (which is not a nameable anchor).""" + (tmp_path / "src.py").write_text("def helper(x):\n return x + 1\n") + (tmp_path / "dst.py").write_text( + "from u import is_hip\n" + "\n" + "_is_hip = is_hip()\n" + "\n" + "if TYPE_CHECKING:\n" + " from m import Thing\n" + ) + r = Repro("b", "t").move_symbol( + "helper", src="src.py", dst="dst.py", into_class=None, after="_is_hip" + ) + _apply(r, tmp_path) + dst_out = (tmp_path / "dst.py").read_text() + assert ( + dst_out.index("_is_hip = is_hip()") + < dst_out.index("def helper") + < dst_out.index("if TYPE_CHECKING:") + ) + + +def test_move_symbol_before_and_after_are_mutually_exclusive(tmp_path: Path) -> None: + """Passing both before= and after= is rejected up front.""" + (tmp_path / "src.py").write_text("def moved():\n return 1\n") + (tmp_path / "dst.py").write_text("def z():\n return 0\n") + with pytest.raises(AssertionError): + Repro("b", "t").move_symbol( + "moved", + src="src.py", + dst="dst.py", + into_class=None, + before="z", + after="z", + ) + + +def test_move_symbol_asserts_when_after_symbol_missing(tmp_path: Path) -> None: + """An after= anchor absent from the destination must raise, not fall back to append.""" + (tmp_path / "src.py").write_text("def moved():\n return 1\n") + (tmp_path / "dst.py").write_text("def z():\n return 0\n") + r = Repro("b", "t").move_symbol( + "moved", src="src.py", dst="dst.py", into_class=None, after="NO_SUCH_SYMBOL" + ) + with pytest.raises(AssertionError): + _apply(r, tmp_path) + + def test_move_symbol_asserts_when_before_sibling_missing(tmp_path: Path) -> None: """A before= anchor absent from the destination must raise, not fall back to append.""" (tmp_path / "src.py").write_text("def moved():\n return 1\n") @@ -357,4 +427,21 @@ def test_move_symbol_negative_dedent_indents_into_the_class(tmp_path: Path) -> N assert " def helper(x):\n return x\n" in (tmp_path / "dst.py").read_text() +def test_move_symbol_relocates_a_top_level_class(tmp_path: Path) -> None: + """move_symbol relocates a whole top-level class (with its methods) verbatim.""" + (tmp_path / "src.py").write_text( + "x = 1\n\n\nclass Widget:\n def get(self, rank):\n return rank\n" + ) + (tmp_path / "dst.py").write_text("y = 2\n") + r = Repro("b", "t").move_symbol( + "Widget", src="src.py", dst="dst.py", into_class=None + ) + _apply(r, tmp_path) + assert "class Widget:" not in (tmp_path / "src.py").read_text() + assert ( + "class Widget:\n def get(self, rank):\n return rank\n" + in (tmp_path / "dst.py").read_text() + ) + + # --- adversarial audit: leave_delegate stubs ------------------------------------- diff --git a/.claude/skills/mechanical-refactor-verify/scripts/tests/reproduction_utils/test_move_symbol_delegate.py b/.claude/skills/mechanical-refactor-verify/scripts/tests/reproduction_utils/test_move_symbol_delegate.py index b9e20da71..6761a0490 100644 --- a/.claude/skills/mechanical-refactor-verify/scripts/tests/reproduction_utils/test_move_symbol_delegate.py +++ b/.claude/skills/mechanical-refactor-verify/scripts/tests/reproduction_utils/test_move_symbol_delegate.py @@ -193,3 +193,121 @@ def test_move_symbol_async_leave_delegate_awaits_the_forwarded_call( ) _apply(r, tmp_path) assert "return await self.cfg.compute(n)" in (tmp_path / "src.py").read_text() + + +def test_move_symbol_leave_delegate_on_self_annotated_staticmethod( + tmp_path: Path, +) -> None: + """A de-self'd staticmethod (self: Target) moves into Target; the stub drops the + decorator and the self annotation.""" + (tmp_path / "src.py").write_text( + "class Runner:\n" + " @staticmethod\n" + " def work(self: Comp, n: int) -> int:\n" + " return n + self.base\n" + ) + (tmp_path / "dst.py").write_text( + "class Comp:\n def existing(self):\n return 0\n" + ) + r = Repro("b", "t").move_symbol( + "work", + src="src.py", + dst="dst.py", + into_class="Comp", + from_class="Runner", + drop_self_annotation=True, + leave_delegate="comp", + ) + _apply(r, tmp_path) + assert (tmp_path / "src.py").read_text() == ( + "class Runner:\n" + " def work(self, n: int) -> int:\n" + " return self.comp.work(n)\n" + ) + assert (tmp_path / "dst.py").read_text() == ( + "class Comp:\n" + " def existing(self):\n" + " return 0\n" + "\n" + " def work(self, n: int) -> int:\n" + " return n + self.base\n" + ) + + +def test_move_symbol_leave_delegate_keeps_unrelated_self_annotation( + tmp_path: Path, +) -> None: + """A self annotation naming a class other than the destination survives in the stub.""" + (tmp_path / "src.py").write_text( + "class Mixin:\n" + " def work(self: Runner, n: int) -> int:\n" + " return n + self.base\n" + ) + (tmp_path / "dst.py").write_text( + "class Comp:\n def existing(self):\n return 0\n" + ) + r = Repro("b", "t").move_symbol( + "work", + src="src.py", + dst="dst.py", + into_class="Comp", + from_class="Mixin", + drop_self_annotation=True, + leave_delegate="comp", + ) + _apply(r, tmp_path) + assert (tmp_path / "src.py").read_text() == ( + "class Mixin:\n" + " def work(self: Runner, n: int) -> int:\n" + " return self.comp.work(n)\n" + ) + + +def test_move_symbol_delegate_name_forwards_to_the_renamed_collaborator_method( + tmp_path: Path, +) -> None: + """delegate_name makes the stub call a differently-named method on the collaborator.""" + (tmp_path / "src.py").write_text( + "class Mixin:\n" + " def compute(self, n: int) -> int:\n" + " return n + self.cfg.base\n" + ) + (tmp_path / "dst.py").write_text( + "class Cfg:\n def existing(self):\n return 0\n" + ) + r = Repro("b", "t").move_symbol( + "compute", + src="src.py", + dst="dst.py", + into_class="Cfg", + leave_delegate="cfg", + delegate_name="compute_impl", + ) + _apply(r, tmp_path) + assert "return self.cfg.compute_impl(n)" in (tmp_path / "src.py").read_text() + assert "def compute(self, n: int) -> int:" in (tmp_path / "dst.py").read_text() + + +def test_move_symbol_leave_delegate_on_unannotated_staticmethod_raises( + tmp_path: Path, +) -> None: + """A staticmethod with no self: Target annotation has no receiver to forward through, so + leave_delegate refuses rather than author a bogus self..(...) stub.""" + (tmp_path / "src.py").write_text( + "class Runner:\n" + " @staticmethod\n" + " def work(x: int) -> int:\n" + " return x + 1\n" + ) + (tmp_path / "dst.py").write_text( + "class Comp:\n def existing(self):\n return 0\n" + ) + r = Repro("b", "t").move_symbol( + "work", + src="src.py", + dst="dst.py", + into_class="Comp", + leave_delegate="comp", + ) + with pytest.raises(AssertionError): + _apply(r, tmp_path) diff --git a/.claude/skills/mechanical-refactor-verify/scripts/tests/reproduction_utils/test_remove_import.py b/.claude/skills/mechanical-refactor-verify/scripts/tests/reproduction_utils/test_remove_import.py index 17e89cb2f..0f7a49452 100644 --- a/.claude/skills/mechanical-refactor-verify/scripts/tests/reproduction_utils/test_remove_import.py +++ b/.claude/skills/mechanical-refactor-verify/scripts/tests/reproduction_utils/test_remove_import.py @@ -118,6 +118,21 @@ def test_remove_import_leaves_other_statements_on_a_semicolon_line( assert "import sys" in out and "print(sys.path)" in out +def test_remove_import_trailing_on_a_semicolon_line_leaves_no_dangling_separator( + tmp_path: Path, +) -> None: + """Removing the trailing import on a semicolon-joined line drops the dangling ';' too + (a trailing space may remain for the formatter to strip, but the separator is gone). + """ + (tmp_path / "m.py").write_text("import sys; import os\nprint(sys.path)\n") + r = Repro("b", "t").remove_import("m.py", "import os") + _apply(r, tmp_path) + out = (tmp_path / "m.py").read_text() + assert ";" not in out + assert "import os" not in out + assert "import sys" in out and "print(sys.path)" in out + + def test_remove_import_does_not_overmatch_a_submodule_import(tmp_path: Path) -> None: """Removing 'import os' must not also remove 'import os.path'.""" (tmp_path / "m.py").write_text("import os\nimport os.path\nprint(os.path.sep)\n") diff --git a/.claude/skills/mechanical-refactor-verify/scripts/tests/reproduction_utils/test_remove_imported_name.py b/.claude/skills/mechanical-refactor-verify/scripts/tests/reproduction_utils/test_remove_imported_name.py index 3fe06a681..1b5a7a694 100644 --- a/.claude/skills/mechanical-refactor-verify/scripts/tests/reproduction_utils/test_remove_imported_name.py +++ b/.claude/skills/mechanical-refactor-verify/scripts/tests/reproduction_utils/test_remove_imported_name.py @@ -75,16 +75,49 @@ def test_remove_imported_name_asserts_when_absent(tmp_path: Path) -> None: # --- add_import ---------------------------------------------------------------- -def test_remove_imported_name_collapses_a_multiline_import_to_one_line( +def test_remove_imported_name_preserves_the_multiline_form( tmp_path: Path, ) -> None: - """Pruning a name from a parenthesized import rebuilds it as a single sorted-later line.""" + """Pruning a name from an exploded import deletes only that line, so the parens and the + magic trailing comma survive and the formatter keeps it multi-line (a flat rebuild would + collapse an import the target left multi-line).""" (tmp_path / "m.py").write_text( "from pkg import (\n a,\n moved,\n b,\n)\n\nx = a + b\n" ) r = Repro("b", "t").remove_imported_name("m.py", module="pkg", name="moved") _apply(r, tmp_path) - assert (tmp_path / "m.py").read_text() == "from pkg import a, b\n\nx = a + b\n" + assert ( + tmp_path / "m.py" + ).read_text() == "from pkg import (\n a,\n b,\n)\n\nx = a + b\n" + + +def test_remove_imported_name_multiline_down_to_one_collapses( + tmp_path: Path, +) -> None: + """Pruning an exploded import down to a single surviving name collapses it to one line: + the formatter does not keep a lone name exploded, so a preserved-multiline form would + not match the target.""" + (tmp_path / "m.py").write_text( + "from pkg import (\n moved,\n a,\n)\n\nx = a\n" + ) + r = Repro("b", "t").remove_imported_name("m.py", module="pkg", name="moved") + _apply(r, tmp_path) + assert (tmp_path / "m.py").read_text() == "from pkg import a\n\nx = a\n" + + +def test_remove_imported_name_down_to_one_with_a_comment_stays_exploded( + tmp_path: Path, +) -> None: + """A lone survivor that carries a comment stays exploded (a rebuild would drop the + comment); only its own line is deleted.""" + (tmp_path / "m.py").write_text( + "from pkg import (\n moved,\n a, # keep me\n)\n\nx = a\n" + ) + r = Repro("b", "t").remove_imported_name("m.py", module="pkg", name="moved") + _apply(r, tmp_path) + assert ( + tmp_path / "m.py" + ).read_text() == "from pkg import (\n a, # keep me\n)\n\nx = a\n" def test_remove_imported_name_matches_a_relative_module(tmp_path: Path) -> None: @@ -111,3 +144,20 @@ def test_remove_imported_name_preserves_comments_in_a_multiline_import( r = Repro("b", "t").remove_imported_name("m.py", module="pkg", name="moved") _apply(r, tmp_path) assert "# used by frobnicator" in (tmp_path / "m.py").read_text() + + +def test_remove_imported_name_keep_exploded_holds_a_lone_survivor_multiline( + tmp_path: Path, +) -> None: + """With keep_exploded, pruning down to a single survivor deletes only the removed line, + so the survivor keeps its magic trailing comma and the import stays multi-line (the + author's choice, which the source cannot reveal). A regenerating impl would collapse. + """ + (tmp_path / "m.py").write_text( + "from pkg import (\n moved,\n a,\n)\n\nx = a\n" + ) + r = Repro("b", "t").remove_imported_name( + "m.py", module="pkg", name="moved", keep_exploded=True + ) + _apply(r, tmp_path) + assert (tmp_path / "m.py").read_text() == "from pkg import (\n a,\n)\n\nx = a\n" diff --git a/.claude/skills/mechanical-refactor-verify/spec-reproduction-cli.md b/.claude/skills/mechanical-refactor-verify/spec-reproduction-cli.md new file mode 100644 index 000000000..8ec1617c4 --- /dev/null +++ b/.claude/skills/mechanical-refactor-verify/spec-reproduction-cli.md @@ -0,0 +1,153 @@ +# Reproduction CLI — chain verification specification (source of truth) + +## 1. Scope + +- Source of truth for `scripts/mechanical_refactor_reproduction_cli.py`: the + **verified-chain property** (§2), the CLI contract (§3), the report (§4), and the exit + codes (§5). +- The single-commit clean-move property and the proof scripts themselves are specified in + `spec-reproduction-utils.md`; this file only says how a whole chain of commits is + checked against a folder of such proofs. +- The CLI, its tests, and the guides defer to this file; on any disagreement, this file + wins. + +## 2. The property — a "verified chain" + +> A branch is a **verified chain** over a base iff every commit in `base..branch` is +> **classified** (§2.1) and every `mechanical_provable` commit has exactly one **proof** +> in the proof folder whose run **PASSes** (§2.2). + +### 2.1 Classification — the word rule + +- Every commit message must contain **exactly one** of the two words: + - `mechanical_provable` — the commit claims to be a machine-provable relocation; + - `non_mechanical_provable` — the commit declares that **nothing in it** is + expressible as the whitelisted relocations of `spec-reproduction-utils.md` §2 — it + is the minimal unprovable residue, left to human review. +- The declaration is an assertion, not an opt-out: labeling provable content + `non_mechanical_provable` to dodge the verifier **violates the chain property**, even + where no machine check catches it. A provable part hiding inside a semantic commit + belongs in its own `mechanical_provable` commit with a proof + (`guide-split.md` §2.2). +- The rest of the message format is unconstrained **by the machine rule**: the word may + appear anywhere in the subject or body, in any surrounding syntax. The authoring + contract additionally fixes the subject format + (`(,): `, `guide-split.md` §1.1), which satisfies + this rule by construction; the verifier deliberately checks only the word, so a chain + from a different convention still verifies. +- A word counts only standalone: delimited by a non-`[0-9A-Za-z_]` character or the + message boundary, lowercase, so `non_mechanical_provable` never also counts as the bare + word, and `xmechanical_provable` counts as neither. +- Repeating the same word is fine; the rule is about **which** of the two is declared: + - neither word present → `UNCLASSIFIED`; + - both words present → `AMBIGUOUS_KIND`. + +### 2.2 The proof obligation + +- Each `mechanical_provable` commit must resolve to exactly one proof script (§3.3); + none is `MISSING_PROOF`, several is `AMBIGUOUS_PROOF`. +- The proof must run to a PASS (§3.4): the commit reproduces byte-for-byte from its + parent (`spec-reproduction-utils.md` §4). Anything else is `FAIL`. +- A `non_mechanical_provable` commit has no machine obligation; its verdict is + `HUMAN_REVIEW` — the report marks it for eyes, never certifies it. Whether its + declaration is honest is the reviewer's duty to check (`guide-verify-proof.md` §1). +- The chain verdict is PASS iff every commit's verdict is `PASS` or `HUMAN_REVIEW`. + +## 3. The CLI contract + +### 3.1 Invocation + +```bash +python3 .claude/skills/mechanical-refactor-verify/scripts/mechanical_refactor_reproduction_cli.py \ + --base --branch --proof path/to/proof/folder +``` + +- `--base` / `--branch`: any commit-ish; both must resolve, `base` must be an ancestor of + `branch`. +- `--proof`: the proof folder (must exist) — typically the generator's `--out` product + (`guide-construct-proof.md` §1.2). +- `--repo-root DIR`: run against that repo instead of the cwd's. +- `--report PATH`: write the report there instead of `/chain_report.md`. +- `--jobs N`: run up to N proofs concurrently (default 3). +- `--skip-passed`: reuse this machine's own earlier PASS verdicts (§3.5). + +### 3.2 The chain + +- The commits are `git rev-list --reverse base..branch`, i.e. the whole chain in order. +- The chain must be **linear**: a merge commit anywhere in it is a setup error — per-commit + proofs are meaningless across a merge. +- An empty range is a setup error, not a trivially-green chain. + +### 3.3 Proof resolution + +- A commit's proof is a `.py` whose stem is lowercase hex, at least 7 + characters, and a prefix of the commit's full sha. +- Searched locations, in order, both always considered: `/repro_scripts/` (the + generator layout) and `/` flat (the gist layout, + `guide-construct-proof.md` §1.3.1). +- Proofs are keyed by current shas: after a rebase the shas change, so the proofs must be + regenerated for the rebased chain. + +### 3.4 Proof execution and the PASS criterion + +- Each proof runs as `python3