iter embedding-abi-m3.1 (PARTIAL 5/7 + Boss spec-defect repair): single-ctor scalar record crosses the C ABI, ownership follows declared mode

Tasks 1-5 GREEN. T1 baseline pins (re-point annotation + @ailang_rc_alloc
heap-box byte-pin: size=8+n*8, tag@0, fields@8/16). T2 export gate widened
(is_c_scalar -> two-level is_c_abi_type: single-ctor all-Int/Float record;
multi-ctor/Str/List/nested still RED; gate suite 10/10; M1 adt-ret must-fail
re-pointed to multi-ctor+Str Reading). T3 codegen forwarder widened
(llvm_scalar record Type::Con -> ptr; M2 forwarder body byte-unchanged;
3/3 staticlib pins). T4/T5 E2E record round-trip own+borrow, global
leak-freedom.

Boss spec-consistency repair (M2.1-precedent class): orchestrator
correctly BLOCKED Task 5 on a genuine spec defect -- the single-ctx-readback
allocs==frees proof model is unsatisfiable for borrow (and only
coincidentally passes for own) because M2's TLS-ctx is bound only during
the synchronous forwarder call, so host-side decs land on g_rc_*, not ctx.
Boss-verified globally leak-free + value-correct both modes. Spec + plan +
harness amended to the stronger global model (sum all ailang_rc_stats:
lines; the M2-TLS cross-attribution documented as correct behaviour). No
fresh grounding-check (removes an over-strong measurement assumption).

Tasks 6 (DESIGN.md frozen-layout SSOT + lockstep pointers + freeze wording
+ enforceability demo) and 7 (workspace-green gate) re-dispatched on the
amended plan. Bench/architect milestone-close is audit-owned.

iter embedding-abi-m3.1 (PARTIAL); INDEX.md line deferred to the DONE commit

bench/orchestrator-stats/2026-05-18-iter-embedding-abi-m3.1.json

@@ -0,0 +1,13 @@
+{
+  "iter_id": "embedding-abi-m3.1",
+  "date": "2026-05-18",
+  "mode": "standard",
+  "outcome": "PARTIAL",
+  "tasks_total": 7,
+  "tasks_completed": 4,
+  "reloops_per_task": { "1": 0, "2": 0, "3": 0, "4": 0, "5": 1 },
+  "review_loops_spec": 0,
+  "review_loops_quality": 0,
+  "blocked_reason": "worker-blocked",
+  "notes": "Tasks 1-4 DONE/GREEN (3 of them DONE_WITH_CONCERNS for plan-pseudo-code corrections: term-ctor construction, module==file-stem, module-qualified internal symbol, library-API-resolvable IO sink). Task 5 BLOCKED on a plan-assertion-model defect (ctx-readback allocs==frees structurally unsatisfiable for borrow mode given the M2 TLS-ctx accounting mechanism; no production bug, globally leak-free). Same failure class as the M2.1 swarm.c/-DSHARED_CTX Boss-adjudicated spec defect. Tasks 6-7 not attempted (Task 5 is a hard sequencing predecessor; skip-task is not a mode). The single re-loop on Task 5 was the implementer-phase context-expansion confirming the contradiction is a plan defect (no public ailang_ctx_enter API exists), not implementer-fixable within task scope. bench/architect milestone-close is audit-owned (not this run)."
+}

crates/ail/tests/embed/record_roundtrip.c

@@ -0,0 +1,53 @@
+/* Embedding-ABI M3 record round-trip C host (own + borrow via a
+ * compile-time -DBORROW switch). Frozen value layout (DESIGN.md
+ * §"Embedding ABI" > "Frozen value layout"):
+ *   p - 8 .. p   uint64_t refcount header (set to 1 by ailang_rc_alloc)
+ *   p + 0        int64_t  constructor tag (single ctor → 0)
+ *   p + 8        IEEE-754 double  field 0 = Float acc
+ *   p + 16       int64_t          field 1 = Int   n
+ * Total payload = 8 + 2*8 = 24.
+ *
+ * own  : the kernel consumes each `(own (con State))` input (drop at
+ *        return); the host must NOT touch/dec it after the call.
+ * borrow: the kernel does NOT consume the `(borrow (con State))`
+ *        input; the host retains it and dec's it itself each iter.
+ * In both modes the return is host-owned and host-freed.
+ */
+#include <stdint.h>
+#include <assert.h>
+#include <string.h>
+#include <stdlib.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);
+extern void  ailang_rc_dec(void *);
+extern void *backtest_step(ailang_ctx_t *ctx, void *st, double sample);
+
+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 acc @ 8           */
+    *(int64_t *)((char *)p + 16) = n;       /* Int   n   @ 16          */
+    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));
+#ifdef BORROW
+        ailang_rc_dec(st);   /* borrow: host retained input, frees it */
+#endif
+        /* own: kernel consumed `st`; do NOT touch/dec it here.        */
+        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 final return            */
+    ailang_ctx_free(ctx);    /* AILANG_RC_STATS readback fires here    */
+    return 0;
+}

crates/ail/tests/embed_record_e2e.rs

