spec: amend §C4 carve-outs — prelude.ail.json as compile-time-embed exception

Iter form-a.1 recon surfaced a load-bearing constraint the original
spec didn't anticipate: ailang-core embeds prelude.ail.json at
compile time via include_str! + serde_json::from_str (workspace.rs:417,
main.rs:474), and ailang-core cannot import ailang-surface to switch
the embed to .ail (crate-cycle, documented at loader.rs:9-13).

§C4 splits into two carve-out categories:
- (a) seven subject-matter carve-outs (unchanged, the original list)
- (b) one compile-time-embed carve-out: prelude.ail.json

Acceptance criteria #1, #2 and §T4 carve-out inventory test updated
from 7 to 8.

Roadmap: new [milestone] "Prelude embed: Form-A as compile-time source"
queued to retire §C4(b) by either splitting the workspace loader
(prelude-init moves to ailang-surface) or generating prelude.ail.json
via build.rs. examples/prelude.ail (rendered iter form-a.0) is the
dual-form symptom that milestone exists to resolve. Strike the [todo]
"Author examples/prelude.ail" entry — satisfied by iter form-a.0.

Re-grounding-checked PASS over six load-bearing assumptions (embed
sites verified at workspace.rs:417 + main.rs:474; crate-cycle
constraint real; eight carve-outs all on disk; prelude.ail green
under both roundtrip tests).

docs/roadmap.md

@@ -89,20 +89,10 @@ context. Pick the next milestone from P1.)_
     separate so migration runs against a frozen architecture. Same
     call milestone 23 made for `==` / `eq`.
 
-- [ ] **\[todo\]** Author `examples/prelude.ail` alongside
+- [x] **\[todo\]** Author `examples/prelude.ail` alongside
-  `examples/prelude.ail.json`. Today the prelude exists only as
+  `examples/prelude.ail.json`. (Satisfied 2026-05-13 by iter
-  canonical-form JSON-AST; the textual surface form has to be
+  form-a.0 — `examples/prelude.ail` rendered via `ail render`,
-  reconstructed via `ail render` every time someone wants to read
+  116 lines / 6386 bytes, round-trip-CI green.)
-  it. Check in the Form-A text as the authoring source and let
-  `ail parse` regenerate the JSON-AST at build time (or keep both
-  and gate equivalence via the existing round-trip invariant).
-  Either way the LLM-author's natural reading surface (Form A
-  text) becomes the entry point rather than a derived view.
-  - context: surfaced 2026-05-13 while demonstrating the
-    Show + print milestone via `ail prose`; the prelude is the
-    one file most likely to be read by humans and by LLM authors
-    learning the language, and it's the only fixture without a
-    `.ail` sibling.
 
 - [ ] **\[milestone\]** Form-A as the default authoring surface for
   examples and docs. Render every `examples/*.ail.json` to its
@@ -154,6 +144,72 @@ context. Pick the next milestone from P1.)_
     hits) by treating Form A as the privileged surface in the
     working tree, not just in flavour text.
 
