diff --git a/docs/roadmap.md b/docs/roadmap.md index dd1c785..1d6bd66 100644 --- a/docs/roadmap.md +++ b/docs/roadmap.md @@ -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 - anticipates this ("The ABI defined here is stable … unless - the layout itself shifts"). + - 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"). - [ ] **\[milestone\]** Embedding ABI — M4: sequence crossing via the existing `List` ADT. Host builds a `List Record` per chunk; diff --git a/docs/specs/2026-05-18-embedding-abi-m3.md b/docs/specs/2026-05-18-embedding-abi-m3.md new file mode 100644 index 0000000..d565330 --- /dev/null +++ b/docs/specs/2026-05-18-embedding-abi-m3.md @@ -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 (`@(scalars…)`); M2 threaded a +per-thread `ailang_ctx_t*` through it (`@(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__` +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__` 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__`: 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__`: 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 +#include +#include + +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__(...) and the TLS + save/store/restore are identical to M2. + @ail__ + _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__` + `_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__` / `_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 (`@_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__` 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.