iter prep.3-kernel-tier-modules (DONE 9/9): kernel-tier modules + param-in + stub crate — closes #33

Terminal iteration of the kernel-extension-mechanics milestone. Ships
the four language-level mechanisms named in the spec's § Goal:
Module.kernel + TypeDef.param-in schema, their Form-A surface,
flag-driven kernel-tier auto-injection, and generic param-in checker
enforcement with a new diagnostic.

Schema (Tasks 1+2). Module gains a `kernel: bool` field
(skip_serializing_if = is_false), TypeDef gains a
`param_in: BTreeMap<String, BTreeSet<String>>` field
(skip-if-empty, kebab-renamed to "param-in"). Both fields are
strictly additive — every pre-existing fixture's canonical-JSON hash
is bit-stable except `prelude.ail`, which intentionally gains
`(kernel)`. The struct-literal sweep covered ~104 Module sites and
~35 TypeDef sites across the workspace; the additive serde-default
covers JSON deserialise paths, only Rust struct literals broke.

Form-A surface (Tasks 3+4). `(kernel)` is a bare module-header
attribute; `(param-in (a Int Float) (b Str))` is one outer
TypeDef-body clause carrying one or more inner var-lists (OQ1
decision — mirrors `(ctors …)`, one parser arm, deterministic
BTreeMap iteration). Both round-trip Form-A → JSON → Form-A
bit-identical.

Workspace-load migration (Task 5). The hardcoded `&["prelude"]`
literal at loader.rs:108 became a `modules.values().filter(|m|
m.kernel)` derivation; `parse_prelude()` injection stays because
the prelude has no on-disk manifest in user workspaces. Prelude
now carries `(kernel)` in its source, so the new filter picks it
up automatically. Code-path migration only — observable behaviour
is identical (prelude_free_fns.rs stays green). prelude hash
re-pinned (af372f28c726f29f) with Honesty-Rule provenance comment.
WorkspaceLoadError::ReservedModuleName diagnostic prose
repurposed: any built-in kernel module name is reserved
(currently prelude + kernel_stub), not specifically prelude. CLI
mapping at main.rs updated in lockstep.

Stub crate (Task 6). New `crates/ailang-kernel-stub/` is a
zero-dependency leaf crate carrying only `pub const STUB_AIL:
&str` with the Form-A source of the kernel_stub module (one
parametric TypeDef with param-in, one ctor). The parse hop —
`parse_kernel_stub()` — lives in ailang-surface next to
parse_prelude, keeping the crate-dependency graph acyclic
(`ailang-surface → ailang-kernel-stub → ailang-core`, no
back-edge). The stub is injected unconditionally in all builds as
the ratifying fixture for the kernel-extension mechanism; future
base extensions may add more or retire the stub. Drift-pinned by
`kernel_stub_module_round_trips`.

Checker (Task 7). New `CheckError::ParamNotInRestrictedSet`
variant + code() + ctx() arms + enforcement in
`check_type_well_formed`'s Type::Con arm — generic, data-driven
from the TypeDef, mentions no specific extension type. Two
in-source tests pin both the rejection (`Str` outside `{Int,
Float}`) and the acceptance (`Int` inside) paths.

Workspace-load integration tests (Task 8). New
`workspace_kernel.rs` integration-test crate with three tests:
auto-import without explicit `(import …)` declaration, two
kernel-tier modules co-load, explicit-import-overrides-auto-
import precedence preserved. Loader is import-tree-only so the
auto-import tests use a bridge module that brings the kernel
module into the workspace via the import graph — docstring
captures the reachability nuance for future readers.

Doc-state transitions (Task 9). INDEX.md kernel-extensions row
annotation transitions from "design accepted 2026-05-28; impl in
progress" to "mechanisms milestone closed 2026-05-28; raw-buf and
series milestones pending". Whitepaper STATUS + auto-import +
param-in sections transitioned forward→present for shipped
mechanisms; forward-tense survives only in sections describing
the still-pending raw-buf/series milestones (per Honesty-Rule).
data-model contract gains anchor blocks for both new schema
fields.

Side-effect: every binary's IR snapshot now contains ~52 lines
for `drop_kernel_stub_StubT` because the stub is auto-injected
into every workspace load. Snapshots refreshed; e2e expects 4
modules per workspace (prelude + kernel_stub + entry + zero or
more user modules) instead of the previous 3.