+- [ ] **\[milestone\]** Prelude embed: Form-A as compile-time source.
+  Retire `examples/prelude.ail.json` by switching the
+  `include_str!`-then-`serde_json::from_str` embed sites in
+  `crates/ailang-core/src/workspace.rs:417` and
+  `crates/ail/src/main.rs:474` to consume `examples/prelude.ail`
+  at compile time, parsed via `ailang_surface::parse`. After this
+  milestone the only surviving `.ail.json` carve-outs are the
+  seven subject-matter rejection fixtures (§C4 (a) of the
+  form-a-default-authoring spec); §C4 (b) becomes empty and is
+  removed from the spec.
+
+  **Motivation.** The form-a-default-authoring milestone (just
+  closed) made `.ail` the authoring surface for every program in
+  the corpus, with one exception: the prelude. The prelude is
+  the language's most-read file and the canonical demonstration
+  of every language feature stacked into one module; that it is
+  the *one* file the user authors as `.ail.json` is a doctrine
+  inconsistency relative to CLAUDE.md "authors write `.ail`; the
+  build derives the JSON-AST in-process via `ailang_surface::parse`".
+
+  **Problem.** `ailang-core` consumes the prelude at compile time
+  via `include_str!("../../../examples/prelude.ail.json")` plus
+  `serde_json::from_str`. Switching the embed to `prelude.ail`
+  requires parsing via `ailang_surface::parse`, but `ailang-core`
+  cannot import `ailang-surface` (the crate-cycle constraint
+  documented at `crates/ailang-surface/src/loader.rs:9-13` —
+  `ailang-surface` depends on `ailang-core` for the AST types).
+  The same embed exists at `crates/ail/src/main.rs:474`; that
+  site *can* import `ailang-surface` but is in lockstep with the
+  `ailang-core` one (both must reproduce the same `Module` value
+  for prelude semantics to be uniform between CLI dispatch and
+  workspace loading).
+
+  **Resolution options** (decide at brainstorm time):
+  - (β) Split the workspace loader: move the prelude-injection
+    step from `ailang-core::load_workspace` to a new
+    `ailang-surface::load_workspace_with_prelude` (or wrapper).
+    `ailang-core` retains a prelude-free workspace primitive;
+    `ailang-surface` is the entry point that injects the parsed
+    prelude. Substantive refactor of ~3-5 sites.
+  - (γ) `build.rs` generates `examples/prelude.ail.json` at build
+    time from `examples/prelude.ail` via either an in-tree parser
+    (would re-create a similar crate-graph issue) or a snapshot
+    test that fails on drift. Avoids the loader-split but introduces
+    a build-time artefact and a bootstrap concern (the `ail` binary
+    itself is built from `ailang-core`).
+  - (δ) Some hybrid: prelude stays canonical as `.ail.json` in
+    storage but is rendered to `prelude.ail` at every commit by a
+    pre-commit hook; the dual-form is preserved as a lockstep
+    invariant rather than retired. Trades one inconsistency for
+    another but is the smallest change.
+
+  **Carve-out today.** Per spec §C4 (b) (added 2026-05-13),
+  `prelude.ail.json` is the sole compile-time-embed carve-out
+  during the form-a-default-authoring milestone. `examples/prelude.ail`
+  already exists alongside it (rendered in iter form-a.0) as the
+  authoring surface; the dual-form for prelude is the symptom this
+  milestone exists to retire.
+
+  - context: surfaced 2026-05-13 during iter form-a.1 recon; the
+    crate-cycle issue was not anticipated by the spec authors and
+    forced a brainstorm-level amendment to §C4. The fix exceeds
+    the form-a-default-authoring milestone's scope and is
+    sequenced as its own milestone to keep the architectural
+    change auditable in isolation.
+
 - [ ] **\[feature\]** Operator routing through `Eq` / `Ord` — `==`,
   `<` etc. resolved via the typeclass instead of the built-in
   primitive comparators. No commitment; gated on bench re-baselining

docs/specs/2026-05-13-form-a-default-authoring.md

@@ -227,10 +227,15 @@ property is replaced by parse-determinism plus idempotency — the
 two together discharge the load-bearing concern (hashing is well-
 defined for any `.ail` source).
 
-### C4. The seven carve-outs (immutable list)
+### C4. The carve-outs (immutable list)
 
