spec: embedding-abi-m2 — per-thread runtime context + concurrency safety (user-approved, grounding-check PASS 9/9); open in-flight [~]

docs/roadmap.md

@@ -218,7 +218,7 @@ work progresses.
     finding [spec_gap]#2;
     `docs/journals/2026-05-18-iter-emit-ir-staticlib.md`.
 
-- [ ] **\[milestone\]** Embedding ABI — M2: per-thread runtime
+- [~] **\[milestone\]** Embedding ABI — M2: per-thread runtime
   context + concurrency safety. `ailang_ctx_new()/_free` threaded
   through every call; neutralise the two process-global hazards
   the runtime read surfaced — the non-atomic
@@ -236,6 +236,14 @@ work progresses.
   - depends on: Embedding ABI — M1.
   - context: 2026-05-18 chat; runtime hazard read
     (`runtime/rc.c` global stats + `atexit`).
+    Spec'd + user-approved 2026-05-18 (grounding-check PASS 9/9):
+    `docs/specs/2026-05-18-embedding-abi-m2.md` — ctx as mandatory
+    explicit C-ABI param (TLS-forwarder, internal conv + `_adapter`/
+    `_clos` byte-untouched); ctx near-empty by discipline
+    (`{alloc,free}_count` only); hazards neutralised in the swarm
+    artefact, `g_rc_*`+atexit retained as the null-ctx executable
+    fallback; staticlib RC-only enforced; no schema/surface change.
+    Plan next.
 
 - [ ] **\[milestone\]** Embedding ABI — M3: frozen value layout +
   single ADT/record crossing + RC ownership contract. Host

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

