spec: embedding-abi-m1 — linkable artifact + scalar C entrypoint

Brainstorm complete for Embedding ABI M1 (first of the M1–M5 arc).
User-approved 2026-05-18. Grounding-check PASS on 3rd dispatch
(dispatch 1 false-BLOCK on an in-source unit test it missed;
dispatch 2 PASS + located the pin; dispatch 3 PASS after honest
prose correction).

7 design decisions pinned, all derived from the M1–M5 arc except
the one genuine fork the user decided:
- additive FnDef.export: Option<String> (FnDef.doc precedent)
- (export "<sym>") author-chosen, mangling-decoupled C symbol
- lib<entry>.a (program only) + separate libailang_rt.a
- no runtime lifecycle API — documented no-call contract
- --emit=staticlib suppresses @main + MissingEntryMain; needs >=1 (export)
- export-signature gate: scalar-only + effect-free (clause-3 discriminator)
- Task 1 fixed: MissingEntryMain build-path baseline pin (RED-first)

Roadmap M1 flipped [ ] -> [~]. Next: planner in a fresh session
(user-chosen session shape).

docs/roadmap.md

@@ -129,7 +129,7 @@ work progresses.
 
 ## P1 — Next
 
-- [ ] **\[milestone\]** Embedding ABI — M1: linkable artifact +
+- [~] **\[milestone\]** Embedding ABI — M1: linkable artifact +
   scalar C entrypoint + `main`-free lifecycle. First of a
   five-milestone arc (M1–M5) that makes a compiled AILang kernel
   callable in-process from a concurrent Rust host, so a swarm of
@@ -178,8 +178,16 @@ work progresses.
   arithmetic callable from C/Rust, proven by a host harness that
   links the `.a`, calls the symbol, asserts the return.
   - context: 2026-05-18 chat (`data-server` analysis →
-    embedding-ABI decomposition). No spec yet; brainstorm
+    embedding-ABI decomposition). Spec landed + user-approved
-    produces `docs/specs/<date>-embedding-abi-m1.md` at M1 start.
+    2026-05-18: `docs/specs/2026-05-18-embedding-abi-m1.md`
+    (grounding-check PASS on 3rd dispatch; 7 design decisions
+    pinned — additive `FnDef.export: Option<String>` /
+    `(export "<sym>")` mangling-decoupled symbol / `lib<entry>.a`
+    + separate `libailang_rt.a` / no runtime lifecycle API /
+    `--emit=staticlib` suppresses `@main`+`MissingEntryMain` /
+    scalar+effect-free export gate / Task 1 fixed =
+    `MissingEntryMain` build-path baseline pin). Next: `planner`
+    in a fresh session (user-chosen session shape).
 
 - [ ] **\[milestone\]** Embedding ABI — M2: per-thread runtime
   context + concurrency safety. `ailang_ctx_new()/_free` threaded

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

