AILang/docs/plans/0082-embedding-abi-m1.1.md

Embedding ABI — M1.1 — Implementation Plan

Parent spec: docs/specs/0040-embedding-abi-m1.md

For agentic workers: REQUIRED SUB-SKILL: use skills/implement to run this plan. Steps use - [ ] checkboxes for tracking.

Goal: Make a compiled AILang scalar fn callable in-process from a C/Rust host: an author marks one fn with (export "<c-symbol>"), ail build --emit=staticlib produces lib<entry>.a + a separate libailang_rt.a, and a C host links both and calls the marked function with scalar args and a typed return.

Architecture: Five pipeline layers change in order — schema (FnDef.export: Option<String>, additive/hash-stable, modelled byte-for-byte on FnDef.doc) → surface ((export "<sym>") Form-A modifier, round-trip-gated) → check (scalar-only + effect-free export gate, two new CheckError Error variants — the clause-3 discriminator in code) → codegen (a Target::StaticLib mode that suppresses the @main trampoline + the MissingEntryMain shape-check and emits an external @<sym> forwarder to @ail_<module>_<fn>) → CLI (--emit=staticlib: clang -c + ar rcs two-archive emit). A test-only C host harness proves the coherent stop. None of ailang-core / ailang-codegen / runtime/ gains any finance/data-server knowledge or dependency (Invariant 1).

Tech Stack: ailang-core (AST/serde), ailang-surface (lex/parse/print), ailang-check (CheckError/check_fn), ailang-codegen (LLVM-IR text emission), crates/ail (clap CLI, clang/ar), C (host harness), docs/DESIGN.md + crates/ailang-core/specs/form_a.md (canonical-doc lockstep).

---

Files this plan creates or modifies

• Create: examples/embed_noentry_baseline.ail — main-free module (Task 1 RED fixture).
• Create: crates/ail/tests/embed_missing_main_baseline.rs — CLI build-path baseline pin (Task 1).
• Modify: crates/ailang-core/src/ast.rs:194–221 — add export: Option<String> to FnDef after doc.
• Modify: ~95 FnDef { … } literal sites across 18 files (compile-driven enumeration, Task 2) — incl. in-source #[cfg(test)] mod tests, crates/ailang-core/tests/design_schema_drift.rs:278, crates/ailang-core/tests/spec_drift.rs:256, crates/ailang-core/tests/hash_pin.rs, crates/ailang-codegen/src/lib.rs:3320.
• Modify: docs/DESIGN.md:2290–2299 — add "export" line to the fn JSON block (Task 2); new §"Embedding ABI (M1)" subsection after §"Mangling scheme" (Task 7).
• Modify: crates/ailang-core/specs/form_a.md:68–92 — add (export STRING)? production + prose (Task 3).
• Modify: crates/ailang-surface/src/parse.rs:438–461,477–552 — parse_export helper + parse_fn modifier arm + unknown-attr string + Ok(FnDef{…}) (Task 3).
• Modify: crates/ailang-surface/src/print.rs:148–166 — write_fn_def export emission (Task 3).
• Modify: crates/ailang-check/src/lib.rs:445,697,1851+ — two CheckError variants + code() arms + the export gate in check_fn (Task 4).
• Modify: crates/ailang-codegen/src/lib.rs:158,223,252,256,419–431,554–558 — Target enum, threaded param, gated regions, forwarder loop, new public wrapper (Task 5).
• Modify: crates/ail/src/main.rs:121–140,691–693,2233+ — emit clap field, dispatch branch, build_staticlib (Task 6).
• Create: examples/embed_backtest_step.ail — headline positive (Int,Int)->Int export (Tasks 3/4/6/7).
• Create: examples/embed_export_str_param_rejected.ail, examples/embed_export_adt_ret_rejected.ail, examples/embed_export_io_rejected.ail, examples/embed_export_effectful_rejected.ail, examples/embed_export_float_ok.ail — check-gate fixtures (Task 4).
• Create: crates/ailang-check/tests/embed_export_gate.rs — export-gate check fixtures pin (Task 4).
• Create: crates/ailang-codegen/tests/embed_staticlib_lowering.rs — staticlib IR-shape pin (Task 5).
• Create: crates/ail/tests/embed_staticlib_cli.rs — --emit=staticlib archive-emit pin (Task 6).
• Create: crates/ail/tests/embed/host.c — C host harness (Task 7).
• Create: crates/ail/tests/embed_e2e.rs — E2E coherent-stop proof (Task 7).

---

Design decisions resolved in this plan (Boss judgement)

1. Explicit threading at all ~95 FnDef literal sites, one task (Task 2). Recon found zero functional-record-update / .. / Default anywhere in the workspace — every FnDef { … } is an exhaustive field list, and the prior additive field suppress (Iter 19b) was threaded explicitly at 16/16 desugar.rs sites. Substantive reason (not effort): FnDef construction is uniform across the workspace — an LLM reading any FnDef { … } sees the complete field set; introducing FRU for one field would hide export at most sites. Per planner self-review item 7 the field-add + all-caller threading + the crate-wide cargo build 0-errors gate are therefore one task.
2. Export gate is unconditional at ail check, independent of emit mode. Spec §"Error handling" "(export) present in default executable mode: accepted and ignored … no diagnostic" governs the codegen forwarder (not emitted in exe mode) and the absence of a "you have an export but didn't pick staticlib" warning — it does not relax the signature gate. The scalar-only + effect-free gate fires at ail check whenever f.export.is_some(), unconditionally; that is precisely what makes it the clause-3 discriminator ("wrong code fails to typecheck", period — ail check has no emit mode).
3. Gate order: params → ret → effects, first violation wins. So the spec-named combined fixture embed_export_effectful_rejected.ail (Str param and !IO) deterministically fails with export-non-scalar-signature (the Str param is the first violation). The per-clause fixtures isolate each arm.
4. build_staticlib is a sibling fn, not a refactor of build_to. It re-runs the same load/check/lift/mono prefix (main.rs:2239–2294 shape) then a staticlib-specific lower+archive tail. Substantive reason: the default-executable path is the load-bearing proven path; the two diverge anyway at M2 (ctx threading enters staticlib only). Contained duplication beats destabilising the exe path.
5. DESIGN.md split: the fn-JSON "export" line is schema lockstep → Task 2 (lands with the field). The prose §"Embedding ABI (M1)" subsection documents a capability that only fully exists after codegen+CLI+E2E → Task 7 (DESIGN.md = current-state mirror: document the ABI once it demonstrably works).
6. Fixture module name == file stem (Option 2; revised post-Task-4-BLOCK 2026-05-18). AILang's workspace loader hard- enforces module-name == file-stem (crates/ailang-core/src/workspace.rs:438, WorkspaceLoadError::ModuleNameMismatch, no exception) — so every fixture's (module …) MUST equal its filename stem or ail check panics on load before any gate runs. The original plan's headline used (module backtest) in embed_backtest_step.ail (and bad/bad_io/… in the gate fixtures) — malformed under that invariant; the implement-orchestrator correctly BLOCKED Task 4 on it. Resolution: rename the fixture modules to their file stems, keep the descriptive embed_* filenames (NOT the orchestrator-suggested Option 1 of renaming files to bare module stems). Rationale, from semantics not effort: (a) the spec's load-bearing contract (Decision 2, spec lines 52–59/167–169) is that the exported C symbol is author-chosen and decoupled from ail_<module> mangling — (export "backtest_step") is the contract; the host asserts on backtest_step, which is invariant under module rename. So spec-faithfulness does not discriminate; libbacktest.a/@ail_backtest_step are illustrative (build- output filename + internal mangling — the latter is exactly what the spec decouples from), not frozen-ABI contracts. (b) examples/ is a flat shared corpus auto-enrolled in whole-corpus tests; Option 1's examples/bad.ail/backtest.ail pollute it with collision-prone non-self-describing names — Option 2 keeps the self-describing grouped embed_* set. (c) Option 2 is a concrete demonstration of the spec's own Decision-2 decoupling thesis (module embed_backtest_step, C symbol backtest_step), not a violation of it. The spec's (module backtest)/(module bad) blocks are shape-illustrative (planner contract: spec owns shape, not bytes — same as the spec naming a filename while the contract is the (export …) symbol). Consequences threaded below: entry module embed_backtest_step ⇒ archive libembed_backtest_step.a, internal symbol @ail_embed_backtest_step_step; the external C symbol backtest_step and host.c are UNCHANGED. Architect-at-close note: a fixture module name differing from the spec's illustrative block is expected and correct under the module==stem invariant + Decision 2 — not drift.

