# iter embedding-abi-m3.1 — freeze the value layout + record across the C ABI

**Date:** 2026-05-18
**Started from:** 15ee3c5c8fbb871a9cde6cc7d57c0801bae9ae85
**Status:** DONE (Tasks 1–5 GREEN after the Boss spec-consistency
repair below; Tasks 6–7 completed GREEN in the re-dispatch)
**Tasks completed:** 7 of 7 (Tasks 1–4 DONE/GREEN by the orchestrator;
Task 5 correctly BLOCKED on a genuine spec-defect, M2.1-precedent
class, resolved GREEN by the Boss spec-consistency repair —
global-leak-freedom proof model; Tasks 6–7 DONE/GREEN in the
`task_range:[6,7]` re-dispatch on the amended plan)

## Summary

> **Boss note (read first):** the paragraphs below are the
> orchestrator's *first-dispatch* account (present-tense as written
> then) — Task 5's BLOCK was real and is preserved for its
> documentary value. It was resolved by the Boss spec-consistency
> repair and Tasks 6–7 completed in the re-dispatch; the iter is
> **DONE 7/7**. See "## Boss adjudication" and "## Re-dispatch" for
> the resolution. Do not read the "Task 5 is BLOCKED / Task 7 not
> reached" sentences below as the final state.

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 in the first dispatch
  (Task 5 was a hard predecessor in the plan's sequencing; `skip task
  K, continue` is intentionally not a mode). Completed GREEN in the
  `task_range:[6,7]` re-dispatch — see the Re-dispatch section below.

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

## Re-dispatch (2026-05-18 — `task_range:[6,7]`, Tasks 6–7 GREEN)

Re-dispatched from HEAD `d5c565d` (the committed PARTIAL 5/7 + Boss
spec-defect repair). Tasks 1–5 NOT re-implemented or re-verified.

- iter embedding-abi-m3.1.6 (DONE): the substantive freeze.
  DESIGN.md §"Embedding ABI" — both "provisional until M3" sentences
  rewritten to one-way-freeze wording (`:2280-2282` → embedding ABI
  accepts `Int`/`Float`/single-ctor record + "**Frozen as of M3**";
  `:2293-2295` → "**frozen as of M3** (see "Frozen value layout"
  below)") and the new `### Frozen value layout (M3 — one-way
  commitment)` SSOT subsection inserted before `## Data model` (byte
  table `p-8` header / `p+0` tag / `p+8+i*8` fields, size `8+n*8`,
  construction/ownership/free contract). Lockstep `// FROZEN ABI`
  pointers added at the three independent encoders: `runtime/rc.c`
  layout comment block, `match_lower.rs` `lower_ctor` `:107` size
  site, `drop.rs` `:88` tag-load + `:113` field-offset. Three stale
  rustdocs corrected — the two plan-named (`codegen/lib.rs:178`,
  `ailang-core/ast.rs:211`) PLUS the Concerns carry-forward
  `ailang-check/lib.rs:448-450` ("scalar-only…every ADT rejected" →
  frozen-as-of-M3, Boss constraint 2). docs_honesty_pin GREEN
  baseline AND after the rewrite (5/5 both); the pinned line
  ("Export parameters are written **bare**…") shifted `:2297`→`:2299`
  but stays byte-verbatim+contiguous — the pin asserts content not
  line, so pin-safe (planner Step-5 item-6 family honoured). Step-7
  enforceability: perturbed `match_lower.rs` `size_bytes` `8`→`16`
  (the unanchored sed-class literal hit both `:107` and `:400`; both
  feed the byte-pin through `lower_ctor`'s heap path), byte-pin went
  RED (`0 passed; 1 failed`, IR emitted `i64 32` not `i64 24`),
  restored via `git checkout -- crates/ailang-codegen/src/match_lower.rs`
  (working-tree restore only — main HEAD untouched; the single
  legitimate git history-touching op of the run), byte-pin GREEN
  again (1/1). The freeze is proven enforceable, not aspirational.
- iter embedding-abi-m3.1.7 (DONE): milestone-close verification
  gate (no code change). Regression-green-unmodified set GREEN
  (`embed_e2e` 1, `embed_rc_accounting_tsan` 2, `embed_swarm_tsan`
  1, `embed_staticlib_cli` 2, `embed_staticlib_alloc_guard` 2,
  `print_no_leak_pin` 1; `design_schema_drift` 8/8;
  `embed_export_hash_stable` 1/1). Full workspace **639 passed, 0
  failed**, zero compile errors; M3 net-new present + GREEN
  (`embed_record_layout_pin` 1, `embed_export_gate` 10 = orig 6 + 4,
  `embed_staticlib_lowering` 3 = orig 2 + 1, `embed_record_e2e` 2),
  nothing pre-existing removed/weakened. `round_trip` 2/2 (new
  `.ail` fixtures round-trip; no Form-A surface added).

## Concerns (re-dispatch addendum)

- iter embedding-abi-m3.1.7: PLAN TRANSCRIPTION DEFECT (class:
  "plan pseudo-code vs reality" — same family as the iter's existing
  `(app Ctor)`→`(term-ctor)` / module==file-stem Concerns). Plan
  Task-7 Step 1 names `cargo test -p ailang-check --test
  embed_export_hash_stable`, but that test target lives in
  **`ailang-core`** (`crates/ailang-core/tests/embed_export_hash_
  stable.rs`), not `ailang-check`. The substantive requirement
  ("no schema field added; hashes/drift byte-unchanged") is
  unaffected — ran the pin in its actual crate, 1/1 GREEN. Crate
  name corrected at execution; observation not correctness. The
  recon "named this exact set" claim was wrong for this one target
  (recurring `feedback_grounding_check_misses_insource_tests` /
  `feedback_plan_pseudo_vs_reality` family — a planner Step-5 scrub
  item, recorded here for Boss visibility).
- iter embedding-abi-m3.1.6: the plan places the Step-5 match_lower.rs
  `// FROZEN ABI` comment edit and the Step-7 `git checkout --
  match_lower.rs` enforceability restore in the SAME task on the SAME
  file. The checkout necessarily reverts the uncommitted Step-5
  comment along with the perturbation (it restores to HEAD `d5c565d`,
  where neither exists). Re-applied the Step-5 comment after the
  enforceability demo so Step 5 stays satisfied — this is a plan
  step-ordering wrinkle, not a defect: the freeze demo MUST run on a
  tree where the only delta is the perturbation, and the comment is
  re-addable post-demo. Recorded for planner-scrub awareness.

## Known debt (re-dispatch addendum)

- `llvm_scalar` identifier still slightly narrower than its post-M3
  behaviour (carried from the first dispatch's Concerns) — out of
  scope for Tasks 6/7; the doc-comment disambiguates. Unchanged.
- Bench + architect milestone-close (spec Testing items 8/9) remain
  the `audit` skill's job — NOT this implement run, as the original
  account and Boss adjudication both record. audit is the next
  pipeline step.

## Files touched (re-dispatch addendum — Tasks 6–7)

Modified (Task 6; all uncommitted in the working tree):
- `docs/DESIGN.md` (two "provisional until M3" rewrites + the new
  "### Frozen value layout" SSOT subsection)
- `runtime/rc.c` (lockstep `// FROZEN ABI` comment in the layout
  block)
- `crates/ailang-codegen/src/match_lower.rs` (`lower_ctor` `:107`
  lockstep comment)
- `crates/ailang-codegen/src/drop.rs` (`:88` tag-load + `:113`
  field-offset lockstep comments)
- `crates/ailang-codegen/src/lib.rs` (`Target::StaticLib` rustdoc
  "provisional until M3" → frozen)
- `crates/ailang-core/src/ast.rs` (`FnDef.export` rustdoc
  "provisional until M3" → frozen)
- `crates/ailang-check/src/lib.rs` (`ExportNonScalarSignature`
  rustdoc "scalar-only…every ADT rejected" → frozen — Concerns
  carry-forward)

Task 7: verification only, no files.

## Stats

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