# Embedding ABI — M1.1 — Implementation Plan

> **Parent spec:** `docs/specs/2026-05-18-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).

---

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

```rust
//! 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\` def` substring + absent-binary triple
fails if any of (a) `MissingEntryMain` stops firing, (b) the message
text drifts, (c) a binary is emitted anyway. The verbatim substring
`has no \`main\` def` is the exact `CodegenError::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`:

```rust
//! 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: the `content_hash_fn` symbol + `Type::fn_implicit` /
> `Term::Var` constructors are the ones already used by
> `crates/ailang-core/tests/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):

```rust
    /// 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** reported `FnDef { … }` literal (production AND in-source
`#[cfg(test)] mod tests` AND integration tests), add the line
`export: None,` to that literal. Known non-production sites that MUST
be threaded (the in-source-test blind spot — see
`feedback_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` (its `FnDef` literal(s)),
plus the ~50 in-source `mod tests` literals recon enumerated
(`mono.rs` uses the alias `AstFnDef = 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,
verbatim):

```
(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 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\`` (current `parse_fn` modifier 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):

```rust
    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:
```rust
        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):
```rust
                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:
```rust
                            "unknown fn attribute `{other}`; expected `doc`, `suppress`, `type`, `params`, or `body`"
```
to:
```rust
                            "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,`:
```rust
        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):

```rust
    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 bad_str_param
  (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 bad_adt_ret
  (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 bad_io
  (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 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))))
```

`examples/embed_export_float_ok.ail` (positive — `(Float,Float)->Float`,
pure; the second scalar type beyond the Int headline):
```
(module embed_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))))
```

> The implementer verifies `*.` is the Form-A Float-multiply head
> against an existing Float example (`examples/floats.ail`); if the
> Float-multiply surface differs, use the same head that example
> uses. The fixture's *role* is "scalar+pure export passes the gate".

- [ ] **Step 2: Write the gate pin — verify RED**

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

```rust
//! 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:

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

```rust
            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`:

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

```rust
//! Embedding-ABI M1 codegen (spec §4): `Target::StaticLib` lowering
//! emits NO `@main` trampoline, NO `MissingEntryMain`, and one
//! external `define i64 @backtest_step(...)` forwarding to
//! `@ail_backtest_step`. 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");
    assert!(ir.contains("@ail_backtest_step("),
        "the forwarder must call the internal @ail_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:

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

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

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

```rust
    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):

```rust
/// 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`, forwards to `@ail_backtest_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`:

```rust
//! 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("libbacktest.a").exists(),
        "expected libbacktest.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:

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

```rust
        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:

```rust
/// 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 `libbacktest.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):

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

- [ ] **Step 2: Write the E2E coherent-stop pin — verify RED**

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

```rust
//! 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 `libbacktest.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("libbacktest.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 — `libbacktest.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":

```markdown
### 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` /
   `libbacktest.a` / `libailang_rt.a` / `backtest_step` — used
   identically across every task that references them. Module
   `backtest` ⇒ entry `backtest` ⇒ `lib backtest.a` = `libbacktest.a`
   (spec-exact).
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 the
   `build_staticlib` `anyhow::bail!` literal in Task 6 Step 4, which
   contains `at least one \`(export "<sym>")\` 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`.