iter embedding-abi-m1.1 (PARTIAL 3/7): schema + surface + baseline prerequisites; plan Repair

Tasks 1-3 of docs/plans/embedding-abi-m1.1.md, a verified known-good
subset (cargo build --workspace exit 0; full workspace green; the
roundtrip_cli all-examples gate green):

- Task 1: CLI build-path MissingEntryMain baseline pin
  (examples/embed_noentry_baseline.ail + embed_missing_main_baseline.rs;
  triple-assertion, layered on the green codegen-unit pin lib.rs:3314).
- Task 2: additive FnDef.export: Option<String> (serde default +
  skip_serializing_if, modelled on FnDef.doc); compile-driven thread
  of export: None across ~85 FnDef/AstFnDef literals / 18 files incl.
  all in-source #[cfg(test)] mod tests + drift/hash/spec-drift
  literals + the codegen lib.rs:3320 in-source pin; hash-stability
  golden pin; DESIGN.md fn-JSON "export" line. DONE_WITH_CONCERNS
  (plan symbol content_hash_fn -> def_hash per hash_pin.rs, plan-
  pseudo-vs-reality class, plan corrected).
- Task 3: Form-A (export "<sym>") modifier — parse_export +
  parse_fn thread + write_fn_def emission + form_a.md grammar;
  byte-identical round-trip.

Task 4 BLOCKED (Boss plan-defect: fixtures declared module != file
stem; AILang's loader hard-enforces module==stem at workspace.rs:438,
so ail check panicked on load before the gate). Boss resolution
(Option 2, overriding the orchestrator's Option 1, rationale in the
journal + plan Design-decision 6): 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 becomes
libembed_backtest_step.a, internal symbol @ail_embed_backtest_step_step,
host.c unchanged. Plan fixed (Design-decision 6 + Task-4 module==stem
+ Task-5/6/7 dependent strings + the no-*. Float-head + content_hash_fn
concerns folded). Headline fixture corrected; blocked-Task-4 WIP
discarded (recreated by the [4,7] re-dispatch from the fixed plan).

PARTIAL commit (not the iter's final commit): the implement Repair
path mandates committing the known-good subset so the [4,7]
re-dispatch starts from a clean tree that includes Tasks 1-3 (Tasks
4-7 structurally depend on the schema field + surface). INDEX line
added when the full iter lands post-re-dispatch.

docs/DESIGN.md

@@ -2295,6 +2295,7 @@ are real surface forms.
   "params": ["<id>"...],   // names bound in body, in type.params order
   "body": Term,
   "doc": "<optional string>",
+  "export": "<optional C symbol>", // omitted when absent (hash-stable when omitted); see §"Embedding ABI (M1)"
   "suppress": [Suppress...] // omitted when empty
 }
 

docs/journals/2026-05-18-iter-embedding-abi-m1.1.md

