AILang/docs/specs/0040-embedding-abi-m1.md

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:

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

// 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:

// 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):

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:

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.