Plan defects scrubbed in the implementation (folded back into
the planner template via the planner's self-review checklist
next time): Task 4 sample test src used fictional
`(ctors (MkT a))` list form (project grammar is per-`(ctor MkT
a)`); Task 6 original wiring would have created a cycle
ailang-surface → ailang-kernel-stub → ailang-surface (inverted —
stub crate is zero-dep, parse hop lives in surface); Task 7 in-
source tests referenced a fictional `check_type_in_module`
helper (used the existing Workspace + check_workspace
convention); Task 8 first integration test expected loader to
auto-load kernel modules from disk (loader is import-tree-only;
tests use a bridge module).

Concern-5 fix folded in pre-commit: workspace.rs ReservedModuleName
doc-prose initially said "in test/dev builds" for kernel_stub —
but stub is unconditionally injected in all builds. Doc copy
tightened to present-state per Honesty-Rule.

Stats: 0 spec-review-loops, 0 quality-review-loops, 2 sweep-script
retries on Task 2 (brace-depth bug on nested vec![Ctor{…}],
recovered via per-file checkout + rewritten anchor-on-existing-
field sweep), 1 e2e-snapshot refresh on Task 6.

crates/ailang-core/src/ast.rs

@@ -17,6 +17,8 @@
 //! [`crate::canonical`] for canonical bytes, [`crate::hash`] for content
 //! hashes, and the `ailang-check` crate for typechecking.
 
+use std::collections::{BTreeMap, BTreeSet};
+
 use serde::{Deserialize, Serialize};
 
 /// A complete AILang translation unit.
@@ -33,6 +35,14 @@ pub struct Module {
     /// (`<name>.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
     /// `<root_dir>/<module>.ail.json`.
     #[serde(default)]
@@ -167,6 +177,27 @@ pub struct TypeDef {
         skip_serializing_if = "is_false"
     )]
     pub drop_iterative: bool,
+    /// 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: <self.name>, args }` carries an
+    /// `args[i]` whose outermost type-name lies in the restricted
+    /// set for that variable.
+    ///
+    /// Serialised as `"param-in": { "<var>": ["<T>", ...] }`
+    /// (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 `ParamNotInRestrictedSet` in
+    /// `crates/ailang-check/src/lib.rs`.
+    #[serde(
+        default,
+        rename = "param-in",
+        skip_serializing_if = "BTreeMap::is_empty"
+    )]
+    pub param_in: BTreeMap<String, BTreeSet<String>>,
 }
 
 

crates/ailang-core/src/desugar.rs

