plan: raw-buf.6 kernel-stub-retirement (refs #7)

2026-05-30 15:53:54 +02:00
parent c5eca7e91d
commit fb0dd92a6c
1 changed files with 787 additions and 0 deletions
@@ -0,0 +1,787 @@
+# raw-buf.6 — kernel_stub Retirement — Implementation Plan
+
+> **Parent spec:** `docs/specs/0054-raw-buf.md` (§Architecture item 6,
+> Components-table row "kernel_stub retirement | raw-buf.6",
+> Testing-strategy block "raw-buf.6 (retirement)").
+>
+> **For agentic workers:** REQUIRED SUB-SKILL: use the `implement`
+> skill to run this plan. Steps use `- [ ]` checkboxes for tracking.
+
+**Goal:** Retire the now-redundant `kernel_stub` kernel-tier module —
+`raw_buf` (shipped raw-buf.1–.5) has subsumed every ratification role
+the stub held — leaving the `ailang-kernel` family-crate as the home
+for `raw_buf` alone.
+
+**Architecture:** This is a pure-removal iteration. The stub
+auto-injects into every workspace build, so its retirement ripples
+through five layers: (1) the Rust surface that embeds and parses it
+(`ailang-kernel`, `ailang-surface`); (2) the codegen intercept
+registry (`answer`, `StubT_peek__{Int,Float}` entries + emit fns); (3)
+the tests and `.ail` example fixtures that consume it; (4) the
+workspace-module-count content-pins (5 → 4) and the IR snapshots that
+embed the stub's emitted defs; (5) the design ledger + architecture
+comments that name the stub as the live ratifier. Removal is sequenced
+compile-coupled first (one atomic build gate), then runtime-coupled
+(tests/examples/pins), then snapshot regen, then the present-state
+doc/comment sweep, then full verification.
+
+**Tech Stack:** `ailang-kernel` family-crate, `ailang-surface` loader,
+`ailang-codegen` intercept registry, the `ail` E2E + IR-snapshot
+suites, `ailang-core`/`ailang-check` workspace machinery, the
+`design/` ledger.
+
+**Orchestrator scope decisions (made before planning, not implementer
+judgement calls):**
+
+- **Inline check-layer fixtures stay.** `crates/ailang-check/src/lib.rs`
+  contains self-contained unit tests that build a `StubT`/`kernel_stub`
+  Module *inline* via `serde_json` (module names `"k"` and
+  `"kernel_stub"`) to exercise generic check behaviour (`param-in`
+  enforcement, kernel-tier reachability, `Term::New` resolution). They
+  do **not** depend on the real stub module — they construct what they
+  reference. The name overlap is incidental; these are NOT
+  stub-ratification and are deliberately left untouched. Their presence
+  is the one permitted `kernel_stub`/`StubT` residual after this
+  iteration (Task 5 gate accounts for it).
+- **`examples/fieldtest/kem_3_stub_consumer.ail` is deleted.** It
+  references `kernel_stub.StubT` / `(term-ctor StubT Stub 7)` — both
+  gone after retirement — and documents a since-fixed auto-import bug
+  (`new_stubt_smoke.ail`/`peek_mono_pin_smoke.ail`, both green, prove
+  the mechanism now works). A `.ail` referencing a deleted type is a
+  broken example.
+- **`examples/fieldtest/kem_4_paramin_box_green.ail` is kept,
+  comment-only edit.** It uses a self-contained user `NumBox` ADT, not
+  the stub; only its prose comment names `kernel_stub.StubT` as a
+  comparison. Rephrased to `raw_buf.RawBuf`.
+- **`crates/ailang-core/src/hash.rs:33` is left as-is.** `name:
+  "answer"` there is a generic serde doc-example string, not a
+  reference to the retired `answer` intrinsic. Cosmetic, not drift.
+
+---
+
+## Files this plan creates or modifies
+
+**Create:** none — pure-removal iteration.
+
+**Delete:**
+
+- Delete: `crates/ailang-kernel/src/kernel_stub/` (whole dir: `mod.rs`,
+  `source.ail`)
+- Delete: `crates/ail/tests/mono_scoped_symbol.rs` (whole file — the
+  raw-buf.3 stub-peek mono ratifier; the mechanism is now exercised by
+  RawBuf's ops)
+- Delete: `examples/kernel_answer.ail`, `examples/new_stubt_smoke.ail`,
+  `examples/peek_mono_pin_smoke.ail`,
+  `examples/fieldtest/kem_3_stub_consumer.ail`
+
+**Modify (Rust surface — compile-coupled):**
+
+- Modify: `crates/ailang-kernel/src/lib.rs:8,11,14` — drop `mod
+  kernel_stub;` + `STUB_AIL` re-export + module-doc hop reference
+- Modify: `crates/ailang-surface/src/loader.rs:45-57,60,137-146` —
+  delete `parse_kernel_stub` fn + its rustdoc, delete the injection
+  block, fix the `parse_raw_buf` rustdoc cross-ref
+- Modify: `crates/ailang-surface/src/lib.rs:40` — drop
+  `parse_kernel_stub` from the re-export list
+- Modify: `crates/ailang-codegen/src/intercepts.rs:167-187,555-591,
+  811,817` — delete 3 INTERCEPTS entries + 3 emit fns + the
+  `parse_kernel_stub()` marker-collector line + stale prose
+- Modify: `crates/ailang-core/tests/design_schema_drift.rs:736-774` —
+  delete `kernel_stub_module_round_trips` (it calls
+  `parse_kernel_stub`)
+
+**Modify (tests + examples — runtime-coupled):**
+
+- Modify: `crates/ail/tests/e2e.rs:85-107,877-892` — delete two
+  stub-consumer tests + re-baseline the workspace-count pin 5 → 4
+- Modify: `crates/ailang-core/tests/workspace_pin.rs:52-60` —
+  re-baseline count 5 → 4, drop the `kernel_stub` `contains_key`
+- Modify: `examples/fieldtest/kem_4_paramin_box_green.ail` — comment
+  rephrase only
+
+**Modify (IR snapshots — regenerated by tooling):**
+
+- Modify: `crates/ail/tests/snapshots/{hello,list,max3,sum,ws_main}.ll`
+  — regenerated via `UPDATE_SNAPSHOTS=1`
+
+**Modify (present-state doc + comment sweep):**
+
+- Modify: `design/INDEX.md:112`
+- Modify: `design/models/0007-kernel-extensions.md:3-9,222-223,234-236`
+- Modify: `crates/ailang-core/src/workspace.rs:307-312`
+- Modify: `crates/ailang-check/src/mono.rs:369`
+- Modify: `crates/ailang-check/src/lib.rs:1086,1704-1708,1868,4618`
+  (production architecture comments — example-name swap only; the
+  inline test fixtures at 8187/8226/8340-8399 are LEFT, per scope
+  decision)
+- Modify: `crates/ailang-core/tests/workspace_kernel.rs:14` (header
+  comment only — the test body uses synthetic `k_mod`/`k_a`/`k_b`,
+  not the stub)
+
+**Parse-the-bytes-you-inline gate (planner Step-5 item 9):** documented
+no-op. This plan inlines no *new* surface-language (`.ail`/`.ail.json`)
+or `.ll` program bodies — it deletes existing example fixtures and
+regenerates IR snapshots via the build tool. The only `.ail` edit
+(Task 2, `kem_4`) is a comment-line rephrase, no code change. Nothing
+to pre-parse.
+
+---
+
+## Task 1: Atomic compile-coupled removal of the kernel_stub Rust surface + source
+
+**Files:**
+- Modify: `crates/ailang-kernel/src/lib.rs`
+- Delete: `crates/ailang-kernel/src/kernel_stub/`
+- Modify: `crates/ailang-surface/src/loader.rs`
+- Modify: `crates/ailang-surface/src/lib.rs`
+- Modify: `crates/ailang-codegen/src/intercepts.rs`
+- Modify: `crates/ailang-core/tests/design_schema_drift.rs`
+
+This task removes every reference to the stub's Rust symbols
+(`STUB_AIL`, `parse_kernel_stub`, `emit_answer`,
+`emit_stubt_peek_int/float`, the three INTERCEPTS entries). All of
+these are compile-coupled: the workspace will not compile (including
+test targets) until every one is threaded, so the task ends with a
+single build-of-everything gate. The runtime-failing tests/snapshots
+are addressed in Tasks 2–3.
+
+- [ ] **Step 1: Drop the `kernel_stub` submodule + re-export in the kernel crate**
+
+In `crates/ailang-kernel/src/lib.rs`, replace the module doc hop
+reference and the two `kernel_stub` lines.
+
+Replace:
+
+```rust
+//! The acyclic dependency chain is preserved:
+//! `ailang-surface → ailang-kernel → ailang-core`. Per-module parse
+//! hops live in `ailang-surface` (`parse_kernel_stub`, …) so this
+//! crate carries zero parser code.
+
+mod kernel_stub;
+mod raw_buf;
+
+pub use kernel_stub::SOURCE as STUB_AIL;
+pub use raw_buf::SOURCE as RAW_BUF_AIL;
+```
+
+With:
+
+```rust
+//! The acyclic dependency chain is preserved:
+//! `ailang-surface → ailang-kernel → ailang-core`. Per-module parse
+//! hops live in `ailang-surface` (`parse_raw_buf`, …) so this
+//! crate carries zero parser code.
+
+mod raw_buf;
+
+pub use raw_buf::SOURCE as RAW_BUF_AIL;
+```
+
+- [ ] **Step 2: Delete the kernel_stub source submodule**
+
+Run: `git rm -r crates/ailang-kernel/src/kernel_stub`
+Expected: removes `mod.rs` + `source.ail`.
+
+- [ ] **Step 3: Delete `parse_kernel_stub` and its injection in the loader**
+
+In `crates/ailang-surface/src/loader.rs`, delete the `parse_kernel_stub`
+fn together with its rustdoc (the block currently at lines 45–57):
+
+```rust
+/// prep.3 (kernel-extension-mechanics): parse the embedded
+/// kernel-stub bytes into a `Module`. Mirror of [`parse_prelude`].
+///
+/// Source-of-truth: `ailang_kernel::STUB_AIL`. The stub
+/// ratifies the end-to-end kernel-tier path: `Module.kernel`,
+/// `TypeDef.param-in`, and auto-import without `(import …)`.
+///
+/// Panics on parse failure — the stub is build-time-validated by
+/// every drift test run.
+pub fn parse_kernel_stub() -> Module {
+    crate::parse(ailang_kernel::STUB_AIL)
+        .expect("ailang_kernel::STUB_AIL must parse as a Module")
+}
+
+```
+
+Then fix the surviving `parse_raw_buf` rustdoc cross-ref. Replace:
+
+```rust
+/// raw-buf.4: parse the embedded raw_buf kernel-tier base-extension
+/// module bytes into a `Module`. Mirror of [`parse_kernel_stub`].
+```
+
+With:
+
+```rust
+/// raw-buf.4: parse the embedded raw_buf kernel-tier base-extension
+/// module bytes into a `Module`. Mirror of [`parse_prelude`].
+```
+
+- [ ] **Step 4: Delete the stub injection block in `load_workspace`**
+
+In `crates/ailang-surface/src/loader.rs`, delete the whole stub
+injection block (currently lines 137–146, including the blank line that
+separates it from the raw_buf block):
+
+```rust
+    // parse_kernel_stub() injects the ratifying stub kernel module —
+    // exercises Module.kernel + TypeDef.param-in end-to-end. The
+    // kernel-flag filter below picks it up automatically because its
+    // source carries `(kernel)`.
+    if modules.contains_key("kernel_stub") {
+        return Err(WorkspaceLoadError::ReservedModuleName {
+            name: "kernel_stub".to_string(),
+        });
+    }
+    modules.insert("kernel_stub".to_string(), parse_kernel_stub());
+
+```
+
+The `parse_prelude()` block above and the `parse_raw_buf()` block below
+stay unchanged.
+
+- [ ] **Step 5: Drop `parse_kernel_stub` from the `ailang-surface` re-export**
+
+In `crates/ailang-surface/src/lib.rs:40`, remove `parse_kernel_stub`
+from the `pub use loader::{…}` list, keeping `parse_prelude` and
+`parse_raw_buf`. (Exact edit: delete the `parse_kernel_stub,` token from
+the re-export list.)
+
+- [ ] **Step 6: Delete the three stub INTERCEPTS entries**
+
+In `crates/ailang-codegen/src/intercepts.rs`, delete the three entries
+(currently lines 167–187):
+
+```rust
+    Intercept {
+        name: "answer",
+        expected_params: &[],
+        expected_ret: "i64",
+        wants_alwaysinline: false,
+        emit: emit_answer,
+    },
+    Intercept {
+        name: "StubT_peek__Int",
+        expected_params: &["ptr"], // borrow (con StubT Int) lowers to ptr
+        expected_ret: "i64",
+        wants_alwaysinline: false,
+        emit: emit_stubt_peek_int,
+    },
+    Intercept {
+        name: "StubT_peek__Float",
+        expected_params: &["ptr"],
+        expected_ret: "double",
+        wants_alwaysinline: false,
+        emit: emit_stubt_peek_float,
+    },
+```
+
+The `ne__Int` entry above and the `RawBuf_*` block below stay.
+
+- [ ] **Step 7: Delete the three stub emit fns**
+
+In `crates/ailang-codegen/src/intercepts.rs`, delete `emit_answer`,
+`emit_stubt_peek_int`, and `emit_stubt_peek_float` together with their
+rustdoc (currently lines 555–591):
+
+```rust
+/// Ratifier intrinsic for intrinsic-bodies.1: `answer : () -> Int`
+/// returns the constant 42. Exercises the Term::Intrinsic → registry
+/// route end-to-end. May be retired once a real kernel-tier intrinsic
+/// (raw-buf) lands.
+pub(crate) fn emit_answer(emitter: &mut Emitter<'_>) -> Result<()> {
+    emitter.body.push_str("  ret i64 42\n");
+    emitter.body.push_str("}\n\n");
+    emitter.block_terminated = true;
+    Ok(())
+}
+
+/// raw-buf.3 ratifier emit. NOTE: never instantiated to codegen this
+/// iteration (no Term::New to build a StubT; unit-test-ratified only).
+/// The load offset/correctness is exercised end-to-end only by
+/// raw-buf.4's RawBuf path; here the entry exists to satisfy the
+/// bijection. Retires with the stub in raw-buf.5.
+pub(crate) fn emit_stubt_peek_int(emitter: &mut Emitter<'_>) -> Result<()> {
+    let n = emitter.locals.len();
+    let s = emitter.locals[n - 1].1.clone();
+    let v = emitter.fresh_ssa();
+    emitter.body.push_str(&format!("  {v} = load i64, ptr {s}\n"));
+    emitter.body.push_str(&format!("  ret i64 {v}\n"));
+    emitter.body.push_str("}\n\n");
+    emitter.block_terminated = true;
+    Ok(())
+}
+
+pub(crate) fn emit_stubt_peek_float(emitter: &mut Emitter<'_>) -> Result<()> {
+    let n = emitter.locals.len();
+    let s = emitter.locals[n - 1].1.clone();
+    let v = emitter.fresh_ssa();
+    emitter.body.push_str(&format!("  {v} = load double, ptr {s}\n"));
+    emitter.body.push_str(&format!("  ret double {v}\n"));
+    emitter.body.push_str("}\n\n");
+    emitter.block_terminated = true;
+    Ok(())
+}
+
+```
+
+- [ ] **Step 8: Drop the stub from the bijection marker-collector**
+
+In `crates/ailang-codegen/src/intercepts.rs`, the `#[cfg(test)]`
+`workspace_intrinsic_markers` fn parses each kernel-tier source to
+collect its `(intrinsic)` markers. Remove the stub from both the prose
+and the parse list. Replace:
+
+```rust
+    /// Collect the mangled name of every `(intrinsic)` marker reachable
+    /// in the kernel-tier source modules (prelude + kernel_stub — the
+    /// only modules where an intrinsic body is legal today).
+    fn workspace_intrinsic_markers() -> BTreeSet<String> {
+        let mut markers = BTreeSet::new();
+        for module in [
+            ailang_surface::parse_prelude(),
+            ailang_surface::parse_kernel_stub(),
+            ailang_surface::parse_raw_buf(),
+        ] {
+```
+
+With:
+
+```rust
+    /// Collect the mangled name of every `(intrinsic)` marker reachable
+    /// in the kernel-tier source modules (prelude + raw_buf — the
+    /// only modules where an intrinsic body is legal today).
+    fn workspace_intrinsic_markers() -> BTreeSet<String> {
+        let mut markers = BTreeSet::new();
+        for module in [
+            ailang_surface::parse_prelude(),
+            ailang_surface::parse_raw_buf(),
+        ] {
+```
+
+(The `answer` / `StubT_peek` markers leave with the deleted source, and
+their INTERCEPTS entries left in Steps 6–7 — the marker↔entry bijection
+holds in lockstep. The `Def::Fn` "Top-level intrinsic" comment at line
+~851 still names `answer` as an example; swap that example to
+`float_eq` to keep the comment present-state: replace `(float_eq,
+answer, ...)` with `(float_eq, ...)`.)
+
+- [ ] **Step 9: Delete `kernel_stub_module_round_trips`**
+
+In `crates/ailang-core/tests/design_schema_drift.rs`, delete the
+`kernel_stub_module_round_trips` test together with its rustdoc
+(currently lines 736–774, from the `/// prep.3 …` comment through the
+closing `}` before `raw_buf_module_round_trips`). The surviving
+`raw_buf_module_round_trips` (immediately below) carries the
+kernel-tier round-trip invariant forward.
+
+- [ ] **Step 10: Compile gate — everything builds**
+
+Run: `cargo build --workspace --tests 2>&1 | tail -8`
+Expected: `Finished` with 0 errors (no `unresolved import`, no
+`cannot find function`/`value` for `STUB_AIL`, `parse_kernel_stub`,
+`emit_answer`, `emit_stubt_peek_*`). The test suite is now
+compile-clean but RED at runtime (stub-consumer tests, count pins, IR
+snapshots still reference the gone stub) — Tasks 2–3 green it.
+
+---
+
+## Task 2: Remove runtime-coupled stub-consumer tests + examples, re-baseline count pins
+
+**Files:**
+- Modify: `crates/ail/tests/e2e.rs`
+- Delete: `crates/ail/tests/mono_scoped_symbol.rs`
+- Delete: `examples/kernel_answer.ail`, `examples/new_stubt_smoke.ail`,
+  `examples/peek_mono_pin_smoke.ail`,
+  `examples/fieldtest/kem_3_stub_consumer.ail`
+- Modify: `examples/fieldtest/kem_4_paramin_box_green.ail`
+- Modify: `crates/ailang-core/tests/workspace_pin.rs`
+
+- [ ] **Step 1: Delete the two stub-consumer E2E tests**
+
+In `crates/ail/tests/e2e.rs`, delete `answer_intrinsic_builds_and_runs_printing_42`
+(with its rustdoc, currently lines 85–96) and `new_stubt_builds_and_runs`
+(with its rustdoc, currently lines 98–107):
+
+```rust
+/// Property protected: a kernel-tier `(intrinsic)` fn builds and runs
+/// from source to native via the codegen intercept registry. The
+/// `kernel_stub.answer` intrinsic (body `Term::Intrinsic`, intercept
+/// `emit_answer` → `ret i64 42`) is consumed by a user module and its
+/// value reaches stdout. This is the end-to-end ratifier for the whole
+/// Term::Intrinsic mechanism: parse → signature-only typecheck →
+/// mono-skip → intercept-routed codegen → native 42.
+#[test]
+fn answer_intrinsic_builds_and_runs_printing_42() {
+    let out = build_and_run("kernel_answer.ail");
+    assert_eq!(out.trim(), "42");
+}
+
+/// raw-buf.4: the general `Term::New` desugar. `(new StubT 42)`
+/// desugars to `(app StubT.new 42)` (StubT.new has a real
+/// `(term-ctor StubT Stub x)` body, so it builds independent of
+/// RawBuf), the Int is matched back out and printed. Ratifies the
+/// desugar + the removal of both codegen `Term::New` deferral arms.
+#[test]
+fn new_stubt_builds_and_runs() {
+    let out = build_and_run("new_stubt_smoke.ail");
+    assert_eq!(out.trim(), "42");
+}
+
+```
+
+(The `Term::New` desugar itself stays ratified by the RawBuf path —
+`raw_buf_int_e2e` builds `(new RawBuf (con Int) 3)` end-to-end.)
+
+- [ ] **Step 2: Re-baseline the E2E workspace-count pin 5 → 4**
+
+In `crates/ail/tests/e2e.rs`, replace the count assertion + its comment
+ the `kernel_stub` name check. Replace:
+
+```rust
+    let modules = v["modules"].as_array().expect("modules must be array");
+    // the loader auto-injects every built-in kernel-tier module
+    // (`prelude`; since prep.3 of the kernel-extension-mechanics
+    // milestone, the ratifying `kernel_stub`; and since raw-buf.4 the
+    // first real-payload kernel extension `raw_buf`), so the count is
+    // the user's two modules plus the three built-ins.
+    assert_eq!(modules.len(), 5, "expected 5 modules: {stdout}");
+
+    let names: Vec<&str> = modules
+        .iter()
+        .filter_map(|m| m.get("name").and_then(|n| n.as_str()))
+        .collect();
+    assert!(names.contains(&"ws_main"), "ws_main missing: {names:?}");
+    assert!(names.contains(&"ws_lib"), "ws_lib missing: {names:?}");
+    assert!(names.contains(&"prelude"), "prelude missing: {names:?}");
+    assert!(names.contains(&"kernel_stub"), "kernel_stub missing: {names:?}");
+    assert!(names.contains(&"raw_buf"), "raw_buf missing: {names:?}");
+```
+
+With:
+
+```rust
+    let modules = v["modules"].as_array().expect("modules must be array");
+    // the loader auto-injects every built-in kernel-tier module
+    // (`prelude` and, since raw-buf.4, the first real-payload kernel
+    // extension `raw_buf`), so the count is the user's two modules plus
+    // the two built-ins.
+    assert_eq!(modules.len(), 4, "expected 4 modules: {stdout}");
+
+    let names: Vec<&str> = modules
+        .iter()
+        .filter_map(|m| m.get("name").and_then(|n| n.as_str()))
+        .collect();
+    assert!(names.contains(&"ws_main"), "ws_main missing: {names:?}");
+    assert!(names.contains(&"ws_lib"), "ws_lib missing: {names:?}");
+    assert!(names.contains(&"prelude"), "prelude missing: {names:?}");
+    assert!(names.contains(&"raw_buf"), "raw_buf missing: {names:?}");
+```
+
+- [ ] **Step 3: Delete the stub-peek mono ratifier test file**
+
+Run: `git rm crates/ail/tests/mono_scoped_symbol.rs`
+Expected: removes the whole file. (The scope-qualified mono mechanism it
+pinned — `StubT_peek__Int`/`Float` — is now exercised by RawBuf's
+`RawBuf_{new,get,set,size}__{Int,Float,Bool}` symbols; the bijection
+test in `intercepts.rs` is the surviving pin.)
+
+- [ ] **Step 4: Delete the stub-consumer example fixtures**
+
+Run: `git rm examples/kernel_answer.ail examples/new_stubt_smoke.ail examples/peek_mono_pin_smoke.ail examples/fieldtest/kem_3_stub_consumer.ail`
+Expected: removes all four `.ail` fixtures.
+
+- [ ] **Step 5: Rephrase the kem_4 fieldtest comment to present-state**
+
+In `examples/fieldtest/kem_4_paramin_box_green.ail`, replace the stale
+comparison-comment line. Replace:
+
+```text
+; can declare it just as the stub kernel_stub.StubT does.
+```
+
+With:
+
+```text
+; can declare it just as the raw_buf.RawBuf base extension does.
+```
+
+- [ ] **Step 6: Re-baseline the workspace_pin count 5 → 4**
+
+In `crates/ailang-core/tests/workspace_pin.rs`, replace the comment +
+count + `kernel_stub` check (currently lines 52–60). Replace:
+
+```rust
+    // the loader auto-injects three built-in kernel-tier modules
+    // (`prelude`, `kernel_stub` — see prep.3 of the
+    // kernel-extension-mechanics milestone — and `raw_buf`, the
+    // first real-payload kernel extension, raw-buf.4), so the count
+    // is the user's two modules plus those three.
+    assert_eq!(ws.modules.len(), 5);
+    assert!(ws.modules.contains_key("prelude"));
+    assert!(ws.modules.contains_key("kernel_stub"));
+    assert!(ws.modules.contains_key("raw_buf"));
+```
+
+With:
+
+```rust
+    // the loader auto-injects two built-in kernel-tier modules
+    // (`prelude` and `raw_buf`, the first real-payload kernel
+    // extension, raw-buf.4), so the count is the user's two modules
+    // plus those two.
+    assert_eq!(ws.modules.len(), 4);
+    assert!(ws.modules.contains_key("prelude"));
+    assert!(ws.modules.contains_key("raw_buf"));
+```
+
+- [ ] **Step 7: Test gate — suite green except IR snapshots**
+
+Run: `cargo test --workspace -- --skip ir_snapshot_ 2>&1 | tail -15`
+Expected: `test result: ok` for every target; 0 failed. (The
+`ir_snapshot_*` tests are skipped here — they still embed the stub's
+emitted defs and are regenerated in Task 3.) In particular
+`loads_example_workspace_happy_path`, the e2e `workspace`-JSON test, and
+the `raw_buf_*` suite pass; no test references the gone stub.
+
+---
+
+## Task 3: Regenerate the five IR snapshots
+
+**Files:**
+- Modify: `crates/ail/tests/snapshots/hello.ll`
+- Modify: `crates/ail/tests/snapshots/list.ll`
+- Modify: `crates/ail/tests/snapshots/max3.ll`
+- Modify: `crates/ail/tests/snapshots/sum.ll`
+- Modify: `crates/ail/tests/snapshots/ws_main.ll`
+
+The stub auto-injects into every build, so each snapshot currently
+embeds `@ail_kernel_stub_new*`, `@ail_kernel_stub_answer*`,
+`@drop_kernel_stub_StubT`, `@partial_drop_kernel_stub_StubT`. With the
+stub gone these defs vanish from the emitted IR; the snapshots are
+regenerated, not hand-edited.
+
+- [ ] **Step 1: Regenerate the snapshots from the live tool**
+
+Run: `UPDATE_SNAPSHOTS=1 cargo test --test ir_snapshot ir_snapshot_ 2>&1 | tail -10`
+Expected: the five `ir_snapshot_{sum,max3,hello,list,ws_main}` tests run
+and rewrite their `.ll` files. (`ir_snapshot.rs` writes the snapshot
+when `UPDATE_SNAPSHOTS` is set.)
+
+- [ ] **Step 2: Verify the stub symbols are gone from the snapshots**
+
+Run: `git grep -c kernel_stub -- crates/ail/tests/snapshots/ ; echo "exit=$status"`
+Expected: no output lines (no file matches) — every
+`@ail_kernel_stub_*` / `@drop_kernel_stub_StubT` def is gone. Inspect
+the diff (`git diff --stat crates/ail/tests/snapshots/`) and confirm the
+only removed lines are the stub defs/closures (no user-module IR
+changed).
+
+- [ ] **Step 3: Snapshot gate — tests green without the update flag**
+
+Run: `cargo test --test ir_snapshot ir_snapshot_ 2>&1 | tail -8`
+Expected: `test result: ok. 5 passed` (the regenerated snapshots match
+the live emitter exactly).
+
+---
+
+## Task 4: Present-state sweep — design ledger + architecture comments
+
+**Files:**
+- Modify: `design/INDEX.md`
+- Modify: `design/models/0007-kernel-extensions.md`
+- Modify: `crates/ailang-core/src/workspace.rs`
+- Modify: `crates/ailang-check/src/mono.rs`
+- Modify: `crates/ailang-check/src/lib.rs`
+- Modify: `crates/ailang-core/tests/workspace_kernel.rs`
+
+Per the honesty-rule (`design/contracts/0007-honesty-rule.md`): docs and
+architecture comments mirror only the actual present state. With the
+stub retired, every comment that names `kernel_stub`/`StubT` as the live
+ratifier or example is updated to name `raw_buf`/`RawBuf`. (The
+self-contained inline test fixtures in `lib.rs:8187/8226/8340-8399` are
+left, per the scope decision — they construct what they reference.)
+
+- [ ] **Step 1: Update the design ledger INDEX row**
+
+In `design/INDEX.md:112`, replace:
+
+```text
+| kernel-extensions | onboarding / evolves (mechanisms milestone closed 2026-05-28; ratified end-to-end by the `ailang-kernel/src/kernel_stub` fixture, planned for retirement when raw-buf lands a real second consumer; raw-buf and series milestones pending) | design/models/0007-kernel-extensions.md |
+```
+
+With:
+
+```text
+| kernel-extensions | onboarding / evolves (mechanisms milestone closed 2026-05-28; ratified end-to-end by the `ailang-kernel/src/raw_buf` base extension; series milestone pending) | design/models/0007-kernel-extensions.md |
+```
+
+- [ ] **Step 2: Update the 0007 STATUS block**
+
+In `design/models/0007-kernel-extensions.md`, replace:
+
+```text
+`param-in` — are shipped and ratified by the stub kernel module
+(`crates/ailang-kernel/src/kernel_stub/`). The base-extension and library-
+extension milestones (`raw-buf`, `series`) are pending. This
+```
+
+With:
+
+```text
+`param-in` — are shipped and ratified by the `raw_buf` base
+extension (`crates/ailang-kernel/src/raw_buf/`). The base-extension
+milestone (`raw-buf`) has shipped; the library-extension milestone
+(`series`) is pending. This
+```
+
+- [ ] **Step 3: Update the 0007 auto-injection prose**
+
+In `design/models/0007-kernel-extensions.md`, replace:
+
+```text
+`crates/ailang-surface/src/loader.rs::load_workspace` injects
+`parse_prelude()` and `parse_kernel_stub()` programmatically,
+```
+
+With:
+
+```text
+`crates/ailang-surface/src/loader.rs::load_workspace` injects
+`parse_prelude()` and `parse_raw_buf()` programmatically,
+```
+
+Then replace:
+
+```text
+migration. The ratifying stub kernel module
+(`crates/ailang-kernel/src/kernel_stub/`) and any future kernel-tier
+consumers (Series, Matrix) auto-import through the same filter.
+```
+
+With:
+
+```text
+migration. The `raw_buf` base-extension kernel module
+(`crates/ailang-kernel/src/raw_buf/`) and any future kernel-tier
+consumers (Series, Matrix) auto-import through the same filter.
+```
+
+- [ ] **Step 4: Update the WorkspaceError doc-comment**
+
+In `crates/ailang-core/src/workspace.rs:307-312`, replace:
+
+```rust
+    /// 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).
+```
+
+With:
+
+```rust
+    /// The current built-in set is `prelude` and `raw_buf` (the
+    /// `raw_buf` base extension is injected unconditionally in all
+    /// builds; future base extensions may add more).
+```
+
+- [ ] **Step 5: Update the mono anti-collision comment**
+
+In `crates/ailang-check/src/mono.rs:369`, replace:
+
+```rust
+    // anyway would make `rewrite_mono_calls` treat the local call as a
+    // poly-free-fn site and over-advance the slot cursor (surfaced when
+    // kernel_stub gained a `peek` colliding with a fixture-local
+    // monomorphic `peek`). The dot-qualified / type-scoped spellings
+```
+
+With:
+
+```rust
+    // anyway would make `rewrite_mono_calls` treat the local call as a
+    // poly-free-fn site and over-advance the slot cursor (surfaced when
+    // a kernel-tier type-scoped op collided with a fixture-local
+    // monomorphic fn of the same bare name). The dot-qualified /
+    // type-scoped spellings
+```
+
+- [ ] **Step 6: Swap the stub example-names in the check production comments**
+
+In `crates/ailang-check/src/lib.rs`, these four production comments cite
+the stub as an example of a kernel-tier module; swap the example to the
+live `raw_buf`. (Targeted token edits — these are comment lines, not the
+inline `serde_json` fixtures at 8187/8226/8340-8399, which stay.)
+
+- Line ~1086: replace `kernel_stub.StubT.new` with `raw_buf.RawBuf.new`.
+- Lines ~1704-1708: replace the three `kernel_stub` tokens (`` `kernel_stub.StubT` ``, `` reject `kernel_stub` as ``, `` leaving `kernel_stub` and any future ``) with the `raw_buf` equivalents (`` `raw_buf.RawBuf` ``, `` reject `raw_buf` as ``, `` leaving `raw_buf` and any future ``).
+- Line ~1868: replace `` leaving `kernel_stub` and any future `` with `` leaving `raw_buf` and any future ``.
+- Line ~4618: replace `kernel_stub's StubT.new` with `raw_buf's RawBuf.new`.
+
+- [ ] **Step 7: Update the workspace_kernel test header comment**
+
+In `crates/ailang-core/tests/workspace_kernel.rs:14`, replace the
+`kernel_stub` mention in the module-doc header. Replace:
+
+```rust
+//! built-in `prelude` and `kernel_stub` are always loaded because
+```
+
+With:
+
+```rust
+//! built-in `prelude` and `raw_buf` are always loaded because
+```
+
+(The test bodies use synthetic `k_mod`/`k_a`/`k_b` modules, not the
+stub, so no test logic changes.)
+
+- [ ] **Step 8: Hard symbol gate — every stub Rust symbol is gone**
+
+Run: `git grep -nE 'STUB_AIL|parse_kernel_stub|emit_answer|emit_stubt_peek|StubT_peek__' -- crates/ examples/ design/ docs/ ; echo "done"`
+Expected: only `done` printed — zero matches. These are the
+compile-coupled symbols + the scope-qualified peek mono symbols; none
+may survive anywhere.
+
+- [ ] **Step 9: Soft residual review — report remaining name mentions**
+
+Run: `git grep -ln 'kernel_stub\|StubT' -- crates/ examples/ design/ docs/`
+Expected: the ONLY files listed are `crates/ailang-check/src/lib.rs`
+(the deliberately-kept inline `serde_json` fixtures). Any other file is
+a missed site to fix. (This is a review checkpoint, not a hard
+assertion — report the file list in the task summary.)
+
+---
+
+## Task 5: Full verification + regression
+
+**Files:** none modified — verification only.
+
+- [ ] **Step 1: Full workspace test suite green**
+
+Run: `cargo test --workspace 2>&1 | tail -20`
+Expected: every target `test result: ok`, 0 failed (including the now-
+regenerated `ir_snapshot_*` and the `raw_buf_*` suite).
+
+- [ ] **Step 2: Workspace builds clean**
+
+Run: `cargo build --workspace 2>&1 | tail -5`
+Expected: `Finished`, 0 warnings/errors attributable to the removal.
+
+- [ ] **Step 3: Regression harnesses**
+
+Run: `python3 bench/check.py && python3 bench/compile_check.py && python3 bench/cross_lang.py`
+Expected: each prints its PASS/within-baseline summary and exits 0.
+(`compile_check.py` may shift slightly because the stub's defs no longer
+inject into every compile — a uniform downward delta from removed dead
+IR is expected, not a regression. Report the numbers for orchestrator
+ratification of the baseline.)
+
+- [ ] **Step 4: Confirm the crate shape**
+
+Run: `ls crates/ailang-kernel/src/`
+Expected: `lib.rs` and `raw_buf/` only — `kernel_stub/` is gone, the
+`ailang-kernel` family-crate stays as `raw_buf`'s home.