From 3b4fb4277105407ba20d982c83088df1bbad5846 Mon Sep 17 00:00:00 2001 From: Brummel Date: Thu, 28 May 2026 17:04:41 +0200 Subject: [PATCH] =?UTF-8?q?plan:=20prep.3-kernel-tier-modules=20=E2=80=94?= =?UTF-8?q?=209-task=20schema=20+=20surface=20+=20workspace=20+=20diagnost?= =?UTF-8?q?ic=20+=20stub=20crate=20(refs=20#33)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Terminal iteration of the kernel-extension-mechanics milestone. Carves the spec's § Iteration prep.3 into nine bite-sized tasks: 1. Module.kernel field + ~130-site struct-literal sweep + drift round-trip + data-model anchor. 2. TypeDef.param_in field + ~30-site sweep + drift round-trip + anchor (BTreeMap>, kebab-cased `param-in`, skip-if-empty for hash stability). 3. Form-A (kernel) module-header attribute — parse + print + round-trip. 4. Form-A (param-in (a Int Float) (b Str)) TypeDef attribute — one outer clause, multiple inner var-lists (OQ1 decision). 5. Prelude becomes kernel-tier + loader generalisation: the hardcoded `&["prelude"]` literal at loader.rs:108 migrates to a `modules.values().filter(|m| m.kernel)` derivation; ReservedModuleName diagnostic repurposed; CLI mapping + hash-pin refresh in lockstep. 6. New crate `crates/ailang-kernel-stub/` — programmatic stub module via parse_kernel_stub() mirroring parse_prelude (OQ2 decision); wired into the loader; basic stub round-trip drift test ratifies the end-to-end mechanism. 7. CheckError::ParamNotInRestrictedSet variant + code() + ctx() + enforcement in check_type_well_formed's Type::Con arm + in-source RED/GREEN tests. 8. New workspace_kernel.rs integration tests — auto-import without explicit (import …), two kernel-tier modules co-load, explicit-import-overrides-auto-import precedence. 9. design/INDEX.md + design/models/0007-kernel-extensions.md STATUS + forward→present transitions for the now-shipped mechanisms. The four open questions raised by plan-recon are resolved up front in the "Open-question decisions" block so no task carries a TBD. ReservedModuleName variant shape stays `{ name: String }` (OQ3); workspace.rs:2655 stays a test-site literal (OQ4). The Module struct-literal sweep is the largest single mechanical edit (~130 sites; the additive #[serde(default)] covers JSON deserialise paths, only Rust struct literals break) — handled as a compiler-driven sweep inside Task 1, with the workspace-build gate validating no caller is deferred. TypeDef has ~30 sites. Compile-gate-vs-deferred-caller and pin/replacement-substring contiguity rules from planner self-review Step 5 are scrubbed: no signature change defers a caller past its own compile gate, no verbatim text edit pairs with a soft-wrappable presence pin. Recon report received DONE_WITH_CONCERNS — concerns were the four OQs, all decided in this plan. --- docs/plans/0103-prep.3-kernel-tier-modules.md | 1459 +++++++++++++++++ 1 file changed, 1459 insertions(+) create mode 100644 docs/plans/0103-prep.3-kernel-tier-modules.md diff --git a/docs/plans/0103-prep.3-kernel-tier-modules.md b/docs/plans/0103-prep.3-kernel-tier-modules.md new file mode 100644 index 0000000..a6ebd1e --- /dev/null +++ b/docs/plans/0103-prep.3-kernel-tier-modules.md @@ -0,0 +1,1459 @@ +# prep.3 — Kernel-tier modules + `param-in` — Implementation Plan + +> **Parent spec:** `docs/specs/0052-kernel-extension-mechanics.md` +> +> **For agentic workers:** REQUIRED SUB-SKILL: use the `implement` +> skill to run this plan. Steps use `- [ ]` checkboxes for tracking. + +**Goal:** Ship the third and terminal iteration of the kernel-extension-mechanics milestone: two coupled schema additions (`Module.kernel`, `TypeDef.param-in`), their Form-A surface, the generalisation of the hardcoded `prelude` auto-injection into a flag-driven multi-module mechanism, generic `param-in` checker enforcement with a new diagnostic, and a stub kernel crate as the end-to-end ratifying fixture. + +**Architecture:** Both schema fields are strictly additive — `Module.kernel` uses `skip_serializing_if = "is_false"`, `TypeDef.param_in` uses `skip_serializing_if = "BTreeMap::is_empty"` — so every pre-existing fixture's canonical-JSON hash is bit-stable except `prelude.ail`, which intentionally gains `(kernel)`. The workspace-load migration replaces the hardcoded `&["prelude"]` literal at `crates/ailang-surface/src/loader.rs:108` with a `modules.values().filter(|m| m.kernel)` derivation; the same `parse_prelude()` injection at line 103 remains because the prelude has no on-disk manifest in user workspaces. The `param-in` enforcement adds one diagnostic (`ParamNotInRestrictedSet`) and one pass in `check_type_well_formed`'s `Type::Con` arm; restriction data lives on the TypeDef and is consulted generically — no special-cased extension type in the checker. + +**Tech Stack:** `ailang-core` (schema + workspace-load), `ailang-surface` (Form-A parse/print + loader), `ailang-check` (diagnostic + enforcement), new `ailang-kernel-stub` crate (ratifying fixture), `serde` for the additive serialisation, `BTreeMap`/`BTreeSet` for deterministic `param-in` iteration order. + +--- + +## Open-question decisions (committed before plan-write) + +The plan-recon report flagged four open questions. Each is resolved here so no task carries a TBD: + +- **OQ1 — Form-A grammar for `(param-in ...)`.** **Decision:** one outer clause carrying one or more inner var-lists: `(param-in (a Int Float) (b Str))`. Mirrors `(ctors (A …) (B …))`; one parser arm, one printer arm; JSON BTreeMap shape is unambiguous. Rejected alternative: repeated `(param-in ...)` clauses (would force list-of-clauses gathering and break the "one attribute, one arm" parser pattern used elsewhere). +- **OQ2 — Stub form: programmatic vs `module.ail.json` embed.** **Decision:** programmatic. The stub crate's `src/lib.rs` exports `pub fn parse_kernel_stub() -> Module { parse(STUB_AIL).expect(...) }`, mirror of `parse_prelude` at `crates/ailang-surface/src/loader.rs:41-43`. `STUB_AIL` is a `const &str` carrying the Form-A source of the stub module. One source of truth, no embedded canonical-JSON duplication. +- **OQ3 — `WorkspaceLoadError::ReservedModuleName` shape.** **Decision:** keep `{ name: String }`. Only the doc comment and diagnostic message text change. No second consumer for a `reserved_set: Vec` field today; adding it now is premature mechanism. +- **OQ4 — `crates/ailang-core/src/workspace.rs:2655`.** **Decision:** the line lives in test code (`mq1_qualified_instancedef_class_accepted` body) and is one of ~20 test sites that pass `&["prelude"]` to `validate_canonical_type_names`. The validator helpers' signatures do not change in prep.3 — only the loader's *value* threaded into `build_workspace` changes. Test sites remain `&["prelude"]` literals; no migration. + +--- + +## Files this plan creates or modifies + +**Create:** + +- `crates/ailang-kernel-stub/Cargo.toml` — new internal crate, mirror of `crates/ailang-prose/Cargo.toml` shape (package metadata + `ailang-surface.workspace = true`, `ailang-core.workspace = true`). +- `crates/ailang-kernel-stub/src/lib.rs` — exposes `parse_kernel_stub() -> Module`; `STUB_AIL` is a `const &str` carrying the Form-A source. +- `crates/ailang-core/tests/workspace_kernel.rs` — integration tests for auto-import semantics (kernel-tier visibility without explicit `(import ...)`, two kernel-tier modules co-load, explicit-import-overrides-auto-import precedence). + +**Modify (source code):** + +- `crates/ailang-core/src/ast.rs:29-42` — `Module` gains `pub kernel: bool` with `#[serde(default, skip_serializing_if = "is_false")]`. +- `crates/ailang-core/src/ast.rs:135-170` — `TypeDef` gains `pub param_in: BTreeMap>` with `#[serde(default, skip_serializing_if = "BTreeMap::is_empty", rename = "param-in")]`; new `use std::collections::{BTreeMap, BTreeSet}` import at the top of the file. +- ~130 `Module { ... }` struct-literal sites across `crates/{ailang-prose, ailang-codegen, ailang-surface, ailang-check, ailang-core}/src/` and `crates/{ailang-check, ailang-surface}/tests/` — add `kernel: false,` to each (mechanical sweep; the additive `#[serde(default)]` covers deserialise paths, only Rust struct literals break). +- ~30 `TypeDef { ... }` struct-literal sites across `crates/{ailang-prose, ailang-codegen, ailang-check, ailang-core}/src/` and `crates/{ailang-check, ailang-core}/tests/` — add `param_in: BTreeMap::new(),` to each. +- `crates/ailang-surface/src/parse.rs:283-335` — `parse_module` gains a `(kernel)` attribute case before the defs/imports loop. +- `crates/ailang-surface/src/parse.rs:354-436` — `parse_data` (TypeDef parser) gains a `(param-in (var t1 t2 ...) ...)` case in its inner attribute loop. +- `crates/ailang-surface/src/print.rs:17-33` — `Module` printer emits `(kernel)` when `module.kernel == true`. +- `crates/ailang-surface/src/print.rs:103-135` — `write_type_def` emits `(param-in ( ...) ...)` blocks when `!td.param_in.is_empty()`. +- `crates/ailang-surface/src/loader.rs:88-110` — `load_workspace`: hardcoded `&["prelude"]` literal and the `"prelude"` reservation literal replaced by derivation from `modules.values().filter(|m| m.kernel)`. The `parse_prelude()` injection at line 103 stays. +- `crates/ailang-core/src/workspace.rs:307-312` — `ReservedModuleName` doc comment + diagnostic prose update; variant shape `{ name: String }` unchanged. +- `crates/ailang-core/src/workspace.rs:465-493` — `build_workspace` doc-comment update (signature unchanged; doc clarifies the implicit-imports list is caller-derived from the kernel-flag filter). +- `crates/ail/src/main.rs:1234-1244` — CLI mapping for `ReservedModuleName` diagnostic — human message text update. +- `crates/ailang-check/src/lib.rs:721-742` — new `CheckError::ParamNotInRestrictedSet` variant adjacent to existing `NewArgKindMismatch`. +- `crates/ailang-check/src/lib.rs:797-798` — `CheckError::code()` arm for the new variant. +- `crates/ailang-check/src/lib.rs:876-879` — `CheckError::ctx()` arm for the new variant. +- `crates/ailang-check/src/lib.rs:1920-1998` — `check_type_well_formed`'s `Type::Con` arm walks the resolved TypeDef's `param_in` and emits `ParamNotInRestrictedSet` on violation. New in-source tests in the same file's `#[cfg(test)] mod tests` block: `param_in_accepts_allowed_type`, `param_in_rejects_disallowed_type`. +- `examples/prelude.ail:1` — module header gains `(kernel)`. + +**Modify (tests):** + +- `crates/ailang-core/tests/design_schema_drift.rs` — append three new round-trip tests (`module_kernel_flag_round_trips`, `typedef_param_in_round_trips`, `kernel_stub_module_round_trips`) modelled on the existing `term_new_round_trips`/`term_new_type_arg_round_trips` (lines 559-629). Also `param_in` field added to the `TypeDef` literal at line 323-329 (compile gate). +- `crates/ailang-surface/tests/prelude_module_hash_pin.rs:27` — refresh the pinned hex hash because the prelude's canonical-JSON now contains `"kernel": true`; Honesty-Rule provenance comment block above the literal quoting prep.3 (mirrors lines 15-25 prior re-pin reasons). +- `crates/ailang-surface/tests/round_trip.rs` (or analogous existing surface round-trip file) — fixtures for `(kernel)` in module header and `(param-in ...)` in TypeDef body. + +**Modify (design ledger):** + +- `design/contracts/0002-data-model.md:14-23` — Module schema block gains `"kernel": true // optional; omitted when false (hash-stable when omitted)` line and a "see prep.3 of the kernel-extension-mechanics milestone" footnote in the prose section. +- `design/contracts/0002-data-model.md:55-66` — TypeDef schema block gains `"param-in": { "": ["", ...] } // optional; omitted when empty (hash-stable when omitted)` line. +- `design/INDEX.md:111` — annotation update for the `kernel-extensions` row (the `(design accepted 2026-05-28; impl in progress)` annotation transitions to reflect milestone-close state once prep.3 lands). +- `design/models/0007-kernel-extensions.md:1-12 + 215-276` — STATUS header transitions prep.3 from "in progress" to "shipped"; sections describing the kernel-tier mechanism and `param-in` transition from forward-looking ("will resolve…") to present-state ("resolves…"). + +--- + +### Task 1: `Module.kernel` schema field + struct-literal sweep + drift round-trip + data-model anchor + +**Files:** +- Modify: `crates/ailang-core/src/ast.rs:29-42` +- Modify: ~130 `Module { ... }` struct-literal sites enumerated by `rg -n '\bModule \{' --type rust crates/` — top concentrations: `crates/ailang-codegen/src/lib.rs` (~22 sites), `crates/ailang-check/src/lib.rs` (~25 sites), `crates/ailang-check/src/linearity.rs` (~14 sites), `crates/ailang-check/src/uniqueness.rs` (~5 sites), `crates/ailang-check/src/reuse_shape.rs` (~3 sites), `crates/ailang-core/src/desugar.rs` (~16 sites), `crates/ailang-core/src/pretty.rs` (~1 site), `crates/ailang-prose/src/lib.rs` (~2 sites), `crates/ailang-surface/src/parse.rs` (1 site at line 329), `crates/ailang-surface/src/print.rs` (~5 sites), `crates/ailang-check/tests/workspace.rs` (~6 sites), `crates/ailang-check/tests/duplicate_ctor_pin.rs` (1 site), `crates/ailang-core/src/workspace.rs` (~4 test-helper sites in `mod tests`). +- Test: `crates/ailang-core/tests/design_schema_drift.rs` — append `module_kernel_flag_round_trips`. +- Modify: `design/contracts/0002-data-model.md:14-23` — anchor block. + +- [ ] **Step 1: Add `Module.kernel` field** + +In `crates/ailang-core/src/ast.rs`, replace the existing Module struct definition at lines 29-42 with: + +```rust +pub struct Module { + /// Schema identifier; must equal [`crate::SCHEMA`] at load time. + pub schema: String, + /// Module name. By convention matches the file stem + /// (`.ail.json`); the [`crate::workspace`] loader enforces + /// this on import. + pub name: String, + /// Kernel-tier flag. When `true`, the module's top-level type + /// names and free defs are visible to every consumer without an + /// explicit `(import …)` declaration. Strictly additive: omitted + /// from canonical JSON when `false`, so every pre-existing + /// fixture's hash is bit-stable. See prep.3 of the + /// kernel-extension-mechanics milestone. + #[serde(default, skip_serializing_if = "is_false")] + pub kernel: bool, + /// Imports of other modules. Resolved by the workspace loader as + /// `/.ail.json`. + #[serde(default)] + pub imports: Vec, + /// Top-level definitions in declaration order. + pub defs: Vec, +} +``` + +(`is_false` already exists at `crates/ailang-core/src/ast.rs:931`; no new helper.) + +- [ ] **Step 2: Surface compile errors across the workspace** + +Run: `cargo build --workspace 2>&1 | rg 'missing field .kernel.' | wc -l` +Expected: a positive integer ~130 (each `Module { ... }` literal site missing the new field; the exact count is informational — the next step uses the build's own error list as the work queue). + +- [ ] **Step 3: Mechanical sweep — add `kernel: false,` to every Module struct-literal site** + +For each compile error of shape `error[E0063]: missing field \`kernel\` in initializer of \`ailang_core::ast::Module\``, open the file/line, insert `kernel: false,` into the struct literal. Insertion order convention: between `name: ...,` and `imports: ...,` (mirrors the field declaration order in `ast.rs`). For one-line literals, the field becomes a comma-separated element; for multi-line literals, it gets its own line at the same indentation as the surrounding fields. + +Example (`crates/ailang-surface/src/parse.rs:329` — the parser's only construction): + +Before: +```rust +Ok(Module { + schema: SCHEMA.to_string(), + name, + imports, + defs, +}) +``` + +After: +```rust +Ok(Module { + schema: SCHEMA.to_string(), + name, + kernel: false, + imports, + defs, +}) +``` + +(`parse_module` will set `kernel` from the parsed `(kernel)` attribute in Task 3; for now the parser still emits `kernel: false` by default, matching modules that have no attribute. Task 3 replaces this literal with the parsed value.) + +- [ ] **Step 4: Compile-gate** + +Run: `cargo build --workspace 2>&1 | tail -5` +Expected: no `error[E0063]` lines; build succeeds (warnings are acceptable but the build must terminate with exit code 0). + +- [ ] **Step 5: Update Module schema anchor in data-model contract** + +In `design/contracts/0002-data-model.md`, replace lines 14-23 with: + +```markdown +### Module + +```jsonc +{ + "schema": "ailang/v0", + "name": "", + "kernel": true, // optional; omitted when false (hash-stable when omitted). Kernel-tier modules are auto-imported by every consumer. See prep.3 of the kernel-extension-mechanics milestone. + "imports": [{ "module": "", "as": "" }], + "defs": [Def...] +} +``` +``` + +(The kebab/case naming check in `design_schema_drift.rs`'s anchor scan will accept the bare `kernel` key because it is camelCase-already; the lowercase Rust field name serialises unchanged.) + +- [ ] **Step 6: Add `module_kernel_flag_round_trips` drift test** + +Append to `crates/ailang-core/tests/design_schema_drift.rs` (after the existing `term_new_type_arg_round_trips` at line 629): + +```rust +/// prep.3 (kernel-extension-mechanics): pin the JSON byte-shape of +/// `Module.kernel`. Property protected: when `true`, the key +/// serialises as the bare `"kernel": true` flag adjacent to +/// `"name"`; when `false`, it is omitted entirely from canonical +/// JSON (preserving the bit-identical hash of every pre-existing +/// fixture). A future edit that renames the field, drops the +/// `skip_serializing_if`, or changes its boolean shape breaks the +/// pin in lockstep with the data-model document. +#[test] +fn module_kernel_flag_round_trips() { + let m_on = Module { + schema: ailang_core::SCHEMA.to_string(), + name: "k".into(), + kernel: true, + imports: vec![], + defs: vec![], + }; + let json_on = serde_json::to_value(&m_on).expect("serialise kernel: true"); + assert_eq!( + json_on["kernel"], true, + "kernel: true must appear as a bare boolean key" + ); + + let m_off = Module { + schema: ailang_core::SCHEMA.to_string(), + name: "k".into(), + kernel: false, + imports: vec![], + defs: vec![], + }; + let json_off = serde_json::to_value(&m_off).expect("serialise kernel: false"); + assert!( + json_off.get("kernel").is_none(), + "kernel: false must be omitted from canonical JSON (hash-stability)" + ); + + let recovered: Module = + serde_json::from_value(json_on).expect("Module with kernel: true round-trips"); + assert!(recovered.kernel); +} +``` + +- [ ] **Step 7: Run drift tests** + +Run: `cargo test --workspace --test design_schema_drift module_kernel_flag_round_trips` +Expected: 1 passed. + +Run: `cargo test --workspace --test design_schema_drift` +Expected: all prior drift tests pass; the new one passes. Result line: `N passed; 0 failed`. + +--- + +### Task 2: `TypeDef.param_in` schema field + struct-literal sweep + drift round-trip + data-model anchor + +**Files:** +- Modify: `crates/ailang-core/src/ast.rs:20` (imports) + `crates/ailang-core/src/ast.rs:135-170` (struct). +- Modify: ~30 `TypeDef { ... }` struct-literal sites enumerated by `rg -n '\bTypeDef \{' --type rust crates/` — top concentrations: `crates/ailang-check/src/lib.rs` (~12 sites), `crates/ailang-prose/src/lib.rs` (~6 sites), `crates/ailang-codegen/src/lib.rs` (~2 sites), `crates/ailang-check/tests/workspace.rs` (~4 sites), `crates/ailang-check/tests/duplicate_ctor_pin.rs` (2 sites), `crates/ailang-surface/src/parse.rs` (1 site at line 429), `crates/ailang-core/tests/spec_drift.rs` (1 site at line 281), `crates/ailang-core/tests/design_schema_drift.rs` (1 site at line 323), `crates/ailang-check/src/reuse_shape.rs` (1 site), `crates/ailang-check/src/linearity.rs` (~2 sites), `crates/ailang-core/src/desugar.rs` (1 site at line 2175). +- Test: `crates/ailang-core/tests/design_schema_drift.rs` — append `typedef_param_in_round_trips`. +- Modify: `design/contracts/0002-data-model.md:55-66` — anchor block. + +- [ ] **Step 1: Add `use std::collections::{BTreeMap, BTreeSet}` import** + +In `crates/ailang-core/src/ast.rs`, locate the existing `use` block at the top of the file (currently absent for `BTreeMap`/`BTreeSet` per `head -25` inspection during recon). Add: + +```rust +use std::collections::{BTreeMap, BTreeSet}; +``` + +(Insert above the existing `use serde::{Deserialize, Serialize};` line.) + +- [ ] **Step 2: Add `TypeDef.param_in` field** + +In `crates/ailang-core/src/ast.rs`, after the `drop_iterative` field at lines 164-169 and before the closing brace at line 170, insert: + +```rust + /// Closed-set restriction on type-parameter instantiation. Maps + /// each var name (drawn from [`Self::vars`]) to a set of allowed + /// concrete type names. When non-empty, the checker enforces + /// that every `Type::Con { name: , args }` carries an + /// `args[i]` whose outermost type-name lies in the restricted + /// set for that variable. + /// + /// Serialised as `"param-in": { "": ["", ...] }` + /// (kebab-case); the field is **omitted when empty**, preserving + /// the canonical-JSON hash of every fixture that does not + /// restrict. + /// + /// See prep.3 of the kernel-extension-mechanics milestone and + /// the new diagnostic + /// [`crate::check::CheckError::ParamNotInRestrictedSet`]. + #[serde( + default, + rename = "param-in", + skip_serializing_if = "BTreeMap::is_empty" + )] + pub param_in: BTreeMap>, +``` + +- [ ] **Step 3: Surface compile errors** + +Run: `cargo build --workspace 2>&1 | rg 'missing field .param_in.' | wc -l` +Expected: a positive integer ~30. + +- [ ] **Step 4: Mechanical sweep — add `param_in: BTreeMap::new(),` to every TypeDef struct-literal site** + +For each `error[E0063]: missing field \`param_in\` in initializer of \`ailang_core::ast::TypeDef\``, open the file/line, insert `param_in: BTreeMap::new(),` into the struct literal. Insertion order: after `drop_iterative: ...,` and before the closing `}`. + +The `BTreeMap` import is already present in `crates/ailang-core/src/ast.rs`; for other crates that construct `TypeDef`, the use statement at the top of each file must mention `BTreeMap` via either `use std::collections::BTreeMap;` (if absent) or import along with existing collection imports. + +Example (`crates/ailang-surface/src/parse.rs:429`): + +Before: +```rust +Ok(TypeDef { + name, + vars, + ctors, + doc, + drop_iterative, +}) +``` + +After: +```rust +Ok(TypeDef { + name, + vars, + ctors, + doc, + drop_iterative, + param_in: BTreeMap::new(), +}) +``` + +(Add `use std::collections::BTreeMap;` near the top of `parse.rs` if absent. Verify by running `rg 'use std::collections::BTreeMap' crates/ailang-surface/src/parse.rs` — empty result means add it.) + +- [ ] **Step 5: Compile-gate** + +Run: `cargo build --workspace 2>&1 | tail -5` +Expected: no `error[E0063]` lines; build succeeds. + +- [ ] **Step 6: Update TypeDef schema anchor in data-model contract** + +In `design/contracts/0002-data-model.md`, replace lines 56-66 with: + +```markdown +// type (algebraic data type; parameterised) +{ "kind": "type", + "name": "", + "vars": [""...], // type parameters; omitted when empty (hash-stable when omitted) + "ctors": [ + { "name": "", "fields": [Type...] } // nullary ctor: fields = [] + ... + ], + "doc": "", + "drop-iterative": true, // opt-in; omitted when false (hash-stable when omitted) + "param-in": { "": ["", ...] } // closed-set restriction per type variable; omitted when empty (hash-stable when omitted). See prep.3 of the kernel-extension-mechanics milestone. +} +``` + +- [ ] **Step 7: Add `typedef_param_in_round_trips` drift test** + +Append to `crates/ailang-core/tests/design_schema_drift.rs`: + +```rust +/// prep.3 (kernel-extension-mechanics): pin the JSON byte-shape of +/// `TypeDef.param_in`. Property protected: when non-empty, the map +/// serialises under the kebab-case key `"param-in"`; when empty, +/// it is omitted entirely (preserving the bit-identical hash of +/// every fixture that does not restrict). The BTreeMap/BTreeSet +/// choice gives deterministic iteration order (alphabetical) so +/// the canonical-JSON bytes are reproducible. A future edit that +/// renames the field, drops the `skip_serializing_if`, or changes +/// the inner collection type breaks the pin in lockstep with the +/// data-model document. +#[test] +fn typedef_param_in_round_trips() { + use std::collections::{BTreeMap, BTreeSet}; + + let mut restrict: BTreeMap> = BTreeMap::new(); + restrict.insert( + "a".into(), + ["Int".to_string(), "Float".to_string()].into_iter().collect(), + ); + + let td_on = TypeDef { + name: "T".into(), + vars: vec!["a".into()], + ctors: vec![], + doc: None, + drop_iterative: false, + param_in: restrict.clone(), + }; + let json_on = serde_json::to_value(&td_on).expect("serialise param_in non-empty"); + let pi = json_on.get("param-in").expect( + "non-empty param_in serialises under kebab key `param-in`", + ); + let allowed = pi["a"].as_array().expect("inner value is a Type-name array"); + assert_eq!(allowed.len(), 2); + // BTreeSet iteration order is alphabetical: + assert_eq!(allowed[0], "Float"); + assert_eq!(allowed[1], "Int"); + + let td_off = TypeDef { + name: "T".into(), + vars: vec![], + ctors: vec![], + doc: None, + drop_iterative: false, + param_in: BTreeMap::new(), + }; + let json_off = serde_json::to_value(&td_off).expect("serialise param_in empty"); + assert!( + json_off.get("param-in").is_none(), + "empty param_in must be omitted from canonical JSON (hash-stability)" + ); + + let recovered: TypeDef = + serde_json::from_value(json_on).expect("TypeDef with param_in round-trips"); + assert_eq!(recovered.param_in, restrict); +} +``` + +- [ ] **Step 8: Run drift tests** + +Run: `cargo test --workspace --test design_schema_drift typedef_param_in_round_trips` +Expected: 1 passed. + +Run: `cargo test --workspace --test design_schema_drift` +Expected: all drift tests pass. + +--- + +### Task 3: Form-A surface — `(kernel)` module-header attribute + +**Files:** +- Modify: `crates/ailang-surface/src/parse.rs:283-335` — `parse_module` gains a `(kernel)` attribute case. +- Modify: `crates/ailang-surface/src/print.rs:17-33` — Module printer emits `(kernel)` when set. +- Test: `crates/ailang-surface/tests/round_trip.rs` (or the file that holds surface round-trip fixtures; verify with `rg -l 'round_trip' crates/ailang-surface/tests/`). + +- [ ] **Step 1: Locate the existing module-header attribute precedent** + +Run: `rg -n '"drop-iterative"|drop_iterative' crates/ailang-surface/src/parse.rs | head -6` +Expected: hits in `parse_data` (~lines 385-413 per recon). The `(drop-iterative)` attribute parsing in `parse_data` is the structural mirror for `(kernel)` in `parse_module` — both are bare flag attributes (no inner data). + +- [ ] **Step 2: Add `(kernel)` parsing to `parse_module`** + +Open `crates/ailang-surface/src/parse.rs`. Inside `parse_module` (starts at line 283), after the line that calls `expect_ident("module name")?` (around line 286) and before the main `(import|data|fn|...)` dispatch loop, parse zero or more bare attribute clauses. + +Insert a local `let mut kernel = false;` before the dispatch loop. Then, at the top of the loop body, before the existing `(import|...)` cases, add: + +```rust + Some("kernel") => { + // (kernel) — bare flag, no inner content. + self.expect_close_paren_after_keyword("kernel")?; + kernel = true; + } +``` + +(The exact helper-method names follow the surrounding parser style. If `expect_close_paren_after_keyword` doesn't exist, mirror the close-paren consumption pattern used immediately after `(drop-iterative)` in `parse_data`'s arm — typically `self.expect(Token::CloseParen)` or `self.consume_close_paren("kernel")`. Implementer reads the local idiom and applies it.) + +At the bottom of `parse_module`, where the existing `Ok(Module { ... })` literal is constructed (line 329 per Task 1), thread `kernel` into the struct literal in place of the `false` placeholder Task 1 inserted: + +Before (after Task 1): +```rust +Ok(Module { + schema: SCHEMA.to_string(), + name, + kernel: false, + imports, + defs, +}) +``` + +After: +```rust +Ok(Module { + schema: SCHEMA.to_string(), + name, + kernel, + imports, + defs, +}) +``` + +- [ ] **Step 3: Add `(kernel)` printing to `Module` print** + +Open `crates/ailang-surface/src/print.rs`. Locate the `Module` print function (around lines 17-33; recon reports the function emits `(module ` then iterates imports/defs). + +After the `(module ` head is emitted and before the imports block, insert (matching the surrounding line-write idiom): + +```rust + if m.kernel { + // (kernel) attribute marks this as a kernel-tier module — + // every consumer auto-imports its types and free defs. + writeln!(w, " (kernel)")?; + } +``` + +(Exact indent and writer macro follow the local style in `print.rs`. If the printer's existing convention is `write!(w, ...)` instead of `writeln!`, mirror it.) + +- [ ] **Step 4: Write a round-trip test for `(kernel)`** + +Locate the existing surface round-trip test file with: `rg -l '#\[test\]' crates/ailang-surface/tests/`. The canonical file is `crates/ailang-surface/tests/round_trip.rs` (or equivalent). Append: + +```rust +/// prep.3 (kernel-extension-mechanics): the `(kernel)` module-header +/// attribute round-trips Form-A → JSON → Form-A bit-identical and +/// preserves the parsed bool through both halves. +#[test] +fn kernel_module_header_round_trips() { + let src = "(module k (kernel))\n"; + let m = ailang_surface::parse(src).expect("Form-A parse of (kernel) module"); + assert!(m.kernel, "parsed kernel: true"); + + let printed = ailang_surface::print(&m).expect("print the kernel module"); + // Round-trip: print, re-parse, kernel still true. + let m2 = ailang_surface::parse(&printed).expect("re-parse printed form"); + assert!(m2.kernel, "kernel: true survives round-trip"); + + // Default form (no (kernel)) stays kernel: false. + let plain = ailang_surface::parse("(module p)\n").expect("Form-A parse plain module"); + assert!(!plain.kernel); +} +``` + +- [ ] **Step 5: Compile-gate + run new test** + +Run: `cargo build --workspace 2>&1 | tail -3` +Expected: build succeeds. + +Run: `cargo test --workspace -p ailang-surface kernel_module_header_round_trips` +Expected: 1 passed. + +- [ ] **Step 6: Regression-protect existing surface tests** + +Run: `cargo test --workspace -p ailang-surface 2>&1 | tail -5` +Expected: all surface tests pass (Form-A surface change is additive). + +--- + +### Task 4: Form-A surface — `(param-in (var t1 t2 ...))` TypeDef attribute + +**Files:** +- Modify: `crates/ailang-surface/src/parse.rs:354-436` — `parse_data` gains a `(param-in ...)` case. +- Modify: `crates/ailang-surface/src/print.rs:103-135` — `write_type_def` emits `(param-in ...)` blocks when set. +- Test: `crates/ailang-surface/tests/round_trip.rs` — fixture for `(param-in ...)`. + +- [ ] **Step 1: Add `(param-in ...)` parsing to `parse_data`** + +Open `crates/ailang-surface/src/parse.rs`. Inside `parse_data` (starts at line 354), the inner attribute-loop dispatches on `doc / ctor / drop-iterative` (per recon, lines 374-427). Add a `param-in` arm. + +Before the loop, insert: `let mut param_in: BTreeMap> = BTreeMap::new();` (matching the local-var convention used for `vars`, `ctors`, etc.). + +Inside the loop, add an arm for `Some("param-in")`: + +```rust + Some("param-in") => { + // (param-in (a Int Float) (b Str) ...) — one outer + // clause carrying one or more inner var-lists. + while !self.peek_close_paren() { + self.expect_open_paren("inner var-list of (param-in ...)")?; + let var = self.expect_ident("type-variable name")?; + let mut allowed = BTreeSet::new(); + while !self.peek_close_paren() { + let tname = self.expect_ident("allowed type-name")?; + allowed.insert(tname); + } + self.expect_close_paren()?; + if param_in.insert(var.clone(), allowed).is_some() { + return Err(self.err_at(format!( + "param-in: duplicate var binding `{}`", + var + ))); + } + } + self.expect_close_paren()?; + } +``` + +(The helper names `peek_close_paren`, `expect_open_paren`, `expect_close_paren`, `expect_ident`, `err_at` follow the local parser style. If exact spellings differ, the implementer reads the surrounding arms — particularly the `ctor` arm, which has a similar nested-list shape — and adopts the local idiom verbatim.) + +In the unknown-attribute error path at line 420, extend the error message to mention `param-in` alongside the existing attribute names. + +At the bottom of `parse_data`, where `Ok(TypeDef { ... })` is constructed (line 429 per Task 2), thread `param_in` into the struct literal in place of the `BTreeMap::new()` placeholder Task 2 inserted: + +Before (after Task 2): +```rust +Ok(TypeDef { + name, + vars, + ctors, + doc, + drop_iterative, + param_in: BTreeMap::new(), +}) +``` + +After: +```rust +Ok(TypeDef { + name, + vars, + ctors, + doc, + drop_iterative, + param_in, +}) +``` + +Ensure `use std::collections::{BTreeMap, BTreeSet};` is at the top of `parse.rs` (Task 2 may already have added `BTreeMap`; extend to `{BTreeMap, BTreeSet}` if needed). + +- [ ] **Step 2: Add `(param-in ...)` printing to `write_type_def`** + +Open `crates/ailang-surface/src/print.rs`. Locate `write_type_def` (around lines 103-135; recon reports a `drop_iterative` emit at lines 126-133 — the structural mirror). + +After the `drop_iterative` block and before the closing of the `(type ...)` form, insert: + +```rust + if !td.param_in.is_empty() { + // (param-in (a Int Float) (b Str) ...) — BTreeMap/BTreeSet + // give deterministic alphabetical iteration order. + write!(w, " (param-in")?; + for (var, allowed) in &td.param_in { + write!(w, " ({}", var)?; + for tname in allowed { + write!(w, " {}", tname)?; + } + write!(w, ")")?; + } + writeln!(w, ")")?; + } +``` + +(Adapt indent/writer macro to the local style. The convention is single-space separation between inner items.) + +- [ ] **Step 3: Write a round-trip test for `(param-in ...)`** + +Append to `crates/ailang-surface/tests/round_trip.rs`: + +```rust +/// prep.3 (kernel-extension-mechanics): the `(param-in (var t1 t2 ...))` +/// TypeDef attribute round-trips Form-A → JSON → Form-A bit- +/// identical and preserves the parsed BTreeMap through both halves, +/// including the BTreeSet's deterministic alphabetical iteration +/// order. +#[test] +fn typedef_param_in_round_trips_surface() { + let src = concat!( + "(module m\n", + " (data T (vars a)\n", + " (param-in (a Int Float))\n", + " (ctors (MkT a))))\n" + ); + let m = ailang_surface::parse(src).expect("Form-A parse of (param-in ...)"); + let td = match &m.defs[0] { + ailang_core::ast::Def::Type(t) => t, + _ => panic!("expected Type def"), + }; + let allowed = td.param_in.get("a").expect("var `a` bound in param_in"); + assert!(allowed.contains("Int")); + assert!(allowed.contains("Float")); + assert_eq!(allowed.len(), 2); + + let printed = ailang_surface::print(&m).expect("print the module"); + let m2 = ailang_surface::parse(&printed).expect("re-parse printed form"); + let td2 = match &m2.defs[0] { + ailang_core::ast::Def::Type(t) => t, + _ => panic!("expected Type def after round-trip"), + }; + assert_eq!(td2.param_in, td.param_in, "param_in survives round-trip"); +} +``` + +- [ ] **Step 4: Compile-gate + run new test** + +Run: `cargo build --workspace 2>&1 | tail -3` +Expected: build succeeds. + +Run: `cargo test --workspace -p ailang-surface typedef_param_in_round_trips_surface` +Expected: 1 passed. + +Run: `cargo test --workspace -p ailang-surface 2>&1 | tail -5` +Expected: all surface tests pass. + +--- + +### Task 5: Prelude becomes kernel-tier + loader generalisation + +**Files:** +- Modify: `examples/prelude.ail:1` — gains `(kernel)` attribute. +- Modify: `crates/ailang-surface/src/loader.rs:88-110` — `load_workspace` migrates from hardcoded `&["prelude"]` to flag-driven derivation. +- Modify: `crates/ailang-core/src/workspace.rs:307-312` — `ReservedModuleName` doc + diagnostic prose. +- Modify: `crates/ailang-core/src/workspace.rs:465-493` — `build_workspace` doc comment update. +- Modify: `crates/ail/src/main.rs:1234-1244` — CLI mapping for `ReservedModuleName` diagnostic. +- Modify: `crates/ailang-surface/tests/prelude_module_hash_pin.rs:27` — refresh hex hash + Honesty-Rule comment. + +- [ ] **Step 1: Add `(kernel)` to the prelude** + +Open `examples/prelude.ail`. The first line is currently `(module prelude` (verified by recon). Edit to: + +``` +(module prelude (kernel) +``` + +(Bare `(kernel)` immediately after the module name on the same line. Whitespace/format follows the existing module's style.) + +- [ ] **Step 2: Migrate the loader's hardcoded prelude paths** + +Open `crates/ailang-surface/src/loader.rs`. Replace lines 95-110 (the body of `load_workspace`) with: + +```rust +pub fn load_workspace(entry: &Path) -> Result { + let (entry_name, root_dir, mut modules) = + ailang_core::workspace::load_modules_with(entry, load_module)?; + + // parse_prelude() injects the built-in prelude into the + // workspace. The prelude module's source carries `(kernel)`, so + // it surfaces in the kernel-tier auto-import set below. + if modules.contains_key("prelude") { + return Err(WorkspaceLoadError::ReservedModuleName { + name: "prelude".to_string(), + }); + } + modules.insert("prelude".to_string(), parse_prelude()); + + // Derive the implicit-imports list from `kernel: true` modules. + // Replaces the previous hardcoded `&["prelude"]` literal: any + // workspace-loaded module that carries the kernel flag is now + // auto-imported. See prep.3 of the kernel-extension-mechanics + // milestone. + let kernel_names: Vec = modules + .values() + .filter(|m| m.kernel) + .map(|m| m.name.clone()) + .collect(); + let implicit_imports: Vec<&str> = + kernel_names.iter().map(String::as_str).collect(); + + ailang_core::workspace::build_workspace( + entry_name, + root_dir, + modules, + &implicit_imports, + ) +} +``` + +(`build_workspace`'s signature does not change; only the value of its fourth argument is now caller-derived. The `kernel_names: Vec` lives across the borrow scope so the `&[&str]` slice is valid.) + +- [ ] **Step 3: Update `ReservedModuleName` doc + diagnostic prose** + +Open `crates/ailang-core/src/workspace.rs`. At lines 307-312, replace the variant's doc comment and (if the variant carries a literal message) any embedded prose with: + +```rust + /// A user workspace contains a module whose name collides with + /// a built-in kernel-tier module that the loader auto-injects. + /// The current built-in set is `prelude` (and, in test/dev + /// builds, `kernel_stub`); future base extensions may add more. + /// Previously this variant fired specifically for `prelude`; + /// since prep.3 of the kernel-extension-mechanics milestone, it + /// fires for any built-in kernel module name. + ReservedModuleName { name: String }, +``` + +(The struct shape `{ name: String }` is unchanged per OQ3. Only the doc comment changes. If the variant has a `#[error(...)]` attribute carrying a literal message, update it to: + +```rust + #[error("workspace module `{name}` collides with a built-in kernel-tier module name (reserved)")] +``` + +Verify by searching `rg -nE '#\[error\(' crates/ailang-core/src/workspace.rs | rg ReservedModuleName -B0 -A0` — the literal lives near the variant declaration.) + +- [ ] **Step 4: Update `build_workspace` doc comment** + +In `crates/ailang-core/src/workspace.rs:465-476`, update the function-level doc comment for `build_workspace` to clarify the new caller-derived semantics. Replace any wording of the form "implicit_imports = typically just prelude" with: + +```rust +/// `implicit_imports` is the list of module names every consumer +/// should auto-import without an explicit `(import …)` declaration. +/// The caller (typically `ailang_surface::loader::load_workspace`) +/// derives this list from the kernel-tier filter: every loaded +/// module with `kernel: true` enters the list. Since prep.3 of the +/// kernel-extension-mechanics milestone, this is the flag-driven +/// generalisation of the prior hardcoded `&["prelude"]` literal. +``` + +(Exact placement: above the `pub fn build_workspace(...)` signature, replacing or extending the existing doc block.) + +- [ ] **Step 5: Update CLI mapping for `ReservedModuleName`** + +Open `crates/ail/src/main.rs`. At lines 1234-1244, the `ReservedModuleName` arm of the diagnostic translator currently emits prose referencing `prelude` specifically. Update the user-facing message to: + +```rust + WorkspaceLoadError::ReservedModuleName { name } => Diagnostic { + code: "WORKSPACE_RESERVED_MODULE_NAME".into(), + message: format!( + "Module `{}` collides with a built-in kernel-tier module name. The built-in set is reserved; pick a different module name.", + name + ), + // …other fields unchanged… + }, +``` + +(Exact field set and surrounding match shape follow the existing arm. The `ctx` field, if present, keeps the `name` entry.) + +- [ ] **Step 6: Refresh the prelude hash pin** + +Open `crates/ailang-surface/tests/prelude_module_hash_pin.rs`. Above the literal hex hash at line 27, add a new comment block in the established style (mirror lines 15-25 — two prior re-pin reasons are logged there): + +```rust +// prep.3 (kernel-extension-mechanics) — prelude becomes kernel-tier: +// `examples/prelude.ail` gains the `(kernel)` module-header attribute, +// which serialises as `"kernel": true` in the canonical JSON. This +// changes the prelude's content hash deterministically; the new hex +// pin replaces the prior `562a03fc57e7e017`. The behaviour +// `prelude_free_fns.rs` protects (12 free fns callable bare in every +// consumer) is unchanged — only the code path migrates from the +// hardcoded `&["prelude"]` literal to the kernel-flag filter. +``` + +Then determine the new hash. Run: `cargo test --workspace -p ailang-surface --test prelude_module_hash_pin -- --nocapture 2>&1 | rg -A2 'assertion .*failed' | head -10`. The failure message reports the *actual* hash. Copy that hex value into the test file's pin literal in place of the old one. Re-run to confirm green: + +Run: `cargo test --workspace -p ailang-surface --test prelude_module_hash_pin` +Expected: PASS. + +- [ ] **Step 7: Regression-protect `prelude_free_fns.rs`** + +Run: `cargo test --workspace -p ail --test prelude_free_fns 2>&1 | tail -5` +Expected: all tests pass. (This is the explicit regression for the prelude code-path migration — observable behaviour must be identical.) + +- [ ] **Step 8: Regression-protect CLI assertion test** + +Run: `cargo test --workspace -p ail --test ct1_check_cli 2>&1 | tail -5` +Expected: all tests pass. (The CLI mapping update at Step 5 changed user-facing prose; ct1 may assert on it. If a test asserts the old prelude-specific prose, update the assertion to the new wording. The diagnostic *code* is unchanged.) + +- [ ] **Step 9: Workspace-wide test sweep** + +Run: `cargo test --workspace 2>&1 | tail -5` +Expected: all tests pass. + +--- + +### Task 6: New crate `crates/ailang-kernel-stub/` + kernel-stub drift round-trip + +**Files:** +- Create: `crates/ailang-kernel-stub/Cargo.toml` +- Create: `crates/ailang-kernel-stub/src/lib.rs` +- Modify: workspace-root `Cargo.toml:3-9` (members list). +- Modify: `crates/ailang-surface/src/loader.rs:load_workspace` — inject `parse_kernel_stub()` alongside `parse_prelude()`. +- Test: `crates/ailang-core/tests/design_schema_drift.rs` — append `kernel_stub_module_round_trips`. + +- [ ] **Step 1: Create the crate's `Cargo.toml`** + +Verify the precedent layout: `cat crates/ailang-prose/Cargo.toml`. Mirror its top-level shape. Write `crates/ailang-kernel-stub/Cargo.toml`: + +```toml +[package] +name = "ailang-kernel-stub" +version.workspace = true +edition.workspace = true + +[lib] +path = "src/lib.rs" + +[dependencies] +ailang-core.workspace = true +ailang-surface.workspace = true +``` + +(If `ailang-prose`'s `Cargo.toml` has additional shared fields like `license`, `repository`, or `[package]`-level inherits — mirror them.) + +- [ ] **Step 2: Create `src/lib.rs` with the stub module's Form-A source** + +Write `crates/ailang-kernel-stub/src/lib.rs`: + +```rust +//! Kernel-tier stub module — minimal ratifying fixture for the +//! kernel-extension-mechanics milestone (prep.3). +//! +//! The stub exists solely to exercise the four shipped mechanisms +//! end-to-end: `Module.kernel`, `TypeDef.param-in`, `Term::New` (via +//! the stub's own `new` def), and type-scoped resolution (the stub's +//! type and `new` are visible to every consumer without an +//! `(import …)` declaration). +//! +//! No domain content. The stub may be retired or repositioned when +//! a real second kernel-tier consumer (the `raw-buf` milestone) lands. + +use ailang_core::ast::Module; + +/// Source-of-truth Form-A text for the stub kernel module. Parsing +/// this string is byte-equivalent to the canonical JSON produced +/// from the resulting `Module` value (round-trip-pinned by +/// `kernel_stub_module_round_trips` in `design_schema_drift.rs`). +const STUB_AIL: &str = r#"(module kernel_stub (kernel) + + (type StubT (vars a) + (param-in (a Int Float)) + (ctors (Stub a))) + + (fn new + (doc "Construct StubT from an Int. Exercises Term::New end-to-end.") + (type (fn-type (params (con Int)) (ret (con StubT (con Int))))) + (params x) + (body (term-ctor StubT Stub x)))) +"#; + +/// Parse the embedded stub kernel module. Mirror of +/// [`ailang_surface::loader::parse_prelude`] (both return their +/// home crate's built-in kernel-tier module). +/// +/// Panics on parse failure — the stub is build-time-validated by +/// every drift test run, so a parse failure here is a build- +/// correctness bug, not a runtime concern. +pub fn parse_kernel_stub() -> Module { + ailang_surface::parse(STUB_AIL).expect("kernel_stub source must parse as a Module") +} +``` + +- [ ] **Step 3: Register the crate in the workspace** + +Open the workspace-root `Cargo.toml`. Locate the `[workspace] members = [...]` array (lines 3-9 per recon). Add `"crates/ailang-kernel-stub"` to the list (alphabetical position by convention, between `ailang-core` and `ailang-prose` if the list is sorted). + +- [ ] **Step 4: Inject the stub via the loader** + +Open `crates/ailang-surface/src/loader.rs`. In `load_workspace` (rewritten in Task 5), add stub injection alongside `parse_prelude()`: + +```rust + if modules.contains_key("prelude") { + return Err(WorkspaceLoadError::ReservedModuleName { + name: "prelude".to_string(), + }); + } + modules.insert("prelude".to_string(), parse_prelude()); + + if modules.contains_key("kernel_stub") { + return Err(WorkspaceLoadError::ReservedModuleName { + name: "kernel_stub".to_string(), + }); + } + modules.insert( + "kernel_stub".to_string(), + ailang_kernel_stub::parse_kernel_stub(), + ); +``` + +(The kernel-flag filter built later in `load_workspace` automatically picks up `kernel_stub` because its source carries `(kernel)`.) + +Add the corresponding dependency in `crates/ailang-surface/Cargo.toml`: + +```toml +ailang-kernel-stub.workspace = true +``` + +(Or, if workspace dependency inheritance is not yet used for this crate edge, the explicit `ailang-kernel-stub = { path = "../ailang-kernel-stub" }`. Mirror the local convention.) + +- [ ] **Step 5: Add `kernel_stub_module_round_trips` drift test** + +Append to `crates/ailang-core/tests/design_schema_drift.rs`: + +```rust +/// prep.3 (kernel-extension-mechanics): pin the JSON byte-shape of +/// the kernel-stub module — exercises all three new schema items +/// in a single fixture (`Module.kernel = true`, one TypeDef with +/// `param-in`, one Term::New-targetable `new` def). A future edit +/// that breaks any of the three additive schema fields will trip +/// this pin in lockstep with the per-field round-trip tests +/// (`module_kernel_flag_round_trips`, `typedef_param_in_round_trips`, +/// `term_new_round_trips`). +#[test] +fn kernel_stub_module_round_trips() { + let m = ailang_kernel_stub::parse_kernel_stub(); + assert!(m.kernel, "stub module is kernel-tier"); + assert_eq!(m.name, "kernel_stub"); + + let json = serde_json::to_value(&m).expect("serialise stub module"); + assert_eq!(json["kernel"], true); + assert_eq!(json["name"], "kernel_stub"); + + let recovered: Module = + serde_json::from_value(json).expect("stub module round-trips through serde"); + assert!(recovered.kernel); + assert_eq!(recovered.name, "kernel_stub"); + + // Locate the StubT TypeDef and confirm param_in is intact. + let td = recovered.defs.iter().find_map(|d| match d { + ailang_core::ast::Def::Type(t) if t.name == "StubT" => Some(t), + _ => None, + }).expect("StubT TypeDef present in stub module"); + let allowed = td.param_in.get("a").expect("StubT.a restricted"); + assert!(allowed.contains("Int")); + assert!(allowed.contains("Float")); +} +``` + +Add the test crate's dev-dependency on `ailang-kernel-stub` in `crates/ailang-core/Cargo.toml`'s `[dev-dependencies]` block: + +```toml +ailang-kernel-stub.workspace = true +``` + +- [ ] **Step 6: Compile-gate + run new tests** + +Run: `cargo build --workspace 2>&1 | tail -3` +Expected: build succeeds (the new stub crate compiles; loader changes compile; drift test compiles). + +Run: `cargo test --workspace --test design_schema_drift kernel_stub_module_round_trips` +Expected: 1 passed. + +Run: `cargo test --workspace --test design_schema_drift` +Expected: every drift test passes. + +--- + +### Task 7: `CheckError::ParamNotInRestrictedSet` variant + enforcement in `check_type_well_formed` + in-source tests + +**Files:** +- Modify: `crates/ailang-check/src/lib.rs:721-742` — new `CheckError` variant. +- Modify: `crates/ailang-check/src/lib.rs:797-798` — `code()` arm. +- Modify: `crates/ailang-check/src/lib.rs:876-879` — `ctx()` arm. +- Modify: `crates/ailang-check/src/lib.rs:1920-1998` — `check_type_well_formed`'s `Type::Con` arm. +- Test: `crates/ailang-check/src/lib.rs` in-source `#[cfg(test)] mod tests` block — `param_in_accepts_allowed_type`, `param_in_rejects_disallowed_type`. + +- [ ] **Step 1: Add the new `CheckError` variant** + +Open `crates/ailang-check/src/lib.rs`. Locate the existing `CheckError::NewArgKindMismatch` variant at lines 733-742 (recon found it). After the `NewArgKindMismatch` variant and before whatever variant follows (or before the enum's closing `}`), insert: + +```rust + /// `param-in` violation: a `Type::Con` for a TypeDef that + /// restricts a type variable was instantiated with a type-arg + /// outside the allowed set. The diagnostic carries the type + /// name (which TypeDef restricts), the variable name (which + /// var was violated), the rejected concrete type name + /// (`found`), and the allowed set (`allowed`). See prep.3 of + /// the kernel-extension-mechanics milestone. + #[error( + "type-arg `{found}` is not in the restricted set for type-variable `{var}` of `{type_name}`" + )] + ParamNotInRestrictedSet { + type_name: String, + var: String, + found: String, + allowed: Vec, + }, +``` + +(Vec rather than BTreeSet in the diagnostic payload because diagnostics' ctx field is JSON-ish; the order of `allowed` for the user message is deterministic via the source BTreeSet's natural order.) + +- [ ] **Step 2: Add the `code()` arm** + +At lines 797-798 (the arm for `NewArgKindMismatch`), after that arm and inside the same `match` block, add: + +```rust + CheckError::ParamNotInRestrictedSet { .. } => "param-not-in-restricted-set", +``` + +- [ ] **Step 3: Add the `ctx()` arm** + +At lines 876-879 (the arm for `NewArgKindMismatch`), after that arm and inside the same `match` block, add: + +```rust + CheckError::ParamNotInRestrictedSet { type_name, var, found, allowed } => { + vec![ + ("type_name".into(), serde_json::json!(type_name)), + ("var".into(), serde_json::json!(var)), + ("found".into(), serde_json::json!(found)), + ("allowed".into(), serde_json::json!(allowed)), + ] + } +``` + +(Mirror the surrounding arms' return type and helper-macro conventions; the implementer reads the `NewArgKindMismatch` arm and adopts the local idiom.) + +- [ ] **Step 4: Add enforcement in `check_type_well_formed`** + +Open `check_type_well_formed` (lines 1920-1998). Locate the `Type::Con { name, args }` arm — after the TypeDef lookup at line 1961 (`td_opt`) and before recursing into `args` at line 1969, insert the param-in walk: + +```rust + if let Some(td) = td_opt { + // param-in enforcement: every restricted var must have + // its corresponding positional arg's outermost type-name + // in the allowed set. + for (var, allowed) in &td.param_in { + let var_position = td.vars.iter().position(|v| v == var); + let Some(pos) = var_position else { + // Defensive: param_in keys should always match + // TypeDef.vars (enforced at workspace-load). + continue; + }; + let Some(arg_ty) = args.get(pos) else { + // Arity mismatch is a separate diagnostic; skip + // param-in check when the arg slot does not exist. + continue; + }; + // Peel the outermost type-name out of the arg. + if let ailang_core::ast::Type::Con { name: arg_name, .. } = arg_ty { + if !allowed.contains(arg_name) { + return Err(CheckError::ParamNotInRestrictedSet { + type_name: name.clone(), + var: var.clone(), + found: arg_name.clone(), + allowed: allowed.iter().cloned().collect(), + }); + } + } + // Non-Con arg-types (Forall vars, fn types, etc.) are + // not currently restrictable by param-in — the spec + // names the mechanism as a "closed-set type-parameter + // restriction" over named concrete types. Future + // axes (structural-predicate-based restriction) are + // out of scope per the spec's § Out of scope. + } + } +``` + +(Exact placement: the implementer reads the surrounding context — particularly the existing arity-check arm — and inserts the param-in pass immediately after TypeDef resolution and before the recursive args walk.) + +- [ ] **Step 5: Add RED test `param_in_rejects_disallowed_type`** + +Locate the in-source `#[cfg(test)] mod tests { ... }` block at the end of `crates/ailang-check/src/lib.rs` (line ~6900+; existing test fns like `new_type_not_constructible` live here). Append: + +```rust + /// prep.3 (kernel-extension-mechanics): param-in enforcement. + /// A `Type::Con { name: "StubT", args: [Type::Con { name: "Str" }] }` + /// against a TypeDef whose `param_in["a"] = {"Int","Float"}` fires + /// `ParamNotInRestrictedSet` with the right type-name, var, found, + /// and allowed-set payload. + #[test] + fn param_in_rejects_disallowed_type() { + use std::collections::{BTreeMap, BTreeSet}; + + let mut restrict: BTreeMap> = BTreeMap::new(); + restrict.insert( + "a".into(), + ["Int".to_string(), "Float".to_string()].into_iter().collect(), + ); + let stub_td = ailang_core::ast::TypeDef { + name: "StubT".into(), + vars: vec!["a".into()], + ctors: vec![], + doc: None, + drop_iterative: false, + param_in: restrict, + }; + let m = ailang_core::ast::Module { + schema: ailang_core::SCHEMA.to_string(), + name: "k".into(), + kernel: false, + imports: vec![], + defs: vec![ailang_core::ast::Def::Type(stub_td)], + }; + + // Build a workspace with this single module and call + // check_type_well_formed on (con StubT (con Str)). + let ty = ailang_core::ast::Type::Con { + name: "StubT".into(), + args: vec![ailang_core::ast::Type::Con { + name: "Str".into(), + args: vec![], + }], + }; + + // Use whichever helper the existing in-source tests use to + // run check_type_well_formed on a synthetic Type+Module pair; + // mirror the call shape of `new_type_not_constructible` two + // arms above. + let err = check_type_in_module(&m, &ty) + .expect_err("(con StubT (con Str)) violates param_in"); + match err { + CheckError::ParamNotInRestrictedSet { type_name, var, found, allowed } => { + assert_eq!(type_name, "StubT"); + assert_eq!(var, "a"); + assert_eq!(found, "Str"); + assert!(allowed.contains(&"Int".to_string())); + assert!(allowed.contains(&"Float".to_string())); + } + other => panic!("expected ParamNotInRestrictedSet, got {other:?}"), + } + } +``` + +(`check_type_in_module` is the placeholder for whichever helper the existing in-source tests use to drive `check_type_well_formed`. The implementer reads `new_type_not_constructible` and the surrounding helpers, and adopts the local convention. If the existing tests inline a checker context creation rather than calling a helper, mirror that.) + +- [ ] **Step 6: Add GREEN test `param_in_accepts_allowed_type`** + +Append the GREEN counterpart in the same module: + +```rust + /// prep.3 (kernel-extension-mechanics): param-in enforcement + /// accepts a type-arg inside the allowed set. Same TypeDef as + /// the RED test, but `(con StubT (con Int))` — Int is in + /// {Int, Float}, so the check passes. + #[test] + fn param_in_accepts_allowed_type() { + use std::collections::{BTreeMap, BTreeSet}; + + let mut restrict: BTreeMap> = BTreeMap::new(); + restrict.insert( + "a".into(), + ["Int".to_string(), "Float".to_string()].into_iter().collect(), + ); + let stub_td = ailang_core::ast::TypeDef { + name: "StubT".into(), + vars: vec!["a".into()], + ctors: vec![], + doc: None, + drop_iterative: false, + param_in: restrict, + }; + let m = ailang_core::ast::Module { + schema: ailang_core::SCHEMA.to_string(), + name: "k".into(), + kernel: false, + imports: vec![], + defs: vec![ailang_core::ast::Def::Type(stub_td)], + }; + + let ty = ailang_core::ast::Type::Con { + name: "StubT".into(), + args: vec![ailang_core::ast::Type::Con { + name: "Int".into(), + args: vec![], + }], + }; + + check_type_in_module(&m, &ty).expect("(con StubT (con Int)) passes param_in"); + } +``` + +- [ ] **Step 7: Run new tests + ensure exhaustiveness compile-gate clean** + +Run: `cargo test --workspace -p ailang-check param_in_rejects_disallowed_type` +Expected: 1 passed. + +Run: `cargo test --workspace -p ailang-check param_in_accepts_allowed_type` +Expected: 1 passed. + +Run: `cargo build --workspace 2>&1 | rg 'non-exhaustive\|missing.*ParamNotInRestrictedSet' | wc -l` +Expected: 0. (The variant addition forces exhaustive `match CheckError { ... }` sites to be updated; the three explicit arms inserted in Steps 1-3 cover the only exhaustive-match sites per `crates/ailang-check/src/lib.rs:754, 805, 917` enumerated by recon. If any other site flares, fix in-place with a trailing arm if the surrounding context allows non-exhaustive matching, or with a fully-specified arm otherwise.) + +Run: `cargo test --workspace -p ailang-check 2>&1 | tail -5` +Expected: all checker tests pass. + +--- + +### Task 8: Workspace-load integration tests — `crates/ailang-core/tests/workspace_kernel.rs` + +**Files:** +- Create: `crates/ailang-core/tests/workspace_kernel.rs` + +- [ ] **Step 1: Locate the integration-test pattern** + +Read `crates/ailang-core/tests/workspace_pin.rs:1-22` for the dev-dep posture (the integration-test crate is the home for tests that call `ailang_surface::load_workspace`, per the documented dev-dep cycle constraint). The pattern: create a temp directory, write `.ail` source files, call `ailang_surface::load_workspace(entry)`, assert on the resulting `Workspace`. + +- [ ] **Step 2: Write three integration tests** + +Create `crates/ailang-core/tests/workspace_kernel.rs`: + +```rust +//! prep.3 (kernel-extension-mechanics): workspace-load tests for +//! kernel-tier auto-import. These tests exercise the flag-driven +//! generalisation of the prior hardcoded `&["prelude"]` literal — +//! every loaded module with `kernel: true` joins the implicit- +//! imports list. + +use std::collections::BTreeMap; +use tempfile::TempDir; + +/// Write a Form-A source file into the temp dir and return its path. +fn write_module(dir: &TempDir, name: &str, src: &str) -> std::path::PathBuf { + let path = dir.path().join(format!("{}.ail", name)); + std::fs::write(&path, src).expect("write fixture"); + path +} + +#[test] +fn kernel_tier_module_auto_imports_without_explicit_import() { + // Consumer has no `(import …)` declaration; the kernel-tier + // module's types should still resolve. + let dir = TempDir::new().expect("tempdir"); + write_module( + &dir, + "k_mod", + r#"(module k_mod (kernel) + (type KT (vars a) (ctors (KCtor a)))) +"#, + ); + let entry = write_module( + &dir, + "consumer", + r#"(module consumer + (fn use_kt + (type (fn-type (params (con KT (con Int))) (ret (con Unit)))) + (params k) (body unit))) +"#, + ); + + let ws = ailang_surface::load_workspace(&entry).expect("workspace loads"); + assert!( + ws.modules.contains_key("k_mod"), + "k_mod was loaded into the workspace" + ); + // The consumer's reference to bare `KT` resolves through the + // kernel-flag-driven implicit-imports list. The workspace must + // validate without producing a `BareCrossModuleTypeRef` error. + // (Exact API for "did validation pass" follows whichever + // accessor `Workspace` exposes; the implementer mirrors the + // pattern used in `workspace_pin.rs`.) +} + +#[test] +fn two_kernel_tier_modules_coload() { + let dir = TempDir::new().expect("tempdir"); + write_module(&dir, "k_a", "(module k_a (kernel) (type A (ctors (AC))))\n"); + write_module(&dir, "k_b", "(module k_b (kernel) (type B (ctors (BC))))\n"); + let entry = write_module( + &dir, + "consumer", + r#"(module consumer + (fn use_ab + (type (fn-type (params (con A) (con B)) (ret (con Unit)))) + (params a b) (body unit))) +"#, + ); + + let ws = ailang_surface::load_workspace(&entry).expect("workspace with two kernel modules"); + assert!(ws.modules.contains_key("k_a")); + assert!(ws.modules.contains_key("k_b")); +} + +#[test] +fn explicit_import_takes_precedence_over_auto_import() { + // When a consumer has an explicit `(import k_mod)` declaration, + // the existing precedence rule keeps the explicit form; the + // auto-import does not double-resolve or change behaviour. + // This test pins the precedence rule's continuity through the + // loader migration. + let dir = TempDir::new().expect("tempdir"); + write_module( + &dir, + "k_mod", + "(module k_mod (kernel) (type KT (ctors (KC))))\n", + ); + let entry = write_module( + &dir, + "consumer", + r#"(module consumer + (import k_mod) + (fn use_kt + (type (fn-type (params (con KT)) (ret (con Unit)))) + (params k) (body unit))) +"#, + ); + + let ws = ailang_surface::load_workspace(&entry).expect("explicit + auto coexist"); + assert!(ws.modules.contains_key("k_mod")); + // No error from double-resolution. Workspace validation passes. +} +``` + +(If `Workspace.modules` is not the actual field name on the `Workspace` type, the implementer adapts to whatever accessor exists — `workspace_pin.rs` shows the canonical access pattern. If `tempfile` is not yet a dev-dependency of `ailang-core`, add it to `[dev-dependencies]` in `crates/ailang-core/Cargo.toml`.) + +- [ ] **Step 3: Verify `tempfile` is available as a dev-dependency** + +Run: `rg -n 'tempfile' crates/ailang-core/Cargo.toml` +Expected: at least one hit under `[dev-dependencies]`. If absent, add `tempfile = "3"` to `[dev-dependencies]`. + +- [ ] **Step 4: Compile-gate + run new tests** + +Run: `cargo build --workspace 2>&1 | tail -3` +Expected: build succeeds. + +Run: `cargo test --workspace --test workspace_kernel` +Expected: 3 passed. + +- [ ] **Step 5: Workspace-wide regression sweep** + +Run: `cargo test --workspace 2>&1 | tail -5` +Expected: all tests pass. + +--- + +### Task 9: Doc-state updates — INDEX.md + whitepaper STATUS + forward→present transitions + +**Files:** +- Modify: `design/INDEX.md:111` +- Modify: `design/models/0007-kernel-extensions.md:1-12, 215-276` + +- [ ] **Step 1: Update INDEX.md milestone annotation** + +Open `design/INDEX.md`. Locate the `kernel-extensions` row (line 111 per recon). The current annotation likely reads `(design accepted 2026-05-28; impl in progress)`. Replace with text reflecting the milestone-close state: + +```markdown +| kernel-extensions | design/models/0007-kernel-extensions.md | Whitepaper for the kernel-extensions design; mechanisms milestone closed YYYY-MM-DD (prep.1, prep.2, prep.3 landed); raw-buf and series milestones pending. | +``` + +(`YYYY-MM-DD` is the close date — typically today's date when prep.3 lands.) + +- [ ] **Step 2: Update whitepaper STATUS header** + +Open `design/models/0007-kernel-extensions.md`. The STATUS section at lines 1-12 currently describes the design as forward-looking. Replace the relevant lines with the present-state framing: + +```markdown +# Kernel extensions — design whitepaper + +**Status:** Mechanisms milestone closed YYYY-MM-DD (kernel-extension-mechanics; iterations prep.1, prep.2, prep.3). The base-extension and library-extension milestones (`raw-buf`, `series`) are pending. The four language-level mechanisms — type-scoped namespacing, `Term::New`, kernel-tier modules + auto-import, and `param-in` — are shipped and ratified by the stub kernel crate (`crates/ailang-kernel-stub/`). +``` + +(Mirror the existing whitepaper STATUS-header convention; if the file uses a different fenced-block or front-matter style, preserve it.) + +- [ ] **Step 3: Transition mechanism sections from forward→present** + +In `design/models/0007-kernel-extensions.md`, sections at lines 215-237 (kernel-tier auto-import) and 239-276 (param-in) currently use forward-looking language ("after the kernel-extensions design lands, …", "we will …", "future …"). For each such forward-looking sentence about a *now-shipped* mechanism, rewrite to present-state: + +- "We will introduce kernel-tier modules …" → "Kernel-tier modules are modules with `kernel: true` set in their schema header. Every loaded kernel-tier module's top-level types and free defs auto-import into every consumer." +- "The `param-in` restriction will allow …" → "The `param-in` restriction is a closed-set type-parameter restriction declared on TypeDefs: `pub param_in: BTreeMap>`, serialised as the kebab-cased `param-in` key. The checker enforces it during `Type::Con` well-formedness." +- "We will need a stub module to …" → "The stub module `crates/ailang-kernel-stub/` ratifies the mechanism end-to-end. It exercises `kernel: true`, `param-in`, and `Term::New` in one fixture; no domain content." + +(The implementer reads each forward-looking sentence and rewrites in present-state. Forward-looking framing remains for the *still-pending* base-extension and library-extension milestones — those are explicitly out of scope per § Out of scope of the parent spec.) + +- [ ] **Step 4: Confirm no remaining forward-tense in shipped sections** + +Run: `rg -n 'will (introduce|allow|need|ship|implement|add) ' design/models/0007-kernel-extensions.md` +Expected: matches occur only in sections that describe the **still-pending** `raw-buf` and `series` milestones. Matches inside sections describing prep.1/prep.2/prep.3 mechanisms are bugs from this step — re-edit. + +- [ ] **Step 5: cargo doc clean** + +Run: `cargo doc --no-deps --workspace 2>&1 | tail -10` +Expected: no new warnings (doc-comments added in Tasks 1, 2, 6, 7 carry no inline LaTeX or broken intra-doc links). + +- [ ] **Step 6: Final workspace test sweep** + +Run: `cargo test --workspace 2>&1 | tail -5` +Expected: all tests pass. + +Run: `bench/check.py 2>&1 | tail -10` +Expected: no performance regression beyond noise — this milestone touches resolver/parser/schema, not codegen/runtime; regression is unexpected but the regression script is part of the close-out per audit discipline. + +--- + +## Self-review notes + +1. **Spec coverage.** Every numbered item in the spec's § Iteration prep.3 maps to a task: + - Schema additions (`Module.kernel`, `TypeDef.param_in`) → Tasks 1, 2. + - Form-A surface (`(kernel)`, `(param-in …)`) → Tasks 3, 4. + - Workspace-load generalisation → Task 5 (prelude migration + loader rewrite). + - Generic checker enforcement of param-in → Task 7. + - `ParamNotInRestrictedSet` diagnostic → Task 7. + - `ReservedModuleName` repurposed → Task 5 Step 3 + Step 5. + - New `crates/ailang-kernel-stub/` crate → Task 6. + - Drift pins (`module_kernel_flag_round_trips`, `typedef_param_in_round_trips`, basic stub-module round-trip) → Tasks 1 Step 6, 2 Step 7, 6 Step 5. + - Workspace-load tests → Task 8. + - Hash-pin refresh for prelude → Task 5 Step 6. + - § Acceptance criteria item 8 (whitepaper STATUS + forward→present) → Task 9 Steps 2-4. + - § Acceptance criteria item 9 (INDEX.md annotation) → Task 9 Step 1. + +2. **Placeholder scan.** Grepped this document for "TBD", "TODO", "fill in later", "similar to Task", "add appropriate error handling": no hits. + +3. **Type consistency.** `Module.kernel` (bool), `TypeDef.param_in` (BTreeMap>), `ParamNotInRestrictedSet { type_name, var, found, allowed }`, `parse_kernel_stub()`, `kernel_stub` module name — all used consistently across tasks. + +4. **Step granularity.** Each step is one mechanical action: write a struct edit, run a command, write a single test function. The 130-site `Module { ... }` sweep in Task 1 Step 3 is the largest single step — handled as a mechanical replace-all driven by the compiler's error list (the implementer's "iterate over `cargo build` errors and fix each" pattern, not a 130-step plan). + +5. **No commit steps.** Confirmed: no `git commit` instructions anywhere. + +6. **Pin/replacement substring contiguity.** The only verbatim-text edits are in `design/contracts/0002-data-model.md` (Task 1 Step 5, Task 2 Step 6) and the prelude hash refresh (Task 5 Step 6). None pair a presence-pin with a soft-wrappable replacement — the data-model edits are full block replacements, and the hash pin's new hex literal is whatever the failing test reports. + +7. **Compile-gate vs. deferred-caller ordering.** The two struct-addition tasks (1 and 2) each include the full sweep of their respective struct-literal sites inside the same task as the field declaration. The compile gate at the end of each task validates that no caller is deferred. The `CheckError` variant addition (Task 7) includes the three accessor-arm updates (code/ctx/match exhaustiveness) inside the same task as the variant declaration, plus the workspace-wide build check (Step 7). + +8. **Verification-command filter strings resolve.** Each `cargo test --test` invocation targets either a known existing test file (`design_schema_drift`, `prelude_module_hash_pin`, `prelude_free_fns`, `ct1_check_cli`) or a new file created in the same task (`workspace_kernel`). Each `--test`-with-filter form names a test function created earlier in the same task (`module_kernel_flag_round_trips`, `typedef_param_in_round_trips`, `kernel_module_header_round_trips`, `typedef_param_in_round_trips_surface`, `kernel_stub_module_round_trips`, `param_in_rejects_disallowed_type`, `param_in_accepts_allowed_type`). No silently-skipped filter strings. + +--- + +## Handoff + +This plan is ready for the `implement` skill. Standard mode dispatch: + +``` +ailang-implement-orchestrator + mode: standard + iter_id: prep.3-kernel-tier-modules + plan_path: docs/plans/0103-prep.3-kernel-tier-modules.md +``` + +The whole plan runs in one orchestrator dispatch (no task-range split anticipated — tasks are sequenced by their dependency chain: 1→2 are schema, 3→4 are surface, 5 migrates prelude+loader, 6 lands the stub crate, 7 ships the diagnostic+enforcement, 8 validates workspace-load behaviour, 9 closes the documentation state). + +On `DONE`, the orchestrator (Boss) commits as one cohesive iter-level commit with subject `iter prep.3-kernel-tier-modules (DONE 9/9): kernel-tier modules + param-in + stub crate — closes #33`. The commit body covers: the four shipped mechanisms, the prelude code-path migration with prelude_free_fns regression-protection, the stub crate's role as ratifying fixture, and the milestone-close transition in INDEX.md + the whitepaper.