-These seven files stay `.ail.json` post-milestone and gain no `.ail`
+Two structural reasons keep `.ail.json` alive post-milestone:
-sibling:
+(a) **subject-matter** carve-outs (seven files; the canonical
+list as drafted) and (b) **compile-time-embed** carve-outs (one
+file as of 2026-05-13; subject to a separate milestone). Both
+gain no `.ail` sibling.
+
+**(a) Subject-matter carve-outs (immutable, seven files):**
 
 ```
 examples/test_ct1_bare_xmod_rejected.ail.json
@@ -262,9 +267,54 @@ Justification per file:
   (changing the diagnostic) or refuse to encode at all (changing
   the test subject).
 
-The orchestrator agrees these are the only legitimate carve-outs.
+**(b) Compile-time-embed carve-outs (one file as of 2026-05-13):**
-Any future addition to this list requires brainstorm-level
+
-justification on the same semantic grounds.
+```
+examples/prelude.ail.json
+```
+
+Justification:
+- `prelude.ail.json` is `include_str!`-embedded at
+  `crates/ailang-core/src/workspace.rs:417` and
+  `crates/ail/src/main.rs:474`, then parsed via
+  `serde_json::from_str` at compile-time-fixed sites in production
+  code. Switching the embed to `prelude.ail` would require parsing
+  via `ailang_surface::parse`, but `ailang-core` cannot import
+  `ailang-surface` (crate-cycle constraint documented at
+  `crates/ailang-surface/src/loader.rs:9-13`). The mechanism is a
+  structurally distinct from the runtime-loaded-program corpus the
+  rest of this milestone migrates: `.ail.json` carve-outs in
+  category (a) are kept because their *content* cannot be expressed
+  in Form A; `prelude.ail.json` is kept because its *embed mechanism*
+  requires the JSON-AST form.
+
+  This is a real spec gap relative to §A4's authoring-doctrine
+  ("authors write `.ail`; the build derives the JSON-AST in-process
+  via `ailang_surface::parse`"). The prelude is currently authored
+  as `.ail.json` and embedded as bytes; the doctrine says it should
+  be authored as `.ail` and parsed at compile time. Resolving the
+  inconsistency requires either (i) splitting the workspace loader
+  so prelude-init lives in `ailang-surface`, (ii) generating
+  `prelude.ail.json` at build time from `prelude.ail` via a
+  `build.rs`, or (iii) some other refactor — all of which exceed
+  the scope of this milestone.
+
+  The resolution lives in a separate roadmap milestone:
+  **"Prelude embed: Form-A as compile-time source"** (see
+  `docs/roadmap.md`). After that milestone closes, this carve-out
+  category becomes empty and the spec text drops it.
+
+  Note: `examples/prelude.ail` was rendered in iter form-a.0 and
+  remains the authoring projection (it stays in the tree; both
+  forms coexist for prelude specifically, mirroring the iter-0
+  pilot's dual-form witness arrangement, until the
+  prelude-embed-refactor milestone resolves the inconsistency).
+
+**Future additions to either list require brainstorm-level
+justification on the same structural grounds** — not "this test
+is annoying to migrate" or "the diff is large", but a named
+mechanism (canonical-form rejection / compile-time embed / etc.)
+that the surface cannot satisfy.
 
 ## Data flow
 
@@ -409,21 +459,29 @@ as a follow-up rename.
 ### T4. Carve-out coverage check
 
 A new test `crates/ailang-core/tests/carve_out_inventory.rs`
-asserts that exactly the seven named carve-out files exist under
+asserts that exactly the eight named carve-out files exist under
-`examples/*.ail.json` after milestone close. The test fails if a
+`examples/*.ail.json` after milestone close (seven from §C4 (a) +
-new `.ail.json` is added or a carve-out goes missing. The list
+one from §C4 (b)). The test fails if a new `.ail.json` is added
-is hardcoded in the test body — this is intentional: the carve-out
+or a carve-out goes missing. The list is hardcoded in the test
-list is part of the language's negative-test surface and any change
+body — this is intentional: the carve-out list is part of the
-to it is a deliberate, brainstorm-level decision.
+language's negative-test surface and any change to it is a
+deliberate, brainstorm-level decision. The test's pass-count
+drops to seven once the prelude-embed-refactor milestone retires
+`prelude.ail.json` from category (b); the test body is then
+re-published with the smaller list in that milestone's iter.
 
 ## Acceptance criteria
 
 The milestone closes when all of the following are true:
 
-1. `ls examples/*.ail.json | wc -l` returns `7`, and the seven
+1. `ls examples/*.ail.json | wc -l` returns `8`, and the eight
-   files match the carve-out list verbatim.
+   files match the carve-out list verbatim (§C4 category (a) +
-2. Every program in `examples/` other than the seven carve-outs
+   category (b)).
+2. Every program in `examples/` other than the eight carve-outs
    exists as a `.ail` file with no `.ail.json` sibling.
+   `examples/prelude.ail` exists in addition to
+   `examples/prelude.ail.json` per §C4 (b) (dual-form for prelude
+   only, pending the prelude-embed-refactor milestone).
 3. The roundtrip-CI restatement (T1) is green: parse is
    deterministic, idempotent under print, CLI-pipeline idempotent,
    and the carve-out inventory test (T4) passes.