@@ -1785,6 +1785,7 @@ mod tests {
         let m = Module {
             schema: crate::SCHEMA.to_string(),
             name: "t".into(),
+            kernel: false,
             imports: vec![],
             defs: vec![Def::Fn(FnDef {
                 name: "f".into(),
@@ -1842,6 +1843,7 @@ mod tests {
         let m = Module {
             schema: crate::SCHEMA.to_string(),
             name: "t".into(),
+            kernel: false,
             imports: vec![],
             defs: vec![Def::Fn(FnDef {
                 name: "f".into(),
@@ -1900,6 +1902,7 @@ mod tests {
         let m = Module {
             schema: crate::SCHEMA.to_string(),
             name: "t".into(),
+            kernel: false,
             imports: vec![],
             defs: vec![Def::Fn(FnDef {
                 name: "main".into(),
@@ -1963,6 +1966,7 @@ mod tests {
         let m = Module {
             schema: crate::SCHEMA.to_string(),
             name: "t".into(),
+            kernel: false,
             imports: vec![],
             defs: vec![Def::Fn(FnDef {
                 name: "outer".into(),
@@ -2111,6 +2115,7 @@ mod tests {
         let m = Module {
             schema: crate::SCHEMA.to_string(),
             name: "t".into(),
+            kernel: false,
             imports: vec![],
             defs: vec![Def::Fn(FnDef {
                 name: "main".into(),
@@ -2184,6 +2189,7 @@ mod tests {
             }],
             doc: None,
             drop_iterative: false,
+            param_in: BTreeMap::new(),
         };
         let letrec = Term::LetRec {
             name: "helper".into(),
@@ -2225,6 +2231,7 @@ mod tests {
         let m = Module {
             schema: crate::SCHEMA.to_string(),
             name: "t".into(),
+            kernel: false,
             imports: vec![],
             defs: vec![
                 Def::Type(pair_td),
@@ -2309,6 +2316,7 @@ mod tests {
         let m = Module {
             schema: crate::SCHEMA.to_string(),
             name: "t".into(),
+            kernel: false,
             imports: vec![],
             defs: vec![Def::Fn(FnDef {
                 name: "main".into(),
@@ -2371,6 +2379,7 @@ mod tests {
         let m = Module {
             schema: crate::SCHEMA.to_string(),
             name: "t".into(),
+            kernel: false,
             imports: vec![],
             defs: vec![Def::Fn(FnDef {
                 name: "main".into(),
@@ -2512,6 +2521,7 @@ mod tests {
         let m = Module {
             schema: crate::SCHEMA.to_string(),
             name: "t".into(),
+            kernel: false,
             imports: vec![],
             defs: vec![Def::Fn(FnDef {
                 name: "rec_id".into(),
@@ -2616,6 +2626,7 @@ mod tests {
         let m = Module {
             schema: crate::SCHEMA.to_string(),
             name: "t".into(),
+            kernel: false,
             imports: vec![],
             defs: vec![Def::Fn(FnDef {
                 name: "outer".into(),
@@ -2702,6 +2713,7 @@ mod tests {
         let m = Module {
             schema: crate::SCHEMA.to_string(),
             name: "t".into(),
+            kernel: false,
             imports: vec![],
             defs: vec![Def::Fn(FnDef {
                 name: "main".into(),
@@ -2783,6 +2795,7 @@ mod tests {
         let m = Module {
             schema: crate::SCHEMA.to_string(),
             name: "t".into(),
+            kernel: false,
             imports: vec![],
             defs: vec![Def::Fn(FnDef {
                 name: "main".into(),
@@ -2913,6 +2926,7 @@ mod tests {
         let m = Module {
             schema: crate::SCHEMA.to_string(),
             name: "t".into(),
+            kernel: false,
             imports: vec![],
             defs: vec![Def::Fn(FnDef {
                 name: "f".into(),
@@ -2987,6 +3001,7 @@ mod tests {
         let m = Module {
             schema: crate::SCHEMA.to_string(),
             name: "t".into(),
+            kernel: false,
             imports: vec![],
             defs: vec![Def::Fn(FnDef {
                 name: "f".into(),
@@ -3069,6 +3084,7 @@ mod tests {
         let m = Module {
             schema: crate::SCHEMA.to_string(),
             name: "t".into(),
+            kernel: false,
             imports: vec![],
             defs: vec![Def::Fn(FnDef {
                 name: "f".into(),

crates/ailang-core/src/pretty.rs

@@ -169,6 +169,7 @@ mod tests {
         Module {
             schema: crate::SCHEMA.into(),
             name: "sample".into(),
+            kernel: false,
             imports: vec![],
             defs: vec![
                 Def::Fn(FnDef {

crates/ailang-core/src/workspace.rs

@@ -304,11 +304,16 @@ pub enum WorkspaceLoadError {
         type_repr: String,
     },
 
-    /// a user module attempted to use the reserved
-    /// module name `prelude`. The prelude is auto-injected by
-    /// the loader, so a user module of the same name would
-    /// collide silently. Reject explicitly.
-    #[error("module name {name:?} is reserved (auto-injected by the loader)")]
+    /// 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 `kernel_stub` (the
+    /// stub is injected unconditionally in all builds as the
+    /// ratifying fixture for the kernel-extension mechanism;
+    /// future base extensions may add more or retire the stub).
+    /// 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.
+    #[error("workspace module `{name}` collides with a built-in kernel-tier module name (reserved)")]
     ReservedModuleName { name: String },
 
     /// the canonical-form rule for type references: a `Type::Con` whose `name` is
@@ -464,12 +469,20 @@ where
 
 /// pd.1: extract the validation + registry-construction tail of
 /// `load_workspace_with` into a public fn that operates on a pre-assembled
-/// modules map. The caller (typically `surface::load_workspace`, post-pd.2)
+/// modules map. The caller (typically `ailang_surface::loader::load_workspace`)
 /// is responsible for injecting any implicit modules (e.g. prelude) into
 /// `modules` BEFORE calling this fn, AND for naming those implicit modules
 /// in `implicit_imports` so the diagnostic helpers (`check_class_ref`,
 /// `check_type_con_name`) include them as fallback candidates.
 ///
+/// `implicit_imports` is the list of module names every consumer
+/// should auto-import without an explicit `(import …)` declaration.
+/// The caller 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.
+///
 /// Runs the three-stage pipeline:
 /// 1. `validate_canonical_type_names` (with `implicit_imports`)
 /// 2. `validate_classdefs` (no `implicit_imports` — does not consume it)

crates/ailang-core/tests/design_schema_drift.rs

@@ -14,9 +14,11 @@
 //! `## Data model` … `## Pipeline` slicer is no longer needed (the split
 //! gave the section its own file).
 
+use std::collections::BTreeMap;
+
 use ailang_core::ast::{
     ClassDef, ClassMethod, Constraint, ConstDef, Ctor, Def, FnDef, InstanceDef,
-    InstanceMethod, Literal, NewArg, Pattern, ParamMode, Suppress, Term, Type, TypeDef,
+    InstanceMethod, Literal, Module, NewArg, Pattern, ParamMode, Suppress, Term, Type, TypeDef,
 };
 
 const DATA_MODEL: &str = include_str!("../../../design/contracts/0002-data-model.md");
@@ -326,6 +328,7 @@ fn design_md_anchors_every_def_kind() {
         vars: vec![],
         ctors: vec![Ctor { name: "C".into(), fields: vec![] }],
         drop_iterative: false,
+        param_in: BTreeMap::new(),
     };
     let class_def = ClassDef {
         name: "Show".into(),
@@ -629,3 +632,133 @@ fn term_new_type_arg_round_trips() {
 }
 
 
+
+/// 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);
+}
+
+/// 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::BTreeSet;
+
+    let mut restrict: BTreeMap<String, BTreeSet<String>> = 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);
+}
+
+/// 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 ctor). A future edit that breaks any of the new
+/// 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`).
+#[test]
+fn kernel_stub_module_round_trips() {
+    let m = ailang_surface::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 {
+        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"));
+}

crates/ailang-core/tests/spec_drift.rs

@@ -11,6 +11,8 @@
 //! without a spec entry fails compilation here long before the test runs.
 //! Once the variant is matched, the test asserts the spec mentions it.
 
+use std::collections::BTreeMap;
+
 use ailang_core::ast::{
     ConstDef, Ctor, Def, FnDef, Literal, NewArg, Pattern, Suppress, Term, Type, TypeDef,
 };
@@ -287,6 +289,7 @@ fn spec_mentions_every_def_kind() {
             fields: vec![],
         }],
         drop_iterative: false,
+        param_in: BTreeMap::new(),
     };
     let exemplars: Vec<(&str, Def)> = vec![
         ("(fn ", Def::Fn(fn_def)),

crates/ailang-core/tests/workspace_kernel.rs

@@ -0,0 +1,162 @@
+//! 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 workspace-loaded module with `kernel: true` joins the
+//! implicit-imports list and therefore makes its types visible bare
+//! to every consumer, even consumers that did not name it under
+//! `(import …)`.
+//!
+//! Reachability: a user `(kernel)` module enters the workspace's
+//! modules map only if some module in the import chain reaches it
+//! (the standard import-graph DFS). The kernel-tier flag does NOT
+//! cause unreachable `.ail` files in the entry's directory to be
+//! loaded — see Concern in the iter prep.3 end-report. The
+//! built-in `prelude` and `kernel_stub` are always loaded because
+//! the loader injects them programmatically; user kernel-tier
+//! modules need a path from the entry.
+
+use ailang_surface::load_workspace;
+use std::path::{Path, PathBuf};
+
+/// Write a Form-A source file into the temp dir and return its path.
+fn write_module(dir: &Path, name: &str, src: &str) -> PathBuf {
+    let path = dir.join(format!("{name}.ail"));
+    std::fs::write(&path, src).expect("write fixture");
+    path
+}
+
+/// prep.3: a workspace-loaded `(kernel)` module makes its types
+/// visible bare to consumers that did NOT name it under
+/// `(import …)`. Property: the kernel-flag filter derives the
+/// implicit-imports list from every `kernel: true` module in the
+/// modules map — `consumer` references `KT` bare and validates
+/// because `bridge` brought `k_mod` into the workspace.
+#[test]
+fn kernel_tier_module_auto_imports_without_explicit_import() {
+    let dir = tempfile::tempdir().expect("tempdir");
+    // k_mod carries (kernel) and declares KT.
+    write_module(
+        dir.path(),
+        "k_mod",
+        "(module k_mod\n  (kernel)\n  (data KT (vars a) (ctor KCtor a)))\n",
+    );
+    // bridge imports k_mod so it enters the workspace.
+    write_module(
+        dir.path(),
+        "bridge",
+        concat!(
+            "(module bridge\n",
+            "  (import k_mod)\n",
+            "  (fn anchor\n",
+            "    (type (forall (vars a) (fn-type (params (con KT a)) (ret (con Unit)))))\n",
+            "    (params k) (body unit)))\n",
+        ),
+    );
+    // The entry imports bridge (transitively pulling k_mod), and
+    // uses `(con KT (var a))` bare — no explicit import of k_mod.
+    let entry = write_module(
+        dir.path(),
+        "consumer",
+        concat!(
+            "(module consumer\n",
+            "  (import bridge)\n",
+            "  (fn use_kt\n",
+            "    (type (forall (vars a) (fn-type (params (con KT a)) (ret (con Unit)))))\n",
+            "    (params k) (body unit)))\n",
+        ),
+    );
+
+    let ws = load_workspace(&entry).expect("workspace loads (kernel-tier auto-import)");
+    assert!(
+        ws.modules.contains_key("k_mod"),
+        "k_mod was loaded transitively via bridge"
+    );
+    assert!(
+        ws.modules.get("k_mod").unwrap().kernel,
+        "k_mod is marked kernel-tier"
+    );
+}
+
+/// prep.3: two `(kernel)` modules co-load without conflict; both
+/// enter the implicit-imports list and both are visible to a
+/// consumer that imported neither directly. Property: the filter
+/// `modules.values().filter(|m| m.kernel)` walks ALL modules (not
+/// just the first match), so every kernel-tier module gets
+/// auto-imported.
+#[test]
+fn two_kernel_tier_modules_coload() {
+    let dir = tempfile::tempdir().expect("tempdir");
+    write_module(
+        dir.path(),
+        "k_a",
+        "(module k_a\n  (kernel)\n  (data A (ctor AC)))\n",
+    );
+    write_module(
+        dir.path(),
+        "k_b",
+        "(module k_b\n  (kernel)\n  (data B (ctor BC)))\n",
+    );
+    // bridge imports both kernel modules; consumer transitively
+    // sees both via the kernel-flag filter without explicit import.
+    write_module(
+        dir.path(),
+        "bridge",
+        concat!(
+            "(module bridge\n",
+            "  (import k_a)\n",
+            "  (import k_b)\n",
+            "  (fn anchor\n",
+            "    (type (fn-type (params (con A) (con B)) (ret (con Unit))))\n",
+            "    (params a b) (body unit)))\n",
+        ),
+    );
+    let entry = write_module(
+        dir.path(),
+        "consumer",
+        concat!(
+            "(module consumer\n",
+            "  (import bridge)\n",
+            "  (fn use_ab\n",
+            "    (type (fn-type (params (con A) (con B)) (ret (con Unit))))\n",
+            "    (params a b) (body unit)))\n",
+        ),
+    );
+
+    let ws = load_workspace(&entry).expect("workspace with two kernel modules");
+    assert!(ws.modules.contains_key("k_a"));
+    assert!(ws.modules.contains_key("k_b"));
+    assert!(ws.modules.get("k_a").unwrap().kernel);
+    assert!(ws.modules.get("k_b").unwrap().kernel);
+}
+
+/// prep.3: an explicit `(import …)` for a kernel-tier module
+/// coexists with the auto-import — no double-resolution error, no
+/// behaviour drift. Property: the implicit-imports list and the
+/// explicit-imports list are both consulted by the validator;
+/// having the same name in both does not produce a duplicate-
+/// import diagnostic.
+#[test]
+fn explicit_import_takes_precedence_over_auto_import() {
+    let dir = tempfile::tempdir().expect("tempdir");
+    write_module(
+        dir.path(),
+        "k_mod",
+        "(module k_mod\n  (kernel)\n  (data KT (ctor KC)))\n",
+    );
+    // consumer explicitly imports k_mod AND uses KT bare.
+    let entry = write_module(
+        dir.path(),
+        "consumer",
+        concat!(
+            "(module consumer\n",
+            "  (import k_mod)\n",
+            "  (fn use_kt\n",
+            "    (type (fn-type (params (con KT)) (ret (con Unit))))\n",
+            "    (params k) (body unit)))\n",
+        ),
+    );
+
+    let ws = load_workspace(&entry).expect("explicit + auto coexist");
+    assert!(ws.modules.contains_key("k_mod"));
+    assert!(ws.modules.get("k_mod").unwrap().kernel);
+}