---

Task 1: CLI build-path MissingEntryMain baseline pin (FIXED FIRST)

Spec Testing-strategy item 0 + §"Iteration sequencing": this task is fixed as task 1 and ships before any staticlib code. The codegen-unit layer is already pinned green (crates/ailang-codegen/src/lib.rs:3314 missing_entry_main_is_error); this adds the CLI build-path-layer pin the staticlib mode actually branches on (defence in depth at the layer the suppression is introduced). No production code changes in this task — it pins existing behaviour so the later suppression rests on a pinned baseline. "RED-first" here = the pin is demonstrated to exercise the real build-path rejection (Step 3 confirms it is not a no-op).

Files:

• Create: examples/embed_noentry_baseline.ail

• Create: crates/ail/tests/embed_missing_main_baseline.rs

• Step 1: Write the main-free fixture

Create examples/embed_noentry_baseline.ail:

(module embed_noentry_baseline
  (fn helper
    (type
      (fn-type
        (params (con Int))
        (ret (con Int))))
    (params x)
    (body
      (app * x x))))

(Parses + round-trips — roundtrip_cli.rs will enroll it; ail check passes it, main is only required at codegen.)

• Step 2: Write the CLI build-path pin

Create crates/ail/tests/embed_missing_main_baseline.rs:

//! Baseline pin (Embedding-ABI M1, spec Testing-strategy item 0):
//! `ail build` (default executable mode) on a `main`-free module
//! surfaces `CodegenError::MissingEntryMain` at the CLI build-path
//! layer. The staticlib emit-mode (Task 5/6) is *defined* as
//! suppressing exactly this rejection; this pin guards the baseline
//! at the layer the suppression branches on. The codegen-unit layer
//! is independently pinned by
//! `crates/ailang-codegen/src/lib.rs` `missing_entry_main_is_error`.
//!
//! Pure reader: writes nothing to the repo.

use std::path::{Path, PathBuf};
use std::process::Command;

fn ail_bin() -> &'static str {
    env!("CARGO_BIN_EXE_ail")
}

fn workspace_root() -> PathBuf {
    let manifest_dir = env!("CARGO_MANIFEST_DIR");
    Path::new(manifest_dir).parent().unwrap().parent().unwrap().to_path_buf()
}

#[test]
fn ail_build_on_main_free_module_is_rejected_at_cli() {
    let fixture = workspace_root()
        .join("examples")
        .join("embed_noentry_baseline.ail");
    assert!(fixture.exists(), "missing fixture {fixture:?}");

    let out_bin = std::env::temp_dir().join(format!(
        "ailang-embed-baseline-{}", std::process::id()
    ));
    let output = Command::new(ail_bin())
        .args([
            "build",
            fixture.to_str().unwrap(),
            "-o",
            out_bin.to_str().unwrap(),
        ])
        .output()
        .expect("run `ail build`");

    assert!(
        !output.status.success(),
        "ail build of a main-free module unexpectedly succeeded; \
         stdout={} stderr={}",
        String::from_utf8_lossy(&output.stdout),
        String::from_utf8_lossy(&output.stderr),
    );
    let stderr = String::from_utf8_lossy(&output.stderr);
    assert!(
        stderr.contains("has no `main` def"),
        "expected the MissingEntryMain message \
         (`entry module ... has no `main` def`); got stderr: {stderr}",
    );
    assert!(
        !out_bin.exists(),
        "no binary should be produced for a main-free module",
    );
}

• Step 3: Run the pin — verify GREEN and that it is not a no-op

Run: cargo test -p ail --test embed_missing_main_baseline Expected: PASS (1 passed). The assertions are non-trivial: the non-zero-exit + has no \main` defsubstring + absent-binary triple fails if any of (a)MissingEntryMainstops firing, (b) the message text drifts, (c) a binary is emitted anyway. The verbatim substringhas no `main` defis the exactCodegenError::MissingEntryMain Display (crates/ailang-codegen/src/lib.rs:129, #[error("entry module `{0}` has no `main` def")]`).

• Step 4: Confirm the round-trip gate still green with the new fixture

