roadmap: close Embedding ABI — M3 ([~]->[x]) — milestone substantively closed + sound (record crosses C ABI in/out, ownership follows declared mode, value layout frozen+byte-pin-enforced, all invariants held, Invariant 1 clean, bench causally exonerated NO-ratify); no WhatsNew (next item M4 is a new milestone — a /boss bounce-back, not done-state)

docs/roadmap.md

@@ -263,22 +263,46 @@ work progresses.
     `docs/journals/2026-05-18-audit-embedding-abi-m2.md`;
     `docs/journals/2026-05-18-iter-embedding-abi-m2.tidy.md`.
 
-- [~] **\[milestone\]** Embedding ABI — M3: frozen value layout +
-  single ADT/record crossing + RC ownership contract. Host
-  constructs a single-ctor record (Int/Float fields), passes it,
-  the kernel returns a record the host reads and frees; the RC
-  ownership-transfer contract at the call boundary is specified
-  and the `rc_header`/ADT-box layout documented as a *frozen*
-  ABI. Sequenced after M2 — a one-way stability commitment, so
-  the frozen ABI must already include the ctx parameter shape
-  (substantive ordering reason, not effort). Covers the `State`
-  value crossing in/out. Coherent stop: a record in/out with
-  alloc==free across many calls.
+- [x] **\[milestone\]** Embedding ABI — M3: frozen value layout +
+  single ADT/record crossing + RC ownership contract — CLOSED
+  2026-05-18. A single-constructor record of `Int`/`Float` fields
+  now crosses the embedding C ABI in **and** out; ownership follows
+  the declared `own`/`borrow` mode (mechanically inherited — the M2
+  forwarder body is byte-unchanged, all mode-driven RC stays in the
+  byte-unchanged internal `@ail_<mod>_<fn>`); the record memory
+  layout (header@p-8 / i64 tag@0 / fields i64-strided@8+i·8 /
+  size=8+n·8) is **frozen** as a one-way commitment — a new
+  DESIGN.md §"Embedding ABI" `### Frozen value layout` SSOT +
+  `// FROZEN ABI` lockstep pointers at the three encoders + an
+  enforceable `@ailang_rc_alloc` heap-box byte-pin (RED-on-offset-
+  perturbation proven); host construction via `ailang_rc_alloc`,
+  host-free via `ailang_rc_dec` (leak-free *because* M3 fields are
+  scalar — no boxed children; non-scalar recursive-free named M4-
+  additive). No authoring-surface / schema / Form-A / `CheckError`
+  change (M2-style — the `.ail` is the minimal evolution of the
+  M1/M2 scalar kernel into a record `State`). The `(State,Float)->
+  State` fold round-trip is proven **globally leak-free** for both
+  `own` and `borrow`. Process: spec `1fbb9c4` (grounding-check PASS
+  8/8) → plan `15ee3c5` → iter `d5c565d` (PARTIAL 5/7 + a Boss
+  spec-consistency repair: the orchestrator correctly BLOCKED on a
+  genuine spec defect — the single-ctx-readback proof model is
+  unsatisfiable for `borrow` by M2's TLS-ctx design; Boss
+  M2.1-precedent adjudication → a stronger global-leak-freedom proof
+  model) + `4ea8bc5` (DONE 6-7: the freeze). Milestone-close `audit`
+  `b8a60b1` (architect: Invariant 1 clean, M1/M2 byte-invariant
+  held, frozen-SSOT consistent — DRIFT only `[medium]`+`[low]`
+  doc-honesty → tidy; bench `check.py` exit 1 **decisively causally
+  exonerated** — byte-identical generated IR HEAD vs pre-M3
+  `9a609ae` for every firing bench, the two tracked-P2 noise
+  families, NO ratify) → tidy `63d7d60` (pin-safe; drift resolved).
+  No fieldtest (zero authoring-surface change). Stays here briefly
+  for context; remove once stale (full record in
+  `docs/journals/INDEX.md`).
   - depends on: Embedding ABI — M2.
-  - context: `docs/specs/2026-05-18-embedding-abi-m3.md`
-    (user-approved, grounding-check PASS 8/8); 2026-05-18 chat.
-    `runtime/rc.c`'s header already anticipates this ("The ABI
-    defined here is stable … unless the layout itself shifts").
+  - context: `docs/specs/2026-05-18-embedding-abi-m3.md`;
+    `docs/journals/2026-05-18-iter-embedding-abi-m3.1.md`;
+    `docs/journals/2026-05-18-audit-embedding-abi-m3.md`;
+    `docs/journals/2026-05-18-iter-embedding-abi-m3.tidy.md`.
 
 - [ ] **\[milestone\]** Embedding ABI — M4: sequence crossing via
   the existing `List` ADT. Host builds a `List Record` per chunk;