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

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`
-   (via the M2 per-ctx counters — the existing instrument). Result
-   value asserted (`n == N`).
+   `ailang_rc_dec`. **Global leak-freedom proof model:** the
+   harness parses *every* `ailang_rc_stats:` line the run emits
+   (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
-   "ownership follows the declared mode" in **both** directions —
-   the frozen contract is tested, not asserted.
+   not consume it (correct `borrow`, ratified by
+   `e2e.rs::alloc_rc_borrow_only_recursive_list_drop`). Same
+   **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
-  `allocs == frees` (`own` variant — coherent-stop proof).
+  `ailang_rc_dec`s the return, and the run is **globally
+  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
-  `allocs == frees` — "follows the declared mode" proven both ways.
+  host-retained input freed by the host) is likewise globally
+  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`