@@ -0,0 +1,428 @@
+# Embedding ABI — M1: linkable artifact + scalar C entrypoint + `main`-free lifecycle — Design Spec
+
+**Date:** 2026-05-18
+**Status:** Draft — awaiting user spec review
+**Authors:** Brummel (orchestrator) + Claude
+
+## Goal
+
+Make a compiled AILang function callable in-process from a Rust/C host.
+Today AILang is a whole-program compiler whose only output is an
+executable wrapping `main` (hard-coded `define i32 @main() { call i8
+@ail_<entry>_main() }`, `crates/ailang-codegen/src/lib.rs:554–561`).
+There is no way to invoke a compiled AILang function from a host with
+structured arguments and a typed return — that missing call surface,
+not the math, is the entire blocker for the financial-backtest swarm
+this language is meant to run (roadmap M1–M5 motivation).
+
+M1 delivers the **first, narrowest** slice: an author marks one `fn`
+as the embedding boundary, `ail build --emit=staticlib` produces a
+relocatable archive instead of an executable, and a C/Rust host links
+it and calls the marked function with scalar arguments. Scalar
+signatures only (`(Int)->Int`, `(Float,Float)->Float`). No ADT, no
+record, no list, no IO crosses the boundary yet — those are M3/M4.
+
+This is a backend/packaging capability. The language's **evaluation**
+semantics do not change: no new term, no new effect, no RC behaviour
+change. The one schema addition (`FnDef.export`) is additive and
+hash-stable, gates only codegen-symbol selection plus a static
+signature check, and is justified strategically (this is where the
+language is meant to run) per the user-made direction call recorded in
+the roadmap — not the standard authoring-utility gate. The
+feature-acceptance criterion is still applied (see Acceptance
+criteria); its clause-3 discriminator (wrong code *fails to
+typecheck*) is the load-bearing part here.
+
+**Coherent stop:** AILang scalar arithmetic callable from C/Rust,
+proven by a host harness that links the `.a`, calls the symbol, and
+asserts the return value — with every M1-arc invariant audited.
+
+### Position in the M1–M5 arc (load-bearing for two M1 decisions)
+
+The arc is a one-way stability progression. Two M1 design decisions
+are *derived from downstream milestones*, not chosen freely:
+
+- **M2** threads `ailang_ctx_new()/_free` "through every call" — the
+  C signature of an exported kernel *changes* at M2. M1's signature
+  is therefore provisional by construction and is labelled as such in
+  DESIGN.md (honesty rule). M1 ships **no** runtime lifecycle API:
+  shipping `ailang_runtime_init/shutdown` stubs now would be replaced
+  by `ctx_new/free` at M2 — exactly the API churn the M3 freeze
+  exists to forbid.
+- **M3** freezes the value/ABI layout as a one-way commitment, and
+  **M5**'s `ail-embed` adapter binds against that frozen ABI as the
+  sole `data-server`↔AILang meeting point. The exported **symbol
+  name** must therefore be author-controlled and decoupled from
+  AILang's internal `ail_<module>_<def>` mangling, so a module/fn
+  refactor in M4/M5 cannot break the M3-frozen ABI. This is why the
+  export marker carries an explicit C symbol string, not a bare
+  boolean (Approach A, chosen 2026-05-18).
+
+## Architecture
+
+Five layers change, in pipeline order. None of `ailang-core`,
+`ailang-codegen`, or `runtime/` gains any `data-server`/finance
+knowledge or dependency (Invariant 1; audited at close).
+
+1. **Schema (`ailang-core`).** One additive field
+   `FnDef.export: Option<String>`, serialised
+   `#[serde(default, skip_serializing_if = "Option::is_none")]` —
+   byte-for-byte the established `FnDef.doc` precedent
+   (`crates/ailang-core/src/ast.rs:206–207`). `None` for every
+   pre-M1 fixture ⇒ all existing canonical-JSON hashes stay
+   bit-identical. DESIGN.md §"Data model" / §Def gains the field;
+   `crates/ailang-core/tests/design_schema_drift.rs` moves in
+   lockstep; a new DESIGN.md §"Embedding ABI (M1)" subsection
+   documents the scalar C ABI and labels the M1 signature
+   *provisional until M3*.
+
+2. **Surface (`ailang-surface`).** The Form-A `fn` head accepts an
+   optional `(export "<c-symbol>")` modifier, positioned like the
+   existing optional fn modifiers. Lex + parse + print, gated by the
+   round-trip invariant: `(export "sym")` ↔ the JSON `"export":"sym"`
+   field is byte-isomorphic both directions. `crates/ailang-core/specs/form_a.md`
+   (verified present) gains the grammar production.
+
+3. **Check (`ailang-check`).** A new diagnostic family gates every
+   `(export …)` fn: its parameter types and return type must each be
+   `Int` or `Float` (M1 scalar scope — `Bool`, `Str`, every ADT
+   rejected), and its effect set must be empty (a pure
+   `(State,Chunk)->State` fold has no effects; an effectful export is
+   the clause-3 wrong-code that must *fail to typecheck*). This is
+   the feature-acceptance clause-3 discriminator, in code, not prose.
+
+4. **Codegen (`ailang-codegen`).** When lowering for the staticlib
+   target: (a) suppress the `@main` trampoline emission
+   (`lib.rs:554–561`) and the `MissingEntryMain` workspace-shape
+   check (`lib.rs:419–431`) — a kernel module is a library and has no
+   `main`; (b) for each `(export "sym")` fn, additionally emit an
+   externally-visible C entrypoint `@sym` with the scalar signature,
+   forwarding to the existing `@ail_<module>_<fn>`. The
+   `_adapter`/`_clos` closure pair is orthogonal and left untouched.
+
+5. **CLI (`crates/ail`).** `ail build` gains an `--emit=staticlib`
+   mode. Instead of `clang … -o <exe>` it: compiles the program `.ll`
+   to `<entry>.o` (`clang -c`), archives it to `lib<entry>.a`
+   (`ar rcs`), and **separately** emits `libailang_rt.a` from the RC
+   runtime glue (`rc.c`/`str.c` → `.o` → `ar rcs`). Two artefacts,
+   cleanly layered: the program archive carries no runtime objects
+   (chosen 2026-05-18 — Invariant 1, and so M2's runtime rebuild
+   touches only `libailang_rt.a`).
+
+6. **Host harness (test only).** A small C harness in the test tree
+   links `lib<entry>.a` + `libailang_rt.a`, calls the exported
+   symbol, asserts the return. This is the E2E proof of the coherent
+   stop. It is **not** a new crate — `ail-embed` is M5; M1's harness
+   is test scaffolding.
+
+## Concrete code shapes
+
+### The AILang program M1 delivers (headline)
+
+`examples/embed_backtest_step.ail` — the `(State, Sample) -> State`
+fold the embedding boundary exists for, in the scalar M1 form an LLM
+author writes when asked "make this AILang fold callable from a Rust
+host":
+
+```
+(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))))
+
+  (fn helper
+    (type
+      (fn-type
+        (params (con Int))
+        (ret (con Int))))
+    (params x)
+    (body
+      (app * x x))))
+```
+
+`step` is the boundary; `helper` is internal — no `(export)`, no C
+symbol, **not** in the (M3-frozen) ABI. The host:
+
+```c
+#include <stdint.h>
+#include <assert.h>
+extern int64_t backtest_step(int64_t state, int64_t sample);
+int main(void) {
+    int64_t s = 0;
+    s = backtest_step(s, 3);   /* 0 + 9  */
+    s = backtest_step(s, 4);   /* 9 + 16 */
+    assert(s == 25);
+    return 0;
+}
+/* cc host.c libbacktest.a libailang_rt.a -o t && ./t */
+```
+
+`backtest_step` is decoupled from the `ail_backtest_step` mangling: a
+later rename of module `backtest` or fn `step` does **not** move the
+C symbol, so the M3-frozen ABI and the M5 adapter survive refactors.
+
+### The must-fail fixture (clause-3 discriminator — mandatory)
+
+`examples/embed_export_effectful_rejected.ail` — parses fine, **must
+fail `ail check`**. An effectful (and non-scalar) export is exactly
+the wrong code the gate exists to reject *at typecheck*, not by
+documentation:
+
+```
+(module bad
+  (fn log_step
+    (export "log_step")
+    (type
+      (fn-type
+        (params (con Int) (con Str))
+        (ret (con Int))
+        (effects IO)))
+    (params state label)
+    (body
+      (seq (do io/print_str label) state))))
+```
+
+The program is otherwise well-formed (body returns `state : Int` after
+the effectful `do`), so the **only** reason it fails is the export
+gate: the `Str` parameter is not C-scalar **and** the `!IO` effect
+set is non-empty. (Narrower must-fail fixtures isolate each clause
+separately; see Testing strategy.)
+
+### North-star slice (provisional surface, explicitly flagged)
+
+The M5 swarm shape this M1 boundary is the first brick of —
+**provisional, not M1 surface, shown only to anchor the arc**:
+
+```rust
+// M5 — ail-embed adapter, NOT delivered in M1, shape provisional:
+let ctx = ailang_ctx_new();                 // M2
+for chunk in data_server.chunks() {         // M5 wiring
+    state = backtest_step(ctx, state, chunk); // M2 ctx + M4 chunk
+}
+ailang_ctx_free(ctx);
+```
+
+M1 delivers only the `state = backtest_step(state, sample)` scalar
+call with no `ctx` and no chunk — everything else above is later
+milestones, drawn here solely so the M1 signature's
+provisional-until-M3 labelling is concrete.
+
+### Implementation shape (secondary — supporting, not the point)
+
+Schema field, modelled byte-for-byte on `FnDef.doc`:
+
+```rust
+// crates/ailang-core/src/ast.rs — pub struct FnDef, after `doc`:
+/// M1 embedding ABI: when `Some(sym)`, this fn is the embedding
+/// boundary and codegen additionally emits an externally-visible
+/// C entrypoint `@<sym>` (scalar signature, provisional until M3).
+/// Author-chosen symbol, decoupled from `ail_<module>_<def>`
+/// mangling so the M3-frozen ABI survives module/fn refactors.
+#[serde(default, skip_serializing_if = "Option::is_none")]
+pub export: Option<String>,
+```
+
+Codegen, staticlib path (schematic — exact bytes are planner's job):
+
+```text
+before (lib.rs:554–561, executable target — UNCHANGED for default mode):
+  define i32 @main() { call i8 @ail_<entry>_main()  ret i32 0 }
+
+after (staticlib target, per (export "backtest_step") fn):
+  ; no @main trampoline, no MissingEntryMain check
+  define i64 @backtest_step(i64 %s, i64 %x) {
+    %r = call i64 @ail_backtest_step(i64 %s, i64 %x)
+    ret i64 %r
+  }
+  ; @ail_backtest_step + its _adapter/_clos pair: unchanged
+```
+
+CLI, schematic:
+
+```text
+before:  clang <opt> -o <entry>            <entry>.ll      (+ link rc.o/str.o)
+after :  clang <opt> -c -o <entry>.o       <entry>.ll
+         ar    rcs    lib<entry>.a         <entry>.o
+         clang -O2 -c -o rc.o rc.c ; clang -O2 -c -o str.o str.c
+         ar    rcs    libailang_rt.a       rc.o str.o
+```
+
+## Components
+
+| Component | Crate | Change |
+|---|---|---|
+| `FnDef.export` field | `ailang-core` | additive `Option<String>`, `skip_serializing_if` |
+| DESIGN.md §Data model / §Def / §Mangling / new §"Embedding ABI (M1)" | docs | field + scalar ABI + provisional-until-M3 label |
+| `design_schema_drift.rs` | `ailang-core` | lockstep with the new field |
+| Form-A `(export "<sym>")` modifier | `ailang-surface` | lex/parse/print + round-trip |
+| `form_a.md` grammar production | `ailang-core/specs` | new production |
+| export-signature gate diagnostic | `ailang-check` | scalar-only + effect-free, new `CheckError` |
+| staticlib lowering | `ailang-codegen` | suppress `@main`/`MissingEntryMain`; emit `@<sym>` forwarders |
+| `ail build --emit=staticlib` | `crates/ail` | `.o` + `ar` two-archive emit, no exe link |
+| host harness | test tree | C harness, link + call + assert |
+
+## Data flow
+
+```
+backtest.ail
+  → ail parse            → JSON-AST  (FnDef.export = Some("backtest_step"))
+  → ail check            → export-signature gate (scalar-only + effect-free)
+  → desugar / lift / monomorphise        (unchanged)
+  → lower_workspace [staticlib]          (no @main; emit @backtest_step → @ail_backtest_step)
+  → backtest.ll
+  → clang -c             → backtest.o
+  → ar rcs               → libbacktest.a
+( rc.c/str.c → clang -c → rc.o/str.o → ar rcs → libailang_rt.a )   [parallel, independent]
+
+host:  cc host.c libbacktest.a libailang_rt.a -o t  →  ./t  →  exit 0 (assert holds)
+```
+
+## Error handling
+
+- **Non-scalar `(export)` signature** (`Bool`/`Str`/ADT in any
+  param or ret): new `ailang-check` Error diagnostic naming the
+  offending position and that M1's embedding ABI is scalar-only
+  (`Int`/`Float`).
+- **Effectful `(export)` fn** (non-empty effect set): new
+  `ailang-check` Error diagnostic — an embedding kernel must be
+  pure.
+- **`--emit=staticlib` with zero `(export)` fns**: CLI error
+  ("staticlib target needs at least one `(export …)` fn"), the
+  staticlib-mode analogue of `MissingEntryMain`. Default executable
+  mode still requires `main` exactly as today.
+- **`(export)` present in default executable mode**: accepted and
+  ignored (the field is inert unless the staticlib target is
+  selected) — keeps the field orthogonal to the existing
+  `main`-executable path; no diagnostic.
+- **Existing `MissingEntryMain`**: unchanged for the default
+  executable target.
+
+## Testing strategy
+
+RED-first throughout (`skills/debug` / TDD discipline).
+
+0. **`MissingEntryMain` build-path baseline pin (prerequisite —
+   first task, RED-first).** The staticlib design is defined as
+   *suppressing* `MissingEntryMain` for the staticlib target. That
+   suppression is only meaningful if the check demonstrably *fires*
+   on a `main`-free workspace in the default executable target. The
+   *codegen-unit* layer of this is already pinned green —
+   `crates/ailang-codegen/src/lib.rs:3314–3342`
+   `tests::missing_entry_main_is_error` builds a `main`-free
+   `noentry` module and asserts `emit_ir` returns
+   `CodegenError::MissingEntryMain("noentry")`; reverting/weakening
+   the `:429` guard already turns that test red (grounding-check
+   re-dispatch, 2026-05-18). What is **not** yet pinned is the same
+   behaviour *at the CLI build-path layer the staticlib mode actually
+   branches on*: that `ail build` (default executable mode) on a
+   `main`-free module surfaces the rejection with
+   `entry module \`{0}\` has no \`main\` def`. This task adds that
+   build-path-level regression fixture, layered on the existing
+   codegen-unit pin (defence in depth at the layer the suppression is
+   introduced). It ships **before** any staticlib code, so the
+   suppression is built atop a baseline pinned at its own layer — the
+   2026-05-11 failure class pre-empted in its proper order.
+1. **Round-trip pin.** `(export "sym")` Form-A ↔ JSON byte-isomorphic
+   both directions; a fixture with `export` and one without, asserting
+   canonical-JSON hash of the without-fixture is unchanged from a
+   pre-M1 golden (additive-field hash stability).
+2. **Schema drift.** `design_schema_drift.rs` green with the new
+   field present in DESIGN.md §Data model.
+3. **Check RED (clause-3).** Three must-fail `ail check` fixtures:
+   (a) `Str` param export, (b) ADT ret export, (c) `!IO` export —
+   each fails with the new diagnostic. Plus a positive fixture
+   (scalar, pure) that passes.
+4. **Codegen.** `--emit`-staticlib lowering emits **no** `@main`,
+   emits `define i64 @backtest_step(...)` with external linkage
+   forwarding to `@ail_backtest_step`; default mode still emits the
+   `@main` trampoline (regression pin).
+5. **E2E host harness.** Build `libbacktest.a` + `libailang_rt.a`,
+   compile + link the C harness, run it, assert exit 0 (the
+   `s == 25` assertion holds). This is the coherent-stop proof.
+6. **Clean-core invariant.** No new dependency in `ailang-core` /
+   `ailang-codegen` / `runtime/` `Cargo.toml`/build; architect
+   audits at close (Invariant 1).
+7. **Bench regression trio** unaffected (no runtime/codegen change
+   on the default executable path) — `bench/check.py`,
+   `compile_check.py`, `cross_lang.py` carry-on.
+
+## Acceptance criteria
+
+Feature-acceptance criterion (DESIGN.md §"Feature-acceptance
+criterion"), applied honestly to a strategic infra milestone:
+
+1. **LLM author naturally produces it.** Asked "make this AILang fold
+   callable from a Rust host", an LLM author writes exactly
+   `examples/embed_backtest_step.ail` above — the `(export "sym")`
+   marker on the fold fn. The worked `.ail` *is* this evidence (not a
+   prose assertion).
+2. **Measurably improves correctness / removes redundancy.** This is
+   a *capability* gate, not a correctness delta — the embedding
+   boundary does not exist at all today. Recorded honestly: the
+   justification is strategic (the language's target deployment),
+   the explicit user-made direction call in the roadmap, *not* the
+   standard authoring-utility metric. No pretence otherwise.
+3. **Reintroduces no bug class the core eliminates.** The
+   export-signature gate makes effectful / non-scalar exports *fail
+   to typecheck* (clause-3 in code, not documentation). Invariant 1
+   (clean core — no finance knowledge/dep in core/codegen/runtime),
+   Invariant 2 (single-threaded — no value crosses a thread
+   boundary; nothing here introduces sharing), and Invariant 3
+   (native-AOT only — no interpreter) all hold and are audited.
+
+Milestone-close ("coherent stop") is met when **all** hold:
+
+- `examples/embed_backtest_step.ail` builds with
+  `ail build --emit=staticlib`, producing `libbacktest.a` +
+  `libailang_rt.a`.
+- The C host harness links both archives, calls `backtest_step`, and
+  the `s == 25` assertion holds (E2E test green).
+- All three must-fail fixtures fail `ail check` with the new
+  diagnostic; the positive fixture passes.
+- Round-trip + schema-drift + every pre-M1 canonical hash unchanged.
+- Architect audit confirms Invariant 1 (no finance/`data-server`
+  knowledge or dependency entered `ailang-core` / `ailang-codegen` /
+  `runtime/`); bench trio carry-on.
+- DESIGN.md §"Embedding ABI (M1)" documents the scalar C ABI and
+  labels the M1 signature **provisional until M3**.
+
+## Iteration sequencing (prerequisite-first)
+
+The planner decomposes M1 into bite-sized tasks, but **task 1 is
+fixed**: the `MissingEntryMain` build-path baseline pin (Testing
+strategy item 0). Rationale: the staticlib path is *defined* as
+suppressing `MissingEntryMain` at the CLI build-path layer. The
+codegen-unit layer of that check is already pinned green
+(`lib.rs:3314` `missing_entry_main_is_error`), but the CLI
+build-path layer the staticlib mode actually branches on is not;
+introducing the suppression before its own layer's baseline is
+pinned would rest the milestone's load-bearing branch on an
+un-pinned layer — the 2026-05-11 failure-class shape. (This spec's
+first grounding-check, 2026-05-18, BLOCKed here on the mistaken
+premise that *no* layer was pinned; the re-dispatch found the
+codegen-unit pin, so task 1 is retained as the *build-path-layer*
+hardening — defence in depth where the suppression is introduced —
+not as a missing-coverage backfill.) Only after task 1 is green
+does the schema/surface/check/codegen/CLI work proceed. No other
+inter-task ordering is mandated by this spec; the planner owns the
+rest.
+
+## Out of scope (explicit)
+
+- Any non-scalar crossing — record/ADT (M3), list (M4), `Str` in/out.
+- Any runtime lifecycle API (`ailang_runtime_init/shutdown`,
+  `ailang_ctx_new/free`) — M2; M1 ships the documented
+  no-call contract only.
+- Per-thread context / concurrency safety / `atexit`-hook
+  neutralisation / `g_rc_*` counter de-globalisation — M2.
+- The `ail-embed` adapter crate + `data-server` wiring + thread
+  swarm — M5.
+- Array/slice primitive — P2, post-M5, measurement-driven.
+- Touching the `_adapter`/`_clos` closure pair.