diff --git a/bench/orchestrator-stats/2026-05-18-iter-embedding-abi-m1.1.json b/bench/orchestrator-stats/2026-05-18-iter-embedding-abi-m1.1.json
index 17786b7..9f4cf67 100644
--- a/bench/orchestrator-stats/2026-05-18-iter-embedding-abi-m1.1.json
+++ b/bench/orchestrator-stats/2026-05-18-iter-embedding-abi-m1.1.json
@@ -2,22 +2,31 @@
   "iter_id": "embedding-abi-m1.1",
   "date": "2026-05-18",
   "mode": "standard",
-  "outcome": "PARTIAL",
+  "outcome": "DONE",
   "tasks_total": 7,
-  "tasks_completed": 3,
-  "reloops_per_task": { "1": 0, "2": 0, "3": 0, "4": 0 },
+  "tasks_completed": 7,
+  "reloops_per_task": { "1": 0, "2": 0, "3": 0, "4": 0, "5": 0, "6": 0, "7": 0 },
   "review_loops_spec": 0,
   "review_loops_quality": 0,
-  "blocked_reason": "spec-ambiguous",
+  "blocked_reason": null,
   "notes": {
-    "blocked_task": 4,
-    "blocked_detail": "load_workspace stem-match (workspace.rs:182 ModuleNameMismatch) is mutually unsatisfiable with the plan's verbatim fixtures (spec-mandated module `backtest` in file embed_backtest_step.ail; bad/bad_io/... in embed_export_*_rejected.ail) plus the verbatim load_workspace-based gate pin. Structural spec/plan defect rippling Tasks 4-7; Boss/spec decision required (Option 1: rename fixture files to module stems, keep module backtest).",
+    "dispatch_history": "Two dispatches. First dispatch: Tasks 1-3 DONE + Boss-committed at 818177d; Task 4 BLOCKED (spec-ambiguous) on a Boss plan-defect (fixtures declared module != file-stem; loader hard-enforces module == file-stem at workspace.rs:438). Boss Repaired the plan (Design-decision 6 / Option 2: module == file stem, C symbol decoupled via (export ...)) and re-dispatched task_range [4,7]. Second dispatch (this run): Tasks 4-7 all DONE on the corrected plan, zero re-loops, zero review loops.",
+    "first_dispatch_block": {
+      "blocked_task": 4,
+      "blocked_reason": "spec-ambiguous",
+      "resolution": "Boss plan Repair (Design-decision 6, Option 2 over the orchestrator-recommended Option 1) + Tasks 4-7 re-dispatch; resolved cleanly."
+    },
     "concerns": [
-      "Task 2: plan symbol content_hash_fn(&FnDef) nonexistent; mirrored hash_pin.rs def_hash(&Def) per the plan NOTE's own resolution clause (planner pseudo-vs-reality class).",
-      "Task 4: plan fixture `*.` Float-multiply head nonexistent; used the typeclass-generic `*` head per the plan NOTE (not yet exercised — gate BLOCKED before run).",
-      "INFRA: docs/roadmap.md externally modified mid-session; path-disjoint from iter; left untouched (Boss-owned)."
+      "Task 2 (committed at 818177d): plan symbol content_hash_fn(&FnDef) nonexistent; mirrored hash_pin.rs def_hash(&Def) per the plan NOTE (planner pseudo-vs-reality class).",
+      "Task 4: no `*.` Float-multiply head; embed_export_float_ok.ail uses `(app * a b)` per the corrected plan (concern folded into the plan Repair; now exercised — gate GREEN).",
+      "Task 5: plan Step 3(b) says emit_ir calls lower_workspace_inner directly; reality emit_ir->lower_workspace->lower_workspace_inner(_,_,Executable). Intent (in-source missing_entry_main_is_error pin byte-unchanged) delivered + verified GREEN; behaviour-neutral planner pseudo-vs-reality note.",
+      "Task 7: plan-verbatim embed_e2e.rs imported unused std::path::Path; reduced to PathBuf (warning-clean, behaviour-identical).",
+      "Task 7: plan code-block showed `### Embedding ABI (M1)` but the same step's prose says 'same heading level as Mangling scheme' (## in DESIGN.md); used ## for document consistency.",
+      "INFRA (first dispatch, resolved): docs/roadmap.md externally modified mid-session; Boss-committed separately as roadmap maintenance; NOT in the Tasks 4-7 working tree."
     ],
-    "fnDef_threading_sites": "~85 export:None literals across 18 files via compile-driven enumeration (2 dependency-ordered waves), cargo build --workspace exits 0",
-    "tests_state": "Tasks 1-3 + pre-existing all green; only the deliberately-RED embed_export_gate (6 tests) fails workspace-wide"
+    "cross_checks_executed": "All six named implementer-judgement cross-checks resolved as plan-confirming (Type::Con {name,args} no mode field; declared_effs already Vec<String> so no into_iter().collect() needed; synth::llvm_type Int->i64/Float->double exact mirror; no pre-existing run_cmd; ailang_core::Def crate-root re-exported; load_workspace/check_workspace/Diagnostic.code are the main.rs:580-581 symbols).",
+    "tests_state": "Full workspace 0 failures. New: embed_export_gate 6/6, embed_staticlib_lowering 2/2, embed_staticlib_cli 2/2, embed_e2e 1/1 (coherent-stop). roundtrip_cli green; codegen in-source missing_entry_main_is_error green; design_schema_drift 8/8 + spec_drift 8/8.",
+    "bench_trio": "compile_check.py exit 0; cross_lang.py exit 0; check.py exit 1 = tracked P2 *.bump_s / *.max_us known-noise envelope (3 regressed/2 improved/58 stable), plan Step 6 = audit-adjudicated not a plan gate; architect_sweeps.sh exit 1 pre-existing both with/without the DESIGN.md edit (no new flagged phrasing introduced).",
+    "fnDef_threading_sites": "~85 export:None literals across 18 files (committed at 818177d, Task 2)"
   }
 }