@@ -0,0 +1,317 @@
+# iter embedding-abi-m1.1 — Embedding ABI M1: linkable artifact + scalar C entrypoint
+
+**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)
+
+## Summary
+
+Tasks 1–3 of the Embedding-ABI M1 plan landed cleanly: 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.
+
+## Per-task notes
+
+- iter embedding-abi-m1.1.1: CLI build-path `MissingEntryMain`
+  baseline pin. Created `examples/embed_noentry_baseline.ail`
+  (main-free module) + `crates/ail/tests/embed_missing_main_baseline.rs`
+  (triple-assertion: non-zero exit + verbatim `has no \`main\` def`
+  Display substring [codegen lib.rs:129] + absent binary). GREEN on
+  write; not-a-no-op confirmed; `roundtrip_cli` green with the new
+  fixture. DONE.
+- iter embedding-abi-m1.1.2: additive `FnDef.export` schema field +
+  workspace-wide threading. Added the field to `FnDef` after `doc`
+  (verbatim plan doc-comment, `#[serde(default,
+  skip_serializing_if = "Option::is_none")]`). Compile-driven
+  enumeration via `cargo build --workspace --all-targets
+  --keep-going` over two dependency-ordered waves threaded
+  `export: None` into ~85 `FnDef`/`AstFnDef` literals across 18
+  files incl. all named blind-spot sites (codegen lib.rs:3320
+  `missing_entry_main_is_error`, design_schema_drift.rs:278,
+  spec_drift.rs:256, hash_pin.rs, the in-source `#[cfg(test)]
+  mod tests` literals, the `mono.rs` `AstFnDef` alias, the
+  `parse.rs`/`print.rs` literals). `cargo build --workspace`
+  exits 0 (planner self-review item 7 gate met). DESIGN.md
+  fn-JSON `"export"` line + drift test green (Recon Q2 confirmed:
+  no nested-struct-key anchor forced). Hash pin green (golden
+  `b4662aa70839f60b`). Full workspace test gate: 611/0.
+  DONE_WITH_CONCERNS.
+- iter embedding-abi-m1.1.3: Form-A `(export "<sym>")` surface
+  modifier. `parse_export` helper (faithful `parse_doc` mirror);
+  `parse_fn` threaded (`let mut export`, `Some("export")` arm with
+  duplicate-clause guard, unknown-attr string updated, `Ok(FnDef{…})`
+  uses parsed `export`); `write_fn_def` export emission block (doc →
+  export → suppress → type order); form_a.md production +
+  `(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.
+
+## Concerns
+
+- iter embedding-abi-m1.1.2: the plan's RED-pin symbol
+  `ailang_core::hash::content_hash_fn(&FnDef)` does not exist. The
+  real entry point is `def_hash(&Def) -> String` (the one
+  `crates/ailang-core/tests/hash_pin.rs` uses). Resolved by
+  mirroring `hash_pin.rs` exactly (wrap the `FnDef` in
+  `Def::Fn(...)`, call `def_hash`) — this is explicitly authorised
+  by the plan's own Step-1 NOTE ("the implementer mirrors the exact
+  hashing entry point that `hash_pin.rs` uses if the name differs").
+  Property and shape unchanged; recorded because the plan's literal
+  symbol was wrong (planner pseudo-vs-reality class — the
+  `feedback_specs_need_concrete_code` / `feedback_plan_pseudo_vs_reality`
+  family).
+- iter embedding-abi-m1.1.4: the plan fixture `embed_export_float_ok.ail`
+  uses `(app *. a b)`. There is no `*.` Float-multiply head in
+  AILang — Float arithmetic uses the same typeclass-generic head as
+  Int (`examples/floats.ail` / `examples/mut_sum_floats.ail` both
+  use `(app + …)`; codegen lowers to `fadd/fmul double` by type).
+  Per the plan NOTE ("if the Float-multiply surface differs, use the
+  same head that example uses"), the fixture as written uses
+  `(app * a b)`. The fixture's role ("scalar+pure Float export
+  passes the gate") is preserved. Recorded; not yet exercised
+  (Task 4 BLOCKED before the gate ran).
+- INFRA (not iter-authored): `docs/roadmap.md` became dirty in the
+  working tree during this run (a ~98-line P2 "DESIGN.md → design/
+  role-split" milestone proposal, mtime mid-session). Phase 0's
+  `git status --porcelain` was empty (clean start). Nothing in this
+  iter writes `roadmap.md`; it was modified by an external/concurrent
+  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.
+
+## 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.
+
+## Blocked detail
+
+**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
+sub-status table → BLOCKED to Boss).
+
+**Worker says:** The plan's Task-4 gate pin
+(`crates/ailang-check/tests/embed_export_gate.rs`) is verbatim and
+correct Rust; it calls `ailang_surface::load_workspace(&path)` on
+each fixture (the exact call shape `crates/ail/src/main.rs:580–581`
+uses). `load_workspace` →
+`ailang_core::workspace::load_modules_with` →
+`module_name_from_path` (`workspace.rs:1566`) hard-enforces
+`in-file module name == file stem`, returning
+`WorkspaceLoadError::ModuleNameMismatch` (`workspace.rs:182`)
+otherwise. The plan's verbatim fixtures deliberately violate this:
+
+  - `examples/embed_backtest_step.ail` has `(module backtest …)` —
+    spec-mandated, because the entry module name `backtest` is what
+    produces `libbacktest.a` (Task 6), `@ail_backtest_step` and the
+    exported C symbol `backtest_step` (Tasks 5/7, the spec headline
+    host `host.c` declares `extern int64_t backtest_step(...)`).
+    Stem is `embed_backtest_step` ⇒ `ModuleNameMismatch`.
+  - `embed_export_str_param_rejected.ail` → module `bad_str_param`;
+    `embed_export_io_rejected.ail` → `bad_io`;
+    `embed_export_effectful_rejected.ail` → `bad`;
+    `embed_export_adt_ret_rejected.ail` → `bad_adt_ret`;
+    `embed_export_float_ok.ail` → `embed_float_ok`. All
+    stem-mismatched ⇒ every `check_codes()` call panics on load
+    before the gate is ever consulted.
+
+These three plan facts cannot all hold simultaneously: (a) fixture
+files named `examples/embed_*` (every Task 4/5/6/7 path cites these
+exact names), (b) the spec-headline module/C-symbol naming
+(`backtest` → `libbacktest.a` / `backtest_step`), (c) a
+`load_workspace`-based check-side gate pin. `roundtrip_cli` (Task 1/3)
+sidesteps this only because it drives `ail parse` (single-file, no
+workspace stem-match). The contradiction is therefore invisible until
+the first `load_workspace`-based fixture test — exactly Task 4.
+
+This is not one of the six named implementer-judgement cross-checks
+(Float `*.` head, public-symbol confirmation, `Type::Con` field set,
+`declared_effs` element type, `run_cmd` pre-existence, `llvm_scalar`
+callee-ABI). It is a structural spec/plan defect requiring a
+Boss/spec decision among at least:
+
+  1. Rename each fixture **file** to its module stem
+     (`examples/backtest.ail`, `examples/bad_str_param.ail`, …) and
+     update every Task 4/5/6/7 path citation accordingly (preserves
+     the spec headline module/C-symbol naming; ripples ~12 plan
+     path references + the Task-6/7 `libbacktest.a` math still holds
+     since module stays `backtest`).
+  2. Rename each fixture **module** to its filename stem
+     (`(module embed_backtest_step …)`, …) and re-derive the spec's
+     C-symbol / `lib<entry>.a` story from `embed_backtest_step`
+     (changes the spec headline; `libembed_backtest_step.a`,
+     `@ail_embed_backtest_step_step` — almost certainly not what the
+     spec wants).
+  3. Change the Task-4 gate pin to a loader that does not
+     stem-enforce (e.g. parse the single file directly), which
+     diverges from the plan's verbatim `load_workspace`-based test
+     and from how `ail check` actually loads (`main.rs:580`).
+
+Option 1 is the most spec-faithful (it keeps the headline module
+`backtest` and only moves files), but it is a cross-task plan edit
+(≥12 path citations) and therefore the planner's / Boss's call, not
+an inline implementer substitution. I did NOT silently pick one
+(reverted my own speculative fixture-module renames so the Boss sees
+the contradiction unobscured); no gate production code was written.
+
+**Suggested next step:** Boss adopts Option 1 — re-issue the plan
+for Tasks 4–7 with fixture files renamed to their module stems
+(`examples/backtest.ail` etc.) and the ~12 path citations updated;
+keep module `backtest` so the spec's `libbacktest.a` /
+`backtest_step` headline is preserved — then re-dispatch this iter
+with `task_range: [4, 7]` (Tasks 1–3 are clean and can be committed
+now or carried).
+
+## Boss resolution (2026-05-18)
+
+The BLOCK was verified accurate against source:
+`crates/ailang-core/src/workspace.rs:438` (`entry_module.name !=
+module_name_from_path(entry_path)` → `ModuleNameMismatch`, no
+exception) — module name MUST equal file stem. The defect is a
+**Boss plan-write error**: the plan's headline + gate fixtures
+declared `(module backtest)` / `(module bad)` / … in `embed_*.ail`
+files, malformed under that invariant. The orchestrator correctly
+stopped at the Iron Law instead of guessing. Recon maps file
+structure, not fixture-content invariants; the Boss source-
+verification focused on code-edit anchors, not cross-checking each
+fixture's module name against its filename against the loader —
+this is the `feedback_specs_need_concrete_code` /
+`feedback_plan_pseudo_vs_reality` family (the fixture as written
+would not load), now also a fixture-well-formedness lesson.
+
+**Decision: Option 2, overriding the orchestrator-recommended
+Option 1.** (Agent recommendations are not directives — own
+judgement formed first.) Keep the descriptive `embed_*` filenames;
+rename the fixture *modules* to their file stems
+(`embed_backtest_step`, `embed_export_str_param_rejected`, …).
+Rationale from semantics, not effort:
+
+- The spec's load-bearing contract (Decision 2, spec lines
+  52–59 / 167–169) is that the exported C symbol is *author-chosen
+  and decoupled from `ail_<module>` mangling* —
+  `(export "backtest_step")` is the contract; `host.c` asserts on
+  `backtest_step`, which is invariant under module rename. So
+  spec-faithfulness does **not** discriminate between the options;
+  `libbacktest.a` / `@ail_backtest_step` are *illustrative*
+  (build-output filename + internal mangling — the latter is
+  exactly what the spec decouples from), not frozen-ABI contracts.
+  The orchestrator's "Option 1 most spec-faithful" over-weighted
+  the illustrative `libbacktest.a` string.
+- `examples/` is a flat shared corpus auto-enrolled in whole-corpus
+  tests (`roundtrip_cli`); Option 1's `examples/bad.ail` /
+  `backtest.ail` / `bad_io.ail` pollute it with collision-prone,
+  non-self-describing names. Option 2 keeps the self-describing
+  grouped `embed_*` set — a real maintainability argument in a
+  ~100-file flat dir read by future LLM authors.
+- Option 2 (module = stem, C symbol stays `backtest_step` via the
+  `(export …)` string) is a *concrete demonstration of the spec's
+  own Decision-2 decoupling thesis* — the first fixture proving
+  module-name ≠ C-symbol — not a violation of it. The spec's
+  `(module backtest)` / `(module bad)` blocks are shape-
+  illustrative (planner contract: spec owns shape, not bytes).
+
+Consequence: entry module `embed_backtest_step` ⇒ archive
+`libembed_backtest_step.a`, internal symbol
+`@ail_embed_backtest_step_step`; the external C symbol
+`backtest_step` and `host.c` are UNCHANGED (the actual coherent-
+stop contract). Architect-at-close note recorded in the plan
+(Design-decision 6): a fixture module name differing from the
+spec's illustrative block is expected under module==stem +
+Decision 2, not drift.
+
+Actions taken: (1) plan `docs/plans/embedding-abi-m1.1.md` fixed —
+Design-decision 6 added, Task-4 fixtures → module==stem, Task-5/6/7
+dependent strings updated (`libembed_backtest_step.a`,
+`@ail_embed_backtest_step_step`; C symbol `@backtest_step`
+unchanged), the two iter-1 concerns folded (no `*.` Float head →
+`(app * a b)`; `content_hash_fn` → `def_hash(&Def)`); (2) the
+already-created headline `examples/embed_backtest_step.ail`
+corrected to `(module embed_backtest_step)`; (3) the 5 blocked-
+Task-4 fixtures + the RED `embed_export_gate.rs` discarded
+(untracked WIP — recreated correctly by the re-dispatch from the
+fixed plan); (4) Tasks 1–3 committed as a verified known-good
+partial subset (`cargo build --workspace` exit 0, full workspace
+green with zero FAILED after the WIP discard, `roundtrip_cli`
+green); (5) orchestrator re-dispatched with `task_range: [4, 7]`
+on the clean tree + corrected plan. The user's path-disjoint
+roadmap addition (P2 "DESIGN.md → `design/` role-split") was
+committed separately as Boss roadmap maintenance, not bundled
+into this iter.
+
+## Files touched
+
+Schema / canonical docs:
+- crates/ailang-core/src/ast.rs (FnDef.export field)
+- docs/DESIGN.md (fn-JSON "export" line)
+- crates/ailang-core/specs/form_a.md (grammar production + prose)
+
+Workspace-wide compile-gate threading (~85 `export: None,` literals):
+- crates/ailang-core/src/desugar.rs, pretty.rs
+- crates/ailang-core/tests/{design_schema_drift,hash_pin,spec_drift}.rs
+- crates/ailang-check/src/{lib,lift,linearity,mono,reuse_shape,suppress_filter,uniqueness}.rs
+- crates/ailang-check/tests/workspace.rs
+- crates/ailang-codegen/src/lib.rs
+- crates/ailang-prose/src/lib.rs
+
+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):
+- examples/embed_noentry_baseline.ail
+- examples/embed_backtest_step.ail
+- 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)
+
+NOT iter-authored, present in tree, Boss-decides separately:
+- docs/roadmap.md (external mid-session modification; path-disjoint)
+
+## Stats
+
+bench/orchestrator-stats/2026-05-18-iter-embedding-abi-m1.1.json

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

@@ -95,6 +95,45 @@ finance/`data-server` knowledge or dependency (Invariant 1).
    ABI (M1)" subsection documents a capability that only fully exists
    after codegen+CLI+E2E → Task 7 (DESIGN.md = current-state mirror:
    document the ABI once it demonstrably works).
+6. **Fixture module name == file stem (Option 2; revised
+   post-Task-4-BLOCK 2026-05-18).** AILang's workspace loader hard-
+   enforces `module-name == file-stem`
+   (`crates/ailang-core/src/workspace.rs:438`,
+   `WorkspaceLoadError::ModuleNameMismatch`, no exception) — so every
+   fixture's `(module …)` MUST equal its filename stem or `ail check`
+   panics on load before any gate runs. The original plan's headline
+   used `(module backtest)` in `embed_backtest_step.ail` (and
+   `bad`/`bad_io`/… in the gate fixtures) — malformed under that
+   invariant; the implement-orchestrator correctly BLOCKED Task 4 on
+   it. Resolution: **rename the fixture *modules* to their file
+   stems, keep the descriptive `embed_*` filenames** (NOT the
+   orchestrator-suggested Option 1 of renaming files to bare module
+   stems). Rationale, from semantics not effort: (a) the spec's
+   load-bearing contract (Decision 2, spec lines 52–59/167–169) is
+   that the exported C symbol is *author-chosen and decoupled from
+   `ail_<module>` mangling* — `(export "backtest_step")` is the
+   contract; the host asserts on `backtest_step`, which is invariant
+   under module rename. So spec-faithfulness does not discriminate;
+   `libbacktest.a`/`@ail_backtest_step` are *illustrative* (build-
+   output filename + internal mangling — the latter is exactly what
+   the spec decouples from), not frozen-ABI contracts. (b) `examples/`
+   is a flat shared corpus auto-enrolled in whole-corpus tests;
+   Option 1's `examples/bad.ail`/`backtest.ail` pollute it with
+   collision-prone non-self-describing names — Option 2 keeps the
+   self-describing grouped `embed_*` set. (c) Option 2 *is* a
+   concrete demonstration of the spec's own Decision-2 decoupling
+   thesis (module `embed_backtest_step`, C symbol `backtest_step`),
+   not a violation of it. The spec's `(module backtest)`/`(module
+   bad)` blocks are shape-illustrative (planner contract: spec owns
+   shape, not bytes — same as the spec naming a filename while the
+   contract is the `(export …)` symbol). Consequences threaded below:
+   entry module `embed_backtest_step` ⇒ archive
+   `libembed_backtest_step.a`, internal symbol
+   `@ail_embed_backtest_step_step`; the external C symbol
+   `backtest_step` and `host.c` are UNCHANGED. **Architect-at-close
+   note:** a fixture module name differing from the spec's
+   illustrative block is expected and correct under the module==stem
+   invariant + Decision 2 — not drift.
 
 ---
 
@@ -266,9 +305,15 @@ fn fn_without_export_hash_is_unchanged() {
 }
 ```
 
