# 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.