diff --git a/crates/ail/src/main.rs b/crates/ail/src/main.rs
index 18798d5..e1dc0c8 100644
--- a/crates/ail/src/main.rs
+++ b/crates/ail/src/main.rs
@@ -137,6 +137,14 @@ enum Cmd {
         /// every allocation by design.
         #[arg(long, default_value = "rc", value_parser = ["gc", "bump", "rc"])]
         alloc: String,
+        /// 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,
     },
     /// Build into a tempdir and execute. Exits with the binary's exit code.
     /// Convenience wrapper around `build` + invocation of the resulting
@@ -688,10 +696,15 @@ fn main() -> Result<()> {
                 None => print!("{ir}"),
             }
         }
-        Cmd::Build { path, out, opt, alloc } => {
+        Cmd::Build { path, out, opt, alloc, emit } => {
             let strategy = parse_alloc_strategy(&alloc)?;
-            let bin = build_to(&path, out, &opt, strategy)?;
-            eprintln!("built {}", bin.display());
+            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());
+            }
         }
         Cmd::Run { path, opt, alloc, args } => {
             // Iter 9b: build into a fresh tempdir per run, exec, propagate
@@ -2404,6 +2417,110 @@ fn build_to(
     Ok(out_bin)
 }
 
+/// 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 → libailang_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(())
+}
+
 /// ct.1 migration helper: rewrite bare cross-module Type::Con names
 /// and Term::Ctor.type_name to their qualified form. Sets
 /// `*changed` to `true` if any rewrite happened. Uses the
diff --git a/crates/ail/tests/embed/host.c b/crates/ail/tests/embed/host.c
new file mode 100644
index 0000000..cc59f04
--- /dev/null
+++ b/crates/ail/tests/embed/host.c
@@ -0,0 +1,10 @@
+#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;
+}
diff --git a/crates/ail/tests/embed_e2e.rs b/crates/ail/tests/embed_e2e.rs
new file mode 100644
index 0000000..634c191
--- /dev/null
+++ b/crates/ail/tests/embed_e2e.rs
@@ -0,0 +1,46 @@
+//! 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::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));
+}
diff --git a/crates/ail/tests/embed_staticlib_cli.rs b/crates/ail/tests/embed_staticlib_cli.rs
new file mode 100644
index 0000000..d2f679c
--- /dev/null
+++ b/crates/ail/tests/embed_staticlib_cli.rs
@@ -0,0 +1,57 @@
+//! 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));
+}
diff --git a/crates/ailang-check/src/lib.rs b/crates/ailang-check/src/lib.rs
index aa3069f..87ab435 100644
--- a/crates/ailang-check/src/lib.rs
+++ b/crates/ailang-check/src/lib.rs
@@ -444,6 +444,20 @@ pub enum CheckError {
     #[error("const `{0}` may not have effects (got !{1:?})")]
     ConstHasEffects(String, Vec<String>),
 
+    /// 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>),
+
     /// A `Type::Con` named a type not in [`Env::types`] or with a wrong
     /// arity for a parameterised ADT. Code: `unknown-type`.
     #[error("unknown type: `{0}`")]
@@ -695,6 +709,8 @@ impl CheckError {
             CheckError::ParamCountMismatch { .. } => "param-count-mismatch",
             CheckError::PolymorphicNotSupported(_) => "polymorphic-not-supported",
             CheckError::ConstHasEffects(..) => "const-has-effects",
+            CheckError::ExportNonScalarSignature(..) => "export-non-scalar-signature",
+            CheckError::ExportHasEffects(..) => "export-has-effects",
             CheckError::UnknownType(_) => "unknown-type",
             CheckError::UnknownCtor { .. } => "unknown-ctor",
             CheckError::UnknownCtorInPattern(_) => "unknown-ctor-in-pattern",
@@ -1895,6 +1911,41 @@ fn check_fn(f: &FnDef, env: &Env, out_warnings: &mut Vec<Diagnostic>) -> Result<
     }
     check_type_well_formed(&ret_ty, &env)?;
 
+    // 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(),
+            ));
+        }
+    }
+
     // mq.3: build the post-superclass-expansion declared-constraint
     // set ONCE here and stash on env, so synth's Var-arm class-method
     // branch can hand it to `resolve_method_dispatch`'s constraint-
diff --git a/crates/ailang-check/tests/embed_export_gate.rs b/crates/ailang-check/tests/embed_export_gate.rs
new file mode 100644
index 0000000..2b6d249
--- /dev/null
+++ b/crates/ailang-check/tests/embed_export_gate.rs
@@ -0,0 +1,63 @@
+//! 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:?}");
+}
diff --git a/crates/ailang-codegen/src/lib.rs b/crates/ailang-codegen/src/lib.rs
index 02f1d92..5bb3c56 100644
--- a/crates/ailang-codegen/src/lib.rs
+++ b/crates/ailang-codegen/src/lib.rs
@@ -162,6 +162,19 @@ pub enum AllocStrategy {
     Rc,
 }
 
+/// 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,
+}
+
 impl AllocStrategy {
     /// LLVM IR-level name of the allocator fn (without leading `@`).
     fn fn_name(self) -> &'static str {
@@ -221,7 +234,17 @@ pub fn emit_ir(m: &Module) -> Result<String> {
 /// `runtime/bump.c`). Used by `ail build --alloc=bump` to quantify the
 /// GC's runtime overhead via an A/B comparison.
 pub fn lower_workspace_with_alloc(ws: &Workspace, alloc: AllocStrategy) -> Result<String> {
-    lower_workspace_inner(ws, alloc)
+    lower_workspace_inner(ws, alloc, Target::Executable)
+}
+
+/// 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)
 }
 
 /// Multi-module entry point. Lowers an entire [`Workspace`] (entry
@@ -250,10 +273,10 @@ pub fn lower_workspace_with_alloc(ws: &Workspace, alloc: AllocStrategy) -> Resul
 /// Use [`emit_ir`] for the single-file shortcut when there are no
 /// imports.
 pub fn lower_workspace(ws: &Workspace) -> Result<String> {
-    lower_workspace_inner(ws, AllocStrategy::Gc)
+    lower_workspace_inner(ws, AllocStrategy::Gc, Target::Executable)
 }
 
-fn lower_workspace_inner(ws: &Workspace, alloc: AllocStrategy) -> Result<String> {
+fn lower_workspace_inner(ws: &Workspace, alloc: AllocStrategy, target: Target) -> Result<String> {
     // Iter 16a: desugar every module before any lowering work runs.
     // The pass is idempotent and structurally identical to what
     // `ailang-check` runs at its public entries, so the codegen
@@ -417,17 +440,20 @@ fn lower_workspace_inner(ws: &Workspace, alloc: AllocStrategy) -> Result<String>
     }
 
     // Trampoline: verify that the entry module has a
-    // `main : () -> Unit !IO`. If not, the workspace isn't runnable.
-    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()));
+    // `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()));
+        }
     }
 
     let mut out = String::new();
