358 lines
19 KiB
Markdown
358 lines
19 KiB
Markdown
# Split a mechanical refactor
|
|
|
|
- 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
|
|
<group-id>(<commit-id>,<kind>): <message>
|
|
```
|
|
|
|
with `<kind>` exactly `mechanical_provable` or `non_mechanical_provable`, and
|
|
`<group-id>` / `<commit-id>` kebab-case (contiguous same-`<group-id>` 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 `<commit-id>` 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 '(?<!_)mechanical_provable'` (the lookbehind keeps `non_mechanical_provable`
|
|
from matching).
|
|
|
|
## 2. Split one piece into prepare + move + postpare
|
|
|
|
### 2.1 Why split
|
|
|
|
- A "move a method/function" change is really **two operations with different
|
|
correctness criteria**:
|
|
|
|
| Operation | What it does | How you check it |
|
|
|---|---|---|
|
|
| **Semantic reshape** | method → free function or method; `self.X` → a parameter, or `self` retyped to the target class; signature / typing change | behavior unchanged: lint + tests pass |
|
|
| **Physical move** | cut from the source, paste into the target, fix imports | the moved body is byte-identical, line for line; the only other changes are move artifacts |
|
|
|
|
- Put both in one commit and the criteria contaminate each other:
|
|
- one hunk then holds the reshape **and** an indentation shift **and** a cross-file
|
|
relocation;
|
|
- neither a human nor a tool can mechanically confirm "the body that landed is the
|
|
body that left" — you must re-read the logic.
|
|
|
|
### 2.2 The rule — up to three commits, in this order
|
|
|
|
- **prepare (optional)** — a **minimal** in-place reshape the relocation needs (de-self a
|
|
method, retype `self`). Human-reviewed, so: small, **no cross-file def relocation, no
|
|
body relocation** — the code stays where it is.
|
|
- **move** — the pure relocation; carries the **bulk**; certified by the reproduce proof
|
|
(`guide-construct-proof.md`; property: `spec-reproduction-utils.md`).
|
|
- **postpare (optional)** — a **minimal** tail fixup the move cannot do mechanically (a
|
|
module path inside a string literal, a doc reference). Human-reviewed.
|
|
|
|
Hard lines ("prep" below = the prepare phase):
|
|
|
|
- Both ends are optional, minimal, and covered by tests; neither ever relocates a def
|
|
across files or moves a body.
|
|
- The move-artifact whitelist is what a relocation *forces* — **not** a licence to fold
|
|
reshape work into the move. Anything outside the artifacts in the move's diff = the
|
|
reshape leaked; push it back into prep.
|
|
- **A large semantic refactor is not a phase.** Consolidating bookkeeping, deduplicating
|
|
logic, restructuring control flow, redesigning an API → its **own commit**, reviewed for
|
|
**equivalence** (tests or a written argument). Never smuggled into prep as a "small
|
|
reshape".
|
|
- **Provable content never hides in a non-provable commit.** The dual of the previous
|
|
two rules: a commit declared `non_mechanical_provable` must be the **minimal residue**
|
|
the relocation primitives cannot express. Any part reproducible as whitelisted
|
|
relocations (`spec-reproduction-utils.md` §2.1) — a def moved across files, a scattered
|
|
extract, an import repoint riding along — is split into its own `mechanical_provable`
|
|
commit with a proof, never folded into a semantic commit where the verifier cannot see
|
|
it. Declaring provable work non-provable to dodge the verifier violates the chain
|
|
property (`spec-reproduction-cli.md` §2.1); the reviewer is instructed to hunt for
|
|
exactly this (`guide-verify-proof.md` §1).
|
|
- **"Semantic" is not banned from prepare — oversized or hidden semantics are.** prepare's
|
|
own edits *are* meaning-carrying (de-self, retype-`self`, co-locating bookkeeping);
|
|
"minimal" caps their **size**, it does not forbid semantics. The two bans are narrower:
|
|
(1) no semantic change inside the **move** commit — the move is a pure relocation; and
|
|
(2) don't pass a **large** reshape off as a trivial "small reshape" to dodge the
|
|
equivalence review. A large but honestly-labeled, equivalence-reviewed reshape placed
|
|
*before* the move is legitimate — that is exactly what "its own commit" means, and it
|
|
may serve as the prepare.
|
|
|
|
- The prep's shape depends on the destination: a module-level function (§2.3) or a class
|
|
(§2.4).
|
|
- The move is the same idea in both: a pure relocation, body byte-identical.
|
|
|
|
### 2.3 Case 1: method → free function
|
|
|
|
#### 2.3.1 Commit 1 — prep: de-self in place (no relocation)
|
|
|
|
Reshape the method **in its original file and position** so it no longer needs `self`.
|
|
The body stays put:
|
|
|
|
- `self.X` (read) → pass `X` in as a parameter.
|
|
- `self.X = v` (write) → `return v`; the caller assigns. (Or pass an explicit mutable
|
|
object.)
|
|
- `self.other_method(...)` → prep that method in the same commit, or inject it as a
|
|
`Callable` argument.
|
|
- Once `self` is gone → mark `@staticmethod`; the body **does not move**.
|
|
- Call site: `self.foo(args)` → `TheClass.foo(args)`.
|
|
- **Seed the destination's module-level scaffolding here too**, if the target module
|
|
lacks what the moved body needs — a `logger = logging.getLogger(__name__)`, a
|
|
module-level constant the body reads (`_is_hip = is_hip()`), and the `import` each
|
|
requires. This is destination groundwork (like a class skeleton, §2.7.4), **not** the
|
|
body: adding it in prep keeps the move a pure cut+paste. Folding it into the move
|
|
instead bundles a non-relocation edit and breaks the byte proof (the move would both
|
|
paste the body **and** author a new `logger`, which the whitelist does not forgive).
|
|
A move into a **new** module is the exception — there the whole header, logger
|
|
included, is authored in the move itself (§2.5).
|
|
|
|
- The decorator and the qualifier are the only artifacts the move will carry — exactly
|
|
what the whitelist (`spec-reproduction-utils.md` §2.1) forgives.
|
|
|
|
**Check:** lint + tests pass; the diff is the body reshape, the call-site qualifier, and
|
|
any destination scaffolding seeded above; nothing moved.
|
|
|
|
#### 2.3.2 Commit 2 — move: relocate to the module
|
|
|
|
- Cut the `@staticmethod` block; paste into the target module.
|
|
- Drop `@staticmethod`, dedent to module level — body **unchanged, line for line**.
|
|
- Source file: import the moved symbol; drop now-unused imports.
|
|
- Call site: `TheClass.foo(args)` → `foo(args)` (args untouched).
|
|
|
|
**Check:** `mechanical_refactor_proof_generator.py <commit>` reports `PASS`. Cross-check:
|
|
`git show <commit> --color-moved=dimmed-zebra --color-moved-ws=allow-indentation-change`
|
|
marks the whole block as moved.
|
|
|
|
### 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.
|
|
|
|
#### 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).
|
|
2. Wire an instance into the call path — composition (`self.component = Target(...)` in
|
|
the source ctor), construction at the call site, or temporarily both.
|
|
3. Retype each moved method as a `@staticmethod` whose parameter is still **named** `self`
|
|
but **typed** as the target class — body unchanged:
|
|
|
|
```python
|
|
class Source:
|
|
component: Target
|
|
|
|
@staticmethod
|
|
def foo(self: Target) -> None:
|
|
... # body still reads self.field_a / self.field_b
|
|
```
|
|
|
|
4. Caller: `self.foo(...)` → `Source.foo(self.component, ...)`.
|
|
|
|
Why keep the name `self`:
|
|
|
|
- it is an ordinary parameter name, so every `self.X` resolves against the target class
|
|
statically and at runtime (the argument *is* a target-class instance);
|
|
- renaming it would rewrite every `self.X` and destroy the "body unchanged across both
|
|
commits" invariant.
|
|
|
|
Boundaries:
|
|
|
|
- **Prep stays minimal.** Signature redesign, helper extraction, parameter objects,
|
|
mutate→return, renames, method splits, dead-branch removal → later non-mechanical
|
|
commits, never prep.
|
|
- **Runtime-mutable state → inject a `Callable` getter (still prep).** State that changes
|
|
every step (counters, the current batch, running stats): inject `Callable[[], T]` into
|
|
the target ctor; rewrite `self.X` → `self.get_X()`. Do **not** thread it per call and do
|
|
**not** reach back into the source object — per-call kwargs make every call site noisy,
|
|
the API non-self-contained, and the threading a caller chore.
|
|
|
|
```python
|
|
class Target:
|
|
def __init__(self, *, static_field, get_running_state: "Callable[[], State]"):
|
|
self.static_field = static_field
|
|
self.get_running_state = get_running_state
|
|
|
|
@staticmethod
|
|
def check(self: "Target") -> None:
|
|
running = self.get_running_state() # was self.running_state
|
|
...
|
|
```
|
|
|
|
```python
|
|
# source ctor
|
|
self.component = Target(
|
|
static_field=...,
|
|
get_running_state=lambda: self.running_state,
|
|
)
|
|
```
|
|
|
|
**Check:** lint + tests pass; body unchanged; types check (`self: Target` matches the
|
|
instance the caller passes).
|
|
|
|
#### 2.4.2 Commit 2 — move: relocate into the class
|
|
|
|
- Cut `foo` into the target class; drop `@staticmethod` — body **unchanged, line for
|
|
line**.
|
|
- Header: `def foo(self: Target)` → `def foo(self)` (type redundant inside the class).
|
|
- Caller: `Source.foo(self.component, ...)` → `self.component.foo(...)` — the receiver
|
|
moves out of the argument list (replayed by `lower_call_sites`).
|
|
|
|
**Check:** `mechanical_refactor_proof_generator.py <commit>` reports `PASS`. The split
|
|
paid off: prep left the body untouched, so the move is a clean cut/paste.
|
|
|
|
### 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`.
|
|
- Each def/class is cut **verbatim** (the byte diff certifies the bodies); the new file's
|
|
small header (imports, a logger, constants, a `TYPE_CHECKING` block) is authored from
|
|
the target and audited (`spec-reproduction-utils.md` §2.1).
|
|
- A module-level constant that moved into the header (e.g. `_is_hip = is_hip()`) is
|
|
dropped from the source too.
|
|
- 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 (§2.3); the proof reports `UNSUPPORTED` until then.
|
|
|
|
### 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
|
|
interface (signature, optional `return`, the replacing `call`).
|
|
- Faithful **only when the body moves unchanged.** De-self, control-flow restructure, or a
|
|
bookkeeping change folded in → do that as a separate semantic commit (reviewed for
|
|
equivalence) **first**, then move the now-unchanged body.
|
|
- An extraction that rewrites the body *as* it extracts is a semantic commit, not a
|
|
certifiable move — do not dress it up as one.
|
|
|
|
### 2.7 Remarks
|
|
|
|
#### 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
|
|
*before* the move (rename in place, update call sites).
|
|
- A move that also renames cannot be machine-certified: split it — rename first, then
|
|
move.
|
|
|
|
#### 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.
|
|
- Correct order: prep leaves the body in the source (target skeleton, header retype,
|
|
caller qualification only); the move does the 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.
|
|
|
|
#### 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.
|
|
|
|
#### 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.
|
|
|
|
| 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) |
|
|
| platform conditionals carried along with the body | mechanical (prep / move) |
|
|
| cross-file import path rewrites | mechanical (move) |
|
|
| field-ownership migration into the component ctor | mechanical (a single pre-step) |
|
|
| inlining an `init_*` method body into a ctor | mechanical (a single pre-step) |
|
|
| privacy flip (`_x` ↔ `x`) | mechanical (a single rename) |
|
|
| signature redesign (new kwargs, changed defaults, positional → kw-only) | **not** mechanical |
|
|
| body simplification / dead-branch removal / logic rewrite | **not** mechanical |
|
|
| semantic method rename | **not** mechanical |
|
|
|
|
- The smaller the prep, the easier "behavior unchanged" is to confirm.
|
|
- Many small, independently reviewable commits beat one big prep mixing ten flavors of
|
|
change.
|
|
- Review order = commit order: prep → move → non-mechanical follow-ups.
|
|
|
|
#### 2.7.6 Anti-pattern: the non-mechanical label as an escape hatch
|
|
|
|
- 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.
|