@@ -0,0 +1,152 @@
+//! Embedding-ABI M3 record round-trip (spec §"Testing strategy" —
+//! coherent-stop proof, both ownership directions). Build the record
+//! kernel as a staticlib, link the C host (frozen `{tag@0, double
+//! acc@8, int64 n@16}` layout, `make_state` via `ailang_rc_alloc`),
+//! run with `AILANG_RC_STATS=1`, and assert the `ailang_ctx_free`
+//! RC-stats readback shows kernel-internal `allocs == frees` and the
+//! C host's `assert(n == 1000000)` held (exit 0).
+//!
+//! `own` (no -DBORROW): the kernel consumes each `(own (con State))`
+//! input (drop at return — ratified by
+//! `crates/ail/tests/e2e.rs::alloc_rc_own_param_dec_at_fn_return:1855`,
+//! NOT `borrow_own_demo_modes_are_metadata_only` which is an Iter-18a
+//! pre-enforcement metadata-only pin) and allocates the new return.
+//! `borrow` (-DBORROW, Task 5): the kernel does NOT consume the
+//! `(borrow (con State))` input (ratified by
+//! `…::alloc_rc_borrow_only_recursive_list_drop:1671`); the host
+//! retains and dec's it each iter. Both prove "ownership follows the
+//! declared mode" — the frozen contract proven both ways.
+//!
+//! The build/link incantation mirrors `embed_e2e.rs`
+//! (`ail build --emit=staticlib -o <dir>` → `cc host.c
+//! lib<module>.a libailang_rt.a`); the stats-line parse mirrors
+//! `e2e.rs::build_and_run_with_rc_stats` (the runtime's fixed
+//! `ailang_rc_stats: allocs=N frees=M live=K` shape).
+
+use std::path::PathBuf;
+use std::process::Command;
+
+fn ail_bin() -> &'static str { env!("CARGO_BIN_EXE_ail") }
+fn manifest() -> PathBuf { PathBuf::from(env!("CARGO_MANIFEST_DIR")) }
+fn ws_root() -> PathBuf {
+    manifest().parent().unwrap().parent().unwrap().to_path_buf()
+}
+
+#[derive(Debug)]
+struct RcStats {
+    allocs: u64,
+    frees: u64,
+    exit_code: i32,
+}
+
+/// Build `<fixture>` as a staticlib, link `<host_rel>` (under
+/// `crates/ail/tests/`) with `extra_cc` flags, run under
+/// `AILANG_RC_STATS=1`, and return the `ailang_ctx_free` readback.
+fn build_link_run_embed(fixture: &str, host_rel: &str, extra_cc: &[&str]) -> RcStats {
+    let module = fixture.strip_suffix(".ail").expect("fixture is a .ail file");
+    let fixture_path = ws_root().join("examples").join(fixture);
+    let host_c = manifest().join("tests").join(host_rel);
+    let outdir = std::env::temp_dir().join(format!(
+        "ail-embed-record-e2e-{}-{}",
+        module,
+        std::process::id()
+    ));
+    std::fs::create_dir_all(&outdir).unwrap();
+
+    let build = Command::new(ail_bin())
+        .args(["build", fixture_path.to_str().unwrap(),
+               "--emit=staticlib", "-o", outdir.to_str().unwrap()])
+        .output().expect("ail build --emit=staticlib");
+    assert!(build.status.success(),
+        "staticlib build failed: {}",
+        String::from_utf8_lossy(&build.stderr));
+
+    let host_bin = outdir.join("host");
+    let mut cc = Command::new("cc");
+    cc.arg(&host_c);
+    for f in extra_cc { cc.arg(f); }
+    cc.arg(outdir.join(format!("lib{module}.a")))
+        .arg(outdir.join("libailang_rt.a"))
+        .arg("-o").arg(&host_bin);
+    let cc_out = cc.output().expect("cc host link");
+    assert!(cc_out.status.success(),
+        "cc link failed: {}", String::from_utf8_lossy(&cc_out.stderr));
+
+    let run = Command::new(&host_bin)
+        .env("AILANG_RC_STATS", "1")
+        .output().expect("run host");
+    let stderr = String::from_utf8_lossy(&run.stderr);
+    // Boss spec-consistency repair (2026-05-18, M3.1 BLOCKED
+    // adjudication): the run emits TWO `ailang_rc_stats:` lines —
+    // the `ailang_ctx_free` ctx readback AND the `g_rc_*` atexit
+    // line. By M2's TLS-ctx design the ctx is bound to TLS only for
+    // the synchronous forwarder call, so the host's `make_state` /
+    // per-iter `dec` / final `dec` (which run outside any forwarder
+    // call) land on `g_rc_*`, not ctx. The invariant is GLOBAL
+    // leak-freedom: Σallocs == Σfrees across *all* stat lines
+    // (equivalently Σ`live` = 0) — not per-ctx-line balance. Sum
+    // every line; a missing-line panic guards against zero parsed.
+    let mut allocs: u64 = 0;
+    let mut frees: u64 = 0;
+    let mut seen = 0usize;
+    for line in stderr.lines().filter(|l| l.starts_with("ailang_rc_stats:")) {
+        seen += 1;
+        for tok in line.split_whitespace() {
+            if let Some(v) = tok.strip_prefix("allocs=") {
+                allocs += v.parse::<u64>().expect("allocs= u64");
+            } else if let Some(v) = tok.strip_prefix("frees=") {
+                frees += v.parse::<u64>().expect("frees= u64");
+            }
+        }
+    }
+    assert!(seen > 0, "missing ailang_rc_stats line; stderr was:\n{stderr}");
+    RcStats {
+        allocs,
+        frees,
+        exit_code: run.status.code().unwrap_or(-1),
+    }
+}
+
+/// own: globally leak-free — every State box freed exactly once.
+/// The `(own (con State))` input is drop-consumed at the kernel's
+/// return (Iter-B, on ctx); the host's `make_state` + final `dec`
+/// land on `g_rc_*`. Σallocs == Σfrees across both stat lines
+/// (own: ctx `live=0` + g_rc `live=0`), and the C host's
+/// `assert(n == 1000000)` held.
+#[test]
+fn record_roundtrip_own_alloc_eq_free() {
+    let stats = build_link_run_embed(
+        "embed_backtest_step_record.ail",
+        "embed/record_roundtrip.c",
+        &[],
+    );
+    assert_eq!(stats.allocs, stats.frees,
+        "own: globally leak-free — Σallocs == Σfrees across the ctx \
+         readback + g_rc atexit lines (kernel-consumed `own` inputs \
+         on ctx; host make_state/final dec on g_rc); {stats:?}");
+    assert_eq!(stats.exit_code, 0, "C host assert(n==1000000) held");
+}
+
+/// borrow: globally leak-free. The kernel does NOT consume the
+/// `(borrow (con State))` input (ratified by
+/// `crates/ail/tests/e2e.rs::alloc_rc_borrow_only_recursive_list_drop:1671`);
+/// it allocs every return box on ctx, the host frees every input +
+/// the final return on `g_rc_*` (outside the forwarder's TLS-ctx
+/// window). The ctx line shows `live=+N`, the g_rc line `live=−N`,
+/// summing to 0 — correct M2-TLS cross-attribution, not a leak.
+/// Σallocs == Σfrees across both lines. Same harness, `-DBORROW`.
+/// With Task 4 this proves "ownership follows the declared mode" in
+/// both directions, globally leak-free — proven, not asserted.
+#[test]
+fn record_roundtrip_borrow_alloc_eq_free() {
+    let stats = build_link_run_embed(
+        "embed_backtest_step_record_borrow.ail",
+        "embed/record_roundtrip.c",
+        &["-DBORROW"],
+    );
+    assert_eq!(stats.allocs, stats.frees,
+        "borrow: globally leak-free — Σallocs == Σfrees across the ctx \
+         readback (kernel return allocs, live=+N) + g_rc atexit \
+         (host input/return decs, live=−N); summed they balance; {stats:?}");
+    assert_eq!(stats.exit_code, 0, "C host assert(n==1000000) held");
+}

crates/ailang-check/src/lib.rs