@@ -551,15 +577,81 @@ fn lower_workspace_inner(ws: &Workspace, alloc: AllocStrategy) -> Result<String>
     out.push_str(&header);
     out.push_str(&body);
 
-    // 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
-    ));
+    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(", "),
+                            ));
+                        }
+                    }
+                }
+            }
+        }
+    }
 
     Ok(out)
 }
 
+/// 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",
+    }
+}
+
 fn main_is_void(t: &Type) -> bool {
     match t {
         Type::Fn { params, ret, .. } => {
diff --git a/crates/ailang-codegen/tests/embed_staticlib_lowering.rs b/crates/ailang-codegen/tests/embed_staticlib_lowering.rs
new file mode 100644
index 0000000..0025967
--- /dev/null
+++ b/crates/ailang-codegen/tests/embed_staticlib_lowering.rs
@@ -0,0 +1,44 @@
+//! 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}");
+}
diff --git a/docs/DESIGN.md b/docs/DESIGN.md
index d90eaf5..e8f6401 100644
--- a/docs/DESIGN.md
+++ b/docs/DESIGN.md
@@ -2260,6 +2260,30 @@ overlay shape. The asymmetry between the check side and the mono
 side is by design and is pinned by
 `crates/ailang-check/tests/duplicate_ctor_pin.rs`.
 
+## 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.
+
 ## Data model
 
 The on-disk JSON-AST is what the toolchain hashes, typechecks, and
diff --git a/docs/journals/2026-05-18-iter-embedding-abi-m1.1.md b/docs/journals/2026-05-18-iter-embedding-abi-m1.1.md
index 7c735a7..afa57a8 100644
--- a/docs/journals/2026-05-18-iter-embedding-abi-m1.1.md
+++ b/docs/journals/2026-05-18-iter-embedding-abi-m1.1.md
@@ -2,38 +2,52 @@
 
 **Date:** 2026-05-18
 **Started from:** b0bd7efeaff137af22bb12f5e751260804e770c3
-**Status:** PARTIAL — Tasks 1–3 committed as a known-good subset
-(see "Boss resolution" below); plan defect fixed; Tasks 4–7
-re-dispatched on the corrected plan.
-**Tasks completed:** 3 of 7 (Tasks 1–3 DONE + committed; Task 4
-BLOCKED on a Boss plan-defect — fixture module≠stem — before any
-gate code was written; resolved by Boss + re-dispatched; Tasks
-5–7 follow in the re-dispatch)
+(Tasks 1–3 committed at 818177d; Tasks 4–7 re-dispatched from 818177d)
+**Status:** DONE — all 7 tasks complete. Tasks 1–3 committed
+(818177d); Tasks 4–7 implemented on the corrected plan and sit
+unstaged in the working tree. The E2E coherent-stop proof
+(`embed_e2e.rs`: `cc` link + run, `s == 25`, exit 0) is GREEN.
+**Tasks completed:** 7 of 7 (Tasks 1–3 DONE + committed; Task 4
+initially BLOCKED on a Boss plan-defect — fixture module≠stem —
+resolved by Boss plan Repair [Design-decision 6] + re-dispatch;
+Tasks 4–7 then completed cleanly on the corrected plan)
 
 ## Summary
 
-Tasks 1–3 of the Embedding-ABI M1 plan landed cleanly: the CLI
-build-path `MissingEntryMain` baseline pin (Task 1), the additive
+The Embedding-ABI M1 iter is complete across all 5 pipeline
+layers. Tasks 1–3 landed in the first dispatch and were committed
+(818177d) as a verified known-good subset: the CLI build-path
+`MissingEntryMain` baseline pin (Task 1), the additive
 `FnDef.export: Option<String>` schema field threaded across the
 whole workspace via compile-driven enumeration with a hash-stability
 golden pin (Task 2), and the Form-A `(export "<sym>")` surface
 modifier with full parse/print/grammar lockstep and a byte-identical
-round-trip (Task 3). Task 4 (the check-side export-signature gate)
-is BLOCKED before any production code: the plan's verbatim gate-pin
-test (`crates/ailang-check/tests/embed_export_gate.rs`, using
-`ailang_surface::load_workspace`) is mutually unsatisfiable with the
-plan's verbatim fixtures, because `load_workspace` hard-enforces
-`module-name == file-stem` (`crates/ailang-core/src/workspace.rs:182`
-`ModuleNameMismatch`) while the fixtures (spec-mandated module
-`backtest` in file `embed_backtest_step.ail`; `bad`/`bad_io`/… in
-`embed_export_*_rejected.ail`) deliberately diverge module name from
-filename. This is not an implementer-judgement cross-check (the six
-named ones were executed where reached) — it is a structural
-contradiction that ripples across Tasks 4–7 and can only be resolved
-by a Boss/spec-level decision. Per the Iron Law (`unclear` spec
-ambiguity → BLOCKED, no implementing on a hunch), the iter stopped.
-Tasks 1–3 sit clean and green in the working tree; only the
-deliberately-RED Task 4 pin fails workspace-wide.
+round-trip (Task 3).
+
+Task 4 was BLOCKED in the first dispatch on a Boss plan-defect
+(fixtures declared `module ≠ file-stem`; the loader hard-enforces
+`module == file-stem` at `workspace.rs:438`). The Boss Repaired the
+plan (Design-decision 6: fixture `(module …)` == file stem; the
+C symbol stays `backtest_step` via `(export …)`, demonstrating spec
+Decision 2's mangling-decoupling) and re-dispatched Tasks 4–7. On
+the corrected plan all four landed cleanly: the check-side
+scalar-only + effect-free export gate with two new `CheckError`
+variants (`export-non-scalar-signature` / `export-has-effects`, the
+clause-3 discriminator *in code*, Task 4); the codegen
+`Target::StaticLib` mode suppressing `@main`/`MissingEntryMain` and
+emitting one external `@<sym>` forwarder per export to
+`@ail_<module>_<fn>` (Task 5); the CLI `ail build --emit=staticlib`
+two-archive emit (`libembed_backtest_step.a` + `libailang_rt.a`,
+Task 6); and the C-host E2E coherent-stop proof — `cc` links both
+archives, calls `backtest_step(0,3)=9`, `backtest_step(9,4)=25`,
+the `s == 25` assertion holds, exit 0 (Task 7), plus the DESIGN.md
+§"Embedding ABI (M1)" current-state subsection. Full workspace
+green (0 failures); `roundtrip_cli` green; `compile_check.py` /
+`cross_lang.py` exit 0; `check.py` fires only the tracked P2
+`*.bump_s` / `*.max_us` known-noise envelope (plan Step 6: audit-
+adjudicated, not a plan-level gate — the default-executable
+codegen/runtime path is byte-unchanged). No clean-core dependency
+added (Invariant 1).
 
 ## Per-task notes
 
@@ -70,12 +84,66 @@ deliberately-RED Task 4 pin fails workspace-wide.
   `(export STRING)?` + prose paragraph. RED verified
   (`unknown fn attribute \`export\``), then GREEN: round-trip gate
   byte-identical, surface crate 72/0, ailang-core 111/0. DONE.
-- iter embedding-abi-m1.1.4: check-side export-signature gate.
-  Wrote the five plan fixtures + the verbatim gate pin; ran it →
-  RED for the WRONG reason (a `ModuleNameMismatch` load failure,
-  not the absence of the gate). BLOCKED — see Blocked detail.
-  No `CheckError` variant, no `code()` arm, no `check_fn` gate
-  written.
+- iter embedding-abi-m1.1.4 (FIRST dispatch — BLOCKED, audit
+  trail): wrote the five plan fixtures + the verbatim gate pin; ran
+  it → RED for the WRONG reason (a `ModuleNameMismatch` load
+  failure, not the absence of the gate). BLOCKED — see Blocked
+  detail + Boss resolution. No gate production code written; the
+  WIP fixtures + RED test were discarded by the Boss for the
+  re-dispatch.
+- iter embedding-abi-m1.1.4 (RE-dispatch — DONE): check-side
+  export-signature gate on the corrected plan (Design-decision 6,
+  module==stem). Recreated the five fixtures (module == file stem;
+  `embed_export_float_ok.ail` uses `(app * a b)` — no `*.` head)
+  + the verbatim gate pin `crates/ailang-check/tests/embed_export_gate.rs`.
+  RED verified for the RIGHT reason (fixtures load cleanly, 4
+  `*_rejected` fail because no gate exists, 2 positives already
+  pass). Added two `CheckError` Error variants
+  (`ExportNonScalarSignature(String,&'static str,String)` /
+  `ExportHasEffects(String,Vec<String>)`) after `ConstHasEffects`,
+  their two `code()` arms, and the gate in `check_fn` after the
+  param/ret well-formedness checks (gate order params→ret→effects,
+  first-violation-wins, unconditional on `f.export.is_some()`).
+  GREEN 6/6; combined fixture fails signature-first. Round-trip +
+  full workspace green. DONE.
+- iter embedding-abi-m1.1.5: codegen `Target::StaticLib`. Added the
+  `Target` enum next to `AllocStrategy`; threaded `target` through
+  `lower_workspace_inner`; `lower_workspace_with_alloc` /
+  `lower_workspace` pin `Target::Executable`; new public
+  `lower_workspace_staticlib_with_alloc`. Gated the
+  `MissingEntryMain` shape-check + the `@main` trampoline behind
+  `Target::Executable`; the `StaticLib` arm emits one external
+  `define {cret} @<sym>(...)` per `(export …)` fn forwarding to
+  `@ail_<module>_<fn>` via the new `fn_scalar_sig` / `llvm_scalar`
+  helpers. RED→GREEN IR-shape pin (no `@main`, has `@backtest_step`,
+  forwards to `@ail_embed_backtest_step_step`; exe target still
+  `MissingEntryMain`). In-source `missing_entry_main_is_error` pin
+  byte-unchanged; codegen crate 0 failures. DONE_WITH_CONCERNS
+  (the `emit_ir`-routes-via-`lower_workspace` plan note).
+- iter embedding-abi-m1.1.6: CLI `ail build --emit=staticlib`.
+  Added the `--emit` clap field (`value_parser = ["exe",
+  "staticlib"]`, default `exe`) after `alloc`; branched
+  `Cmd::Build` (`emit == "staticlib"` → `build_staticlib`); added
+  `build_staticlib` (verbatim `build_to:2239–2294` shared prefix +
+  `has_export` guard + `lower_workspace_staticlib_with_alloc` +
+  two-archive `clang -c`/`ar rcs` tail) and the new shared `run_cmd`
+  helper (confirmed no pre-existing equivalent). RED→GREEN CLI pin
+  (`libembed_backtest_step.a` + `libailang_rt.a` produced;
+  export-less module rejected with the zero-export error).
+  Default-exe regression (floats E2E + Task-1 baseline) green.
+  DONE.
+- iter embedding-abi-m1.1.7: E2E host harness + DESIGN.md
+  §"Embedding ABI (M1)". Wrote `crates/ail/tests/embed/host.c`
+  (spec headline host, verbatim) + `crates/ail/tests/embed_e2e.rs`.
+  E2E GREEN — `cc` links `libembed_backtest_step.a` +
+  `libailang_rt.a`, runs the host, `backtest_step(0,3)=9` /
+  `backtest_step(9,4)=25`, `s == 25` assertion holds, exit 0 (the
+  milestone coherent stop). Added the DESIGN.md §"Embedding ABI
+  (M1)" subsection (verbatim prose, at `##` level for consistency
+  with §"Mangling scheme"). Drift tests 8/8 + 8/8; full workspace
+  0 failures; bench trio per plan Step 6. DONE_WITH_CONCERNS (the
+  dead-`Path`-import correction + the `###`-vs-`##` heading-level
+  resolution).
 
 ## Concerns
 
@@ -109,21 +177,94 @@ deliberately-RED Task 4 pin fails workspace-wide.
   writer. It is path-disjoint from every iter file. Left untouched
   (roadmap.md is Boss-owned per CLAUDE.md; main HEAD sacrosanct).
   The Boss must decide independently whether to keep or discard it;
-  it is NOT part of this iter's commit.
+  it is NOT part of this iter's commit. (RESOLVED at Boss
+  re-dispatch: committed separately as Boss roadmap maintenance —
+  see Boss resolution. Not part of the Tasks 4–7 working tree.)
+- iter embedding-abi-m1.1.5 (plan pseudo-vs-reality, behaviour-
+  neutral): plan Task-5 Step 3(b) third bullet says "`emit_ir`
+  (line 197): its internal `lower_workspace_inner` call passes
+  `Target::Executable`". Reality: `emit_ir` does NOT call
+  `lower_workspace_inner` directly — it calls `lower_workspace`
+  (`codegen lib.rs:214`), which now passes
+  `lower_workspace_inner(ws, AllocStrategy::Gc, Target::Executable)`.
+  The plan's *intent* (the in-source `missing_entry_main_is_error`
+  pin, which calls `emit_ir`, stays byte-unchanged) is delivered
+  transitively and verified GREEN at Task-5 Step 7. Recorded
+  because the plan's literal call-chain description was inaccurate
+  (planner pseudo-vs-reality family); no behavioural deviation.
+- iter embedding-abi-m1.1.7 (plan-verbatim transcription defect,
+  corrected): the plan's verbatim Task-7 `embed_e2e.rs` imports
+  `std::path::{Path, PathBuf}` but the test body uses only
+  `PathBuf` — a transcribed unused import that raises
+  `unused_imports` on every build. Implementer-mindset judgement:
+  a verbatim copy that introduces a compiler warning is not the
+  plan's intent; reduced to `use std::path::PathBuf;`. Test
+  behaviour byte-identical (E2E still GREEN). Recorded as a
+  deviation from plan-literal text in service of plan intent.
+- iter embedding-abi-m1.1.7 (plan code-block vs plan prose, design
+  consistency): plan Task-7 Step 4's code block shows the new
+  section as `### Embedding ABI (M1)`, but the same step's prose
+  instruction says "at the same heading level as §"Mangling
+  scheme"" — §"Mangling scheme" is `## ` (level-2) in DESIGN.md.
+  Used `## Embedding ABI (M1)` for structural consistency with the
+  surrounding §"Mangling scheme" / §"Data model" level-2 sections,
+  following the plan's explicit prose directive over its
+  illustrative code-block `#`-count. Section content byte-verbatim.
+- iter embedding-abi-m1.1 (cross-checks, plan-confirming, no
+  deviation): the six named implementer-judgement cross-checks were
+  executed. (a) `Type::Con` has exactly `{name: String, args:
+  Vec<Type>}` — no mode field; the plan's `matches!` guard is
+  correct. (b) `declared_effs` is already `Vec<String>` (per
+  `lib.rs` `declared_effs.into_iter().collect()`), so the plan's
+  conditional `.into_iter().collect()` conversion did NOT apply —
+  `.clone()` matches `ExportHasEffects(_, Vec<String>)` exactly.
+  (c) `synth::llvm_type` lowers `Int`→`"i64"`, `Float`→`"double"`
+  (`synth.rs:17,21`) — the plan's `llvm_scalar` is an exact mirror
+  for the 2-scalar M1 subset; forwarder `call` types match
+  `@ail_<module>_<fn>`'s emitted signature (also proven by the
+  Task-7 E2E real `cc` link + run). (d) no pre-existing `run_cmd`
+  helper in `main.rs` (only inline `Command::new` blocks) — adding
+  it was correct per the plan. (e) `ailang_core::Def` is crate-root
+  re-exported (`ailang-core lib.rs:76`) — `ailang_core::Def::Fn`
+  valid in `main.rs`. (f) `ailang_surface::load_workspace` +
+  `ailang_check::check_workspace` + `Diagnostic.code: String` are
+  the exact `main.rs:580–581` public symbols. All confirmations of
+  plan assumptions, not contradictions.
 
 ## Known debt
 