Run: cargo test -p ail --test roundtrip_cli Expected: PASS (the new examples/embed_noentry_baseline.ail is auto-enrolled by list_ail_fixtures's read_dir; it parses and round-trips cleanly).

---

Task 2: Additive FnDef.export schema field + workspace-wide threading

Files:

• Modify: crates/ailang-core/src/ast.rs:194–221

• Modify: ~95 FnDef { … } literal sites (compile-driven; 18 files)

• Modify: docs/DESIGN.md:2290–2299

• Modify: crates/ailang-core/tests/design_schema_drift.rs:278–285

• Create: crates/ailang-core/tests/embed_export_hash_stable.rs

• Step 1: Write the hash-stability RED pin

Create crates/ailang-core/tests/embed_export_hash_stable.rs:

//! Additive-field hash stability (Embedding-ABI M1): adding
//! `FnDef.export: Option<String>` with
//! `#[serde(default, skip_serializing_if = "Option::is_none")]`
//! must leave every pre-M1 canonical-JSON hash bit-identical when
//! `export` is `None`. A round-trip-able fixture WITHOUT `export`
//! hashes identically to a hand-frozen pre-M1 golden.

use ailang_core::ast::{FnDef, Term, Type, Literal};
use ailang_core::hash::content_hash_fn;

#[test]
fn fn_without_export_hash_is_unchanged() {
    // A minimal pre-M1-shaped fn (no export). Its content hash must
    // equal the value captured before the field existed.
    let f = FnDef {
        name: "f".into(),
        ty: Type::fn_implicit(vec![Type::int()], Type::int(), vec![]),
        params: vec!["x".into()],
        body: Term::Var { name: "x".into() },
        doc: None,
        suppress: vec![],
        export: None,
    };
    // GOLDEN: filled in Step 4 from the pre-field hash (RED until then).
    let golden = "<<GOLDEN-PLACEHOLDER>>";
    assert_eq!(content_hash_fn(&f), golden,
        "pre-M1 fn hash drifted — additive-field invariant violated");
}

NOTE (corrected post-iter-1): there is no ailang_core::hash::content_hash_fn. The real entry point is def_hash(&Def) -> String — wrap the FnDef in Def::Fn(...) and call def_hash, exactly as crates/ailang-core/tests/hash_pin.rs does. (Task 2 already executed this correctly per this NOTE's original "mirror hash_pin.rs" license; the symbol name above is left only so the diff to the as-executed test is legible.) Type::fn_implicit / Term::Var constructors are the ones already used by hash_pin.rs and design_schema_drift.rs:282; the implementer mirrors the exact hashing entry point that hash_pin.rs uses if the name differs. The <<GOLDEN-PLACEHOLDER>> is resolved deterministically in Step 4 (capture-then-pin); it is not a design TBD.

• Step 2: Capture the pre-field golden hash

Run (BEFORE adding the field), the equivalent of hash_pin.rs's hashing on the same FnDef shape minus export: cargo test -p ailang-core --test hash_pin -- --nocapture Read the existing pinned fn-hash for the f : (Int)->Int / body=x shape (or add a one-line eprintln!(content_hash_fn(&f)) to the new test, run it, copy the printed hash). Record that string.

• Step 3: Add the field to FnDef

In crates/ailang-core/src/ast.rs, in pub struct FnDef, insert immediately after the doc field (after line 207, before the suppress doc-comment at 208):

    /// Iter embedding-abi-m1: when `Some(sym)`, this fn is the
    /// embedding boundary. Codegen's `Target::StaticLib` mode
    /// additionally emits an externally-visible C entrypoint
    /// `@<sym>` (scalar signature, provisional until M3) forwarding
    /// to `@ail_<module>_<fn>`. The symbol is author-chosen and
    /// decoupled from the `ail_<module>_<def>` mangling so the
    /// M3-frozen ABI survives module/fn refactors.
    ///
    /// Serialised `skip_serializing_if = "Option::is_none"` so every
    /// pre-M1 fixture's canonical-JSON hash stays bit-identical —
    /// the same additive-schema pattern as [`FnDef::doc`].
    #[serde(default, skip_serializing_if = "Option::is_none")]
    pub export: Option<String>,

• Step 4: Pin the golden, run the hash test GREEN

Replace <<GOLDEN-PLACEHOLDER>> in crates/ailang-core/tests/embed_export_hash_stable.rs with the string captured in Step 2. Run: cargo test -p ailang-core --test embed_export_hash_stable Expected: PASS — None export omitted from serialisation ⇒ hash unchanged.

• Step 5: Compile-driven enumeration of all FnDef literal sites

Run: cargo build --workspace 2>&1 | grep -E "missing.*\export`|missing field `export`"For **every** reportedFnDef { … }literal (production AND in-source#[cfg(test)] mod testsAND integration tests), add the lineexport: None,to that literal. Known non-production sites that MUST be threaded (the in-source-test blind spot — seefeedback_grounding_check_misses_insource_tests): crates/ailang-codegen/src/lib.rs:3320 (missing_entry_main_is_error), crates/ailang-core/tests/design_schema_drift.rs:278, crates/ailang-core/tests/spec_drift.rs:256, crates/ailang-core/tests/hash_pin.rs(itsFnDefliteral(s)), plus the ~50 in-sourcemod tests literals recon enumerated (mono.rsuses the aliasAstFnDef = FnDef). Repeat until: cargo build --workspace` exits 0.

• Step 6: Crate-wide compile gate

Run: cargo build --workspace Expected: exits 0, zero error[E0063]/missing field diagnostics. (This gate is the planner-self-review-item-7 contract: the field-add

• ALL caller threading complete in this one task.)

• Step 7: DESIGN.md fn-JSON schema lockstep

In docs/DESIGN.md, in the // fn (the unit that gets a content hash) JSON block (lines 2290–2299), insert after the "doc" line (2297) and before the "suppress" line (2298):

  "export": "<optional C symbol>", // omitted when absent (hash-stable when omitted); see §"Embedding ABI (M1)"

• Step 8: Thread the drift-test FnDef literal

crates/ailang-core/tests/design_schema_drift.rs:278–285 (the design_md_anchors_every_def_kind literal) already gets export: None, from Step 5. Confirm the drift assertion itself stays green:

Run: cargo test -p ailang-core --test design_schema_drift Expected: PASS. (Recon Q2: the nested-struct-key anchor list at :389–394 does not contain "doc"/"suppress", so a new "export" anchor is NOT forced there — consistency says do not add one; the DESIGN.md fn-JSON line from Step 7 is the honesty lockstep, and the def-kind anchor for fn is already present. If the test reports a missing anchor, STOP — that is a spec/lockstep surprise to escalate, not an inline guess.)

• Step 9: Full workspace test gate

Run: cargo test --workspace 2>&1 | tail -20 Expected: 0 failures (delta vs pre-task = the 1 new embed_export_hash_stable test; every threaded literal still constructs/serialises identically because export: None is omitted).

---

Task 3: Form-A (export "<sym>") surface modifier

Files:

• Modify: crates/ailang-surface/src/parse.rs:438–461,477–552

• Modify: crates/ailang-surface/src/print.rs:148–166

• Modify: crates/ailang-core/specs/form_a.md:68–92

• Create: examples/embed_backtest_step.ail

• Step 1: Write the headline round-trip RED fixture

Create examples/embed_backtest_step.ail (the spec headline; module name == file stem per Design-decision 6 — the C symbol stays backtest_step via the (export …) string, demonstrating spec Decision 2's mangling-decoupling):

(module embed_backtest_step

  (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 2: Run the round-trip gate — verify RED

Run: cargo test -p ail --test roundtrip_cli Expected: FAIL — ail parse rejects (export "backtest_step") with unknown fn attribute \export`(currentparse_fnmodifier loop,parse.rs:515–524`). This proves the fixture exercises the new surface.

• Step 3: Add the parse_export helper

In crates/ailang-surface/src/parse.rs, after parse_doc (ends line 461), add (mirrors parse_doc exactly, only the keyword differs):

    fn parse_export(&mut self) -> Result<String, ParseError> {
        self.expect_lparen("export-attr")?;
        self.expect_keyword("export")?;
        let s = match self.peek().cloned() {
            Some(Token { tok: Tok::Str(s), .. }) => {
                self.cur += 1;
                s
            }
            Some(t) => {
                return Err(ParseError::Unexpected {
                    expected: "string literal (export C symbol)".into(),
                    got: tok_label(&t.tok),
                    pos: t.span.start,
                });
            }
            None => {
                return Err(ParseError::UnexpectedEof {
                    expected: "string literal (export C symbol)".into(),
                });
            }
        };
        self.expect_rparen("export-attr")?;
        Ok(s)
    }

• Step 4: Thread export through parse_fn

In crates/ailang-surface/src/parse.rs fn parse_fn:

(a) After let mut doc: Option<String> = None; (line 481) add:

        let mut export: Option<String> = None;

(b) In the modifier loop, after the Some("doc") => { … } arm (ends line 495), add a new arm (modelled on the doc arm):

                Some("export") => {
                    if export.is_some() {
                        return Err(self.duplicate_clause_err("fn-def", &format!("fn `{name}`"), "export"));
                    }
                    export = Some(self.parse_export()?);
                }

(c) In the unknown-attribute error string (lines 519–521) change:

                            "unknown fn attribute `{other}`; expected `doc`, `suppress`, `type`, `params`, or `body`"

to:

                            "unknown fn attribute `{other}`; expected `doc`, `export`, `suppress`, `type`, `params`, or `body`"

(d) In the final Ok(FnDef { … }) literal (lines 544–551) add export, after doc,:

        Ok(FnDef {
            name,
            ty,
            params,
            body,
            doc,
            export,
            suppress,
        })

• Step 5: Thread export through write_fn_def (print side)

In crates/ailang-surface/src/print.rs fn write_fn_def, after the doc emission block (ends line 158) and before the suppress loop (line 159 comment / 162 for s in &fd.suppress), insert (mirrors the doc block):

    if let Some(export) = &fd.export {
        out.push('\n');
        indent(out, level + 1);
        out.push_str("(export ");
        write_string_lit(out, export);
        out.push(')');
    }

(Grammar order: doc → export → suppress → type. This matches the headline fixture, where (export …) precedes (type …) with no (doc …).)

• Step 6: Run the round-trip gate — verify GREEN

Run: cargo test -p ail --test roundtrip_cli Expected: PASS — examples/embed_backtest_step.ail survives ail parse | ail render | ail parse byte-identically; (export "backtest_step") is preserved both directions.

• Step 7: Run the surface crate-internal round-trip tests

Run: cargo test -p ailang-surface Expected: PASS (the in-crate round_trip.rs over examples/*.ail also picks up the new fixture; print↔parse lockstep holds).

• Step 8: form_a.md grammar production lockstep

In crates/ailang-core/specs/form_a.md, in the ### Function — \(fn ...)`block, change the production (lines 70–77) to add(export STRING)?after the(doc STRING)?` line (line 72):

(fn NAME
  (doc STRING)?
  (export STRING)?
  (suppress (code STRING) (because STRING))*
  (type FN-TYPE)
  (params NAME*)
  (body TERM))

After the doc prose paragraph (line 79–80) add a new paragraph:

`export` is optional. When present, the string is the C symbol under
which codegen's `--emit=staticlib` mode exposes this fn as an
externally-callable entrypoint (Embedding ABI M1). The symbol is
author-chosen and decoupled from the internal `ail_<module>_<def>`
mangling. M1 requires the fn's parameter and return types to be
scalar (`Int`/`Float`) and its effect set to be empty — see
DESIGN.md §"Embedding ABI (M1)".

• Step 9: Confirm no spec-drift regression from the form_a.md edit

Run: cargo test -p ailang-core Expected: PASS (form_a.md is not hashed; this confirms no design_schema_drift/spec_drift test reads the changed lines).

---

Task 4: Check-side export-signature gate (clause-3 discriminator)

Files:

• Modify: crates/ailang-check/src/lib.rs:445–446,697,1851+

• Create: examples/embed_export_str_param_rejected.ail

• Create: examples/embed_export_adt_ret_rejected.ail

• Create: examples/embed_export_io_rejected.ail

• Create: examples/embed_export_effectful_rejected.ail

• Create: examples/embed_export_float_ok.ail

• Create: crates/ailang-check/tests/embed_export_gate.rs

• Step 1: Write the five gate fixtures

examples/embed_export_str_param_rejected.ail (Str param, else scalar+pure → export-non-scalar-signature):

(module embed_export_str_param_rejected
  (fn f
    (export "f")
    (type
      (fn-type
        (params (con Int) (con Str))
        (ret (con Int))))
    (params n label)
    (body n)))

examples/embed_export_adt_ret_rejected.ail (ADT return → export-non-scalar-signature):

(module embed_export_adt_ret_rejected
  (data Pair
    (ctor Pair (con Int) (con Int)))
  (fn f
    (export "f")
    (type
      (fn-type
        (params (con Int))
        (ret (con Pair))))
    (params n)
    (body (app Pair n n))))

examples/embed_export_io_rejected.ail (scalar params+ret but !IO → export-has-effects):

(module embed_export_io_rejected
  (fn f
    (export "f")
    (type
      (fn-type
        (params (con Int))
        (ret (con Int))
        (effects IO)))
    (params n)
    (body
      (seq (do io/print_str "x") n))))

examples/embed_export_effectful_rejected.ail (spec-named combined: Str param and !IO; gate-order params→ret→effects ⇒ fails export-non-scalar-signature):

(module embed_export_effectful_rejected
  (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))))

examples/embed_export_float_ok.ail (positive — (Float,Float)->Float, pure; the second scalar type beyond the Int headline):

(module embed_export_float_ok
  (fn scale
    (export "embed_scale")
    (type
      (fn-type
        (params (con Float) (con Float))
        (ret (con Float))))
    (params a b)
    (body
      (app * a b))))

NOTE (folded from the iter-1 BLOCK concern): AILang has no *. Float-multiply head — Float arithmetic uses the same typeclass-generic head as Int (examples/floats.ail uses (app + …); codegen lowers to fmul double by type). The fixture above already uses (app * a b). The fixture's role is "scalar+pure Float export passes the gate".

• Step 2: Write the gate pin — verify RED

Create crates/ailang-check/tests/embed_export_gate.rs:

//! Embedding-ABI M1 export-signature gate (spec §3, clause-3
//! discriminator): an `(export …)` fn whose params/ret are not all
//! `Int`/`Float`, or whose effect set is non-empty, MUST fail
//! `ail check` with the new diagnostic. A scalar+pure export passes.

use std::path::PathBuf;

fn examples_dir() -> PathBuf {
    PathBuf::from(env!("CARGO_MANIFEST_DIR"))
        .parent().unwrap().parent().unwrap()
        .join("examples")
}

fn check_codes(file: &str) -> Vec<String> {
    let path = examples_dir().join(file);
    let ws = ailang_surface::load_workspace(&path)
        .unwrap_or_else(|e| panic!("load {file}: {e}"));
    ailang_check::check_workspace(&ws)
        .into_iter()
        .map(|d| d.code)
        .collect()
}

#[test]
fn str_param_export_rejected() {
    assert!(check_codes("embed_export_str_param_rejected.ail")
        .iter().any(|c| c == "export-non-scalar-signature"));
}

#[test]
fn adt_ret_export_rejected() {
    assert!(check_codes("embed_export_adt_ret_rejected.ail")
        .iter().any(|c| c == "export-non-scalar-signature"));
}

#[test]
fn io_export_rejected() {
    assert!(check_codes("embed_export_io_rejected.ail")
        .iter().any(|c| c == "export-has-effects"));
}

#[test]
fn combined_effectful_export_rejected_on_signature_first() {
    let codes = check_codes("embed_export_effectful_rejected.ail");
    assert!(codes.iter().any(|c| c == "export-non-scalar-signature"),
        "combined fixture must fail signature-first; got {codes:?}");
}

#[test]
fn scalar_pure_export_passes() {
    let codes = check_codes("embed_export_float_ok.ail");
    assert!(!codes.iter().any(|c|
        c == "export-non-scalar-signature" || c == "export-has-effects"),
        "scalar+pure export must pass the gate; got {codes:?}");
}

#[test]
fn headline_int_export_passes() {
    let codes = check_codes("embed_backtest_step.ail");
    assert!(!codes.iter().any(|c|
        c == "export-non-scalar-signature" || c == "export-has-effects"),
        "headline export must pass the gate; got {codes:?}");
}

The implementer confirms ailang_surface::load_workspace + ailang_check::check_workspace + Diagnostic.code are the exact public symbols (they are the ones crates/ail/src/main.rs:2239–2240 uses; mirror that call shape).

Run: cargo test -p ailang-check --test embed_export_gate Expected: FAIL — no export-non-scalar-signature / export-has-effects code exists yet; the rejected fixtures currently ail check-pass (the body is well-formed), so every *_rejected test fails.

• Step 3: Add the two CheckError variants

In crates/ailang-check/src/lib.rs, after the ConstHasEffects variant (ends line 445), add:

    /// An `(export …)` fn has a parameter or return type that is not
    /// a C-scalar (`Int`/`Float`). M1's embedding ABI is scalar-only;
    /// `Bool`/`Str`/every ADT is rejected at typecheck (the
    /// feature-acceptance clause-3 discriminator, in code).
    /// Code: `export-non-scalar-signature`.
    #[error("export `{0}`: M1 embedding ABI is scalar-only — {1} type `{2}` is not `Int`/`Float`")]
    ExportNonScalarSignature(String, &'static str, String),

    /// An `(export …)` fn has a non-empty effect set. An embedding
    /// kernel must be pure (a `(State,Chunk)->State` fold has no
    /// effects). Code: `export-has-effects`.
    #[error("export `{0}` must be pure — declared effects !{1:?} are not allowed on an embedding boundary")]
    ExportHasEffects(String, Vec<String>),

• Step 4: Add the two code() arms

In crates/ailang-check/src/lib.rs fn code, after the ConstHasEffects arm (line 697), add:

            CheckError::ExportNonScalarSignature(..) => "export-non-scalar-signature",
            CheckError::ExportHasEffects(..) => "export-has-effects",

(No ctx()/message()/def()/inner() arms needed: ctx() has a _ => catch-all (lib.rs:796), message() is format!("{}", self.inner()) (thiserror Display), def()/inner() have catch-alls. to_diagnostic wraps every CheckError as Severity::Error — so both new diagnostics are Error severity, as the spec requires.)

• Step 5: Implement the gate in check_fn

In crates/ailang-check/src/lib.rs fn check_fn, after the parameter/return well-formedness checks (after check_type_well_formed(&ret_ty, &env)?;, line 1895), insert the gate. param_tys, ret_ty, declared_effs are already bound (lines 1861–1863); f.export / f.name are on the &FnDef:

    // Embedding-ABI M1: an `(export …)` fn is the C call boundary.
    // Its signature must be scalar-only (`Int`/`Float`) and pure.
    // Gate order: params → ret → effects, first violation wins
    // (so a combined Str+IO export deterministically fails on the
    // signature). Unconditional at check-time — independent of the
    // codegen emit mode — this IS the clause-3 discriminator.
    if f.export.is_some() {
        fn is_c_scalar(t: &Type) -> bool {
            matches!(t, Type::Con { name, args, .. }
                if args.is_empty() && (name == "Int" || name == "Float"))
        }
        for p in &param_tys {
            if !is_c_scalar(p) {
                return Err(CheckError::ExportNonScalarSignature(
                    f.name.clone(),
                    "parameter",
                    ailang_core::pretty::type_to_string(p),
                ));
            }
        }
        if !is_c_scalar(&ret_ty) {
            return Err(CheckError::ExportNonScalarSignature(
                f.name.clone(),
                "return",
                ailang_core::pretty::type_to_string(&ret_ty),
            ));
        }
        if !declared_effs.is_empty() {
            return Err(CheckError::ExportHasEffects(
                f.name.clone(),
                declared_effs.clone(),
            ));
        }
    }

The implementer confirms Type::Con's field set (name, args, and any mode field) against ast.rs; the matches! guard rejects parameterised cons (args non-empty) and any non-Int/Float con. declared_effs element type is whatever Type::Fn.effects holds (string-ish); the ExportHasEffects(_, Vec<String>) shape mirrors ConstHasEffects(String, Vec<String>) — match its .into_iter().collect() conversion at lib.rs:2804–2806 if declared_effs is not already Vec<String>.

• Step 6: Run the gate pin — verify GREEN

Run: cargo test -p ailang-check --test embed_export_gate Expected: PASS (6 passed): the three per-clause rejects fire the right code, the combined fixture fails signature-first, both positive fixtures pass the gate.

• Step 7: Round-trip + workspace regression

Run: cargo test -p ail --test roundtrip_cli && cargo test --workspace 2>&1 | tail -15 Expected: PASS — all five new examples/*.ail parse + round-trip (they fail at check, not parse, so roundtrip_cli stays green); workspace delta = the new gate tests only.

---

Task 5: Codegen Target::StaticLib — suppress @main/MissingEntryMain, emit @<sym> forwarder

Files:

• Modify: crates/ailang-codegen/src/lib.rs:158,223–225,252–256,419–431,554–558

• Create: crates/ailang-codegen/tests/embed_staticlib_lowering.rs

• Step 1: Write the staticlib IR-shape pin — verify RED

Create crates/ailang-codegen/tests/embed_staticlib_lowering.rs:

//! Embedding-ABI M1 codegen (spec §4): `Target::StaticLib` lowering
//! emits NO `@main` trampoline, NO `MissingEntryMain`, and one
//! external `define i64 @backtest_step(...)` (the author-chosen C
//! symbol from `(export "backtest_step")`) forwarding to the
//! internal `@ail_embed_backtest_step_step` (module
//! `embed_backtest_step` == file stem, per Design-decision 6).
//! Executable-target lowering is byte-unchanged (the
//! `missing_entry_main_is_error` in-source pin still holds).

use ailang_core::Workspace;
use std::path::PathBuf;

fn load(file: &str) -> Workspace {
    let path = PathBuf::from(env!("CARGO_MANIFEST_DIR"))
        .parent().unwrap().parent().unwrap()
        .join("examples").join(file);
    ailang_surface::load_workspace(&path).unwrap()
}

#[test]
fn staticlib_emits_forwarder_no_main() {
    let ws = load("embed_backtest_step.ail");
    let ir = ailang_codegen::lower_workspace_staticlib_with_alloc(
        &ws, ailang_codegen::AllocStrategy::Rc).unwrap();
    assert!(!ir.contains("define i32 @main()"),
        "staticlib IR must not emit the @main trampoline");
    assert!(ir.contains("@backtest_step("),
        "staticlib IR must emit the external @backtest_step entrypoint \
         (the author-chosen C symbol — invariant under module rename)");
    assert!(ir.contains("@ail_embed_backtest_step_step("),
        "the forwarder must call the internal \
         @ail_embed_backtest_step_step (module embed_backtest_step)");
}

#[test]
fn executable_target_still_emits_main() {
    let ws = load("embed_backtest_step.ail");
    // Default executable lowering is unaffected by the new field;
    // backtest has no `main`, so exe-target lowering still rejects.
    let err = ailang_codegen::lower_workspace_with_alloc(
        &ws, ailang_codegen::AllocStrategy::Rc).unwrap_err();
    assert!(format!("{err}").contains("has no `main` def"),
        "exe target must still surface MissingEntryMain; got {err}");
}

Run: cargo test -p ailang-codegen --test embed_staticlib_lowering Expected: FAIL — lower_workspace_staticlib_with_alloc does not exist (compile error). This is the RED.

• Step 2: Add the Target enum

In crates/ailang-codegen/src/lib.rs, near the AllocStrategy enum (line 158), add:

/// Embedding-ABI M1: codegen output shape.
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub enum Target {
    /// Default: emit the `@main` trampoline; require an entry `main`
    /// (`MissingEntryMain` if absent). Whole-program executable.
    Executable,
    /// `--emit=staticlib`: suppress the `@main` trampoline AND the
    /// `MissingEntryMain` shape-check (a kernel module is a library);
    /// emit one external C entrypoint per `(export …)` fn forwarding
    /// to `@ail_<module>_<fn>`. Provisional signature until M3.
    StaticLib,
}

• Step 3: Thread target through lower_workspace_inner and add the public wrapper

(a) Change fn lower_workspace_inner(ws: &Workspace, alloc: AllocStrategy) (line 256) to fn lower_workspace_inner(ws: &Workspace, alloc: AllocStrategy, target: Target).

(b) Update the three existing internal callers to pass Target::Executable (compile-forced — all in lib.rs, this same task per self-review item 7):

• lower_workspace_with_alloc body (line 224): lower_workspace_inner(ws, alloc, Target::Executable)
• lower_workspace body (line 253): lower_workspace_inner(ws, AllocStrategy::Gc, Target::Executable)
• emit_ir (line 197): its internal lower_workspace_inner call (the implementer locates it within emit_ir's body) passes Target::Executable — so the in-source missing_entry_main_is_error pin (which calls emit_ir) is byte-unchanged.

(c) Add the public staticlib wrapper next to lower_workspace_with_alloc (after line 225):

/// Embedding-ABI M1 entry point. Lowers a [`Workspace`] for the
/// static-library target: no `@main`, no `MissingEntryMain`, one
/// external `@<sym>` forwarder per `(export …)` fn.
pub fn lower_workspace_staticlib_with_alloc(
    ws: &Workspace,
    alloc: AllocStrategy,
) -> Result<String> {
    lower_workspace_inner(ws, alloc, Target::StaticLib)
}

• Step 4: Gate the MissingEntryMain shape-check

In crates/ailang-codegen/src/lib.rs, lines 419–431, wrap the has-main check so it only runs for the executable target:

    // Trampoline: verify that the entry module has a
    // `main : () -> Unit !IO`. Suppressed for the staticlib target —
    // a kernel module is a library and has no `main`.
    if target == Target::Executable {
        let entry_module = ws
            .modules
            .get(&ws.entry)
            .ok_or_else(|| CodegenError::Internal(format!("entry module `{}` not in workspace", ws.entry)))?;
        let has_main = entry_module
            .defs
            .iter()
            .any(|d| matches!(d, Def::Fn(f) if f.name == "main" && main_is_void(&f.ty)));
        if !has_main {
            return Err(CodegenError::MissingEntryMain(ws.entry.clone()));
        }
    }

• Step 5: Gate the @main trampoline and emit forwarders

In crates/ailang-codegen/src/lib.rs, the trampoline push at lines 554–558 — replace with a match target:

    match target {
        Target::Executable => {
            // Trampoline @main → @ail_<entry>_main.
            out.push_str(&format!(
                "\ndefine i32 @main() {{\n  call i8 @ail_{}_main()\n  ret i32 0\n}}\n",
                ws.entry
            ));
        }
        Target::StaticLib => {
            // One external C entrypoint per `(export …)` fn,
            // forwarding to the internal `@ail_<module>_<fn>`.
            // The check-side gate (Task 4) guarantees every param
            // and the ret are `Int`/`Float`; map Int→i64,
            // Float→double. M1 scalar fns have no captured env, so
            // the internal callee takes the scalars positionally
            // (confirmed against `emit_fn`'s signature emission,
            // `lib.rs:1087`).
            for (mname, m) in &ws.modules {
                for d in &m.defs {
                    if let Def::Fn(f) = d {
                        if let Some(sym) = &f.export {
                            let (param_tys, ret_ty) = match fn_scalar_sig(&f.ty) {
                                Some(sig) => sig,
                                None => return Err(CodegenError::Internal(format!(
                                    "export `{sym}`: non-scalar signature reached codegen \
                                     (check-side gate should have rejected it)"))),
                            };
                            let cret = llvm_scalar(&ret_ty);
                            let params: Vec<String> = param_tys.iter().enumerate()
                                .map(|(i, t)| format!("{} %a{i}", llvm_scalar(t)))
                                .collect();
                            let args: Vec<String> = param_tys.iter().enumerate()
                                .map(|(i, t)| format!("{} %a{i}", llvm_scalar(t)))
                                .collect();
                            out.push_str(&format!(
                                "\ndefine {cret} @{sym}({}) {{\n  \
                                 %r = call {cret} @ail_{mname}_{}({})\n  \
                                 ret {cret} %r\n}}\n",
                                params.join(", "),
                                f.name,
                                args.join(", "),
                            ));
                        }
                    }
                }
            }
        }
    }

Add two private helpers near main_is_void (after line 569):

/// Scalar-signature view of an export fn's type. `None` if not the
/// flat `Type::Fn` of scalars the M1 gate guarantees.
fn fn_scalar_sig(t: &Type) -> Option<(Vec<Type>, Type)> {
    let inner = match t {
        Type::Forall { body, .. } => body.as_ref(),
        other => other,
    };
    match inner {
        Type::Fn { params, ret, .. } =>
            Some((params.clone(), (**ret).clone())),
        _ => None,
    }
}

/// `Int` → `i64`, `Float` → `double` (the only two M1 scalars; the
/// check-side gate rejects everything else before codegen).
fn llvm_scalar(t: &Type) -> &'static str {
    match t {
        Type::Con { name, .. } if name == "Float" => "double",
        _ => "i64",
    }
}

The implementer cross-checks llvm_scalar against the existing codegen type lowering (synth.rs llvm_type / emit_fn's signature string at lib.rs:1087–1092): the forwarder's {cret} and arg types MUST equal what @ail_<mname>_<fn> was emitted with, or the call is mistyped. If emit_fn lowers Int to anything other than i64 / Float to other than double, llvm_scalar mirrors that exactly. The RED→GREEN IR assertion in Step 6 + the Task-7 E2E (real cc link + run) jointly catch a signature mismatch.

• Step 6: Run the codegen pin — verify GREEN

Run: cargo test -p ailang-codegen --test embed_staticlib_lowering Expected: PASS (2 passed): staticlib IR has no @main, has external @backtest_step (C symbol), forwards to the internal @ail_embed_backtest_step_step; exe target still returns MissingEntryMain.

• Step 7: Codegen in-source baseline pin still green

Run: cargo test -p ailang-codegen missing_entry_main_is_error Expected: PASS — emit_ir passes Target::Executable, so the codegen-unit MissingEntryMain baseline (spec Testing item 0, codegen layer) is byte-unchanged.

• Step 8: Codegen crate gate

Run: cargo test -p ailang-codegen 2>&1 | tail -15 Expected: 0 failures (delta = the new lowering test; the threaded target param touched only lib.rs callers, all updated this task).

---

Task 6: CLI ail build --emit=staticlib

Files:

• Modify: crates/ail/src/main.rs:121–140,691–693,2233+

• Create: crates/ail/tests/embed_staticlib_cli.rs

• Step 1: Write the staticlib-emit CLI pin — verify RED

Create crates/ail/tests/embed_staticlib_cli.rs:

//! Embedding-ABI M1 CLI (spec §5): `ail build --emit=staticlib`
//! produces `lib<entry>.a` (program-only) + a separate
//! `libailang_rt.a`, and emits NO executable / NO `@main`.

use std::path::{Path, PathBuf};
use std::process::Command;

fn ail_bin() -> &'static str { env!("CARGO_BIN_EXE_ail") }
fn ws_root() -> PathBuf {
    Path::new(env!("CARGO_MANIFEST_DIR"))
        .parent().unwrap().parent().unwrap().to_path_buf()
}

#[test]
fn staticlib_emit_produces_two_archives() {
    let fixture = ws_root().join("examples").join("embed_backtest_step.ail");
    let outdir = std::env::temp_dir()
        .join(format!("ail-embed-cli-{}", std::process::id()));
    std::fs::create_dir_all(&outdir).unwrap();

    let out = Command::new(ail_bin())
        .args([
            "build", fixture.to_str().unwrap(),
            "--emit=staticlib",
            "-o", outdir.to_str().unwrap(),
        ])
        .output().expect("ail build --emit=staticlib");
    assert!(out.status.success(),
        "staticlib build failed: stdout={} stderr={}",
        String::from_utf8_lossy(&out.stdout),
        String::from_utf8_lossy(&out.stderr));

    assert!(outdir.join("libembed_backtest_step.a").exists(),
        "expected libembed_backtest_step.a in {outdir:?}");
    assert!(outdir.join("libailang_rt.a").exists(),
        "expected separate libailang_rt.a in {outdir:?}");
}

#[test]
fn staticlib_emit_requires_an_export() {
    // embed_noentry_baseline has no `(export …)` fn.
    let fixture = ws_root().join("examples")
        .join("embed_noentry_baseline.ail");
    let outdir = std::env::temp_dir()
        .join(format!("ail-embed-noexp-{}", std::process::id()));
    std::fs::create_dir_all(&outdir).unwrap();
    let out = Command::new(ail_bin())
        .args(["build", fixture.to_str().unwrap(),
               "--emit=staticlib", "-o", outdir.to_str().unwrap()])
        .output().expect("ail build");
    assert!(!out.status.success(),
        "staticlib build with zero exports must fail");
    assert!(String::from_utf8_lossy(&out.stderr)
        .contains("at least one `(export"),
        "expected the zero-export staticlib error; got {}",
        String::from_utf8_lossy(&out.stderr));
}

Run: cargo test -p ail --test embed_staticlib_cli Expected: FAIL — --emit is not a known flag (clap rejects it; grep -n "emit" crates/ail/src/main.rs confirms absent).

• Step 2: Add the --emit clap field

In crates/ail/src/main.rs, in the Build subcommand struct (the variant ending at line 140, after the alloc field), add:

        /// Output shape. `exe` (default): whole-program executable
        /// (requires an entry `main`). `staticlib`: a relocatable
        /// `lib<entry>.a` (program objects only) plus a separate
        /// `libailang_rt.a` (RC runtime), with one external C
        /// entrypoint per `(export "<sym>")` fn and no `@main`
        /// (Embedding ABI M1). With `staticlib`, `-o` is a directory.
        #[arg(long, default_value = "exe", value_parser = ["exe", "staticlib"])]
        emit: String,

• Step 3: Branch the Cmd::Build dispatch

In crates/ail/src/main.rs, the Cmd::Build { … } arm (lines 691–693), replace with:

        Cmd::Build { path, out, opt, alloc, emit } => {
            let strategy = parse_alloc_strategy(&alloc)?;
            if emit == "staticlib" {
                let (lib, rt) = build_staticlib(&path, out, &opt, strategy)?;
                eprintln!("built {} + {}", lib.display(), rt.display());
            } else {
                let bin = build_to(&path, out, &opt, strategy)?;
                eprintln!("built {}", bin.display());
            }
        }

• Step 4: Implement build_staticlib

In crates/ail/src/main.rs, add a sibling fn after build_to (after its closing brace; build_to starts line 2233). It reuses build_to's proven load→check→lift→mono prefix verbatim (the body of build_to lines 2239–2294), then diverges to the staticlib lower+archive tail:

/// Embedding-ABI M1: `ail build --emit=staticlib`. Produces
/// `<outdir>/lib<entry>.a` (program objects only) and a separate
/// `<outdir>/libailang_rt.a` (RC runtime: rc.c + str.c). No
/// executable, no `@main`. `out` is the output directory.
fn build_staticlib(
    path: &Path,
    out: Option<PathBuf>,
    opt: &str,
    alloc: ailang_codegen::AllocStrategy,
) -> Result<(PathBuf, PathBuf)> {
    // ---- shared front matter: identical to build_to:2239–2294 ----
    let ws = load_workspace_human(path)?;
    let diags = ailang_check::check_workspace(&ws);
    if !diags.is_empty() {
        for d in &diags {
            eprintln!(
                "{}: [{}] {}{}",
                match d.severity {
                    ailang_check::Severity::Error => "error",
                    ailang_check::Severity::Warning => "warning",
                },
                d.code,
                d.def.as_ref().map(|n| format!("{n}: ")).unwrap_or_default(),
                d.message,
            );
        }
        if diags.iter().any(|d| matches!(d.severity, ailang_check::Severity::Error)) {
            std::process::exit(1);
        }
    }
    let mut lifted_modules = std::collections::BTreeMap::new();
    for (mname, m) in &ws.modules {
        let desugared = ailang_core::desugar::desugar_module(m);
        let lifted = ailang_check::lift_letrecs(&desugared)
            .map_err(|e| anyhow::anyhow!("lift_letrecs in module `{mname}`: {e}"))?;
        lifted_modules.insert(mname.clone(), lifted);
    }
    let ws = ailang_core::Workspace {
        entry: ws.entry.clone(),
        modules: lifted_modules,
        root_dir: ws.root_dir.clone(),
        registry: ws.registry.clone(),
    };
    let ws = ailang_check::monomorphise_workspace(&ws)
        .map_err(|e| anyhow::anyhow!("monomorphise_workspace: {e}"))?;

    // ---- staticlib-specific: require ≥1 export, then lower ----
    let has_export = ws.modules.values().any(|m| m.defs.iter().any(|d|
        matches!(d, ailang_core::Def::Fn(f) if f.export.is_some())));
    if !has_export {
        anyhow::bail!(
            "staticlib target needs at least one `(export \"<sym>\")` fn"
        );
    }
    let ir = ailang_codegen::lower_workspace_staticlib_with_alloc(&ws, alloc)?;

    let tmpdir = std::env::temp_dir().join(format!("ailang-{}", std::process::id()));
    std::fs::create_dir_all(&tmpdir)?;
    let ll_path = tmpdir.join(format!("{}.ll", ws.entry));
    std::fs::write(&ll_path, &ir)?;

    let outdir = out.unwrap_or_else(|| PathBuf::from("."));
    std::fs::create_dir_all(&outdir)?;

    // program object → lib<entry>.a (program objects ONLY — no rt)
    let prog_obj = tmpdir.join(format!("{}.o", ws.entry));
    run_cmd("clang", &[opt, "-c", "-o",
        prog_obj.to_str().unwrap(), ll_path.to_str().unwrap()],
        "compiling program .ll")?;
    let prog_archive = outdir.join(format!("lib{}.a", ws.entry));
    let _ = std::fs::remove_file(&prog_archive);
    run_cmd("ar", &["rcs", prog_archive.to_str().unwrap(),
        prog_obj.to_str().unwrap()], "archiving lib<entry>.a")?;

    // RC runtime → libairlang_rt.a (rc.c + str.c), separate archive
    let rc_src = locate_rc_runtime()?;
    let str_src = locate_str_runtime()?;
    let rc_obj = tmpdir.join("rc.o");
    let str_obj = tmpdir.join("str.o");
    run_cmd("clang", &["-O2", "-c", "-o",
        rc_obj.to_str().unwrap(), rc_src.to_str().unwrap()],
        "compiling runtime/rc.c")?;
    run_cmd("clang", &["-O2", "-c", "-o",
        str_obj.to_str().unwrap(), str_src.to_str().unwrap()],
        "compiling runtime/str.c")?;
    let rt_archive = outdir.join("libailang_rt.a");
    let _ = std::fs::remove_file(&rt_archive);
    run_cmd("ar", &["rcs", rt_archive.to_str().unwrap(),
        rc_obj.to_str().unwrap(), str_obj.to_str().unwrap()],
        "archiving libailang_rt.a")?;

    Ok((prog_archive, rt_archive))
}

/// Run an external command, bailing with stderr on non-zero exit.
fn run_cmd(bin: &str, args: &[&str], ctx: &str) -> Result<()> {
    let status = std::process::Command::new(bin)
        .args(args).status().context(ctx.to_string())?;
    if !status.success() {
        anyhow::bail!("{ctx}: `{bin}` exited {status}");
    }
    Ok(())
}

The implementer reuses the EXACT shared-prefix code from build_to:2239–2294 (copy, not re-derive) so the two paths share a proven front matter; locate_rc_runtime/locate_str_runtime are the existing locators (main.rs:2158/:2189). run_cmd is added only if no equivalent helper already exists in main.rs — if one does, use it (the implementer greps fn .*Command::new first). ailang_core::Def import path mirrors codegen's usage.

• Step 5: Run the CLI pin — verify GREEN

Run: cargo test -p ail --test embed_staticlib_cli Expected: PASS (2 passed): the headline produces libembed_backtest_step.a + libailang_rt.a; the export-less module is rejected with the zero-export error.

• Step 6: Default-exe path regression

Run: cargo test -p ail --test floats_e2e --test embed_missing_main_baseline Expected: PASS — --emit defaults to exe; build_to is reached unchanged for the default path (Task-1 baseline pin + the floats E2E both still green).

---

Task 7: E2E host harness + DESIGN.md §"Embedding ABI (M1)"

Files:

• Create: crates/ail/tests/embed/host.c

• Create: crates/ail/tests/embed_e2e.rs

• Modify: docs/DESIGN.md (new §"Embedding ABI (M1)" after §"Mangling scheme", before §"Data model" at line 2263)

• Step 1: Write the C host harness

Create crates/ail/tests/embed/host.c (the spec headline host, verbatim):

#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;
}

• Step 2: Write the E2E coherent-stop pin — verify RED

Create crates/ail/tests/embed_e2e.rs:

//! Embedding-ABI M1 coherent-stop proof (spec §"Testing strategy" 5
//! + Acceptance criteria): build `examples/embed_backtest_step.ail`
//! as a staticlib, link the C host against `libembed_backtest_step.a`
//! + `libailang_rt.a`, run it, assert the `s == 25` assertion holds
//! (exit 0). This is the whole-milestone existence proof.

use std::path::{Path, PathBuf};
use std::process::Command;

fn ail_bin() -> &'static str { env!("CARGO_BIN_EXE_ail") }
fn manifest() -> PathBuf { PathBuf::from(env!("CARGO_MANIFEST_DIR")) }
fn ws_root() -> PathBuf {
    manifest().parent().unwrap().parent().unwrap().to_path_buf()
}

#[test]
fn c_host_calls_exported_scalar_kernel() {
    let fixture = ws_root().join("examples").join("embed_backtest_step.ail");
    let host_c = manifest().join("tests").join("embed").join("host.c");
    let outdir = std::env::temp_dir()
        .join(format!("ail-embed-e2e-{}", std::process::id()));
    std::fs::create_dir_all(&outdir).unwrap();

    let build = Command::new(ail_bin())
        .args(["build", fixture.to_str().unwrap(),
               "--emit=staticlib", "-o", outdir.to_str().unwrap()])
        .output().expect("ail build --emit=staticlib");
    assert!(build.status.success(),
        "staticlib build failed: {}",
        String::from_utf8_lossy(&build.stderr));

    let host_bin = outdir.join("host");
    let cc = Command::new("cc")
        .arg(&host_c)
        .arg(outdir.join("libembed_backtest_step.a"))
        .arg(outdir.join("libailang_rt.a"))
        .arg("-o").arg(&host_bin)
        .output().expect("cc host link");
    assert!(cc.status.success(),
        "cc link failed: {}", String::from_utf8_lossy(&cc.stderr));

    let run = Command::new(&host_bin).output().expect("run host");
    assert!(run.status.success(),
        "host assertion `s == 25` failed (exit {:?}); stderr={}",
        run.status.code(), String::from_utf8_lossy(&run.stderr));
}

Run: cargo test -p ail --test embed_e2e Expected: FAIL until Tasks 5+6 are green (here they are; if run in order this is the final GREEN — but it still RED-demonstrates: revert Task 5's forwarder loop and the link is undefined-symbol). Then PASS.

• Step 3: Run the E2E — verify GREEN

Run: cargo test -p ail --test embed_e2e Expected: PASS — libembed_backtest_step.a + libailang_rt.a link with the C host; backtest_step(0,3)=9, backtest_step(9,4)=25; assertion holds; exit 0. This is the coherent stop.

• Step 4: DESIGN.md §"Embedding ABI (M1)" — current-state honesty

In docs/DESIGN.md, immediately after the §"Mangling scheme" section ends (it begins at line 2206) and before the §"Data model" header (line 2263), insert a new subsection at the same heading level as §"Mangling scheme":

### Embedding ABI (M1)

`ail build --emit=staticlib` compiles a module to a relocatable
`lib<entry>.a` (program objects only) plus a separate
`libailang_rt.a` (the RC runtime: `rc.c` + `str.c`), with **no**
`@main` trampoline and **no** `MissingEntryMain` requirement — a
kernel module is a library.

Each `fn` carrying `(export "<sym>")` (schema: `FnDef.export`) is
emitted as an externally-visible C entrypoint `@<sym>` forwarding to
the internal `@ail_<module>_<fn>`. The symbol is author-chosen and
decoupled from the `ail_<module>_<def>` mangling so a module/fn
rename does not move the C symbol.

The M1 ABI is **scalar-only and provisional until M3**: every
parameter and the return type must be `Int` (lowered `i64`) or
`Float` (lowered `double`), and the fn's effect set must be empty.
These are enforced at `ail check` (`export-non-scalar-signature`,
`export-has-effects`) — an effectful or non-scalar export *fails to
typecheck*. M1 ships no runtime lifecycle API: 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.
The value/record layout freeze is M3.

• Step 5: DESIGN.md honesty + drift gate

Run: cargo test -p ailang-core --test design_schema_drift --test spec_drift && bash bench/architect_sweeps.sh 2>&1 | tail -5 Expected: drift tests PASS (the new prose subsection is honest present-tense — it documents what now demonstrably works, per the DESIGN.md current-state-mirror rule; the fn-JSON "export" line landed in Task 2). architect_sweeps.sh residue unchanged modulo the (advisory) new dated-free subsection — no new Wunschdenken / post-mortem phrasing introduced (the "provisional until M3" / "M2 will change" clauses are reserved-unimplemented labelling, which the honesty rule explicitly permits when labelled).

• Step 6: Full workspace + round-trip + bench-trio carry-on

Run: cargo test --workspace 2>&1 | tail -20 Expected: 0 failures. Run: cargo test -p ail --test roundtrip_cli Expected: PASS (all new examples/embed_*.ail round-trip). Run: python3 bench/check.py; python3 bench/compile_check.py; python3 bench/cross_lang.py; echo "exit: $?" Expected: the default-executable codegen/runtime path is byte- unchanged (the target param defaults every existing caller to Executable); bench trio carry-on per spec Testing item 7. Any check.py firing is adjudicated at milestone-close audit against the tracked P2 *.bump_s / *.max_us known-noise items — not a plan-level gate.

---

Self-review (planner Step 5)

1. Spec coverage. Schema §1 → Task 2. Surface §2 → Task 3. Check §3 → Task 4. Codegen §4 → Task 5. CLI §5 → Task 6. Host harness §6 → Task 7. Testing item 0 → Task 1 (fixed first, per spec §"Iteration sequencing"). Testing 1 (round-trip/hash) → Tasks 2+3. Testing 2 (schema drift) → Task 2 Step 8. Testing 3 (check RED, 3 must-fail + positive) → Task 4. Testing 4 (codegen) → Task 5. Testing 5 (E2E) → Task 7. Testing 6 (clean-core invariant) → architect at close (no new dep added by any task; asserted by Task-7 Step-6 having no Cargo.toml edit anywhere in this plan). Testing 7 (bench trio) → Task 7 Step 6. Acceptance §1/§3 → the worked examples/embed_backtest_step.ail + the must-fail fixtures (in code, not prose). Every spec section maps to a task.
2. Placeholder scan. No "TBD"/"implement later"/"similar to". The two <<GOLDEN-PLACEHOLDER>> (Task 2) and the *. Float-head / exact-public-symbol notes are deterministic capture-then-pin or named cross-checks against a cited line, not design holes — each has an exact resolution step. The compile-driven enumeration (Task 2 Step 5) is a deterministic loop with an exact terminating gate (cargo build --workspace exits 0), not "fill in later".
3. Type/name consistency. FnDef.export / lower_workspace_staticlib_with_alloc / Target::StaticLib / ExportNonScalarSignature / export-non-scalar-signature / ExportHasEffects / export-has-effects / build_staticlib / libembed_backtest_step.a / libailang_rt.a / backtest_step (the C symbol) / @ail_embed_backtest_step_step (internal) — used identically across every task that references them. Module == file stem embed_backtest_step ⇒ entry embed_backtest_step ⇒ lib embed_backtest_step.a = libembed_backtest_step.a (Design-decision 6; the C symbol backtest_step is decoupled and invariant per spec Decision 2).
4. Step granularity. Every step is one action ≤5 min; the only long one (Task 2 Step 5, the ~95-site thread) is a single compile-driven mechanical loop with a hard terminating gate — it is one logical action, not a hidden multi-decision step.
5. No commit steps. None present.
6. Pin/replacement substring contiguity. Task 1 asserts contains("has no \main` def")— that substring is the *existing*CodegenError::MissingEntryMain Display (codegen lib.rs:129), not produced by any verbatim replacement in this plan; no soft-wrap split. Task 6's contains("at least one `(export")is matched against thebuild_staticlib anyhow::bail!literal in Task 6 Step 4, which containsat least one `(export "")` fn` contiguously on one line. Task 7 §"Embedding ABI (M1)" carries no presence-pin. Clean.
7. Compile-gate vs deferred-caller ordering. Task 2 (the FnDef-field add — crate-wide compile break) threads ALL ~95 caller sites inside the same task and only then runs the cargo build --workspace 0-errors gate (Step 6). Task 5 (the lower_workspace_inner signature change) updates all three internal callers + the public wrapper inside the same task before its cargo test -p ailang-codegen gate (Step 8). No signature change defers a caller past its own compile gate.
8. Verification-command filter strings resolve. cargo test -p ail --test embed_missing_main_baseline / --test roundtrip_cli / --test embed_staticlib_cli / --test embed_e2e / --test floats_e2e, cargo test -p ailang-check --test embed_export_gate, cargo test -p ailang-codegen --test embed_staticlib_lowering, cargo test -p ailang-core --test embed_export_hash_stable / --test design_schema_drift / --test spec_drift — each --test <name> targets a file this plan creates (or an existing one: roundtrip_cli, floats_e2e, design_schema_drift, spec_drift, hash_pin verified present by recon). cargo test -p ailang-codegen missing_entry_main_is_error is the verified in-source test name (lib.rs:3314). No filter resolves to zero tests masquerading as success.

Plan ready for implement.