@@ -0,0 +1,511 @@
+# Embedding ABI — M2: per-thread runtime context + concurrency safety — Design Spec
+
+**Date:** 2026-05-18
+**Status:** Draft — awaiting user spec review
+**Authors:** Brummel (orchestrator) + Claude
+
+## Goal
+
+Make a compiled AILang scalar kernel callable concurrently from a
+host thread swarm without a data race in the RC runtime. M1 made one
+scalar `fn` callable from a single C/Rust caller
+(`@<sym>(scalars…)`, two-archive `lib<entry>.a` + `libailang_rt.a`).
+M1's DESIGN.md section explicitly forecast this milestone: *"the
+per-thread context parameter that M2 threads through every exported
+call will change this C signature; do not treat the M1 signature as
+frozen."* M2 delivers exactly that parameter and removes the two
+process-global hazards the M1 runtime read surfaced.
+
+M2 has **no new authoring surface**: still scalar-only (`Int`/`Float`,
+effect-free, enforced by the unchanged M1 `export-non-scalar-signature`
+/ `export-has-effects` gate), IO-at-the-boundary explicitly deferred,
+**no** new Form-A modifier, **no** new schema field, **no** new
+checker diagnostic. The `.ail` an LLM author writes is byte-identical
+to M1's kernel. The entire deliverable is a *swarm-safe generated C
+ABI + a de-globalised runtime*, proven by a sanitiser harness — not
+by typecheck. This is the M1-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:** N host threads, each owning its own
+`ailang_ctx_t`, each driving the scalar kernel in a `while
+let next_chunk`-shaped loop, run `-fsanitize=thread`-clean with every
+thread's result matching the serial oracle — *and* a deliberately
+ctx-sharing negative control that tsan correctly flags (the harness
+has teeth), *and* `--emit=staticlib --alloc=gc` failing to build.
+
+### Position in the M1–M5 arc (load-bearing)
+
+The arc is a one-way stability progression; M3 freezes the value/ABI
+layout as a one-way commitment and M5's `ail-embed` adapter binds the
+frozen ABI. Two consequences shape M2:
+
+- The frozen C ABI surface at M3 is the **`@<sym>(ailang_ctx_t*,
+  scalars…)` signature**. M2 must put `ctx` into that signature now,
+  as a mandatory first parameter, so M3 freezes the correct shape. A
+  later "add ctx" would make the M3 freeze a lie.
+- M1 *deliberately decoupled* the author-chosen C symbol from the
+  internal `ail_<module>_<def>` mangling, precisely so the internal
+  calling convention can keep changing while the C ABI is frozen.
+  M2 exploits this: the ctx enters at the C `@<sym>` forwarder only;
+  the internal convention and the `_adapter`/`_clos` closure pair
+  stay **byte-unchanged** (the M1 "orthogonal, left untouched"
+  decision is preserved, and M3's allocation work remains free to
+  alter the internal convention without touching the frozen ABI).
+
+## Architecture
+
+Three layers change: the runtime (`runtime/rc.c`), codegen
+(`crates/ailang-codegen` `Target::StaticLib` forwarder only), and the
+CLI (`crates/ail` `build_staticlib`). No `ailang-core` schema change,
+no `ailang-check` change, no surface change. None of `ailang-core`,
+`ailang-codegen`, or `runtime/` gains any `data-server`/finance
+knowledge or dependency (Invariant 1; audited at close).
+
+### Host concurrency model (settled constraint, not an open fork)
+
+The only stated consumer is `data-server`'s *"`while let next_chunk`
+loop … over a thread swarm"*. `data-server` is external (Invariant 1
+keeps it out of this tree) and not readable; the phrasing is a
+**synchronous blocking pull loop** run per OS worker thread —
+*pinned-thread swarm*: each worker thread creates its own ctx, uses
+it for the thread's lifetime, frees it; the ctx never migrates
+between threads. A cross-thread-tolerant (work-stealing/async) model
+has **no consumer** and was rejected: it would force ctx through the
+M1-protected internal convention for robustness no consumer needs —
+the build-ahead-of-consumer iteration-discipline trap.
+
+**Why TLS transport is sound even under a work-stealing host.** The
+generated kernel is a synchronous native C symbol; there is *no*
+asynchronous entry into it. `ctx` is a **mandatory explicit
+parameter on every call** (the frozen-ABI shape) — never a
+"set-once, call-bare" session. The forwarder writes the TLS slot
+from that explicit parameter at the top of *each* call and
+save/restores it around the synchronous internal call. The TLS-live
+window is therefore strictly inside one synchronous call, which
+contains no suspension point (the worker thread runs the C call to
+completion before polling any other future). The unsound design —
+ctx held in TLS *across* an `.await` — is structurally impossible
+here because ctx is re-derived from the explicit parameter on every
+call and never stored across a call boundary. This holds for a
+pinned-thread swarm *and* a tokio-style work-stealing host; M2
+targets the former because that is the only consumer.
+
+### The two hazards and how M2 neutralises them where they exist
+
+`runtime/rc.c` has exactly two pieces of process-global mutable
+state a kernel's runtime can touch:
+
+1. `g_rc_alloc_count` / `g_rc_free_count` (`rc.c:86–87`),
+   incremented in `ailang_rc_alloc` (`:125`) and the to-zero branch
+   of `ailang_rc_dec` (`:175`).
+2. The `atexit(ailang_rc_stats_atexit)` hook installed by the
+   `__attribute__((constructor)) ailang_rc_stats_install`
+   (`rc.c:89–103`), gated on `AILANG_RC_STATS`.
+
+A hazard is contextual: a process-global counter is only a hazard
+when *concurrently* mutated. M2 makes the **swarm path never touch
+either**: every swarm thread has a ctx, so accounting flows into
+`ctx->{alloc,free}_count` and the stats readback fires at
+`ailang_ctx_free`. The globals + `atexit` are **retained as the
+null-ctx fallback** for the single-threaded default executable path
+(`ail build` without `--emit=staticlib`, no ctx, `__ail_tls_ctx ==
+NULL`), where they are *not* a hazard (single-threaded) and where two
+green tests depend on them (`crates/ail/tests/print_no_leak_pin.rs`,
+`crates/ail/tests/e2e.rs:2178` leak-stat helper). M2 thus neutralises
+the hazards *in the swarm artefact* (zero shared mutable RC state,
+proven tsan-clean) without a behaviour change on the executable
+path. The roadmap's "neutralise the two process-global hazards" is
+satisfied for the context the hazard exists in; deleting the globals
+outright (and breaking the two executable-path leak tests) is
+explicitly *not* the design.
+
+### What `ailang_ctx_t` contains — near-empty by discipline
+
+A scalar `(Int,Int)->Int` kernel allocates nothing — it never calls
+`ailang_rc_alloc`/`ailang_rc_dec`. So the M2 ctx carries only the
+de-globalised accounting:
+
+```c
+typedef struct ailang_ctx {
+    uint64_t alloc_count;   /* per-instance; replaces g_rc_alloc_count */
+    uint64_t free_count;    /* per-instance; replaces g_rc_free_count  */
+} ailang_ctx_t;
+```
+
+Explicitly **not** in the M2 ctx (build-ahead-of-consumer trap, the
+documented project failure mode): no per-thread arena/bump allocator
+(scalar kernels do not allocate; "toward pure per-thread RC" /
+"aligns with the *standing* P2 Boehm-retirement todo" is direction,
+not delivery), no locks, no atomics (each thread owns its ctx ⇒ the
+counters need neither — Decision 10's "single-threaded; non-atomic
+refcounts" stays correct because post-M3 each thread's allocations
+are private to its ctx, no cell crosses a thread), no IO sink /
+effect handler (IO deferred). The ctx is intentionally a near-empty
+mandatory handle whose M2 job is twofold: carry the de-globalised
+accounting, and establish the mandatory-parameter ABI shape M3
+freezes and M3/M4's real allocation hangs off.
+
+### Allocator scope — staticlib is RC-only, enforced
+
+The `--alloc` flag default is already `rc` (`main.rs:146/167`); M2
+changes no default. M2 adds a **reject guard**: `--emit=staticlib`
+combined with `--alloc=gc` or `--alloc=bump` fails the build with a
+diagnostic. The Boehm collector (a process-global shared collector
+with its own threads) is thereby never linkable into a swarm
+artefact *by construction* — the roadmap's "no shared Boehm
+collector". Full tree-wide Boehm retirement stays the separate
+standing P2 todo, untouched.
+
+## Concrete code shapes
+
+### The AILang program M2 delivers (headline — clause-1 evidence)
+
+**Byte-identical to M1.** `examples/embed_backtest_step.ail`,
+unchanged:
+
+```
+(module backtest
+
+  (fn step
+    (export "backtest_step")
+    (type
+      (fn-type
+        (params (con Int) (con Int))
+        (ret (con Int))))
+    (params state sample)
+    (body
+      (app + state (app * sample sample)))))
+```
+
+That the worked author code is *unchanged* **is** the clause-1
+evidence: M2 changes nothing the LLM author writes. Concurrency
+safety is delivered as an ABI/runtime property, not an authoring
+burden — which is precisely the point of the milestone.
+
+### The changed C host (the actual M2 deliverable surface)
+
+```c
+#include <stdint.h>
+#include <assert.h>
+#include <pthread.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 int64_t backtest_step(ailang_ctx_t *ctx, int64_t state, int64_t sample);
+
+static void *worker(void *_arg) {
+    ailang_ctx_t *ctx = ailang_ctx_new();      /* per-thread, owned for the thread's life */
+    int64_t s = 0;
+    for (int i = 0; i < 1000000; i++)
+        s = backtest_step(ctx, s, (i & 7));     /* synchronous; ctx is a mandatory param */
+    ailang_ctx_free(ctx);                       /* per-ctx leak readback fires here */
+    return (void *)(intptr_t)s;
+}
+/* N pthreads run worker(); join; assert each thread's s == serial oracle.
+ * Built with -fsanitize=thread → zero reports == the coherent stop. */
+```
+
+### The must-fail axis (clause-3 discriminator — build layer, honestly not typecheck)
+
+M2 adds no typecheck rejection (no surface change). Its discriminator
+is at the build/runtime layer, and there are two teeth:
+
+1. **Unsafe build config fails to build** — the M2 analogue of M1's
+   `export-non-scalar-signature`:
+
+   ```
+   $ ail build --emit=staticlib --alloc=gc examples/embed_backtest_step.ail -o /tmp/x
+   Error: staticlib (swarm) artefact is RC-only — `--alloc=gc` links the
+   shared Boehm collector, which is not swarm-safe; use `--alloc=rc`
+   ```
+
+   (Same wording shape for `--alloc=bump`.) RED today (`build_staticlib`
+   passes the strategy through and succeeds); GREEN after the guard.
+
+2. **Negative control proves the harness has teeth** — a harness
+   variant where all N threads share one `ailang_ctx_t*` must make
+   tsan report a race on `ctx->alloc_count` (the analogue of M1's
+   must-fail fixture: a test that the safety mechanism is real, not
+   vacuous).
+
+### Implementation shape (secondary — supporting, not the point)
+
+Runtime (`runtime/rc.c`) — the TLS var, ctx struct, and lifecycle
+live in the runtime (codegen only *references* the external
+thread-local symbol):
+
+```c
+/* runtime/rc.c — replaces the g_rc_* statics' role for the ctx path;
+ * the statics + atexit stay as the null-ctx (executable) fallback. */
+typedef struct ailang_ctx { uint64_t alloc_count, free_count; } ailang_ctx_t;
+__thread ailang_ctx_t *__ail_tls_ctx = NULL;   /* set by the forwarder, per call */
+
+ailang_ctx_t *ailang_ctx_new(void)  { return calloc(1, sizeof(ailang_ctx_t)); }
+void ailang_ctx_free(ailang_ctx_t *c) {
+    const char *f = getenv("AILANG_RC_STATS");
+    if (c && f && f[0])
+        fprintf(stderr, "ailang_rc_stats: allocs=%llu frees=%llu live=%lld\n",
+                (unsigned long long)c->alloc_count,
+                (unsigned long long)c->free_count,
+                (long long)(c->alloc_count - c->free_count));
+    free(c);
+}
+/* ailang_rc_alloc: was  g_rc_alloc_count++;  now: */
+/*   ailang_ctx_t *c = __ail_tls_ctx; if (c) c->alloc_count++; else g_rc_alloc_count++; */
+/* ailang_rc_dec (to-zero): symmetric for free_count.                                   */
+/* g_rc_* statics + ailang_rc_stats_atexit + the constructor: retained verbatim,        */
+/* now the null-ctx (single-threaded executable) fallback only.                         */
+```
+
+Codegen (`crates/ailang-codegen/src/lib.rs`, `Target::StaticLib`
+arm, `:600`) — forwarder gains a leading `ptr %ctx`, save/restores
+the external thread-local around the *unchanged* internal call:
+
+```text
+declared once in the staticlib module:
+  @__ail_tls_ctx = external thread_local global ptr
+
+before (M1, per (export "backtest_step") fn):
+  define i64 @backtest_step(i64 %a0, i64 %a1) {
+    %r = call i64 @ail_backtest_step(i64 %a0, i64 %a1)
+    ret i64 %r }
+
+after (M2):
+  define i64 @backtest_step(ptr %ctx, i64 %a0, i64 %a1) {
+    %saved = load ptr, ptr @__ail_tls_ctx
+    store ptr %ctx, ptr @__ail_tls_ctx
+    %r = call i64 @ail_backtest_step(i64 %a0, i64 %a1)   ; internal conv UNCHANGED
+    store ptr %saved, ptr @__ail_tls_ctx                  ; re-entrancy/nesting-safe
+    ret i64 %r }
+  ; @ail_backtest_step + its _adapter/_clos pair: byte-unchanged (M1 decision held)
+```
+
+(The save/restore is two TLS ops; M2 scalar scope has no nesting, but
+it is the correct forwarder shape and avoids an M3 retrofit of the
+frozen-adjacent forwarder — this is the correct shape of the one
+thing built, not speculative infrastructure.)
+
+CLI (`crates/ail/src/main.rs`, `build_staticlib`, `:2443`):
+
+```text
+before: build_staticlib lowers with whatever AllocStrategy was passed.
+after : if alloc != Rc  → bail!("staticlib (swarm) artefact is RC-only …")
+        (default is already Rc; this rejects an *explicit* gc/bump).
+        rc.c rebuilt into libailang_rt.a as today — the M1 decision
+        "program archive carries no runtime objects, so M2's runtime
+        rebuild touches only libailang_rt.a" pays off: lib<entry>.a
+        is byte-unaffected by the rc.c change.
+```
+
+## Components
+
+| Component | Crate / file | Change |
+|---|---|---|
+| `ailang_ctx_t` + `ailang_ctx_new`/`_free` + `__ail_tls_ctx` | `runtime/rc.c` | new struct + lifecycle + `__thread` slot |
+| `g_rc_*` increment sites | `runtime/rc.c` | `if (ctx) ctx->… else g_rc_…` (null-ctx fallback) |
+| `g_rc_*` statics + `atexit` + constructor | `runtime/rc.c` | **retained**, now null-ctx (executable) path only |
+| `@<sym>` forwarder | `ailang-codegen` `Target::StaticLib` `:600` | leading `ptr %ctx`, TLS save/store/restore; internal call + `_adapter`/`_clos` byte-unchanged |
+| `--emit=staticlib` alloc guard | `crates/ail` `build_staticlib` `:2443` | reject `--alloc=gc`/`bump` |
+| DESIGN.md §"Embedding ABI (M1)" | docs | updated in place to post-M2 current state (ctx mandatory; per-thread RC-only swarm; accounting per ctx; "provisional until M3" narrowed to the value/record layout only) |
+| Decision 10 atomicity clause | docs | one-line note: embedding ABI is per-thread-ctx ⇒ no shared cells ⇒ non-atomic RC stays correct |
+| M1 `embed_e2e.rs` host harness | `crates/ail/tests` | migrated to the ctx ABI (RED→GREEN driver) |
+
+No `design_schema_drift.rs` movement (no schema field). No
+`ailang-check` change, no Form-A change. Only the two tests whose
+*observed behaviour* M2 changes are touched: `embed_staticlib_lowering.rs`
+(forwarder IR gains `ptr %ctx` + TLS save/restore) and `embed_e2e.rs`
+(host call gains the ctx parameter + lifecycle). `embed_export_gate.rs`
+(gate unchanged), `embed_export_hash_stable.rs` (no schema field),
+`design_schema_drift.rs`, `print_no_leak_pin.rs`, and the
+`e2e.rs` leak-stat helper stay green **unmodified** — their behaviour
+is byte-preserved by design.
+
+## Data flow
+
+```
+embed_backtest_step.ail   (unchanged; no schema/surface change)
+  → ail check               (unchanged M1 export gate: scalar + effect-free)
+  → desugar / lift / mono   (unchanged)
+  → lower_workspace_staticlib [--alloc=rc enforced]
+        @backtest_step(ptr %ctx, i64, i64): set TLS, call @ail_backtest_step, restore TLS
+  → backtest.ll → clang -c → backtest.o → ar → libbacktest.a   (byte-unaffected by rc.c)
+  ( rc.c [+ctx +TLS] / str.c → libailang_rt.a )                 [the only rebuilt archive]
+
+host: N pthreads × { ctx=ailang_ctx_new(); loop backtest_step(ctx,…); ailang_ctx_free(ctx) }
+      built -fsanitize=thread  →  0 tsan reports + per-thread result == serial oracle
+runtime accounting: swarm path → ctx->{alloc,free}_count (no global touched, no race)
+                    executable path (null ctx) → g_rc_* + atexit (single-threaded, unchanged)
+```
+
+## Error handling
+
+- **`--emit=staticlib` with `--alloc=gc` or `--alloc=bump`**: CLI
+  error, build fails (RC-only swarm contract). Default `--alloc=rc`
+  unaffected; non-staticlib `--alloc=gc` unaffected.
+- **`ailang_ctx_new` OOM**: `calloc` returns NULL → `ailang_ctx_new`
+  returns NULL; a NULL ctx passed to the forwarder sets
+  `__ail_tls_ctx = NULL`, i.e. the kernel runs on the null-ctx
+  fallback path (no accounting) rather than crashing — matches the
+  existing "abort only on allocation we cannot proceed without"
+  runtime posture; the scalar kernel needs no allocation to run.
+- **`ailang_ctx_free(NULL)`**: no-op then `free(NULL)` (no-op) —
+  symmetric with the `ailang_rc_dec(NULL)` null guard already in the
+  runtime.
+- **Executable path leak readback**: unchanged — `g_rc_*` + the
+  `AILANG_RC_STATS` atexit print still fire exactly as today (the
+  two pinning tests stay green).
+
+## Testing strategy
+
+RED-first throughout. The central honesty point: **a scalar kernel
+allocates nothing, so a scalar swarm is already race-free today** —
+tsan on the scalar swarm alone is *not* a meaningful RED→GREEN for
+the de-globalisation. The de-globalisation regression coverage must
+exercise the RC-accounting path *directly*, at the layer that
+actually has the hazard. Hence two distinct test roles, mirroring
+M1's structure (M1: E2E harness = coherent-stop proof; must-fail
+fixtures = the gate's teeth):
+
+0. **Baseline pins (prerequisite, RED-first), at the layers M2
+   changes.** (a) Pin that the executable-path `AILANG_RC_STATS`
+   atexit readback currently works — already green via
+   `print_no_leak_pin.rs` + `e2e.rs:2178`; M2 must keep them green
+   (regression guard on the retained null-ctx fallback). (b) Pin
+   that `ail build --emit=staticlib --alloc=gc <kernel>` currently
+   *succeeds* (so the new guard's RED→GREEN is real).
+1. **De-globalisation regression — direct rc-accounting, N threads,
+   tsan (the teeth).** A C harness (test tree) spawns N threads,
+   each `ailang_ctx_new()`, each performing many
+   `ailang_rc_alloc`/`ailang_rc_dec` cycles, asserting each ctx's
+   `alloc_count == free_count` individually (no lost/cross-counted
+   increments) under `-fsanitize=thread`. This *cannot be written*
+   against today's `g_rc_*` (no per-ctx counters) and a global-
+   hammering variant is tsan-RED today → GREEN after M2. This is the
+   meaningful proof, because it hits the hazard at its own layer.
+2. **Coherent-stop capability demonstration — scalar swarm.** The
+   headline `examples/embed_backtest_step.ail` driven by N threads
+   each through its own ctx (the §"changed C host" harness), tsan-
+   clean, every thread's result == serial oracle. This proves the
+   *capability* (the headline use case runs swarm-safe through the
+   new ABI end-to-end). Honestly recorded: it is the capability
+   proof, not the de-globalisation proof (which is item 1).
+3. **Negative control.** The ctx-shared variant of the item-2
+   harness must make tsan report a race — proves item 2's clean
+   result is not vacuous.
+4. **Forwarder shape.** `embed_staticlib_lowering.rs` extended:
+   `@<sym>` now `define i64 @sym(ptr %ctx, …)` with the TLS
+   save/store/restore around an *unchanged* `call @ail_<mod>_<fn>`;
+   no `@main`; `_adapter`/`_clos` byte-identical to M1 (regression
+   pin on the M1 "untouched" decision).
+5. **M1 E2E migration.** `embed_e2e.rs` migrated from
+   `backtest_step(state,sample)` to
+   `backtest_step(ctx,state,sample)` with ctx lifecycle; still
+   asserts the M1 value result (the ABI changed, the math did not).
+6. **Executable path unchanged.** `print_no_leak_pin.rs` +
+   `e2e.rs` leak-stat helper green unmodified (null-ctx fallback
+   byte-behaviour preserved).
+7. **Schema/hash invariance.** `embed_export_hash_stable.rs` +
+   `design_schema_drift.rs` green *unmodified* — M2 adds no schema
+   field (explicit contrast with M1).
+8. **Clean-core invariant.** No new dependency in `ailang-core` /
+   `ailang-codegen` / `runtime/`; architect audits Invariant 1 at
+   close.
+9. **Bench regression trio.** The retained null-ctx fallback adds a
+   `load __thread ptr; brif null` ahead of the executable path's
+   `g_rc_*++`. The strategy must demonstrate this is bench-neutral
+   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/safety milestone
+with **no authoring surface**:
+
+1. **LLM author naturally produces it.** Vacuously and *by design*:
+   the worked `.ail` is byte-identical to M1's kernel
+   (`examples/embed_backtest_step.ail`, shown above). M2 introduces
+   no construct for an author to reach for — concurrency safety is
+   an ABI/runtime property. The unchanged `.ail` *is* the clause-1
+   evidence; the changed surface is the C host, shown concretely.
+2. **Measurably improves correctness / removes redundancy.** A
+   safety gate, recorded honestly (as M1's clause 2 was): running an
+   *allocating* kernel from N threads is today a C data race on
+   `g_rc_*` (UB); M2 removes that shared mutable state from the
+   swarm artefact by construction, proven tsan-clean (Testing item
+   1). Justification is strategic — the language's target
+   deployment, the explicit user-made roadmap direction call — not
+   the standard authoring-utility metric. No pretence otherwise.
+3. **Reintroduces no bug class the core eliminates.** Decision 10's
+   "single-threaded; non-atomic refcounts" stays *true*: M2
+   introduces no atomic refcounts and no shared cells (per-thread
+   ctx ⇒ no heap cell crosses a thread; scalar kernels allocate
+   nothing in M2). Invariant 1 (clean core), Invariant 2 (no value
+   crosses a thread boundary — strengthened: the ctx is per-thread
+   by construction), Invariant 3 (native-AOT only) all hold and are
+   audited. The clause-3 discriminator is honestly at the
+   build/runtime layer, not typecheck: the unsafe build config
+   *fails to build* (`--alloc=gc`+staticlib) and the safety property
+   is proven by sanitiser + negative control — stated plainly, with
+   no pretence of an authoring-surface clause-3.
+
+Milestone-close ("coherent stop") is met when **all** hold:
+
+- The §"changed C host" N-thread harness on
+  `examples/embed_backtest_step.ail` is `-fsanitize=thread`-clean
+  and every thread's result matches the serial oracle.
+- The direct rc-accounting N-thread+tsan test (item 1) is green;
+  its global-hammering RED variant and the ctx-shared negative
+  control (item 3) both demonstrate the teeth.
+- `ail build --emit=staticlib --alloc=gc` fails with the RC-only
+  diagnostic; `--alloc=rc` (default) builds and links.
+- `embed_e2e.rs` migrated and green on the ctx ABI; the M1 value
+  result unchanged.
+- Executable path byte-behaviour preserved: `print_no_leak_pin.rs`
+  + `e2e.rs` leak-stat helper green unmodified; no schema/hash
+  movement (`embed_export_hash_stable.rs`,
+  `design_schema_drift.rs` green unmodified).
+- Architect audit confirms Invariant 1; bench trio carry-on
+  (null-ctx fallback proven bench-neutral, not hand-waved).
+- DESIGN.md §"Embedding ABI (M1)" updated to the post-M2 current
+  state (ctx-threaded signature is real; "provisional until M3"
+  narrowed to the value/record layout); Decision 10 atomicity note
+  added.
+
+## Iteration sequencing (prerequisite-first)
+
+The planner decomposes M2 into bite-sized tasks, but **task 1 is
+fixed**: the Testing-strategy item-0 baseline pins (executable-path
+atexit readback currently green; `--emit=staticlib --alloc=gc`
+currently succeeds). Rationale, same shape as M1's fixed task 1: M2
+is *defined* as (a) retaining the executable-path readback while
+diverting the swarm path off it, and (b) flipping the
+`--alloc=gc`+staticlib build outcome from success to failure. Both
+load-bearing changes must rest on a pinned baseline 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
+runtime/codegen/CLI work proceed. No other inter-task ordering is
+mandated; the planner owns the rest.
+
+## Out of scope (explicit)
+
+- Any non-scalar crossing — record/ADT (M3), list (M4), `Str` in/out.
+- Any `ctx` content beyond the two accounting counters — no
+  per-thread arena/bump allocator, no locks, no atomics, no IO sink
+  (build-ahead-of-consumer trap; "toward per-thread RC" is direction
+  not delivery).
+- Tree-wide Boehm retirement — the separate standing P2 todo,
+  untouched; M2 only forbids Boehm in the staticlib artefact.
+- Cross-thread-tolerant (work-stealing/async ctx-migration) ABI —
+  no consumer; rejected as build-ahead.
+- Atomic refcounts — Decision 10 stays; per-thread ctx makes them
+  unnecessary, not deferred.
+- The `ail-embed` adapter crate + `data-server` wiring + the real
+  thread-swarm backtest — M5.
+- Touching the internal `@ail_<module>_<fn>` calling convention or
+  the `_adapter`/`_clos` closure pair (M1 decision held).