spec: embedding-abi-m3 — frozen value layout + single ADT/record crossing + RC ownership contract (user-approved, grounding-check PASS 8/8); open in-flight [~]

2026-05-18 20:35:05 +02:00
parent 9a609aecc7
commit 1fbb9c433b
2 changed files with 678 additions and 4 deletions
@@ -263,7 +263,7 @@ 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 +
+- [~] **\[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
@@ -275,9 +275,10 @@ work progresses.
  value crossing in/out. Coherent stop: a record in/out with
  alloc==free across many calls.
  - depends on: Embedding ABI — M2.
-  - context: 2026-05-18 chat. `runtime/rc.c`'s header already
+  - context: `docs/specs/2026-05-18-embedding-abi-m3.md`
-    anticipates this ("The ABI defined here is stable … unless
+    (user-approved, grounding-check PASS 8/8); 2026-05-18 chat.
-    the layout itself shifts").
+    `runtime/rc.c`'s header already anticipates this ("The ABI
    defined here is stable … unless the layout itself shifts").
 - [ ] **\[milestone\]** Embedding ABI — M4: sequence crossing via
  the existing `List` ADT. Host builds a `List Record` per chunk;
@@ -0,0 +1,673 @@
 # Embedding ABI — M3: frozen value layout + single ADT/record crossing + RC ownership contract — Design Spec
 **Date:** 2026-05-18
 **Status:** Draft — awaiting user spec review
 **Authors:** Brummel (orchestrator) + Claude
 ## Goal
 Let a single-constructor record of `Int`/`Float` fields cross the
 embedding C boundary in **and** out, with the RC ownership-transfer
 contract at the call boundary *specified, tested, and frozen*. M1 made
 one scalar `fn` callable (`@<sym>(scalars…)`); M2 threaded a
 per-thread `ailang_ctx_t*` through it (`@<sym>(ctx, scalars…)`) and
 de-globalised RC accounting. Both M1 and M2 explicitly label that C
 signature **scalar-only and provisional until M3** (DESIGN.md
 §"Embedding ABI", `:2280`, `:2293–2295`). M3 delivers the value
 crossing the arc exists for — the `State` of a `(State, Sample) ->
 State` streaming fold — and converts "provisional until M3" into a
 **one-way freeze**: from M3 on, the value/memory layout and the
 ownership rule are a stability promise an external host
 (M5's `ail-embed` adapter, `data-server`) compiles against and the
 compiler must not silently break.
 M3 has **no new authoring surface**: no new Form-A modifier, no new
 schema field, no new `CheckError` variant. The `.ail` an LLM author
 writes is the direct, minimal evolution of the M1/M2 scalar kernel
 into a record `State` (existing `data` + existing `(own (con T))` mode
 + existing `(export "…")`). The deliverable is a *widened export gate*,
 a *transparent record-as-`ptr` forwarder*, a *frozen layout
 documented as the single source of truth and pinned by a byte test*,
 and an *alloc==free proof harness*. This is the M1/M2-style honest
 framing: a strategic capability/safety gate per the user-made
 direction call in the roadmap, **not** the standard authoring-utility
 metric. No pretence otherwise.
 **Coherent stop:** the `(State, Sample) -> State` record fold is
 callable from a C host that constructs the input `State` via the
 runtime allocator, calls the kernel N times, reads and frees each
 returned `State`, and `ailang_ctx_free` reports `allocs == frees` —
 for **both** the `(own (con State))` and the `(borrow (con State))`
 declared modes, each behaving exactly as the declared mode promises;
 with the frozen layout pinned by a byte test that goes RED if codegen
 moves an offset, and every M1/M2-arc invariant audited.
 ### Position in the M1–M5 arc (load-bearing — the freeze is here)
 The arc is a one-way stability progression. M1 and M2 deliberately
 kept the value/ABI layout *provisional* and decoupled the
 author-chosen C symbol from the internal `ail_<module>_<def>`
 mangling, precisely so the internal calling convention could keep
 changing while the external symbol stayed stable. M3 is where the
 *value layout itself* stops moving:
 - **M3 freezes** the record memory layout (8-byte refcount header at
  `payload-8`, an `i64` constructor tag at offset 0, scalar fields
  `i64`-strided from offset 8) and the ownership rule (follows the
  declared `own`/`borrow` mode). After M3, an already-compiled host
  that hand-builds and reads a `State` per this layout must keep
  working across compiler changes — a recompiled AILang must not
  move those bytes or invert the free rule. `runtime/rc.c:25–26`
  already anticipates exactly this: *"The ABI defined here is
  stable … will not require runtime changes unless the layout itself
  shifts."* M3 makes "unless the layout itself shifts" a closed
  door for the embedding-ABI record shape.
 - **M4** (sequence crossing via `List`) and **M5** (`ail-embed`
  adapter + `data-server` wiring) bind against the M3-frozen layout.
  The freeze must therefore already carry the M2 `ctx` parameter
  shape — it does (M2 shipped it); M3 adds only the record value to
  the already-`ctx`-shaped, now-frozen ABI.
 - The internal `@ail_<module>_<fn>` calling convention and the
  `_adapter`/`_clos` closure pair remain **byte-unchanged** (the M1
  decision M2 preserved, preserved again): the forwarder is a
  transparent `ptr` pass-through; all mode-driven RC stays inside the
  internal fn. M3 freezes the *external* shape without touching the
  *internal* convention — exactly the decoupling M1 built for.
 ## Architecture
 Three layers change, in pipeline order. None of `ailang-core`,
 `ailang-codegen`, or `runtime/` gains any `data-server`/finance
 knowledge or dependency (Invariant 1; audited at close). **No
 `ailang-core` schema change, no Form-A surface change, no new
 `CheckError` variant** (explicit contrast with M1; same as M2).
 1. **Check (`ailang-check`).** The export-gate scalar predicate
   `is_c_scalar` (`crates/ailang-check/src/lib.rs:1921–1924`) widens
   to `is_c_abi_type`: a type is permitted at the embedding boundary
   iff it is a C scalar (`Int`/`Float`, bare `Type::Con`, the M1
   rule) **or** a `Type::Con` resolving to a `data` definition with
   **exactly one constructor** whose every field type is itself a
   permitted C-ABI type (recursive, but M3 scope bottoms out at
   scalar fields — a record field that is itself a record is *out
   of scope* and rejected; that is M4's recursion to open). Multi-
   constructor sums, `Str` fields, `List` fields, and effectful
   exports stay RED. The two existing diagnostics
   (`CheckError::ExportNonScalarSignature` `:453`,
   `ExportHasEffects` `:459`) are **reused**; only their message
   text widens to name "a single-constructor record of `Int`/`Float`"
   as permitted and, for a rejected single-ctor record, to name the
   offending field and that nested/`Str`/`List` fields are a future
   (M4) layer rather than "unsupported". No new variant, no
   `code()`-registry (`:712–713`) change.
 2. **Codegen (`ailang-codegen`).** The forwarder signature
   extraction `fn_scalar_sig` (`crates/ailang-codegen/src/lib.rs:659–669`)
   and the LLVM scalar mapper `llvm_scalar` (`:673–678`) widen so an
   M3 record type maps to `ptr`. The M2 forwarder body
   (`:604–651` — leading `ptr %ctx`, `__ail_tls_ctx` save/store/
   restore around the internal call) is **byte-unchanged**: a record
   parameter and a record return are each a single `ptr` (recon
   confirmed ADTs already cross as a bare `ptr`; there is **no**
   `sret`/`byval`/aggregate convention anywhere in codegen or
   runtime, and none is introduced). All RC behaviour stays inside
   the internal `@ail_<module>_<fn>`: the existing mode-driven
   machinery — Iter-B own-param drop-at-return
   (`lib.rs:1287–1335`), the `match_lower.rs:651–657` scrutinee-Own
   arm-close dec, the `drop.rs:445–490` `synth_callee_ret_mode`
   ret-mode trackability — already realises `own` (kernel consumes)
   vs `borrow` (kernel does not) for the internal fn. The forwarder
   inherits that transparently; it performs **no** RC op itself.
 3. **Docs + pins.** DESIGN.md §"Embedding ABI" (`:2266–2317`) gains a
   **frozen value-layout subsection** that becomes the single source
   of truth for: the record memory layout (header/tag/fields,
   offsets and sizes), the host-construction contract (input records
   are allocated via `ailang_rc_alloc`, normative MUST), the
   host-free contract (`ailang_rc_dec`, leak-free *because* M3
   fields are scalar — no child boxes — with the non-scalar case
   explicitly flagged as M4-additive), and the ownership rule
   (follows the declared `own`/`borrow` mode). The "scalar-only and
   provisional until M3" / "provisional until M3" wording
   (`:2280`, `:2293–2295`) becomes one-way-freeze language. A new
   layout **byte-pin test** asserts the offsets/sizes/tag-word as
   codegen emits them today; the three sites that currently encode
   the layout independently (`runtime/rc.c:28–44` comment,
   `match_lower.rs` `lower_ctor`, `drop.rs`) gain a lockstep
   comment pointing at the DESIGN.md SSOT.
 ### What is frozen (the permanent commitment, stated exactly)
 For a single-constructor `data T` whose `n` fields are each `Int` or
 `Float`, a value of type `T` crossing the embedding C boundary is:
 ```
  payload pointer  p   (this is what the C ABI passes/returns — a bare `ptr`)
  p - 8 .. p        :  uint64_t  refcount header   (HEADER_SIZE = 8; rc.c:54-56)
  p + 0  .. p + 8   :  int64_t   constructor tag   (always written; 0 for the
                                                    single ctor — no elision)
  p + 8  .. p + 16  :  field 0   (int64_t for Int; IEEE-754 double bit-pattern
                                  in 8 bytes for Float, declaration order)
  p + 16 .. p + 24  :  field 1
  …                     (field i at p + 8 + i*8;  total box size = 8 + n*8)
 ```
 Frozen rules, permanent from M3:
 - **Layout** as above — the *actual* layout codegen emits today
  (`match_lower.rs` `lower_ctor`: `size_bytes = 8 + n*8`, tag at
  offset 0 written unconditionally, fields `i64`-strided from offset
  8). Frozen *as-is, tag word included* — M3 does **not** elide the
  single-ctor tag (a hot-path codegen change touching every
  single-ctor ADT tree-wide for ABI cosmetics; rejected — see Out
  of scope).
 - **Construction (host → kernel input).** The host MUST obtain an
  input record's storage from `ailang_rc_alloc(8 + n*8)` (an
  already-public runtime symbol; it returns the payload pointer with
  the refcount header pre-set to `1` and the payload zeroed —
  `rc.c:144–159`), then write the tag word (`0`) and the scalar
  fields at the frozen offsets. A raw host `malloc` is a host-side
  contract violation: `own`-consume and `ailang_rc_dec` both require
  the runtime's 8-byte refcount header at `p-8` initialised to `1`.
 - **Ownership follows the declared mode** (no new rule — the
  existing DESIGN.md §"Mode metadata is load-bearing for codegen"
  contract, `:1413–1508`, *as the C ABI*): a `(own (con T))`
  parameter transfers ownership into the kernel — the kernel/RC
  consumes it (the existing Iter-B drop-at-return path), the host
  must **not** touch or `dec` that pointer after the call. A
  `(borrow (con T))` parameter is retained by the host — the kernel
  does not consume it, the host frees it with `ailang_rc_dec` after
  the call. The **return** value is always owned by the host: the
  host reads it and frees it with `ailang_rc_dec`.
 - **Free (host side).** `ailang_rc_dec(payload)` — an already-public
  runtime symbol. Leak-free for an M3 record **because** every field
  is a scalar: `ailang_rc_dec` is header-only (it does not recurse
  into fields — `rc.c:193–210`), and an M3 record has no child boxes
  to recurse into. The frozen subsection states this scoping
  honestly and names the non-scalar case (records with boxed fields,
  M4) as requiring an *additive* mechanism then — not a contradiction
  of the freeze, an extension at a layer M3 does not cover.
 ### Why the ownership contract is mechanically almost free
 The roadmap's "RC ownership-transfer contract" is **not** new RC
 code. AILang already compiles `own` vs `borrow` into the internal
 `@ail_<module>_<fn>`: an `own` parameter that the body consumes is
 dropped before return by Iter-B (`lib.rs:1287–1335`); a `borrow`
 parameter is not. The forwarder calls that internal fn and passes the
 record `ptr` straight through. So "the C ABI ownership follows the
 declared mode" is true *by construction* the moment the forwarder is
 allowed to pass a record `ptr` — there is nothing to implement at the
 boundary beyond widening the type predicate. M3's real work is to
 **specify, prove, and freeze** that already-true behaviour, not to
 build it. (Recon's open question — `fn_scalar_sig` strips
 `param_modes`/`ret_mode` — is a non-issue *for the forwarder*: the
 forwarder needs no mode info because it does no RC; the modes are
 already baked into the internal fn it calls. The forwarder only needs
 to know a record maps to `ptr`.)
 ## Concrete code shapes
 ### The AILang program M3 delivers (headline — clause-1 evidence)
 `examples/embed_backtest_step_record.ail` — the `(State, Sample) ->
 State` streaming fold the embedding boundary exists for, the direct
 minimal evolution of the M1/M2 scalar kernel into a record `State`
 (running accumulator + count — the natural shape of a streaming fold's
 state, the SMA-shaped kernel from the Stateful-islands motivation, now
 expressible *because* M3 lets `State` cross the boundary):
 ```
 (module backtest
  (data State
    (ctor State (con Float) (con Int)))
  (fn step
    (export "backtest_step")
    (type
      (fn-type
        (params (own (con State)) (con Float))
        (ret (con State))))
    (params st sample)
    (body
      (match st
        (case (pat-ctor State acc n)
          (app State (app + acc sample) (app + n 1)))))))
 ```
 No new Form-A modifier, no new schema field — exactly like M2.
 `(data State (ctor State (con Float) (con Int)))`, `(own (con State))`,
 `(con State)`, `(match … (case (pat-ctor State acc n) …))`, and
 `(app State …)` as the constructor application are all **existing**
 surface (grounded against `examples/borrow_own_demo.ail`,
 `examples/box.ail`, `examples/embed_export_adt_ret_rejected.ail`).
 Asked "make this AILang fold with real `State` callable from a Rust
 host", an LLM author writes exactly this — the worked `.ail` *is* the
 clause-1 evidence, not a prose assertion.
 A second delivered fixture pins the `borrow` half of the frozen
 contract — `examples/embed_backtest_step_record_borrow.ail`, identical
 but `(params (borrow (con State)) (con Float))`: the kernel reads `st`
 without consuming it; the host retains and frees the input. This
 fixture exists so the "ownership follows the declared mode" freeze is
 proven in *both* directions, not asserted for one.
 ### The changed C host (the actual M3 deliverable surface)
 ```c
 #include <stdint.h>
 #include <assert.h>
 #include <string.h>
 typedef struct ailang_ctx ailang_ctx_t;
 extern ailang_ctx_t *ailang_ctx_new(void);
 extern void          ailang_ctx_free(ailang_ctx_t *);
 extern void *ailang_rc_alloc(size_t);     /* runtime: header=1, payload zeroed */
 extern void  ailang_rc_dec(void *);       /* runtime: header-only dec + free@0  */
 /* @backtest_step(ailang_ctx_t*, State*, double sample) -> State*  — FROZEN at M3 */
 extern void *backtest_step(ailang_ctx_t *ctx, void *st, double sample);
 /* construct an input State per the frozen layout: {tag@0, Float acc@8, Int n@16} */
 static void *make_state(double acc, int64_t n) {
    void *p = ailang_rc_alloc(8 + 2 * 8);            /* header=1 set by runtime  */
    *(int64_t *)((char *)p + 0)  = 0;                /* single-ctor tag = 0      */
    memcpy((char *)p + 8,  &acc, 8);                 /* Float field, double bits */
    *(int64_t *)((char *)p + 16) = n;                /* Int field                */
    return p;
 }
 int main(void) {
    ailang_ctx_t *ctx = ailang_ctx_new();
    void *st = make_state(0.0, 0);
    for (int i = 0; i < 1000000; i++) {
        void *next = backtest_step(ctx, st, (double)(i & 7));
        /* (own (con State)): the kernel consumed `st`. Do NOT touch/dec st.    */
        st = next;                                   /* return is host-owned    */
    }
    double acc; memcpy(&acc, (char *)st + 8, 8);
    int64_t n = *(int64_t *)((char *)st + 16);
    assert(n == 1000000);
    ailang_rc_dec(st);                               /* host frees the return    */
    ailang_ctx_free(ctx);                            /* AILANG_RC_STATS: allocs==frees */
    return 0;
 }
 /* cc host.c libbacktest.a libailang_rt.a -o t && AILANG_RC_STATS=1 ./t */
 ```
 The `borrow` variant differs only in the loop body: the kernel does
 **not** consume `st`, so the host owns it and must
 `ailang_rc_dec(st)` before overwriting it with `next` (and the input
 of the next iteration is a freshly `make_state`'d record, or the
 returned one threaded as the new input — the fixture uses the
 returned one as the next input, so each iteration frees exactly the
 previous host-owned input). Both variants end at `allocs == frees`.
 ### The must-fail axis (clause-3 discriminator — sharper, not removed)
 `examples/embed_export_adt_ret_rejected.ail` is, *today*, the M1
 must-fail fixture for "an ADT return is rejected" — but its `Pair`
 is single-constructor with two `Int` fields, i.e. **exactly
 M3-shaped**. Under M3 it would no longer be a valid must-fail.
 M3 therefore **re-points** it (and its asserting test) to an ADT that
 is *genuinely still rejected*, so the clause-3 teeth stay
 non-vacuous. The re-pointed fixture rejects on a multi-constructor
 sum **and** a non-scalar field — two independent reasons, the
 sharpened M3 boundary:
 ```
 (module embed_export_adt_ret_rejected
  (data Reading
    (ctor Missing)
    (ctor Sample (con Int) (con Str)))        ; 2 ctors AND a Str field
  (fn f
    (export "f")
    (type
      (fn-type
        (params (con Int))
        (ret (con Reading))))
    (params n)
    (body (app Sample n "tick"))))
 ```
 The body is trivially well-typed (`n : Int`, `"tick" : Str` match
 `Sample`'s `(con Int) (con Str)`), so — exactly as the M1 spec took
 care to ensure — the **only** reason `ail check` fails is the export
 gate: `Reading` has two constructors **and** `Sample` has a `Str`
 field. Both rejection reasons are independent and the M3 boundary
 rejects on either.
 Plus narrower single-reason must-fail fixtures isolating each clause
 (see Testing strategy): a single-ctor record with a `Str` field
 (scalar-field rule), a single-ctor record with a `List` field, a
 multi-ctor sum of all-scalar ctors (single-ctor rule), and the
 unchanged effectful export (`ExportHasEffects`). Each fails
 `ail check` with a precise, self-correcting diagnostic; the positive
 single-ctor Float+Int fixture passes.
 ### Implementation shape (secondary — supporting, not the point)
 Check gate, `crates/ailang-check/src/lib.rs:1921` (schematic — exact
 bytes are the planner's job):
 ```text
 before (M1/M2):
  fn is_c_scalar(t: &Type) -> bool {
      matches!(t, Type::Con { name, args }
          if args.is_empty() && (name == "Int" || name == "Float"))
  }
 after (M3):
  fn is_c_abi_type(t: &Type, /* type-def lookup */ …) -> Result<(), Reason> {
      // C scalar (M1 rule) → ok
      // Type::Con resolving to a data def with exactly 1 ctor
      //   whose every field is_c_abi_type (M3: fields bottom out at
      //   Int/Float — a record-typed field is rejected, that is M4)
      //   → ok
      // else → Err(reason: multi-ctor | non-scalar-field | …)
  }
  // gate (lib.rs:1925-1940): param/ret loop unchanged in shape,
  //   calls is_c_abi_type; on Err emits the *reused*
  //   CheckError::ExportNonScalarSignature with the widened message.
  // effect check (lib.rs:1941-1946): unchanged.
 ```
 Codegen forwarder signature extraction,
 `crates/ailang-codegen/src/lib.rs:659` / `:673`:
 ```text
 before (M1/M2):  llvm_scalar(t): Float -> "double", else -> "i64"
                 fn_scalar_sig matches flat Type::Fn/Forall, scalars only
 after (M3):      a record type (Type::Con → single-ctor data) -> "ptr"
                 scalars unchanged. fn_scalar_sig accepts a record
                 param/ret as "ptr". The forwarder body (lib.rs:604-651)
                 is BYTE-UNCHANGED — it already emits
                   define {ret} @sym(ptr %ctx, {params}) { … }
                 with {ret}/{params} now possibly "ptr"; the internal
                   call ptr @ail_<mod>_<fn>(...) and the TLS
                   save/store/restore are identical to M2.
                 @ail_<mod>_<fn> + _adapter/_clos: byte-unchanged.
 ```
 DESIGN.md §"Embedding ABI" (`docs/DESIGN.md:2266–2317`):
 ```text
 before:  "M1 ABI is scalar-only and provisional until M3"
         "Only the value/record layout remains provisional until M3"
 after :  + a "Frozen value layout (M3 — one-way commitment)" block:
           the layout table above; ailang_rc_alloc construction MUST;
           ailang_rc_dec free (scalar-field leak-free, M4 non-scalar
           flagged); ownership follows declared own/borrow mode.
         "provisional until M3" → "frozen as of M3; a future compiler
           change MUST NOT move these offsets or invert the free rule".
         rc.c:28-44 / lower_ctor / drop.rs each gain:
           // FROZEN ABI — see DESIGN.md §"Embedding ABI" frozen layout
 ```
 ## Components
 | Component | Crate / file | Change |
 |---|---|---|
 | `is_c_scalar` → `is_c_abi_type` | `ailang-check/src/lib.rs:1921` | + single-ctor-all-scalar record (recursive, bottoms out at `Int`/`Float`); returns a reason |
 | `ExportNonScalarSignature` message | `ailang-check/src/lib.rs:452` | widened text: names single-ctor `Int`/`Float` record as permitted; rejected-record reason names the field + M4 |
 | `CheckError` variants / `code()` registry | `ailang-check/src/lib.rs:453,459,712-713` | **unchanged** (no new variant — explicit M2-style contrast) |
 | `fn_scalar_sig` / `llvm_scalar` | `ailang-codegen/src/lib.rs:659/673` | a record type → `ptr`; scalars unchanged |
 | M2 forwarder body | `ailang-codegen/src/lib.rs:604-651` | **byte-unchanged** (regression pin: record crosses as `ptr`, no RC at the forwarder) |
 | internal `@ail_<mod>_<fn>` + `_adapter`/`_clos` | `ailang-codegen` | **byte-unchanged** (M1/M2 decision held) |
 | §"Embedding ABI" frozen-layout SSOT | `docs/DESIGN.md:2266-2317` | new frozen-layout block; "provisional until M3" → one-way freeze |
 | layout-byte pin | `crates/ailang-codegen/tests/` (new) | asserts header/tag/field offsets + sizes + tag-word as emitted today; codegen offset shift → RED |
 | lockstep pointers | `runtime/rc.c:28-44`, `match_lower.rs` `lower_ctor`, `drop.rs` | comment → DESIGN.md frozen SSOT |
 | North-star fixture | `examples/embed_backtest_step_record.ail` (new) | the shown `(own (con State))` `(State,Float)->State` |
 | `borrow` fixture | `examples/embed_backtest_step_record_borrow.ail` (new) | `(borrow (con State))` variant — proves "follows mode" both ways |
 | M1 must-fail re-pointed | `examples/embed_export_adt_ret_rejected.ail` + asserting test | from single-ctor `Pair` (now M3-valid) → multi-ctor + `Str`-field ADT (genuinely still rejected) |
 | narrower must-fail fixtures | `examples/` (new) | single-ctor `Str`-field, single-ctor `List`-field, multi-ctor all-scalar — one rejection reason each |
 | E2E record round-trip harness | `crates/ail/tests/` (M1/M2 style) | host builds State via `ailang_rc_alloc`, N-loop, reads + `ailang_rc_dec`, `ctx_free` asserts `allocs==frees`; `own` and `borrow` variants |
 No `design_schema_drift.rs` movement (no schema field — explicit
 M2-style contrast). No `ailang-core` change, no Form-A change, no
 round-trip-invariant movement (no surface addition). Only the tests
 whose *observed behaviour* M3 changes are touched: the export-gate
 test (a single-ctor scalar record now passes; the re-pointed fixture
 still fails) and the forwarder-IR test (a record param/ret now lowers
 to `ptr` through the unchanged forwarder body). `embed_e2e.rs` (M1
 scalar), the M2 swarm/rc-accounting harness, `embed_export_hash_stable.rs`,
 `print_no_leak_pin.rs`, and the `e2e.rs` leak-stat helper stay green
 **unmodified**.
 ## Data flow
 ```
 embed_backtest_step_record.ail   (no schema/surface change)
  → ail check        is_c_abi_type: (con State) ok [single-ctor, fields Float+Int];
                     (own (con State)) ok; effect set empty
  → desugar / lift / monomorphise        (unchanged)
  → lower_workspace_staticlib [--alloc=rc enforced, M2 guard]
        @backtest_step(ptr %ctx, ptr %st, double %sample) -> ptr
          %saved = load @__ail_tls_ctx ; store %ctx           (M2, byte-identical)
          %r = call ptr @ail_backtest_step(ptr %st, double %sample)
                 ; internal fn: Iter-B drops the `own` %st before ret
          store %saved @__ail_tls_ctx ; ret ptr %r            (M2, byte-identical)
  → backtest.ll → clang -c → backtest.o → ar → libbacktest.a
  ( rc.c / str.c → libailang_rt.a )                           (M2-unchanged)
 host (1 thread, 1 ctx — M3 is single-record; concurrency is M2's, unchanged):
  ctx = ailang_ctx_new()
  st  = ailang_rc_alloc(8+2*8); write tag@0, acc@8, n@16        (alloc #1..)
  loop N×:  next = backtest_step(ctx, st, sample)
            ; (own): kernel consumed st (Iter-B drop = free #k); st = next
            ; (borrow): kernel kept st; ailang_rc_dec(st) (free #k); st = next
  read st[acc@8], st[n@16];  ailang_rc_dec(st)                  (final free)
  ailang_ctx_free(ctx)  →  AILANG_RC_STATS: allocs == frees     ← the proof
                            (M2 per-ctx counters are the instrument; no new one)
 ```
 ## Error handling
 - **Multi-constructor `data` as an export type** (`Maybe`, `List`,
  any 2+-ctor sum): `ExportNonScalarSignature`, RED — message names
  the constructor count and that the embedding ABI accepts a
  *single-constructor* record.
 - **Single-ctor record with a non-scalar field** (`Str`, a nested
  record, `List`): `ExportNonScalarSignature`, RED — message names
  the offending field and position, and that nested/`Str`/`List`
  fields are a future (M4) layer (not "unsupported", per the
  verbose-diagnostic philosophy).
 - **Effectful record export**: `ExportHasEffects`, unchanged RED.
 - **Host allocates the input with raw `malloc`** instead of
  `ailang_rc_alloc`: outside the language boundary (a host-side
  contract violation) — the frozen SSOT states `ailang_rc_alloc` as
  a normative MUST (the refcount header at `p-8` initialised to `1`
  is the precondition for correct `own`-consume and `ailang_rc_dec`).
  Not a checker concern; a documented ABI precondition.
 - **`--emit=staticlib --alloc=gc|bump`**: unchanged M2 RED (the
  swarm artefact is RC-only).
 - **`--emit=staticlib` with zero `(export)` fns**: unchanged M1 CLI
  error.
 ## Testing strategy
 RED-first throughout (`skills/debug` / TDD discipline).
 0. **Baseline pins (prerequisite — fixed first task, the
   2026-05-11 failure class pre-empted in order; same shape as
   M1's/M2's fixed task 1).** (a) Pin that
   `embed_export_adt_ret_rejected.ail` **fails `ail check` today**
   — this is the regression pin M3 *deliberately re-points* (not
   silently inverts: the pin's meaning changes from "any ADT
   rejected" to "non-M3-shaped ADT rejected", and the change is the
   explicit, reviewed content of an M3 task — not a test rewritten
   to dodge a behaviour change). (b) Pin the box layout **as codegen
   emits it today** — a new byte-offset test (`size = 8 + n*8`, tag
   `i64` at offset 0, fields from offset 8, header at `p-8`) green
   *before* the freeze lockstep is attached, so the freeze rests on
   a baseline pinned at its own layer.
 1. **Gate RED trio + positive.** (a) multi-ctor sum return,
   (b) single-ctor record with a `Str` field, (c) single-ctor
   record with a `List` field — each fails `ail check` with
   `ExportNonScalarSignature` naming the precise reason; plus the
   re-pointed combined fixture (multi-ctor **and** `Str`); plus the
   unchanged effectful `ExportHasEffects` fixture. The positive
   single-ctor `Float`+`Int` fixture passes `ail check`.
 2. **Forwarder shape pin.** The forwarder for a record export is
   `define ptr @backtest_step(ptr %ctx, ptr %st, double %sample)`
   with the `__ail_tls_ctx` save/store/restore **byte-identical to
   M2** around an **unchanged** `call ptr @ail_backtest_step(ptr
   %st, double %sample)`; no `@main`; `_adapter`/`_clos`
   byte-identical to M1/M2 (regression pin on the "untouched"
   decision). No `sret`/`byval` emitted (pin: record crosses as a
   bare `ptr`).
 3. **E2E record round-trip — `own` (coherent-stop proof).** The
   §"changed C host" harness on
   `examples/embed_backtest_step_record.ail`: host builds `State`
   via `ailang_rc_alloc`, calls N times, the kernel consumes each
   `own` input (Iter-B), the host frees the final return with
   `ailang_rc_dec`, and `ailang_ctx_free` reports `allocs == frees`
   (via the M2 per-ctx counters — the existing instrument). Result
   value asserted (`n == N`).
 4. **E2E record round-trip — `borrow`.**
   `examples/embed_backtest_step_record_borrow.ail`: the host
   retains and `ailang_rc_dec`s each input itself; the kernel does
   not consume it; `allocs == frees` again. Items 3+4 together prove
   "ownership follows the declared mode" in **both** directions —
   the frozen contract is tested, not asserted.
 5. **Layout byte-pin is enforcing.** The item-0(b) pin is green;
   a deliberate one-off offset perturbation in `lower_ctor` (local
   experiment, reverted) turns it RED — demonstrating the freeze is
   enforceable, not aspirational.
 6. **Schema / hash invariance, unmodified.** `embed_export_hash_stable.rs`
   and `design_schema_drift.rs` green **unmodified** — M3 adds no
   schema field (explicit M2-style contrast).
 7. **Executable path unchanged.** `print_no_leak_pin.rs` + the
   `e2e.rs` leak-stat helper green unmodified; M1 `embed_e2e.rs`
   (scalar) + the M2 swarm/rc-accounting harness green unmodified
   (M3 is additive to the gate/forwarder; the scalar path is
   byte-preserved).
 8. **Clean-core invariant.** No new dependency in `ailang-core` /
   `ailang-codegen` / `runtime/`; architect audits Invariant 1 at
   close.
 9. **Bench regression trio.** No runtime change, no codegen change
   on the benched (non-embed, executable) hot path — `bench/check.py`
   / `compile_check.py` / `cross_lang.py` carry-on, with the
   byte-identical-binary causal-exoneration method if a tracked-noise
   metric fires. Not hand-waved.
 ## Acceptance criteria
 Feature-acceptance criterion (DESIGN.md §"Feature-acceptance
 criterion"), applied honestly to a strategic infra/capability
 milestone with **no authoring surface**:
 1. **LLM author naturally produces it.** The worked `.ail`
   (`examples/embed_backtest_step_record.ail`, shown above) is the
   direct minimal evolution of the M1/M2 scalar kernel into a record
   `State`; asked to make a stateful fold callable from a Rust host,
   an LLM author writes exactly this (existing `data` + existing
   `(own (con T))` + existing `(export …)`). The worked `.ail` *is*
   the clause-1 evidence, not a prose assertion. Recorded honestly:
   the justification is strategic (the language's target deployment,
   the user-made roadmap direction call), not the standard
   authoring-utility metric. No pretence otherwise.
 2. **Measurably improves correctness / removes redundancy.** A
   capability + correctness gate, recorded honestly (as M1's/M2's
   clause 2 were): today a stateful fold *cannot cross the embedding
   boundary at all* (M1/M2 are scalar-only) — the entire
   `(State, Chunk) -> State` backtest the arc exists for is
   unbuildable as an embedded kernel without M3. The correctness
   delta is that the record crossing becomes *memory-safe by a
   specified, tested, frozen contract* (alloc==free proven for both
   modes; layout byte-pinned) rather than undefined.
 3. **Reintroduces no bug class the core eliminates.** The export
   gate still makes wrong code *fail to typecheck* (clause-3 in
   code, not documentation): multi-ctor / `Str`-field / nested-
   record / effectful exports stay RED. M3 *narrows* the gate
   precisely along the single-ctor-all-scalar boundary — it opens no
   hole; the discriminator is *sharper* (the re-pointed must-fail
   rejects on two independent reasons). Decision 10
   ("single-threaded; non-atomic refcounts") stays *true*: M2's
   per-thread ctx ⇒ no cell crosses a thread; an M3 record is
   per-thread by the same construction (built by the host thread
   that owns the ctx, freed by it) — Invariant 2 (no value crosses
   a thread boundary) holds, strengthened. The ownership contract
   *follows the existing declared-mode machinery* (DESIGN.md
   §"Mode metadata is load-bearing for codegen") — no new RC rule.
   The host-free choice (`ailang_rc_dec`) is leak-free *by
   construction* for M3-shaped records; the non-scalar case is
   explicitly flagged as M4-additive, not a hidden hole. The frozen
   commitment freezes the *actual current* layout (tag-included,
   as-is), byte-pinned and enforceable. Invariant 1 (clean core),
   Invariant 3 (native-AOT only) hold and are audited.
 Milestone-close ("coherent stop") is met when **all** hold:
 - `examples/embed_backtest_step_record.ail` builds with
  `ail build --emit=staticlib`; the C host builds the input `State`
  via `ailang_rc_alloc`, calls `backtest_step` N times, reads and
  `ailang_rc_dec`s the return, and `ailang_ctx_free` reports
  `allocs == frees` (`own` variant — coherent-stop proof).
 - The `borrow` variant (`embed_backtest_step_record_borrow.ail`,
  host-retained input freed by the host) is likewise green at
  `allocs == frees` — "follows the declared mode" proven both ways.
 - The gate RED trio + the re-pointed combined must-fail + the
  effectful fixture all fail `ail check` with precise,
  self-correcting diagnostics; the positive single-ctor `Float`+`Int`
  fixture passes.
 - Forwarder / internal `@ail_<mod>_<fn>` / `_adapter`/`_clos` /
  executable path / schema-hash all byte-unchanged
  (`embed_export_hash_stable.rs`, `design_schema_drift.rs`,
  `print_no_leak_pin.rs`, M1 `embed_e2e.rs`, M2 swarm harness green
  **unmodified**).
 - The layout byte-pin is green and demonstrably enforcing (a
  deliberate offset perturbation turns it RED).
 - DESIGN.md §"Embedding ABI" carries the frozen value-layout SSOT;
  "provisional until M3" → one-way-freeze wording; the three
  encoding sites carry the lockstep pointer.
 - Architect audit confirms Invariant 1; bench trio carry-on (no
  hot-path change; byte-identical-binary causal exoneration if a
  tracked-noise metric fires).
 ## Iteration sequencing (prerequisite-first)
 The planner decomposes M3 into bite-sized tasks, but **task 1 is
 fixed**: the Testing-strategy item-0 baseline pins — (a) pin that
 `embed_export_adt_ret_rejected.ail` fails `ail check` today (the pin
 M3 deliberately re-points, made explicit and reviewed, not silently
 inverted), and (b) pin the box layout as codegen emits it today
 *before* the freeze lockstep attaches. Rationale, same shape as
 M1's/M2's fixed task 1: M3 is *defined* as (i) widening the gate
 exactly along the single-ctor-all-scalar boundary the existing
 must-fail corpus brackets, and (ii) converting the
 provisional layout into a frozen, byte-pinned commitment. Both
 load-bearing changes must rest on a baseline pinned at their own
 layer before the change is introduced (the 2026-05-11 failure class,
 pre-empted in order). Only after task 1 is green does the
 check/codegen/docs work proceed. No other inter-task ordering is
 mandated; the planner owns the rest.
 ## Out of scope (explicit)
 - More than one record type crossing the boundary in a single
  signature beyond the `(State, Sample) -> State` shape's needs;
  the milestone's coherent stop is the single `State` round-trip.
 - `List` / sequence crossing — M4.
 - `Str` in/out — M4+ (a `Str` field is a non-scalar field, rejected
  by the M3 gate).
 - Nested records (a record field whose type is itself a record) —
  M4; the M3 recursive scalar check bottoms out at `Int`/`Float`
  and rejects a record-typed field.
 - A typed host-free symbol (`@<sym>_free`, a generic
  `ailang_record_free`) — explicitly **not** introduced; M3 leans
  on the scalar-field restriction so `ailang_rc_dec` is leak-free,
  and names the non-scalar recursive-free as M4's *additive*
  concern (the build-ahead-of-consumer trap, refused as in M1/M2).
 - Single-ctor tag elision — a hot-path codegen change touching every
  single-ctor ADT tree-wide for ABI cosmetics (human ergonomics, not
  LLM-author utility; disfavoured by the feature-acceptance
  criterion); the frozen layout includes the tag word as-is.
 - Any change to the internal `@ail_<module>_<fn>` calling convention
  or the `_adapter`/`_clos` closure pair (M1/M2 decision held).
 - The `ail-embed` adapter crate + `data-server` wiring + the real
  thread-swarm record backtest — M5.
 - Tree-wide Boehm retirement — the separate standing P2 todo,
  untouched.