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