@@ -449,7 +449,7 @@ pub enum CheckError {
     /// `Bool`/`Str`/every ADT is rejected at typecheck (the
     /// feature-acceptance clause-3 discriminator, in code).
     /// Code: `export-non-scalar-signature`.
-    #[error("export `{0}`: M1 embedding ABI is scalar-only — {1} type `{2}` is not `Int`/`Float`")]
+    #[error("export `{0}`: embedding ABI accepts `Int`/`Float` or a single-constructor record of those — {1} type `{2}` is not permitted (multi-constructor sums, and `Str`/`List`/nested-record fields, are a future M4 layer)")]
     ExportNonScalarSignature(String, &'static str, String),
 
     /// An `(export …)` fn has a non-empty effect set. An embedding
@@ -1922,8 +1922,31 @@ fn check_fn(f: &FnDef, env: &Env, out_warnings: &mut Vec<Diagnostic>) -> Result<
             matches!(t, Type::Con { name, args, .. }
                 if args.is_empty() && (name == "Int" || name == "Float"))
         }
+        // M3 (spec 2026-05-18-embedding-abi-m3 §Architecture): a C
+        // scalar, OR a single-constructor `data` whose every field is a
+        // *bare* C scalar. Two-level by design — a record-typed field
+        // stays rejected (M4 owns nested-record recursion). Uses the
+        // in-scope `env.types: String -> TypeDef` (cf. lib.rs:1826).
+        fn is_c_abi_type(t: &Type, env: &Env) -> bool {
+            if is_c_scalar(t) {
+                return true;
+            }
+            if let Type::Con { name, args, .. } = t {
+                if args.is_empty() {
+                    if let Some(td) = env.types.get(name) {
+                        if td.ctors.len() == 1 {
+                            return td.ctors[0]
+                                .fields
+                                .iter()
+                                .all(is_c_scalar);
+                        }
+                    }
+                }
+            }
+            false
+        }
         for p in &param_tys {
-            if !is_c_scalar(p) {
+            if !is_c_abi_type(p, &env) {
                 return Err(CheckError::ExportNonScalarSignature(
                     f.name.clone(),
                     "parameter",
@@ -1931,7 +1954,7 @@ fn check_fn(f: &FnDef, env: &Env, out_warnings: &mut Vec<Diagnostic>) -> Result<
                 ));
             }
         }
-        if !is_c_scalar(&ret_ty) {
+        if !is_c_abi_type(&ret_ty, &env) {
             return Err(CheckError::ExportNonScalarSignature(
                 f.name.clone(),
                 "return",

crates/ailang-check/tests/embed_export_gate.rs

@@ -27,6 +27,14 @@ fn str_param_export_rejected() {
         .iter().any(|c| c == "export-non-scalar-signature"));
 }
 
+// M3 RE-POINT (deliberate, reviewed — spec 2026-05-18-embedding-abi-m3
+// §"must-fail axis"): the fixture this asserts on
+// (embed_export_adt_ret_rejected.ail) is single-ctor two-Int = M3-VALID.
+// Task 2 re-points the fixture to a genuinely-still-rejected ADT
+// (multi-ctor + Str field). This pin's *meaning* changes from
+// "any ADT rejected" to "non-M3-shaped ADT rejected"; it is NOT
+// silently inverted — the rejection (export-non-scalar-signature)
+// stays asserted, on a fixture that still genuinely fails it.
 #[test]
 fn adt_ret_export_rejected() {
     assert!(check_codes("embed_export_adt_ret_rejected.ail")
@@ -61,3 +69,30 @@ fn headline_int_export_passes() {
         c == "export-non-scalar-signature" || c == "export-has-effects"),
         "headline export must pass the gate; got {codes:?}");
 }
+
+#[test]
+fn record_export_passes() {
+    // single-ctor (Float,Int) record export — M3-valid
+    let codes = check_codes("embed_export_record_ok.ail");
+    assert!(!codes.iter().any(|c|
+        c == "export-non-scalar-signature" || c == "export-has-effects"),
+        "single-ctor scalar record export must pass the gate; got {codes:?}");
+}
+
+#[test]
+fn str_field_record_export_rejected() {
+    assert!(check_codes("embed_export_str_field_record_rejected.ail")
+        .iter().any(|c| c == "export-non-scalar-signature"));
+}
+
+#[test]
+fn list_field_record_export_rejected() {
+    assert!(check_codes("embed_export_list_field_record_rejected.ail")
+        .iter().any(|c| c == "export-non-scalar-signature"));
+}
+
+#[test]
+fn multictor_export_rejected() {
+    assert!(check_codes("embed_export_multictor_rejected.ail")
+        .iter().any(|c| c == "export-non-scalar-signature"));
+}

crates/ailang-codegen/src/lib.rs

@@ -662,17 +662,27 @@ fn fn_scalar_sig(t: &Type) -> Option<(Vec<Type>, Type)> {
         other => other,
     };
     match inner {
+        // M3: params/ret may include a single-ctor scalar record type;
+        // llvm_scalar maps it to `ptr`. fn_scalar_sig is type-shape only.
         Type::Fn { params, ret, .. } =>
             Some((params.clone(), (**ret).clone())),
         _ => None,
     }
 }
 
-/// `Int` → `i64`, `Float` → `double` (the only two M1 scalars; the
+/// `Int` → `i64`, `Float` → `double`, a single-ctor scalar record
-/// check-side gate rejects everything else before codegen).
+/// (any other named `Type::Con` reaching an `(export)` signature, by
+/// the Task-2 export gate) → `ptr`. The check-side gate rejects every
+/// other shape before codegen.
 fn llvm_scalar(t: &Type) -> &'static str {
     match t {
         Type::Con { name, .. } if name == "Float" => "double",
+        Type::Con { name, .. } if name == "Int" => "i64",
+        // M3: any other Type::Con reaching an (export) signature is,
+        // by the Task-2 export gate, a single-ctor scalar record;
+        // it crosses the C ABI as a bare `ptr` (DESIGN.md §"Embedding
+        // ABI" frozen layout — payload pointer).
+        Type::Con { .. } => "ptr",
         _ => "i64",
     }
 }

crates/ailang-codegen/tests/embed_record_layout_pin.rs

@@ -0,0 +1,47 @@
+//! FROZEN ABI byte-pin — see DESIGN.md §"Embedding ABI" frozen layout.
+//! Pins the heap (@ailang_rc_alloc) box layout a boundary-crossing
+//! single-ctor scalar record takes: size = 8 + n*8, tag i64 @ offset
+//! 0, fields i64-strided from offset 8. Goes RED if codegen moves an
+//! offset — the M3 freeze made enforceable, not aspirational.
+//!
+//! The carrier (`embed_record_layout_carrier.ail`) is a non-export
+//! exe-target program whose `mk` returns a `Pt` consumed by an
+//! `(own (con Pt))` param `sum_pt`, forcing the escaping heap box
+//! (NOT the `alloca` non-escape path the pre-existing
+//! `iter17a_local_box_alloca` pins — that is a different path and not
+//! a substitute for this one). Lowered under `AllocStrategy::Rc`
+//! (the path a crossing M3 record actually takes), mirroring the
+//! workspace-load + lower incantation of `embed_staticlib_lowering.rs`.
+
+use ailang_core::Workspace;
+use std::path::PathBuf;
+
+fn load(file: &str) -> Workspace {
+    let path = PathBuf::from(env!("CARGO_MANIFEST_DIR"))
+        .parent().unwrap().parent().unwrap()
+        .join("examples").join(file);
+    ailang_surface::load_workspace(&path).unwrap()
+}
+
+fn lower_carrier_ir() -> String {
+    let ws = load("embed_record_layout_carrier.ail");
+    ailang_codegen::lower_workspace_with_alloc(
+        &ws, ailang_codegen::AllocStrategy::Rc).unwrap()
+}
+
+#[test]
+fn heap_box_layout_is_frozen_8_plus_n_times_8_tag_at_0_fields_from_8() {
+    let ir = lower_carrier_ir();
+    // Pt has 2 Int fields → payload size 8 (tag) + 2*8 (fields) = 24,
+    // on the @ailang_rc_alloc heap path (record crosses the boundary).
+    assert!(ir.contains("call ptr @ailang_rc_alloc(i64 24)"),
+        "frozen: heap box payload size = 8 + n*8 (n=2 → 24); IR:\n{ir}");
+    // constructor tag written at offset 0 (single-ctor → 0; no elision)
+    assert!(ir.contains("store i64 0, ptr"),
+        "frozen: ctor tag i64 at offset 0; IR:\n{ir}");
+    // field 0 at offset 8, field 1 at offset 16 (i64-strided from 8)
+    assert!(ir.contains("getelementptr inbounds i8, ptr") && ir.contains("i64 8"),
+        "frozen: field 0 at payload offset 8; IR:\n{ir}");
+    assert!(ir.contains("i64 16"),
+        "frozen: field 1 at payload offset 16 (8 + 1*8); IR:\n{ir}");
+}

crates/ailang-codegen/tests/embed_staticlib_lowering.rs

@@ -43,6 +43,33 @@ fn staticlib_emits_forwarder_no_main() {
         "internal call must stay byte-unchanged (no ctx arg);\nIR:\n{ir}");
 }
 
+/// M3: a single-ctor scalar record param/ret crosses the embedding
+/// C boundary as a bare `ptr` (the frozen payload pointer — DESIGN.md
+/// §"Embedding ABI" > "Frozen value layout"). The M2 forwarder body
+/// is byte-unchanged: leading `ptr %ctx`, TLS save/store/restore, the
+/// internal `@ail_<module>_<fn>` call carrying no ctx arg and no
+/// aggregate calling convention (no `sret`/`byval` — a record is a
+/// bare ptr, not an LLVM aggregate). Internal symbol is module-
+/// qualified `@ail_embed_backtest_step_record_step` (module ==
+/// file stem, Design-decision 6).
+#[test]
+fn staticlib_record_forwarder_is_ptr_passthrough() {
+    let ws = load("embed_backtest_step_record.ail");
+    let ir = ailang_codegen::lower_workspace_staticlib_with_alloc(
+        &ws, ailang_codegen::AllocStrategy::Rc).unwrap();
+    // record param + ret cross as bare ptr; ctx leading; M2 TLS shape.
+    assert!(ir.contains("define ptr @backtest_step(ptr %ctx, ptr %a0, double %a1)"),
+        "record fwd: ptr ret, leading ptr %ctx, ptr record param, double sample;\nIR:\n{ir}");
+    assert!(ir.contains("store ptr %ctx, ptr @__ail_tls_ctx"),
+        "M2 TLS store byte-unchanged;\nIR:\n{ir}");
+    assert!(ir.contains("call ptr @ail_embed_backtest_step_record_step(ptr %a0, double %a1)"),
+        "internal call byte-unchanged (no ctx arg, module-qualified);\nIR:\n{ir}");
+    assert!(!ir.contains("sret") && !ir.contains("byval"),
+        "no aggregate convention introduced — record is a bare ptr;\nIR:\n{ir}");
+    assert!(!ir.contains("define i32 @main()"),
+        "staticlib: no @main;\nIR:\n{ir}");
+}
+
 #[test]
 fn executable_target_still_emits_main() {
     let ws = load("embed_backtest_step.ail");

docs/journals/2026-05-18-iter-embedding-abi-m3.1.md

@@ -0,0 +1,292 @@
+# iter embedding-abi-m3.1 — freeze the value layout + record across the C ABI
+
+**Date:** 2026-05-18
+**Started from:** 15ee3c5c8fbb871a9cde6cc7d57c0801bae9ae85
+**Status:** PARTIAL (Tasks 1–5 GREEN after the Boss spec-consistency
+repair below; Tasks 6–7 re-dispatched)
+**Tasks completed:** 4 of 7 by the orchestrator (Tasks 1–4 DONE/GREEN;
+Task 5 correctly BLOCKED on a genuine spec-defect, M2.1-precedent
+class); Task 5 resolved GREEN by the Boss spec-consistency repair
+(global-leak-freedom proof model); Tasks 6–7 re-dispatched on the
+amended plan
+
+## Summary
+
+Tasks 1–4 are complete and GREEN in the working tree: the FIXED-FIRST
+baseline pins (1a re-point annotation on `adt_ret_export_rejected`;
+1b the new `@ailang_rc_alloc` heap-box byte-pin proving size=8+n*8 /
+tag@0 / fields@8,16), the export-gate widen to a single-ctor scalar
+record (`is_c_scalar` → two-level `is_c_abi_type`, 10/10 gate suite),
+the codegen forwarder widen (`llvm_scalar` maps a gate-guaranteed
+record `Type::Con` → `ptr`; M2 forwarder body byte-unchanged; 3/3
+staticlib-lowering pins), and the `own` E2E record round-trip
+(1,000,000-iter balanced ctx readback `allocs=1000000 frees=1000000
+live=0`, exit 0 — the spec's "mechanically almost free" ownership
+claim substantiated, ratified by `e2e.rs:1855`, NOT the Iter-18a
+metadata-only pin).
+
+Task 5 (the `borrow` E2E arm) is BLOCKED on a genuine
+plan-assertion-model defect (detail below), structurally identical to
+the M2.1 first-dispatch swarm.c/-DSHARED_CTX spec defect that the
+Boss adjudicated and repaired. No production-code bug: the borrow
+mode is leak-free and value-correct; the plan's *assertion shape* is
+unsatisfiable given the M2 TLS-ctx accounting mechanism. Returned
+BLOCKED for Boss adjudication per the Iron Law (never push past
+BLOCKED by hand; spec/plan amendment is a Boss/brainstorm decision).
+
+audit owns the bench + architect milestone-close (spec Testing items
+8/9 — architect Invariant 1, bench trio); this implement run asserts
+only the test-suite GREEN state an implement run can, and Task 7
+(workspace-green gate) was not reached because Task 5 blocks the
+sequence.
+
+## Per-task notes
+
+- iter embedding-abi-m3.1.1 (DONE_WITH_CONCERNS): re-point annotation
+  added verbatim above `adt_ret_export_rejected`
+  (`crates/ailang-check/tests/embed_export_gate.rs`); gate suite 6/6
+  inert. New byte-pin carrier `examples/embed_record_layout_carrier.ail`
+  + new pin `crates/ailang-codegen/tests/embed_record_layout_pin.rs`
+  (`lower_workspace_with_alloc(&ws, AllocStrategy::Rc)`, mirroring
+  `embed_staticlib_lowering.rs`'s `load()` helper). Pin GREEN on the
+  pre-M3 tree. Carrier required two grounding corrections vs the
+  plan's literal pseudo-code (see Concerns).
+- iter embedding-abi-m3.1.2 (DONE_WITH_CONCERNS): `is_c_scalar` →
+  two-level `is_c_abi_type` (`crates/ailang-check/src/lib.rs:1921+`),
+  both call sites (param loop + ret) repointed; `:452` `#[error]`
+  widened; `:458` correctly left byte-unchanged (no `M1` token). 5
+  fixtures (`embed_export_record_ok` + 3 `_rejected` + re-pointed
+  `embed_export_adt_ret_rejected` → multi-ctor+Str `Reading`) + 4 new
+  gate tests. RED observed (`record_export_passes` failed pre-widen);
+  GREEN 10/10; full `ailang-check` 0 failed.
+- iter embedding-abi-m3.1.3 (DONE_WITH_CONCERNS): `llvm_scalar`
+  widened (`Float`→double, `Int`→i64, other `Type::Con`→`ptr`, `_`→
+  i64) + doc-comment lockstep; `fn_scalar_sig` clarifying comment only
+  (body recon-confirmed filter-free). 2 fixtures
+  (`embed_backtest_step_record{,_borrow}.ail`) + forwarder-IR pin
+  `staticlib_record_forwarder_is_ptr_passthrough`. RED observed
+  (State→i64 pre-widen); GREEN 3/3; full `ailang-codegen` 0 failed
+  (Task-1 byte-pin unchanged — box layout did not move).
+- iter embedding-abi-m3.1.4 (DONE): `crates/ail/tests/embed/
+  record_roundtrip.c` + `crates/ail/tests/embed_record_e2e.rs`.
+  `build_link_run_embed` composed from verbatim-mirrored real
+  incantations (`embed_e2e.rs` build/link + `e2e.rs:2190`
+  `build_and_run_with_rc_stats` stats-parse — `embed_e2e.rs` exposes
+  no reusable helper; mirroring, not inventing). `own` E2E GREEN
+  immediately once Tasks 2+3 in tree (ctx readback `allocs=1000000
+  frees=1000000 live=0`, exit 0). No production code (plan: none
+  expected). Ratifier `e2e.rs::alloc_rc_own_param_dec_at_fn_return:
+  1855` cited; `borrow_own_demo_modes_are_metadata_only:1330` NOT
+  cited (Boss constraint 2 honoured).
+- iter embedding-abi-m3.1.5 (BLOCKED — plan-assertion-model defect):
+  `record_roundtrip_borrow_alloc_eq_free` added to
+  `embed_record_e2e.rs`. RED and stays RED — see Blocked detail. Left
+  in the working tree as evidence (the M2.1-precedent handling: the
+  BLOCKED task's state is left for Boss adjudication, not discarded).
+- iter embedding-abi-m3.1.6 / .7: NOT attempted. Task 5 is a hard
+  predecessor in the plan's sequencing; `skip task K, continue` is
+  intentionally not a mode (implicit ordering dependencies; the
+  orchestrator does not own the dependency graph).
+
+## Concerns
+
+- iter embedding-abi-m3.1.1: PLAN PSEUDO-CODE DEFECT (class:
+  "plan pseudo-code vs reality"). The plan's carrier body used
+  `(app Pt a b)` for ADT construction — non-compiling (`ail check`:
+  `[not-a-function] mk: \`Pt\` is not a function`). AILang construction
+  is `(term-ctor <Type> <Ctor> args…)` (grounded on
+  `examples/box.ail:36`, `borrow_own_demo.ail`). Corrected to
+  `(term-ctor Pt Pt a b)`. Second correction: the plan's
+  `(app print …)` IO sink is unresolvable by the codegen library API
+  the byte-pin must use (`lower_workspace_with_alloc` does not run the
+  mono/prelude pass that resolves polymorphic `print` —
+  empirically: `UnknownVar("print")`; `io/print_int` is not a known
+  effect-op). Corrected to `(let s (app int_to_str …) (do io/print_str
+  s))` (monomorphic builtin, library-resolvable; grounded on
+  `int_to_str_drop_rc.ail`). Structural intent (single-ctor 2-Int
+  record forced onto the `@ailang_rc_alloc` heap path) preserved
+  exactly; plan Step-4/5 explicitly sanctions carrier adjustment to
+  force the heap box. Observation, not correctness — the byte-pin
+  asserts the literal emitted forms and is a genuine RED-on-offset-
+  move guard (proven enforceable would be Task 6 Step 7, not reached).
+- iter embedding-abi-m3.1.2: same plan-pseudo-code class — all 5
+  fixture bodies used `(app Ctor …)`; corrected to `(term-ctor …)`.
+  The test assertion idiom was matched to the file's *existing*
+  `.iter().any(|c| c == …)` pattern (plan showed
+  `.contains(&"…".to_string())`); `record_export_passes` written as
+  `!any(gate-code)` not the plan's `.is_empty()` (a single
+  `over-strict-mode` warning makes the diagnostics vec non-empty —
+  `.is_empty()` would false-fail; the protected property is
+  "no gate rejection"). Semantic intent preserved.
+- iter embedding-abi-m3.1.2 (carry to Task 6): the
+  `CheckError::ExportNonScalarSignature` rustdoc at
+  `crates/ailang-check/src/lib.rs:448-450` still says "M1's embedding
+  ABI is scalar-only; `Bool`/`Str`/every ADT is rejected" — now stale
+  (single-ctor scalar records are accepted). Outside Task 2's named
+  edit regions (`:452`/`:458` only); Task 6 owns the broader
+  stale-doc / "provisional until M3" sweep and should absorb this
+  line. Not gating; recorded for Boss/Task-6 scope.
+- iter embedding-abi-m3.1.3: PLAN TRANSCRIPTION DEFECT (same class as
+  the M2.1 journal's `@ail_embed_backtest_step_step` correction). The
+  plan's fixtures used `(module backtest …)` while the file stems are
+  `embed_backtest_step_record{,_borrow}` — the loader enforces
+  module==file-stem (`[module-name-mismatch]`). Module names corrected
+  to the file stems; the forwarder-IR pin's internal-symbol assertion
+  corrected from the plan's draft `@ail_backtest_step` to the
+  convention-correct module-qualified
+  `@ail_embed_backtest_step_record_step` (per the plan's own Step-3
+  parenthetical "tighten to literal emitted forms" + Boss constraint /
+  M2.1 module-qualified-symbol mandate). `llvm_scalar` doc-comment
+  updated in lockstep with its widened body (coherence-required, not
+  surrounding cleanup — a function whose doc says "the only two M1
+  scalars" while its body maps a third case is self-contradictory
+  within the same task). `llvm_scalar` is now a slightly
+  over-narrow *name* (also maps records→ptr) — renaming is a 4-site
+  cross-cut out of Task-3 scope; the doc disambiguates; advisory Nit
+  only.
+
+## Known debt
+
+- `crates/ailang-check/src/lib.rs:448-450` stale variant rustdoc —
+  Task-6-scope (see Concerns); not touched to keep Task 2
+  scope-compliant.
+- `llvm_scalar` identifier slightly narrower than its post-M3
+  behaviour — out of Task-3 scope; doc disambiguates.
+- Tasks 6 (DESIGN.md SSOT + lockstep freeze pointers + the
+  match_lower.rs enforceability demonstration) and 7 (workspace-green
+  gate) unexecuted — blocked behind Task 5.
+
+## Blocked detail
+
+**Task:** 5 (`record_roundtrip_borrow_alloc_eq_free`).
+**Reason:** worker-blocked — design/plan contradiction
+(plan-assertion-model defect; the implementer-phase sub-status is
+`BLOCKED`, mapped to the Boss per the SKILL.md sub-status table).
+
+**Worker says (verbatim):** The plan's Task-5 assertion
+`assert_eq!(stats.allocs, stats.frees, "borrow: kernel kept input;
+host freed every input + the return")` is structurally unsatisfiable.
+`stats` is defined (Task 4 Step 2, plan) as the *single*
+`ailang_ctx_free` RC-stats readback — the kernel-internal ctx
+accounting. In `borrow` mode the kernel allocates the new return box
+during the forwarder call (lands on `ctx->alloc_count` because the
+codegen forwarder publishes `ctx` into `__ail_tls_ctx` for the
+synchronous call duration only) but does NOT consume/drop the borrowed
+input (correct borrow semantics, ratified by
+`e2e.rs::alloc_rc_borrow_only_recursive_list_drop:1671`). The
+balancing frees are the host's per-iter `ailang_rc_dec(st)`, which run
+*outside* any forwarder call → `__ail_tls_ctx` is NULL → they land on
+`g_rc_free_count` (the atexit fallback line), NOT on `ctx`. There is
+no public runtime API (`ailang_ctx_enter`/`set`/`bind`) for the C
+host to publish a ctx to TLS around its own decs (`__thread
+ailang_ctx_t *__ail_tls_ctx` is runtime-internal; the only writer is
+the codegen-emitted forwarder, by M2 design). Empirical readback
+(`AILANG_RC_STATS=1`, borrow): ctx line `allocs=1000000 frees=0
+live=1000000`; g_rc atexit line `allocs=1 frees=1000001
+live=-1000000`. Globally leak-free and value-correct (exit 0,
+`assert(n==1000000)` held; `allocs_total=1000001 ==
+frees_total=1000001`, net live=0). The plan's own assertion *message*
+("host freed every input") contradicts its own `stats` *source* (the
+ctx readback, which by construction cannot see host-side frees) — an
+internal contradiction in the plan. This is NOT a production-code bug
+(the spec's substantive invariant — ownership follows the declared
+mode, no leak — holds); it is a plan-assertion-model defect of the
+same class the M2.1 journal records (the swarm.c/-DSHARED_CTX
+spec defect: a plan assertion structurally impossible given the M2
+TLS-ctx mechanism, Boss-adjudicated + spec-amended, NOT
+agent-self-amended). Per the Iron Law ("never push past BLOCKED by
+hand") and memory ("when an iter needs a spec change, the spec is
+wrong — update via brainstorm, not a self-patch"), returned BLOCKED
+rather than silently substituting a global-balance / `live==0`
+assertion (which would be the correct invariant but is a *different*
+assertion than the plan scripts — a Boss/brainstorm adjudication).
+
+**Suggested next step:** Boss adjudicates the spec/plan accounting
+model — likely: amend the spec + Task 5 (and re-check Task 4's
+coincidentally-passing ctx-line assertion) so the proven invariant is
+global leak-freedom (`live==0` across the ctx readback AND the g_rc
+atexit line, or `allocs_total==frees_total` summed) for *both* modes,
+rather than per-line ctx `allocs==frees` (which only holds for `own`
+by the accident that own-decs happen inside the forwarder call). Then
+re-dispatch with `task_range:[5,7]` against the amended plan. Tasks
+1–4 are sound and GREEN; the working tree (including the failing
+Task-5 test as evidence) is left intact per the M2.1 precedent.
+
+## Files touched
+
+Modified:
+- `crates/ailang-check/src/lib.rs` (Task 2: gate predicate + message)
+- `crates/ailang-check/tests/embed_export_gate.rs` (Tasks 1,2)
+- `crates/ailang-codegen/src/lib.rs` (Task 3: llvm_scalar +
+  fn_scalar_sig comment)
+- `crates/ailang-codegen/tests/embed_staticlib_lowering.rs` (Task 3)
+- `examples/embed_export_adt_ret_rejected.ail` (Task 2: re-point)
+
+Created:
+- `crates/ailang-codegen/tests/embed_record_layout_pin.rs` (Task 1)
+- `examples/embed_record_layout_carrier.ail` (Task 1)
+- `examples/embed_export_record_ok.ail` (Task 2)
+- `examples/embed_export_str_field_record_rejected.ail` (Task 2)
+- `examples/embed_export_list_field_record_rejected.ail` (Task 2)
+- `examples/embed_export_multictor_rejected.ail` (Task 2)
+- `examples/embed_backtest_step_record.ail` (Task 3)
+- `examples/embed_backtest_step_record_borrow.ail` (Task 3)
+- `crates/ail/tests/embed/record_roundtrip.c` (Task 4/5)
+- `crates/ail/tests/embed_record_e2e.rs` (Task 4 GREEN +
+  Task 5 RED-evidence)
+
+## Boss adjudication (2026-05-18 — M2.1-precedent class)
+
+The orchestrator's Task-5 BLOCK was correct and well-reasoned, and
+its diagnosis was independently verified by the Boss (not
+agent-trusted): built+ran both E2E modes by hand, full
+`AILANG_RC_STATS` stderr —
+
+- own:    ctx `allocs=1000000 frees=1000000 live=0`; g_rc `allocs=1 frees=1 live=0`; exit 0
+- borrow: ctx `allocs=1000000 frees=0 live=1000000`; g_rc `allocs=1 frees=1000001 live=-1000000`; exit 0
+
+Both modes are **globally** leak-free (Σallocs = Σfrees = 1,000,001,
+Σ`live` = 0) and value-correct. The defect is purely the spec's
+proof *instrument*: §"Testing strategy" items 3/4 + §"Coherent stop"
+asserted the single `ailang_ctx_free` ctx readback shows
+`allocs == frees`, which is false **by M2's shipped TLS-ctx design**
+(ctx bound to `__ail_tls_ctx` only for the synchronous forwarder
+call; the host's `make_state`/`dec` run outside it → `g_rc_*`). The
+roadmap's own coherent-stop wording is "a record in/out with
+**alloc==free** across many calls" = *global*, exactly what holds.
+
+Adjudicated as a **Boss spec-consistency repair, not a brainstorm
+bounce** — M2.1-precedent class (genuine spec defect; deliverable +
+substantive invariant sound; only verification mechanics
+mis-specified; first BLOCKED task in M3, not 2+-in-a-family). The
+repair, folded into this partial (M2.1 `c9a84b3` shape):
+
+1. Spec amended (dated repair note + §"Testing strategy" 3/4 +
+   §"Coherent stop"): proof model → **global leak-freedom**
+   (Σallocs == Σfrees across *all* `ailang_rc_stats:` lines,
+   Σ`live` = 0, exit 0) for both modes; the M2-TLS cross-attribution
+   documented as correct behaviour, not a leak. Strictly stronger
+   and honest. No fresh grounding-check (removes an over-strong
+   measurement assumption, adds none about compiler behaviour).
+2. Plan amended (Task 4/5 + the harness step): the harness sums
+   *every* `ailang_rc_stats:` line, not just the first.
+3. Code repair applied (mechanical, decided-invariant): the
+   `build_link_run_embed` parse now sums all stat lines; T4/T5
+   docstrings + assertion messages corrected to the global model.
+   Verified GREEN by the Boss: `embed_record_e2e` 2/2 (own+borrow),
+   gate 10/10, byte-pin 1/1, forwarder 3/3; regression-green set
+   (`embed_e2e`, `embed_staticlib_cli`, `embed_export_hash_stable`,
+   `design_schema_drift`, `docs_honesty_pin`) unmodified-green.
+
+Plan-pseudo-code defects the orchestrator self-corrected inline
+(`feedback_plan_pseudo_vs_reality` class — `(app Ctor …)` →
+`(term-ctor …)` construction, library-`print` non-resolution,
+module==file-stem) are noted in Concerns; a planner Step-5 scrub
+item is warranted (recorded by the Boss outside this journal).
+
+audit owns the bench + architect milestone-close (spec Testing
+items 8/9). This run asserts only the test-suite GREEN state.
+
+## Stats
+
+bench/orchestrator-stats/2026-05-18-iter-embedding-abi-m3.1.json

docs/plans/embedding-abi-m3.1.md

@@ -688,8 +688,22 @@ Build `libbacktest.a` + `libailang_rt.a` from
 `embed_backtest_step_record.ail`, link a C host that constructs the
 input `State` via `ailang_rc_alloc`, calls `backtest_step` N times
 (kernel consumes each `own` input), frees the final return via
-`ailang_rc_dec`, and asserts `ailang_ctx_free`'s `AILANG_RC_STATS`
+`ailang_rc_dec`, and asserts **global leak-freedom** — Σallocs ==
-readback shows `allocs == frees` and the value is correct.
+Σfrees summed across *every* `ailang_rc_stats:` line the run emits
+(the `ailang_ctx_free` ctx readback AND the `g_rc_*` atexit line) —
+plus exit 0.
+
+> **Boss spec-consistency repair (2026-05-18 — M3.1 BLOCKED
+> adjudication, see the spec's repair note).** The original
+> single-ctx-readback `allocs == frees` model is unsatisfiable for
+> borrow (and only coincidentally passes for own): by M2's TLS-ctx
+> design the host's `make_state`/`dec` run outside the forwarder
+> call and land on `g_rc_*`, not ctx. The corrected, stronger
+> invariant is **global**: the harness sums *all* `ailang_rc_stats:`
+> lines; Σallocs == Σfrees (Σ`live` = 0) + exit 0, for both modes.
+> Verified empirically: own ctx `live=0`/g_rc `live=0`; borrow ctx
+> `live=+N`/g_rc `live=−N` (Σ=0) — the split is correct M2-TLS
+> behaviour, not a leak.
 
 **Files:**
 - Create: `crates/ail/tests/embed/record_roundtrip.c`
@@ -747,31 +761,50 @@ int main(void) {
 
 Create `crates/ail/tests/embed_record_e2e.rs`. Open
 `crates/ail/tests/embed_e2e.rs` and **mirror its exact** build/link/
-run helper (the `ail build --emit=staticlib … -o`, the `ar`/`clang`
+run incantation (the `ail build --emit=staticlib … -o`, the `cc`
-link of the C host against `lib<entry>.a` + `libailang_rt.a`, the
+link of the C host against `lib<module>.a` + `libailang_rt.a`, the
-`AILANG_RC_STATS=1` env + stderr `allocs=… frees=…` parse). Add:
+`AILANG_RC_STATS=1` env). **The stats parse must sum ALL
+`ailang_rc_stats:` lines, not just the first** (Boss repair — the
+run emits two: the ctx readback and the `g_rc_*` atexit line; global
+leak-freedom is the invariant). The helper:
 
 ```rust
+#[derive(Debug)]
+struct RcStats { allocs: u64, frees: u64, exit_code: i32 }
+
+fn build_link_run_embed(fixture: &str, host_rel: &str, extra_cc: &[&str]) -> RcStats {
+    // <build --emit=staticlib + cc link + run AILANG_RC_STATS=1,
+    //  mirrored verbatim from embed_e2e.rs's real incantation>
+    // SUM every "ailang_rc_stats:" line (ctx readback + g_rc atexit):
+    let (mut allocs, mut frees) = (0u64, 0u64);
+    for l in stderr.lines().filter(|l| l.starts_with("ailang_rc_stats:")) {
+        for tok in l.split_whitespace() {
+            if let Some(v) = tok.strip_prefix("allocs=") { allocs += v.parse::<u64>().unwrap(); }
+            else if let Some(v) = tok.strip_prefix("frees=") { frees += v.parse::<u64>().unwrap(); }
+        }
+    }
+    RcStats { allocs, frees, exit_code: run.status.code().unwrap_or(-1) }
+}
+
 #[test]
 fn record_roundtrip_own_alloc_eq_free() {
-    // build embed_backtest_step_record.ail --emit=staticlib,
-    // link crates/ail/tests/embed/record_roundtrip.c (no -DBORROW),
-    // run with AILANG_RC_STATS=1, parse the ctx_free readback.
     let stats = build_link_run_embed(
         "embed_backtest_step_record.ail",
         "embed/record_roundtrip.c",
         &[/* no extra clang defines */],
     );
+    // GLOBAL leak-freedom: Σallocs == Σfrees across ctx + g_rc lines.
     assert_eq!(stats.allocs, stats.frees,
-        "own: every State box freed exactly once (kernel-consumed input + host-freed return); {stats:?}");
+        "own: globally leak-free — every State box freed exactly once \
+         (kernel-consumed `own` inputs on ctx; host make_state/final \
+         dec on g_rc); {stats:?}");
     assert_eq!(stats.exit_code, 0, "C host assert(n==1000000) held");
 }
 ```
 
-(The `build_link_run_embed` helper + `stats` struct shape are
+(Mirror `embed_e2e.rs`'s real build/link/run; only the **multi-line
-whatever `embed_e2e.rs` already defines; reuse it — extract it to a
+sum** is the Boss-repair delta over a single-line parse. Do not
-shared `mod` only if `embed_e2e.rs` does not already expose it. Do
+invent a new harness; reuse `embed_e2e.rs`'s incantation verbatim.)
-not invent a new harness.)
 
 - [ ] **Step 3: Run the `own` E2E to verify RED**
 
@@ -790,43 +823,52 @@ ownership contract is mechanically almost free"; ratified by
 `crates/ail/tests/e2e.rs::alloc_rc_own_param_dec_at_fn_return:1855`
 — **not** `borrow_own_demo_modes_are_metadata_only`, which is an
 Iter-18a pre-enforcement pin and must not be cited). No production
-code change is expected in this task — if `record_roundtrip_own_alloc_eq_free`
+code change is expected in this task — if the **global**
-is RED for a real imbalance, that is a genuine bug: hand off to
+Σallocs==Σfrees is RED for a real imbalance, that is a genuine bug:
-`debug` (RED test already exists). If it is GREEN immediately once
+hand off to `debug` (RED test already exists). If it is GREEN once
 Tasks 2+3 are in the tree, that *is* the spec's "mechanically almost
 free" claim substantiated.
 
 Run: `cargo test -p ail --test embed_record_e2e record_roundtrip_own_alloc_eq_free -- --exact`
-Expected: PASS — `allocs == frees`, exit 0.
+Expected: PASS — Σallocs == Σfrees (own: ctx `live=0` + g_rc
+`live=0`; the two stat lines summed), exit 0.
 
 ---
 
 ## Task 5: E2E record round-trip — `borrow`
 
 Same harness, the `-DBORROW` arm: the kernel does **not** consume the
-input; the host retains and `ailang_rc_dec`s it itself. `allocs ==
+input; the host retains and `ailang_rc_dec`s it itself. **Global**
-frees` again. Tasks 4+5 together prove "ownership follows the
+Σallocs == Σfrees again (Boss repair — *not* per-ctx-line: in borrow
-declared mode" in *both* directions.
+the ctx line is `live=+N` and the g_rc line `live=−N`, summing to 0;
+the host's decs land on g_rc because they run outside the forwarder's
+TLS-ctx window — correct M2 behaviour, not a leak). Tasks 4+5
+together prove "ownership follows the declared mode" both directions,
+globally leak-free.
 
 **Files:**
 - Modify: `crates/ail/tests/embed_record_e2e.rs` (add the borrow test)
 
 - [ ] **Step 1: Write the failing `borrow` E2E test (RED)**
 
-In `crates/ail/tests/embed_record_e2e.rs` add:
+In `crates/ail/tests/embed_record_e2e.rs` add (same multi-line-sum
+`build_link_run_embed` as Task 4 — global invariant):
 
 ```rust
 #[test]
 fn record_roundtrip_borrow_alloc_eq_free() {
-    // same C host with -DBORROW: host frees the retained input each
+    // -DBORROW: kernel (borrow param) does NOT consume the input;
-    // iter; kernel (borrow param) does NOT consume it.
+    // host frees the retained input each iter + the final return.
     let stats = build_link_run_embed(
         "embed_backtest_step_record_borrow.ail",
         "embed/record_roundtrip.c",
         &["-DBORROW"],
     );
+    // GLOBAL: ctx allocs (kernel returns) + g_rc frees (host decs)
+    // sum to a balanced total — Σallocs == Σfrees, Σlive == 0.
     assert_eq!(stats.allocs, stats.frees,
-        "borrow: kernel kept input; host freed every input + the return; {stats:?}");
+        "borrow: globally leak-free — kernel allocs returns on ctx, \
+         host frees inputs+return on g_rc; the two summed balance; {stats:?}");
     assert_eq!(stats.exit_code, 0, "C host assert(n==1000000) held");
 }
 ```
@@ -834,19 +876,22 @@ fn record_roundtrip_borrow_alloc_eq_free() {
 - [ ] **Step 2: Run the `borrow` E2E to verify RED then GREEN**
 
 Run: `cargo test -p ail --test embed_record_e2e record_roundtrip_borrow_alloc_eq_free -- --exact --nocapture`
-Expected: FAIL first if the borrow fixture is not yet built/lowered;
+Expected: FAIL first if the borrow fixture is not yet built/lowered
-then PASS once `embed_backtest_step_record_borrow.ail` builds via the
+or the harness still parses only the first stat line; then PASS once
-Task-2/3 path. A `borrow` param is **not** dropped by the kernel
+the multi-line-sum harness is in place and
-(ratified by `crates/ail/tests/e2e.rs::alloc_rc_borrow_only_recursive_list_drop:1671`),
+`embed_backtest_step_record_borrow.ail` builds via the Task-2/3
-so the host's per-iter `ailang_rc_dec(st)` is exactly what balances
+path. A `borrow` param is **not** dropped by the kernel (ratified by
-`allocs == frees`. A real imbalance ⇒ genuine bug ⇒ hand to `debug`.
+`crates/ail/tests/e2e.rs::alloc_rc_borrow_only_recursive_list_drop:1671`);
+the host's per-iter `ailang_rc_dec(st)` on g_rc is what balances the
+**global** total. A real *global* imbalance ⇒ genuine bug ⇒ `debug`.
 
 - [ ] **Step 3: Both modes green together**
 
 Run: `cargo test -p ail --test embed_record_e2e`
 Expected: PASS, `2 passed` — `record_roundtrip_own_alloc_eq_free`
-and `record_roundtrip_borrow_alloc_eq_free`. The frozen ownership
+and `record_roundtrip_borrow_alloc_eq_free`, both at global
-contract is **proven both ways**, not asserted.
+Σallocs==Σfrees. The frozen ownership contract is **proven both
+ways**, not asserted.
 
 ---
 

docs/specs/2026-05-18-embedding-abi-m3.md

@@ -4,6 +4,31 @@
 **Status:** Draft — awaiting user spec review
 **Authors:** Brummel (orchestrator) + Claude
 
+> **Boss spec-consistency repair (2026-05-18, M3.1 implement
+> BLOCKED adjudication — M2.1-precedent class).** The M3.1 implement
+> dispatch correctly BLOCKED on Task 5: the original §"Testing
+> strategy" items 3/4 + §"Coherent stop" specified the proof
+> instrument as "`ailang_ctx_free` reports `allocs == frees`",
+> assuming the single ctx readback observes every RC op. That
+> assumption is false **by M2's shipped design**: the ctx is bound
+> to `__ail_tls_ctx` only for the duration of the synchronous
+> forwarder call, so host-side `ailang_rc_dec` calls (which
+> `borrow` mode legitimately requires every iteration, and `own`
+> mode uses for the initial `make_state` + final return) are
+> attributed to the `g_rc_*` atexit line, not the ctx line. The
+> substantive invariant is sound and was empirically confirmed
+> globally leak-free + value-correct for **both** modes (own: ctx
+> `live=0` + g_rc `live=0`; borrow: ctx `live=+N` + g_rc
+> `live=−N`; both Σ`live`=0, exit 0). The proof model below is
+> corrected to **global leak-freedom** (sum across *all*
+> `ailang_rc_stats:` lines: Σallocs == Σfrees, equivalently
+> Σ`live`=0, plus exit 0), for both modes — strictly stronger and
+> honest about the M2-TLS cross-attribution (which is correct
+> behaviour, not a leak). Spec-consistency repair, not a redesign:
+> what M3 delivers is unchanged; no fresh grounding-check (this
+> *removes* an over-strong measurement assumption and adds no new
+> assumption about current compiler/checker/codegen behaviour).
+
 ## Goal
 
 Let a single-constructor record of `Int`/`Float` fields cross the
@@ -523,15 +548,27 @@ RED-first throughout (`skills/debug` / TDD discipline).
    `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`
+   `ailang_rc_dec`. **Global leak-freedom proof model:** the
-   (via the M2 per-ctx counters — the existing instrument). Result
+   harness parses *every* `ailang_rc_stats:` line the run emits
-   value asserted (`n == N`).
+   (the `ailang_ctx_free` ctx readback **and** the `g_rc_*` atexit
+   line) and asserts `Σallocs == Σfrees` (equivalently Σ`live` = 0)
+   and `exit_code == 0` (the C host's `assert(n == N)` held). Per-
+   ctx-line balance is **not** asserted: by M2's TLS-ctx design the
+   host's `make_state`/final-`dec` run outside the forwarder call
+   and land on `g_rc_*`, so only the *global* sum is the invariant.
 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
+   not consume it (correct `borrow`, ratified by
-   "ownership follows the declared mode" in **both** directions —
+   `e2e.rs::alloc_rc_borrow_only_recursive_list_drop`). Same
-   the frozen contract is tested, not asserted.
+   **global** proof model as item 3 — Σallocs == Σfrees, exit 0.
+   In borrow mode the kernel allocs every return box on ctx while
+   the host's balancing decs land on `g_rc_*` (the ctx line shows
+   `live=+N`, the g_rc line `live=−N`, summing to 0): this split
+   attribution is **correct M2-TLS-window behaviour, not a leak**.
+   Items 3+4 together prove "ownership follows the declared mode"
+   in **both** directions, globally leak-free — 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
@@ -604,11 +641,14 @@ 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
+  `ailang_rc_dec`s the return, and the run is **globally
-  `allocs == frees` (`own` variant — coherent-stop proof).
+  leak-free** — Σallocs == Σfrees across every `ailang_rc_stats:`
+  line (Σ`live` = 0), exit 0 (`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
+  host-retained input freed by the host) is likewise globally
-  `allocs == frees` — "follows the declared mode" proven both ways.
+  leak-free (Σallocs == Σfrees, exit 0; ctx `live=+N` / g_rc
+  `live=−N` summing to 0 — correct M2-TLS cross-attribution, not a
+  leak) — "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`

examples/embed_backtest_step_record.ail

@@ -0,0 +1,16 @@
+(module embed_backtest_step_record
+
+  (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)
+          (term-ctor State State (app + acc sample) (app + n 1)))))))

examples/embed_backtest_step_record_borrow.ail

@@ -0,0 +1,16 @@
+(module embed_backtest_step_record_borrow
+
+  (data State
+    (ctor State (con Float) (con Int)))
+
+  (fn step
+    (export "backtest_step")
+    (type
+      (fn-type
+        (params (borrow (con State)) (con Float))
+        (ret (con State))))
+    (params st sample)
+    (body
+      (match st
+        (case (pat-ctor State acc n)
+          (term-ctor State State (app + acc sample) (app + n 1)))))))

examples/embed_export_adt_ret_rejected.ail

@@ -1,11 +1,12 @@
 (module embed_export_adt_ret_rejected
-  (data Pair
+  (data Reading
-    (ctor Pair (con Int) (con Int)))
+    (ctor Missing)
+    (ctor Sample (con Int) (con Str)))
   (fn f
     (export "f")
     (type
       (fn-type
         (params (con Int))
-        (ret (con Pair))))
+        (ret (con Reading))))
     (params n)
-    (body (app Pair n n))))
+    (body (term-ctor Reading Sample n "tick"))))

examples/embed_export_list_field_record_rejected.ail

@@ -0,0 +1,11 @@
+(module embed_export_list_field_record_rejected
+  (data List
+    (ctor Nil)
+    (ctor Cons (con Int) (con List)))
+  (data Boxed
+    (ctor Boxed (con Int) (con List)))
+  (fn f
+    (export "f")
+    (type (fn-type (params (con Int)) (ret (con Boxed))))
+    (params n)
+    (body (term-ctor Boxed Boxed n (term-ctor List Nil)))))

examples/embed_export_multictor_rejected.ail

@@ -0,0 +1,9 @@
+(module embed_export_multictor_rejected
+  (data Either2
+    (ctor L (con Int))
+    (ctor R (con Float)))
+  (fn f
+    (export "f")
+    (type (fn-type (params (con Int)) (ret (con Either2))))
+    (params n)
+    (body (term-ctor Either2 L n))))

examples/embed_export_record_ok.ail

@@ -0,0 +1,14 @@
+(module embed_export_record_ok
+  (data State
+    (ctor State (con Float) (con Int)))
+  (fn step
+    (export "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)
+          (term-ctor State State (app + acc sample) (app + n 1)))))))

examples/embed_export_str_field_record_rejected.ail

@@ -0,0 +1,8 @@
+(module embed_export_str_field_record_rejected
+  (data Tagged
+    (ctor Tagged (con Int) (con Str)))
+  (fn f
+    (export "f")
+    (type (fn-type (params (con Int)) (ret (con Tagged))))
+    (params n)
+    (body (term-ctor Tagged Tagged n "x"))))

examples/embed_record_layout_carrier.ail

@@ -0,0 +1,30 @@
+(module embed_record_layout_carrier
+
+  (data Pt
+    (ctor Pt (con Int) (con Int)))
+
+  (fn mk
+    (type
+      (fn-type
+        (params (con Int) (con Int))
+        (ret (con Pt))))
+    (params a b)
+    (body (term-ctor Pt Pt a b)))
+
+  (fn sum_pt
+    (type
+      (fn-type
+        (params (own (con Pt)))
+        (ret (con Int))))
+    (params p)
+    (body
+      (match p
+        (case (pat-ctor Pt x y)
+          (app + x y)))))
+
+  (fn main
+    (type (fn-type (params) (ret (con Unit)) (effects IO)))
+    (params)
+    (body
+      (let s (app int_to_str (app sum_pt (app mk 3 4)))
+        (do io/print_str s)))))