-- Tasks 5 (codegen `Target::StaticLib`), 6 (CLI `--emit=staticlib`),
-  7 (E2E host harness + DESIGN.md §"Embedding ABI (M1)") not reached
-  — they depend on Task 4's gate (Task 5's forwarder loop trusts the
-  gate; Task 6/7 build on the headline fixture). Not touched because
-  the iter is BLOCKED upstream of them; no speculative partial work.
-- E2E coverage (Phase 3) not written — the iter did not reach
-  completion; the Task 7 host-harness is the milestone's coherent-
-  stop proof and is downstream of the block.
+- None blocking. The M1 ABI is deliberately scalar-only and
+  provisional until M3 (no `Bool`/`Str`/ADT/record marshalling, no
+  per-thread context lifecycle API); this is reserved-unimplemented
+  scope, labelled in DESIGN.md §"Embedding ABI (M1)", not debt.
+- `check.py` fires the tracked P2 `*.bump_s` / `*.max_us`
+  known-noise envelope (3 regressed / 2 improved beyond tolerance /
+  58 stable; e.g. `throughput.bench_list_sum.bump_s` +13.95%,
+  `latency.explicit_at_rc.max_us` +60.61%). This iter touched only
+  check-side gating, a codegen `Target` enum (every existing path
+  pinned `Executable`), and CLI dispatch — none on the runtime hot
+  path these metrics measure; the default-executable codegen/runtime
+  path is byte-unchanged (Task-5 Step 7/8 + Task-6 Step 6 confirm).
+  Per plan Step 6 this is milestone-close-`audit`-adjudicated, NOT
+  a plan-level gate. `compile_check.py` / `cross_lang.py` exit 0.
+- `bench/architect_sweeps.sh` exits 1 both with and without the
+  DESIGN.md edit (pre-existing advisory residue, established
+  carry-on adjudicated at milestone-close `audit`); the new
+  §"Embedding ABI (M1)" introduced no new Wunschdenken / post-
+  mortem phrasing (the "provisional until M3" / "M2 will change"
+  clauses are labelled reserved-unimplemented, which the DESIGN.md
+  honesty rule explicitly permits).
 
 ## Blocked detail
 