-> 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
+> NOTE (corrected post-iter-1): there is **no**
+> `ailang_core::hash::content_hash_fn`. The real entry point is
+> `def_hash(&Def) -> String` — wrap the `FnDef` in `Def::Fn(...)`
+> and call `def_hash`, exactly as `crates/ailang-core/tests/hash_pin.rs`
+> does. (Task 2 already executed this correctly per this NOTE's
+> original "mirror hash_pin.rs" license; the symbol name above is
+> left only so the diff to the as-executed test is legible.)
+> `Type::fn_implicit` / `Term::Var` constructors are the ones
+> already used by `hash_pin.rs` and
 > `design_schema_drift.rs:282`; the implementer mirrors the exact
 > hashing entry point that `hash_pin.rs` uses if the name differs.
 > The `<<GOLDEN-PLACEHOLDER>>` is resolved deterministically in
@@ -381,11 +426,13 @@ constructs/serialises identically because `export: None` is omitted).
 
 - [ ] **Step 1: Write the headline round-trip RED fixture**
 
-Create `examples/embed_backtest_step.ail` (the spec headline,
-verbatim):
+Create `examples/embed_backtest_step.ail` (the spec headline; module
+name == file stem per Design-decision 6 — the C symbol stays
+`backtest_step` via the `(export …)` string, demonstrating spec
+Decision 2's mangling-decoupling):
 
 ```
-(module backtest
+(module embed_backtest_step
 
   (fn step
     (export "backtest_step")
@@ -577,7 +624,7 @@ Expected: PASS (form_a.md is not hashed; this confirms no
 `examples/embed_export_str_param_rejected.ail` (Str param, else
 scalar+pure → `export-non-scalar-signature`):
 ```
-(module bad_str_param
+(module embed_export_str_param_rejected
   (fn f
     (export "f")
     (type
@@ -591,7 +638,7 @@ scalar+pure → `export-non-scalar-signature`):
 `examples/embed_export_adt_ret_rejected.ail` (ADT return →
 `export-non-scalar-signature`):
 ```
-(module bad_adt_ret
+(module embed_export_adt_ret_rejected
   (data Pair
     (ctor Pair (con Int) (con Int)))
   (fn f
@@ -607,7 +654,7 @@ scalar+pure → `export-non-scalar-signature`):
 `examples/embed_export_io_rejected.ail` (scalar params+ret but `!IO`
 → `export-has-effects`):
 ```
-(module bad_io
+(module embed_export_io_rejected
   (fn f
     (export "f")
     (type
@@ -624,7 +671,7 @@ scalar+pure → `export-non-scalar-signature`):
 Str param **and** `!IO`; gate-order params→ret→effects ⇒ fails
 `export-non-scalar-signature`):
 ```
-(module bad
+(module embed_export_effectful_rejected
   (fn log_step
     (export "log_step")
     (type
@@ -640,7 +687,7 @@ Str param **and** `!IO`; gate-order params→ret→effects ⇒ fails
 `examples/embed_export_float_ok.ail` (positive — `(Float,Float)->Float`,
 pure; the second scalar type beyond the Int headline):
 ```
-(module embed_float_ok
+(module embed_export_float_ok
   (fn scale
     (export "embed_scale")
     (type
@@ -649,13 +696,15 @@ pure; the second scalar type beyond the Int headline):
         (ret (con Float))))
     (params a b)
     (body
-      (app *. a b))))
+      (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".
+> NOTE (folded from the iter-1 BLOCK concern): AILang has **no**
+> `*.` Float-multiply head — Float arithmetic uses the same
+> typeclass-generic head as Int (`examples/floats.ail` uses
+> `(app + …)`; codegen lowers to `fmul double` by type). The
+> fixture above already uses `(app * a b)`. The fixture's *role* is
+> "scalar+pure Float export passes the gate".
 
 - [ ] **Step 2: Write the gate pin — verify RED**
 
@@ -858,9 +907,12 @@ 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).
+//! 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;
@@ -880,9 +932,11 @@ fn staticlib_emits_forwarder_no_main() {
     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");
+        "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]
@@ -1077,8 +1131,9 @@ fn llvm_scalar(t: &Type) -> &'static str {
 
 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`.
+`@backtest_step` (C symbol), forwards to the internal
+`@ail_embed_backtest_step_step`; exe target still returns
+`MissingEntryMain`.
 
 - [ ] **Step 7: Codegen in-source baseline pin still green**
 
@@ -1138,8 +1193,8 @@ fn staticlib_emit_produces_two_archives() {
         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("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:?}");
 }
@@ -1328,8 +1383,9 @@ fn run_cmd(bin: &str, args: &[&str], ctx: &str) -> Result<()> {
 - [ ] **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
+Expected: PASS (2 passed): the headline produces
+`libembed_backtest_step.a` + `libailang_rt.a`; the export-less
+module is rejected with the
 zero-export error.
 
 - [ ] **Step 6: Default-exe path regression**
@@ -1373,8 +1429,8 @@ 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
+//! as a staticlib, link the C host against `libembed_backtest_step.a`
+//! + `libailang_rt.a`, run it, assert the `s == 25` assertion holds
 //! (exit 0). This is the whole-milestone existence proof.
 
 use std::path::{Path, PathBuf};
@@ -1405,7 +1461,7 @@ fn c_host_calls_exported_scalar_kernel() {
     let host_bin = outdir.join("host");
     let cc = Command::new("cc")
         .arg(&host_c)
-        .arg(outdir.join("libbacktest.a"))
+        .arg(outdir.join("libembed_backtest_step.a"))
         .arg(outdir.join("libailang_rt.a"))
         .arg("-o").arg(&host_bin)
         .output().expect("cc host link");
@@ -1427,8 +1483,9 @@ 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
+Expected: PASS — `libembed_backtest_step.a` + `libailang_rt.a` link
+with the C host; `backtest_step(0,3)=9`, `backtest_step(9,4)=25`;
+assertion
 holds; exit 0. This is the coherent stop.
 
 - [ ] **Step 4: DESIGN.md §"Embedding ABI (M1)" — current-state honesty**
@@ -1518,10 +1575,13 @@ plan-level gate.
    `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).
+   `libembed_backtest_step.a` / `libailang_rt.a` / `backtest_step`
+   (the C symbol) / `@ail_embed_backtest_step_step` (internal) —
+   used identically across every task that references them. Module
+   == file stem `embed_backtest_step` ⇒ entry `embed_backtest_step`
+   ⇒ `lib embed_backtest_step.a` = `libembed_backtest_step.a`
+   (Design-decision 6; the C symbol `backtest_step` is decoupled
+   and invariant per spec Decision 2).
 4. **Step granularity.** Every step is one action ≤5 min; the only
    long one (Task 2 Step 5, the ~95-site thread) is a single
    compile-driven mechanical loop with a hard terminating gate — it