diff --git a/docs/roadmap.md b/docs/roadmap.md index 1d6bd66..5544ccf 100644 --- a/docs/roadmap.md +++ b/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__`); 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;