+> **RESOLVED (2026-05-18, re-dispatch).** This block was a
+> first-dispatch event; it was resolved by the Boss plan Repair
+> (see "## Boss resolution" below — Design-decision 6, Option 2,
+> module==stem) and the Tasks 4–7 re-dispatch completed all four
+> tasks cleanly. The detail below is **preserved verbatim as the
+> iter's audit trail** and is no longer an open block. Iter status
+> is DONE.
+
 **Task:** 4 (check-side export-signature gate)
 **Reason:** spec-ambiguous (a spec-internal contradiction that
 rippling-binds Tasks 4–7, surfaced as `unclear` per the per-task
@@ -279,6 +420,8 @@ into this iter.
 
 ## Files touched
 
+### Committed at 818177d (Tasks 1–3, first dispatch)
+
 Schema / canonical docs:
 - crates/ailang-core/src/ast.rs (FnDef.export field)
 - docs/DESIGN.md (fn-JSON "export" line)
@@ -296,21 +439,35 @@ Surface modifier (Task 3):
 - crates/ailang-surface/src/parse.rs (parse_export + parse_fn thread)
 - crates/ailang-surface/src/print.rs (write_fn_def export block)
 
-New files (untracked):
+New files committed at 818177d:
 - examples/embed_noentry_baseline.ail
-- examples/embed_backtest_step.ail
+- examples/embed_backtest_step.ail (corrected to `(module embed_backtest_step)`)
+- crates/ail/tests/embed_missing_main_baseline.rs
+- crates/ailang-core/tests/embed_export_hash_stable.rs
+
+### Tasks 4–7 re-dispatch working tree (UNCOMMITTED — this hand-off)
+
+Modified (4 source/doc files):
+- crates/ailang-check/src/lib.rs (2 CheckError variants + 2 code() arms + check_fn gate; +51)
+- crates/ailang-codegen/src/lib.rs (Target enum + threaded target + forwarder loop + fn_scalar_sig/llvm_scalar; +130/-22)
+- crates/ail/src/main.rs (--emit clap field + Cmd::Build branch + build_staticlib + run_cmd; +123)
+- docs/DESIGN.md (new §"Embedding ABI (M1)" subsection; +24)
+
+New files (untracked, this re-dispatch):
 - 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
-- crates/ail/tests/embed_missing_main_baseline.rs
-- crates/ailang-core/tests/embed_export_hash_stable.rs
-- crates/ailang-check/tests/embed_export_gate.rs (deliberately RED —
-  blocks on the spec contradiction; do NOT commit as-is)
+- crates/ailang-check/tests/embed_export_gate.rs (GREEN 6/6)
+- crates/ailang-codegen/tests/embed_staticlib_lowering.rs (GREEN 2/2)
+- crates/ail/tests/embed_staticlib_cli.rs (GREEN 2/2)
+- crates/ail/tests/embed/host.c
+- crates/ail/tests/embed_e2e.rs (GREEN 1/1 — coherent-stop proof)
 
-NOT iter-authored, present in tree, Boss-decides separately:
-- docs/roadmap.md (external mid-session modification; path-disjoint)
+(`docs/roadmap.md` is NOT in this iter's working tree — the
+first-dispatch external modification was Boss-committed separately
+as roadmap maintenance, per the Boss resolution.)
 
 ## Stats
 
diff --git a/docs/journals/INDEX.md b/docs/journals/INDEX.md
index 5efa037..cb8b925 100644
--- a/docs/journals/INDEX.md
+++ b/docs/journals/INDEX.md
@@ -93,3 +93,4 @@
 - 2026-05-18 — fieldtest remove-mut-var-assign (milestone CLOSE, clean — removal thesis empirically confirmed): post-audit downstream-LLM-author field test of the post-removal Form-A surface. The fieldtester (DESIGN.md + form_a.md + public examples only, never compiler source) wrote 4 FRESH real-world programs an imperative-trained author would instinctively reach for a mutable local for — running sum-of-squares accumulator (`loop`/`recur`, 2 binders → `385`), grade-classification cascade (let-threaded flag through 4 `if` → `4`/`2`/`0`), Horner polynomial straight-line build-up (5 `let acc` shadows → `73`), multi-state bracket-balance scanner threading `(rest,depth,ok)` by tail recursion → `true`/`false`) plus an out-of-tree `mut`-keyword rejection probe. **0 bugs, 0 friction, 0 spec_gap, 4 working**: every task expressed cleanly and correctly on the FIRST try with only `let`/`if`/`loop`/`recur`; all 4 `ail parse|render|parse` byte-identical. The closest-to-friction case (the multi-state machine must restate the full state tuple at every tail-call even when a branch changes one component) was carefully classified `working` not `spec_gap` — that explicit-dataflow cost IS the local-reasoning pillar working as designed, and `mut`'s implicit cross-iteration persistence of un-restated state is precisely the clause-3 failure the removal eliminates; the fieldtester explicitly noted the only conceivable sugar (a record to bundle state) is an orthogonal additive future question, NOT evidence against the removal (refused the scope-creep). The `mut` rejection is fail-closed with an actively-guiding diagnostic that enumerates the surviving term heads incl. `loop`/`recur`/`let` (no tombstone, no-nostalgia, as spec'd). Independent Boss verification: all 4 fixtures re-run → `385`/`4 2 0`/`73`/`true false`, zero `mut`/`var`/`assign` construct tokens in any fixture (a doc-faithful author did not produce the removed construct — the affirmative clause-1 evidence). **Verdict: the removal thesis is confirmed** — `mut` was redundant with `let`/`if`/`loop`/`recur` in 100% of the fresh real tasks; no expressivity lost. **The remove-mut-var-assign milestone is fully ratified and CLOSED**: spec+plan+iter, audit clean (architect `[high]` form_a.md fixed in `.tidy`, bench causally exonerated), fieldtest clean on the removal axis. Fixtures `examples/fieldtest/remove-mut_*.ail` + spec `docs/specs/2026-05-18-fieldtest-remove-mut-var-assign.md`; roadmap P0 flipped `[~]`→`[x]`, WhatsNew.md user-facing entry appended; next queue item (DESIGN.md/docs honesty-lint) is a NEW milestone = a /boss new-milestone bounce-back (not auto-started) → 2026-05-18-fieldtest-remove-mut-var-assign.md
 - 2026-05-18 — iter docs-honesty-lint.1 (single-iteration milestone, DONE): canonical docs made present-tense-honest. Stripped Wunschdenken (forward intent stated as fact) + non-citation post-mortem/doc-archaeology from `docs/DESIGN.md` (14 corrections: L484 iter-anchor, L503/L1318/L1504/L2027/L2065/L2135 post-mortem, L650 malformed-Wunschdenken, L655 dated-heading, L1513/L1837/L2046/L2519 Wunschdenken, + the Task-4-Step-14 procedural-catch-all FIX at the Form-B prose-projection bullet "was deferred from milestone 22 entirely … A future iter ships" — a soft-wrapped site the spec's illustrative regex would have missed, the procedural enumeration working exactly as designed) + `docs/PROSE_ROUNDTRIP.md` (tool-use/MCP paragraph); genuine forward intent (LLM tool-use/MCP/LSP) relocated to roadmap P3. Codified the two-pronged tense+modality discriminator as a present-tense `### What this document is — and the honesty rule it holds itself to` meta-subsection in DESIGN.md §"Project ecosystem". Anti-regrowth two ways: wrap-robust enumerated absent/present pin `crates/ailang-core/tests/docs_honesty_pin.rs` (a `norm()` whitespace-collapse helper structurally discharges the recurring grep/contains line-wrap failure family — strictly better than the effect-doc-honesty "keep-on-one-line" precedent; resolves spec Testing-item 0 + planner self-review item 6 at once) + wrap-robust advisory Sweep 5 in `bench/architect_sweeps.sh` (contiguous-fragment regex, since DESIGN.md is hard-wrapped ~70col) with full sweep-count lockstep (header + "All four"→"All five" tail + `ailang-architect.md` "four"→"five sweeps") + a new `ailang-architect.md` "DESIGN.md honesty drift" bullet citing the meta-subsection. Protected-exception KEEPs preserved + pinned-present (Diverge-reserved, regions-considered-and-rejected, the self-labelled "tiebreaker, not a rationale"); `form_a.md` correctly left untouched/unpinned. One plan-internal DONE_WITH_CONCERNS (Task-1 pin string omitted a `**…**` bold the Task-3 body added; resolved by dropping the non-load-bearing emphasis, pin is the contract) — planner self-review-item-3 calibration note. Independent Boss verification: pin 4/4 GREEN, full `cargo test --workspace` 0 failures (delta = +4 pin tests only), sentinel trio (`design_schema_drift`/`spec_drift`/`schema_coverage`) green, `cargo build --workspace` clean, scope = ONLY THE PIN in `crates/` (zero language/checker/codegen/runtime change, `ail check`/`run`/`build` byte-unchanged by construction). Post-iter sweep residue = only the 3 documented deliberate KEEPs (Sweep-1 L50 doc-roles-pointer date + L2060 true `(iter str-concat)` provenance; Sweep-5 L62 self-referential discriminator-catalogue), EXIT=1 architect-adjudicated-expected. Milestone-close `audit` is the next pipeline step (no fieldtest — zero authoring-surface change). spec `docs/specs/2026-05-18-docs-honesty-lint.md` (grounding-check PASS 10/10), plan `docs/plans/docs-honesty-lint.1.md` → 2026-05-18-iter-docs-honesty-lint.1.md
 - 2026-05-18 — audit docs-honesty-lint (milestone close, CLEAN — carry-on, NO ratify): scope `928e1c0..e50b400`. Architect `clean`: scope claim exact (zero `crates/**/src/**` + `runtime/`; sole crates/ change the additive RED-first-now-GREEN `docs_honesty_pin.rs`; lockstep pairs untouched), all 14 DESIGN.md corrections genuinely present-tense with the 4 protected KEEPs (`Diverge`-reserved/`Regions`-rejected/`tiebreaker`/`No deriving`) un-stripped, agent-def "four→five" lockstep complete, sweep residue exactly the 3 documented deliberate KEEPs. One `[medium]` standing advisory wart — Sweep 5's regex self-matches the discriminator subsection's own forbidden-phrasing catalogue (DESIGN.md L62) forever (architect-flagged; orchestrator-adjudicated → filed as a P3 todo, NOT a fix iteration — not a new failure mode since the script is advisory-with-residue by design). Bench: `compile_check.py` 0/24 + `cross_lang.py` 0/25 EXIT 0 (cross_lang independently reads the same `bench_list_sum` bump path +5.95% within tol); `check.py` EXIT 1, 3 firings (`bench_list_sum.bump_s` +13.42%, `latency.implicit_at_rc.{p99_9,max}_us` +37.65%/+134.70%). Bencher causal exoneration **decisive**: HEAD vs `5bb7211` vs `de66eb7` — all 5 firing bench binaries `cmp`-byte-identical, `ail` sha256 identical at all three commits ⇒ zero causal mechanism; `*.max_us` = tracked-P2 `-n 5` tail-jitter (4th occurrence on a zero-runtime-change milestone, median/p99 rock-steady), `*.bump_s` = tracked-P2 environmental-anchor-staleness (persistent ~+15%, stale 0.046s anchor). **EXONERATED, NO baseline ratify** (Iron Law forbids ratifying noise; spec forecloses a zero-codegen baseline bump). Two pre-existing standing P2 items kept orchestrator-owned, explicitly NOT bundled into this close (bencher recommendation honoured). Milestone audit **CLEAN**; no fieldtest (zero authoring-surface change — the wrap-robust pin + Sweep 5 ARE the regression coverage). **docs-honesty-lint fully ratified and CLOSED**: spec (grounding-check PASS 10/10) + plan + single iter + audit clean; roadmap P0 flipped `[~]`→`[x]`, WhatsNew.md user-facing entry appended → 2026-05-18-audit-docs-honesty-lint.md
+- 2026-05-18 — iter embedding-abi-m1.1 (Embedding-ABI M1, DONE across 2 dispatches + a Boss plan Repair): a compiled AILang scalar `fn` is now callable in-process from a C/Rust host. Five pipeline layers shipped: additive `FnDef.export: Option<String>` (serde `default`+`skip_serializing_if`, modelled on `FnDef.doc`, ~85-site compile-driven thread incl. all in-source `#[cfg(test)]`/drift/hash literals, hash-stable golden `b4662aa70839f60b`); Form-A `(export "<sym>")` modifier (parse/print/`form_a.md` lockstep, byte-identical round-trip); check-side scalar-only+effect-free export gate — two new `CheckError` Error variants `export-non-scalar-signature`/`export-has-effects`, params→ret→effects first-violation-wins, unconditional on `f.export.is_some()` (the feature-acceptance clause-3 discriminator *in code*); codegen `Target::StaticLib` (suppresses `@main`+`MissingEntryMain`, emits one external `@<sym>` forwarder per export to `@ail_<module>_<fn>`); CLI `ail build --emit=staticlib` (`build_staticlib`: `libembed_backtest_step.a` program-only + separate `libailang_rt.a`). Coherent stop PROVEN: `embed_e2e.rs` `cc`-links both archives, `backtest_step(0,3)=9`/`(9,4)=25`, `s==25`, exit 0. Task 1 (fixed-first CLI `MissingEntryMain` baseline pin) green before any staticlib code. Process: Task 4 BLOCKED on the first dispatch — a Boss plan-defect (gate/headline fixtures declared `module ≠ file-stem`; the loader hard-enforces `module==stem` at `workspace.rs:438`, so `ail check` panicked on load before the gate). Boss verified, chose **Option 2 over the orchestrator-recommended Option 1** (keep descriptive `embed_*` filenames, rename fixture *modules* to their stems — the C symbol `backtest_step` stays via `(export …)`, *demonstrating* spec Decision 2's mangling-decoupling rather than violating it; archive→`libembed_backtest_step.a`, internal→`@ail_embed_backtest_step_step`, `host.c` unchanged), Repaired the plan (Design-decision 6 + Task-4 module==stem + Task-5/6/7 dependent strings + folded the no-`*.`-Float-head and `content_hash_fn`→`def_hash` concerns), committed Tasks 1–3 as a verified known-good partial (`818177d`), re-dispatched [4,7]. Independent Boss verification post-completion: E2E 1/1, gate 6/6, lowering 2/2, CLI 2/2, full `cargo test --workspace` 0 failures, `roundtrip_cli`+`design_schema_drift`+`spec_drift` green, Invariant 1 holds (no new dep in `ailang-core`/`ailang-codegen`/`runtime`). 3 behaviour-neutral plan pseudo-vs-reality concerns recorded (`emit_ir` routes via `lower_workspace`; dead `Path` import dropped; `##` vs `###` heading). Bench: `compile_check.py`/`cross_lang.py` exit 0; `check.py` exit 1 = tracked-P2 `*.bump_s`/`*.max_us` known-noise (default-exe codegen/runtime byte-unchanged — audit-adjudicated, not a plan gate). spec `docs/specs/2026-05-18-embedding-abi-m1.md` (grounding-check PASS) → plan `docs/plans/embedding-abi-m1.1.md` (Repaired) → commits `818177d` (partial 1–3) + this completion. Milestone-close `audit` then `fieldtest` (surface-touching — `(export …)` is new authoring surface) are the next pipeline steps. → 2026-05-18-iter-embedding-abi-m1.1.md
diff --git a/examples/embed_export_adt_ret_rejected.ail b/examples/embed_export_adt_ret_rejected.ail
new file mode 100644
index 0000000..986795d
--- /dev/null
+++ b/examples/embed_export_adt_ret_rejected.ail
@@ -0,0 +1,11 @@
+(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))))
diff --git a/examples/embed_export_effectful_rejected.ail b/examples/embed_export_effectful_rejected.ail
new file mode 100644
index 0000000..ec05be6
--- /dev/null
+++ b/examples/embed_export_effectful_rejected.ail
@@ -0,0 +1,11 @@
+(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))))
diff --git a/examples/embed_export_float_ok.ail b/examples/embed_export_float_ok.ail
new file mode 100644
index 0000000..ebf4cf3
--- /dev/null
+++ b/examples/embed_export_float_ok.ail
@@ -0,0 +1,10 @@
+(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))))
diff --git a/examples/embed_export_io_rejected.ail b/examples/embed_export_io_rejected.ail
new file mode 100644
index 0000000..78265a4
--- /dev/null
+++ b/examples/embed_export_io_rejected.ail
@@ -0,0 +1,11 @@
+(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))))
diff --git a/examples/embed_export_str_param_rejected.ail b/examples/embed_export_str_param_rejected.ail
new file mode 100644
index 0000000..8d3333a
--- /dev/null
+++ b/examples/embed_export_str_param_rejected.ail
@@ -0,0 +1,9 @@
+(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)))