diff --git a/docs/MATCHING_CONVENTIONS.md b/docs/MATCHING_CONVENTIONS.md
index 0d900fa..ec6c5dd 100644
--- a/docs/MATCHING_CONVENTIONS.md
+++ b/docs/MATCHING_CONVENTIONS.md
@@ -105,6 +105,18 @@ emulates ASPSX 2.56 (the version on the PsyQ 4.0 SDK banner): it emits `.set nor
 `nop`s so delay-slot scheduling matches the original. `--no-maspsx` disables it for comparison;
 `--aspsx-version` overrides the pinned version.
 
+## Drafting a function
+
+For anything larger than a few instructions, draft from Ghidra rather than raw disassembly:
+
+1. `ghidra_get_code --format decompiler` for the function → first-draft C.
+2. Write `src/func_XXXXXXXX.c`; mark every name, type, struct offset and signedness as a hypothesis.
+3. `sf3_match range` until `differing_bytes=0`.
+4. `make gate` before registering.
+
+Ghidra supplies the shape; the byte gate supplies correctness. Decompiler output is never committed
+and never treated as evidence. See [PHASE6_GHIDRA_WORKFLOW.md](PHASE6_GHIDRA_WORKFLOW.md).
+
 ## Verification procedure
 
 ```bash
diff --git a/docs/MATCHING_COOKBOOK.md b/docs/MATCHING_COOKBOOK.md
index 4c8c8cc..40643d0 100644
--- a/docs/MATCHING_COOKBOOK.md
+++ b/docs/MATCHING_COOKBOOK.md
@@ -151,8 +151,23 @@ are now registered and byte-identical.
 *Limit:* one bounded anomaly remains — `0x800F3160`, a 12-byte symbol store whose store-in-delay-slot
 scheduling no tested assembler reproduces. See [PHASE6_FRAMED_BLOCKER.md](PHASE6_FRAMED_BLOCKER.md).
 
+### 12. A real `mult`/`div` for a constant means the operand was not a literal
+
+GCC strength-reduces a constant multiply to shifts/adds (`*68` becomes `sll`/`addu`/`sll`). The
+original sometimes emits a **real `mult`** for the same constant (e.g. `0x8005DEF8`: `li v0,68` /
+`mult v1,v0`). That only happens when the multiply operand was a **variable at RTL expansion** — so
+the constant reached the multiply through a non-const object. A non-const local (`short k = 68;`)
+reproduces it; a literal `68` never does, under any of the ten compilers or any `-O` level tested.
+
+*Basis:* `0x8005DEF8` — literal form gives 73 differing bytes; `short k = 68;` gives 5.
+*Limit:* the remaining 5 bytes of that function are a register-allocation tie-break, not a
+semantics difference; it is not registered. See
+[PHASE6_GHIDRA_WORKFLOW.md](PHASE6_GHIDRA_WORKFLOW.md).
+
 ## Open questions
 
+- `0x8005DEF8` (124 bytes) is a **near-match**: instruction count, order and semantics match, but 5
+  bytes differ in a v0/v1 register-allocation tie-break. Not registered; no tested flag closed it.
 - One bounded scheduling anomaly: `0x800F3160` (`lui at` / `jr ra` / `sw a0,off(at)`) is 12 bytes,
   but PsyQ 4.0 `CC1PSX` + ASPSX 2.56 gives 16 (`sw` before the jump). It is not registered.
 - The exact `-G` small-data threshold is not recoverable from the code; the per-symbol `gp` form is
diff --git a/docs/PHASE6_GHIDRA_WORKFLOW.md b/docs/PHASE6_GHIDRA_WORKFLOW.md
new file mode 100644
index 0000000..3d828de
--- /dev/null
+++ b/docs/PHASE6_GHIDRA_WORKFLOW.md
@@ -0,0 +1,69 @@
+# Phase 6 — Ghidra-Draft Workflow for Hard Functions
+
+**Scope:** P6-T6 follow-up. **Status: adopted.** The Ghidra decompiler is used to draft a function's
+shape; the byte gate remains the only authority on correctness.
+
+## The workflow
+
+```
+1. ghidra_get_code --format decompiler   -> first-draft C skeleton
+2. write src/func_XXXXXXXX.c             -> every name/type/offset marked a hypothesis
+3. sf3_match range                        -> 0 differing bytes required
+4. massage the C against the disassembly  -> iterate
+5. make gate                              -> register only when the whole binary matches
+```
+
+Ghidra contributes the **structure** (argument order, arithmetic, call sites, control flow). The
+project supplies the **toolchain truth** and the byte-exactness. Neither is sufficient alone: the
+compiler identification that unblocked framed functions came from the byte gate, not the decompiler;
+conversely, a decompiler skeleton reaches a plausible first draft far faster than reading raw
+disassembly.
+
+## Worked example: `0x8005DEF8` (bounded near-match)
+
+Ghidra's decompilation:
+
+```c
+void FUN_8005def8(int param_1,int param_2)
+{
+  FUN_800a9fd4(*(undefined4 *)(param_2 + 0xc0),
+               (*(uint *)(param_1 + 0x2e8) & 0xffff) + *(int *)(param_1 + 4),
+               ((int)*(uint *)(param_1 + 0x2e8) >> 0x10) +
+               ((0xc - *(int *)(param_1 + 0x28)) * 0x44) / 0xc + -0x1e + *(int *)(param_1 + 8));
+  return;
+}
+```
+
+That mapped to a 124-byte function (`0x8005DEF8..0x8005DF74`) and gave the correct argument order and
+arithmetic on the first try.
+
+| Step | Result |
+|---|---|
+| Literal reconstruction (`* 0x44`) | 124 bytes, **73 differing** — the compiler strength-reduced `*68` to shifts |
+| Non-const local `short k = 68;` | 124 bytes, **5 differing** |
+| ~40 structural variants, type/order/flag sweeps | no improvement below 5 |
+
+The decisive insight: the original emits a real `mult` by 68 (`li v0,68` / `mult v1,v0`). GCC only
+does that when the multiply operand was a **variable at RTL expansion**, not a compile-time literal —
+so the constant must have reached the multiply through a non-const object. `short k = 68;` reproduces
+it; a literal `68` never does, under any of the ten compilers or any `-O` level tested.
+
+The remaining 5 bytes are a **v0/v1 register-allocation tie-break** in the `12 - f_28` subtract and
+the `- 30`; instruction count, order and semantics all match. It is **not registered** (a match is
+byte-for-byte), and no tested flag closed it.
+
+## Reusable rules
+
+- Use Ghidra for shape, not bytes. Decompiler output is a hypothesis.
+- Treat every decompiler name, type, struct offset and signedness as unproven.
+- A real `mult` (or `div`) for a constant is a signal: the operand was not a literal at expansion
+  time. Try a non-const local, a parameter, or an inlined constant argument.
+- When the instruction count and order match and only register numbers differ, the reconstruction is
+  semantically right; the residual is a register-allocation tie-break, which may not be reachable
+  from C. Record it and move on.
+
+## Limits
+
+- Ghidra recovered only ~1,721 functions / 675 KB of the 1.88 MB payload, so many candidates have no
+  decompilation.
+- Decompiler output is not committed; only hand-written `src/` C and the docs are tracked.
diff --git a/docs/PHASE6_VERIFICATION.md b/docs/PHASE6_VERIFICATION.md
new file mode 100644
index 0000000..ca2131e
--- /dev/null
+++ b/docs/PHASE6_VERIFICATION.md
@@ -0,0 +1,80 @@
+# Phase 6 — Verification Record
+
+**Scope:** P6-T7. **Status:** all gates green; milestone confirmation requested.
+**Date:** 2026-09-23.
+
+## Milestone
+
+At least ten instruction-identical C functions, spanning the three required shapes, with duplicate
+sharing demonstrated, the toolchain gaps closed, a defensible boundary inventory, and the clean
+full-binary gate green.
+
+**12 registered regions / 11 distinct functions**, `c_regions=12`, 0 differing bytes,
+SHA-1 `e173426c157384ebf1b6caf8c6fea18a85a14af9`.
+
+| Shape | Functions |
+|---|---|
+| leaf getter/setter | `func_80012780`, `func_80017AD4`, `func_80017AE8`, `func_80026264`, `func_800262E0` |
+| `la` / `gp`-relative | `func_8002D2A0`, `func_8002D2BC`, `func_80012780` |
+| call with a frame | `func_80017DD0`, `func_80024C14`, `func_80036308`, `func_800697A4` |
+| duplicate body | `func_800262E0` / `func_800262EC` (one source, body occurs exactly twice) |
+
+## Gates
+
+| Check | Command | Result |
+|---|---|---|
+| Synthetic suite | `python3 -m unittest discover -s tools/tests` | exit 0; **86 tests pass** |
+| Clean baseline | `make clean` then `make all` | exit 0 |
+| Full-binary comparison | `cmp build/scus_946_40.rebuilt 'extracted/SCUS_946.40;1'` | exit 0 |
+| Baseline SHA-1 | `sha1sum` on both | `e173426c157384ebf1b6caf8c6fea18a85a14af9` |
+| Ordered C gate | `make gate` | `c_regions=12`, 0 differing, `result=MATCH`, exit 0 |
+| Firewall | `git ls-files` under prohibited roots | 0 tracked |
+| Git hygiene | `git status --short`, `git diff --check` | clean, exit 0 |
+
+## Toolchain (corrected this phase)
+
+| Role | Identity | Basis |
+|---|---|---|
+| Compiler | PsyQ 4.0 `CC1PSX`, banner `GNU C 2.7.2.SN32.3.7.0002` | the real binary executed and compared |
+| Open substitute | `gcc-2.7.2-psx` | instruction-identical to real `CC1PSX` 4.0 on 21/21 probe files |
+| Assembler | ASPSX 2.56 (SDK 4.0) | `Psy-Q ASPSX version 2.56` |
+| Flags | `-quiet -O2 -G0` | macro address form is the default |
+
+This supersedes Phase 5's `egcs-2.91.66` (PsyQ 4.5) identification. Full evidence in
+[PHASE6_TOOLCHAIN_CORRECTION.md](PHASE6_TOOLCHAIN_CORRECTION.md).
+
+## Toolchain gaps closed
+
+| Gap | Closure |
+|---|---|
+| registry symbols | `config/symbols.tsv`, link-time `--defsym` (P6-T2) |
+| per-region flags | optional 4th registry field (P6-T2) |
+| maspsx / ASPSX `la` | maspsx stage + link-time HI16 adjustment (P6-T3) |
+| `-G` small data | per-symbol `gp` marker + `%gp_rel` rewrite (P6-T4) |
+
+## Inventory
+
+`config/function_inventory.tsv` — 2,875 candidates graded `entry` / `jal` / `prologue` / `ghidra`
+(addresses only). 575 `jal` targets are absent from Ghidra's function set. Library-versus-game-code is
+recorded as **unresolved**.
+
+## Open items (recorded, not matched)
+
+| Item | Status |
+|---|---|
+| `0x8005DEF8` (124 bytes) | near-match: 5 bytes differ in a v0/v1 register tie-break; not registered |
+| `0x800F3160` (12 bytes) | no tested compiler+assembler pair reproduces its store-in-delay-slot scheduling; not registered |
+| `-G` numeric threshold | not recoverable from the code; per-symbol `gp` form used instead |
+| entry `[0x800FB368,0x800FB410)` | CRT startup, not C; stays fallback |
+| library vs game code | unresolved |
+
+## Firewall
+
+No game bytes, disassembly, generated assembly, build outputs, expected binaries, Ghidra database,
+RAM dumps, or proprietary SDK material are tracked. The PsyQ 4.0/4.1/4.4/4.5/4.6 SDKs and `wibo` stay
+in ignored `tools/psyq/` and `tools/wibo/`; only checksums and provenance are recorded in
+`docs/SETUP.md`.
+
+## Rules added this phase
+
+None.
diff --git a/phase-ends/CURRENT_PHASE.md b/phase-ends/CURRENT_PHASE.md
index fae139c..b32ec0d 100644
--- a/phase-ends/CURRENT_PHASE.md
+++ b/phase-ends/CURRENT_PHASE.md
@@ -13,7 +13,7 @@
 - [x] **Rules check** — re-read `AGENTS.md` mandatory behavior after P6-T4 and stated the required continuation notice.
 - [x] **P6-T5 — Evidence-graded function-boundary inventory** (complete)
 - [x] **P6-T6 — First matching batch, with duplicate sharing** (complete; the framed shape was unblocked by correcting the compiler identification)
-- [ ] P6-T7 — Cookbook, conventions, verification record, and phase gate
+- [x] **P6-T7 — Cookbook, conventions, verification record, and phase gate** (verification record written, all gates green; **milestone confirmation requested** — awaiting developer)
 
 ## P6-T1 — Baseline revalidation (2026-09-23)
 
@@ -251,3 +251,19 @@ reproduced by any tested (compiler, assembler) pair; it is not registered and is
 cookbook.
 
 **Rules check — re-read complete. Continuing with P6-T7.**
+
+## P6-T6 (continued) — Ghidra-draft workflow adopted (2026-09-23)
+
+On developer direction, the Ghidra decompiler was trialled as the drafting step for hard functions and
+adopted. Recorded in `docs/PHASE6_GHIDRA_WORKFLOW.md` and `docs/MATCHING_CONVENTIONS.md`
+(§Drafting a function).
+
+- Workflow: `ghidra_get_code` decompiler → first-draft `src/func_XXXXXXXX.c` (all names/types/offsets
+  hypotheses) → `sf3_match range` → massage → `make gate`.
+- Worked example `0x8005DEF8` (124 bytes): the Ghidra skeleton gave the correct argument order and
+  arithmetic immediately. The previously unexplained real `mult` by 68 was reproduced by making the
+  constant a non-const local (`short k = 68;`), taking it from 73 differing bytes to **5**.
+- The residual 5 bytes are a v0/v1 register-allocation tie-break; the function is a **near-match and
+  is not registered**. ~40 variants and flag sweeps did not close it.
+- New cookbook finding 12: a real `mult`/`div` for a constant means the operand was not a literal at
+  RTL expansion.