iter raw-buf.6 kernel-stub-retirement (DONE 5/5): retire the stub, raw_buf is the sole base extension (refs #7)

Closes the raw-buf milestone. raw_buf (shipped raw-buf.1-.5; the
owned-drop resolution landed under bug #42/#43) has subsumed every
ratification role kernel_stub held -- Term::New end-to-end, the
param-in reject, kernel-tier auto-import, the monomorphic intrinsic
path, and the type-scoped polymorphic intrinsic mechanism (RawBuf's
four ops). The stub is now redundant; this iteration removes it.

Pure removal (-636/+49 across 22 files, 7 deleted):
- Rust surface: drop `mod kernel_stub` + `STUB_AIL` re-export
  (ailang-kernel), `parse_kernel_stub` + its workspace injection
  (ailang-surface), the `answer` + two `StubT_peek__{Int,Float}`
  INTERCEPTS entries + their three emit fns (ailang-codegen). The
  (intrinsic) markers leave with the deleted source, so the
  marker<->entry bijection holds in lockstep.
- Source + tests: delete crates/ailang-kernel/src/kernel_stub/,
  kernel_stub_module_round_trips, the two stub-consumer e2e tests,
  and mono_scoped_symbol.rs (its scope-qualified-mono mechanism is
  now pinned by RawBuf's ops + the intercepts bijection).
- Fixtures: delete kernel_answer.ail, new_stubt_smoke.ail,
  peek_mono_pin_smoke.ail, and fieldtest kem_3_stub_consumer.ail
  (referenced the deleted StubT; documented a since-fixed bug).
- Pins: re-baseline both workspace-count content-pins 5 -> 4
  (workspace_pin.rs + the e2e.rs twin) and regenerate all five IR
  snapshots (400 stub-IR lines removed; no user IR changed -- the
  stub auto-injected into every build).
- Ledger: design/INDEX.md + design/models/0007 to present-state
  (raw_buf is the live ratifier; raw-buf milestone shipped, series
  pending), plus architecture-comment sweep across workspace.rs,
  mono.rs, check/codegen lib.rs, workspace_kernel.rs.

Scope decisions (orchestrator, pre-plan): the self-contained inline
serde_json check-layer fixtures in ailang-check/src/lib.rs keep their
incidental StubT/kernel_stub sample names (they construct what they
reference; not stub-ratification) -- the one permitted residual.
kem_4 fieldtest kept (uses a user NumBox ADT, comment-only edit).
hash.rs `name: "answer"` left (generic serde doc example).

Plan-gap caught at implement: the planner's verbatim edit list
under-enumerated four honesty sites; one (mono.rs:562) carried a
literal `StubT_peek__Int` -- a hard-gate symbol the verbatim list
missed, which would have failed Task 4's removal gate. Filled
(comment-only, no behaviour). Confirms the planner self-review
filter-completeness risk; the implement gate caught it.

Verification: full workspace suite green (0 failed); hard symbol gate
(STUB_AIL|parse_kernel_stub|emit_answer|emit_stubt_peek|StubT_peek__)
zero matches across crates/ examples/ design/; soft gate residual only
the kept inline fixtures; kernel crate is lib.rs + raw_buf/ only.
Regression: compile_check 24/24 stable (exit 0; uniform downward
check_ms within tol -- stub no longer parsed per compile), cross_lang
25/25, check 34/34 stable (exit 0; an earlier exit-1 on
rc_over_bump was machine-load ratio noise -- denominator bump_s got
faster, rc_s also improved -- confirmed green on re-run, not
baselined).

crates/ail/tests/e2e.rs

@@ -82,30 +82,6 @@ fn sum_1_to_10_is_55() {
     assert_eq!(stdout.trim(), "55");
 }
 
-/// 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");
-}
-
 #[test]
 fn loop_recur_sum_to_runs_to_value() {
     let stdout = build_and_run("loop_sum_to_run.ail");
@@ -875,11 +851,10 @@ fn workspace_lists_imported_modules() {
 
     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
+    // (`prelude` and, since raw-buf.4, the first real-payload kernel
-    // milestone, the ratifying `kernel_stub`; and since raw-buf.4 the
+    // extension `raw_buf`), so the count is the user's two modules plus
-    // first real-payload kernel extension `raw_buf`), so the count is
+    // the two built-ins.
-    // the user's two modules plus the three built-ins.
+    assert_eq!(modules.len(), 4, "expected 4 modules: {stdout}");
-    assert_eq!(modules.len(), 5, "expected 5 modules: {stdout}");
 
     let names: Vec<&str> = modules
         .iter()
@@ -888,7 +863,6 @@ fn workspace_lists_imported_modules() {
     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:?}");
 }
 

crates/ail/tests/mono_scoped_symbol.rs

@@ -1,49 +0,0 @@
-//! raw-buf.3: a type-scoped polymorphic intrinsic call `StubT.peek`
-//! monomorphises to the scope-qualified symbol `StubT_peek__<elem>`
-//! (not the bare `peek__<elem>`). Proves the scope threads
-//! resolution → FreeFnCall → MonoTarget → mint. No codegen / no
-//! Term::New: assertion is on the monomorphised def names.
-
-use ailang_core::ast::Def;
-use ailang_surface::load_workspace;
-use std::path::PathBuf;
-
-fn fixture_path() -> PathBuf {
-    let mut d = PathBuf::from(env!("CARGO_MANIFEST_DIR"));
-    d.pop();
-    d.pop();
-    d.join("examples").join("peek_mono_pin_smoke.ail")
-}
-
-#[test]
-fn stubt_peek_monomorphises_to_scope_qualified_symbols() {
-    let ws = load_workspace(&fixture_path()).expect("workspace loads");
-    let diags = ailang_check::check_workspace(&ws);
-    assert!(diags.is_empty(), "typecheck diagnostics: {diags:?}");
-    let post_mono = ailang_check::monomorphise_workspace(&ws).expect("mono green");
-
-    // Free-fn mono defs are appended to the polymorphic source's
-    // defining module — `kernel_stub`, where `peek` lives.
-    let names: Vec<String> = post_mono
-        .modules
-        .values()
-        .flat_map(|m| m.defs.iter())
-        .filter_map(|d| match d {
-            Def::Fn(f) => Some(f.name.clone()),
-            _ => None,
-        })
-        .collect();
-
-    assert!(
-        names.iter().any(|n| n == "StubT_peek__Int"),
-        "expected scope-qualified StubT_peek__Int; got: {names:?}"
-    );
-    assert!(
-        names.iter().any(|n| n == "StubT_peek__Float"),
-        "expected scope-qualified StubT_peek__Float; got: {names:?}"
-    );
-    assert!(
-        !names.iter().any(|n| n == "peek__Int"),
-        "bare peek__Int must NOT be minted (scope-qualified only)"
-    );
-}

crates/ail/tests/snapshots/hello.ll

@@ -25,8 +25,6 @@ declare ptr @ailang_str_concat(ptr, ptr)
 declare i64 @llvm.fptosi.sat.i64.f64(double)
 
 @ail_hello_main_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_hello_main_adapter, ptr null }
-@ail_kernel_stub_new_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_kernel_stub_new_adapter, ptr null }
-@ail_kernel_stub_answer_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_kernel_stub_answer_adapter, ptr null }
 @ail_prelude_float_eq_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_prelude_float_eq_adapter, ptr null }
 @ail_prelude_float_ne_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_prelude_float_ne_adapter, ptr null }
 @ail_prelude_float_lt_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_prelude_float_lt_adapter, ptr null }
@@ -47,84 +45,6 @@ entry:
   ret i8 %r
 }
 
-define ptr @ail_kernel_stub_new(i64 %arg_x) {
-entry:
-  %v1 = call ptr @ailang_rc_alloc(i64 16)
-  store i64 0, ptr %v1, align 8
-  %v2 = getelementptr inbounds i8, ptr %v1, i64 8
-  store i64 %arg_x, ptr %v2, align 8
-  ret ptr %v1
-}
-
-define ptr @ail_kernel_stub_new_adapter(ptr %_env, i64 %a0) {
-entry:
-  %r = call ptr @ail_kernel_stub_new(i64 %a0)
-  ret ptr %r
-}
-
-define i64 @ail_kernel_stub_answer() {
-entry:
-  ret i64 42
-}
-
-define i64 @ail_kernel_stub_answer_adapter(ptr %_env) {
-entry:
-  %r = call i64 @ail_kernel_stub_answer()
-  ret i64 %r
-}
-
-define void @drop_kernel_stub_StubT(ptr %p) {
-entry:
-  %is_null = icmp eq ptr %p, null
-  br i1 %is_null, label %ret, label %live
-live:
-  %tag = load i64, ptr %p, align 8
-  switch i64 %tag, label %dflt [
-    i64 0, label %arm_0
-  ]
-arm_0:
-  %a0 = getelementptr inbounds i8, ptr %p, i64 8
-  %v1 = load ptr, ptr %a0, align 8
-  call void @ailang_rc_dec(ptr %v1)
-  br label %join
-dflt:
-  unreachable
-join:
-  call void @ailang_rc_dec(ptr %p)
-  br label %ret
-ret:
-  ret void
-}
-
-define void @partial_drop_kernel_stub_StubT(ptr %p, i64 %mask) {
-entry:
-  %is_null = icmp eq ptr %p, null
-  br i1 %is_null, label %ret, label %live
-live:
-  %tag = load i64, ptr %p, align 8
-  switch i64 %tag, label %dflt [
-    i64 0, label %arm_0
-  ]
-arm_0:
-  %b0 = and i64 %mask, 1
-  %s1 = icmp ne i64 %b0, 0
-  br i1 %s1, label %after_0_0, label %do_0_0
-do_0_0:
-  %a2 = getelementptr inbounds i8, ptr %p, i64 8
-  %v3 = load ptr, ptr %a2, align 8
-  call void @ailang_rc_dec(ptr %v3)
-  br label %after_0_0
-after_0_0:
-  br label %join
-dflt:
-  unreachable
-join:
-  call void @ailang_rc_dec(ptr %p)
-  br label %ret
-ret:
-  ret void
-}
-
 define i1 @ail_prelude_float_eq(double %arg_x, double %arg_y) alwaysinline {
 entry:
   %v1 = fcmp oeq double %arg_x, %arg_y

crates/ail/tests/snapshots/list.ll

@@ -22,8 +22,6 @@ declare ptr @ailang_str_clone(ptr)
 declare ptr @ailang_str_concat(ptr, ptr)
 declare i64 @llvm.fptosi.sat.i64.f64(double)
 
-@ail_kernel_stub_new_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_kernel_stub_new_adapter, ptr null }
-@ail_kernel_stub_answer_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_kernel_stub_answer_adapter, ptr null }
 @ail_list_sum_list_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_list_sum_list_adapter, ptr null }
 @ail_list_main_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_list_main_adapter, ptr null }
 @ail_prelude_float_eq_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_prelude_float_eq_adapter, ptr null }
@@ -34,84 +32,6 @@ declare i64 @llvm.fptosi.sat.i64.f64(double)
 @ail_prelude_float_ge_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_prelude_float_ge_adapter, ptr null }
 @ail_prelude_show__Int_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_prelude_show__Int_adapter, ptr null }
 @ail_prelude_print__Int_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_prelude_print__Int_adapter, ptr null }
-define ptr @ail_kernel_stub_new(i64 %arg_x) {
-entry:
-  %v1 = call ptr @ailang_rc_alloc(i64 16)
-  store i64 0, ptr %v1, align 8
-  %v2 = getelementptr inbounds i8, ptr %v1, i64 8
-  store i64 %arg_x, ptr %v2, align 8
-  ret ptr %v1
-}
-
-define ptr @ail_kernel_stub_new_adapter(ptr %_env, i64 %a0) {
-entry:
-  %r = call ptr @ail_kernel_stub_new(i64 %a0)
-  ret ptr %r
-}
-
-define i64 @ail_kernel_stub_answer() {
-entry:
-  ret i64 42
-}
-
-define i64 @ail_kernel_stub_answer_adapter(ptr %_env) {
-entry:
-  %r = call i64 @ail_kernel_stub_answer()
-  ret i64 %r
-}
-
-define void @drop_kernel_stub_StubT(ptr %p) {
-entry:
-  %is_null = icmp eq ptr %p, null
-  br i1 %is_null, label %ret, label %live
-live:
-  %tag = load i64, ptr %p, align 8
-  switch i64 %tag, label %dflt [
-    i64 0, label %arm_0
-  ]
-arm_0:
-  %a0 = getelementptr inbounds i8, ptr %p, i64 8
-  %v1 = load ptr, ptr %a0, align 8
-  call void @ailang_rc_dec(ptr %v1)
-  br label %join
-dflt:
-  unreachable
-join:
-  call void @ailang_rc_dec(ptr %p)
-  br label %ret
-ret:
-  ret void
-}
-
-define void @partial_drop_kernel_stub_StubT(ptr %p, i64 %mask) {
-entry:
-  %is_null = icmp eq ptr %p, null
-  br i1 %is_null, label %ret, label %live
-live:
-  %tag = load i64, ptr %p, align 8
-  switch i64 %tag, label %dflt [
-    i64 0, label %arm_0
-  ]
-arm_0:
-  %b0 = and i64 %mask, 1
-  %s1 = icmp ne i64 %b0, 0
-  br i1 %s1, label %after_0_0, label %do_0_0
-do_0_0:
-  %a2 = getelementptr inbounds i8, ptr %p, i64 8
-  %v3 = load ptr, ptr %a2, align 8
-  call void @ailang_rc_dec(ptr %v3)
-  br label %after_0_0
-after_0_0:
-  br label %join
-dflt:
-  unreachable
-join:
-  call void @ailang_rc_dec(ptr %p)
-  br label %ret
-ret:
-  ret void
-}
-
 define i64 @ail_list_sum_list(ptr %arg_xs) {
 entry:
   %v1 = load i64, ptr %arg_xs, align 8

crates/ail/tests/snapshots/max3.ll

@@ -22,8 +22,6 @@ declare ptr @ailang_str_clone(ptr)
 declare ptr @ailang_str_concat(ptr, ptr)
 declare i64 @llvm.fptosi.sat.i64.f64(double)
 
-@ail_kernel_stub_new_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_kernel_stub_new_adapter, ptr null }
-@ail_kernel_stub_answer_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_kernel_stub_answer_adapter, ptr null }
 @ail_max3_max_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_max3_max_adapter, ptr null }
 @ail_max3_max3_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_max3_max3_adapter, ptr null }
 @ail_max3_main_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_max3_main_adapter, ptr null }
@@ -37,84 +35,6 @@ declare i64 @llvm.fptosi.sat.i64.f64(double)
 @ail_prelude_gt__Int_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_prelude_gt__Int_adapter, ptr null }
 @ail_prelude_show__Int_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_prelude_show__Int_adapter, ptr null }
 @ail_prelude_print__Int_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_prelude_print__Int_adapter, ptr null }
-define ptr @ail_kernel_stub_new(i64 %arg_x) {
-entry:
-  %v1 = call ptr @ailang_rc_alloc(i64 16)
-  store i64 0, ptr %v1, align 8
-  %v2 = getelementptr inbounds i8, ptr %v1, i64 8
-  store i64 %arg_x, ptr %v2, align 8
-  ret ptr %v1
-}
-
-define ptr @ail_kernel_stub_new_adapter(ptr %_env, i64 %a0) {
-entry:
-  %r = call ptr @ail_kernel_stub_new(i64 %a0)
-  ret ptr %r
-}
-
-define i64 @ail_kernel_stub_answer() {
-entry:
-  ret i64 42
-}
-
-define i64 @ail_kernel_stub_answer_adapter(ptr %_env) {
-entry:
-  %r = call i64 @ail_kernel_stub_answer()
-  ret i64 %r
-}
-
-define void @drop_kernel_stub_StubT(ptr %p) {
-entry:
-  %is_null = icmp eq ptr %p, null
-  br i1 %is_null, label %ret, label %live
-live:
-  %tag = load i64, ptr %p, align 8
-  switch i64 %tag, label %dflt [
-    i64 0, label %arm_0
-  ]
-arm_0:
-  %a0 = getelementptr inbounds i8, ptr %p, i64 8
-  %v1 = load ptr, ptr %a0, align 8
-  call void @ailang_rc_dec(ptr %v1)
-  br label %join
-dflt:
-  unreachable
-join:
-  call void @ailang_rc_dec(ptr %p)
-  br label %ret
-ret:
-  ret void
-}
-
-define void @partial_drop_kernel_stub_StubT(ptr %p, i64 %mask) {
-entry:
-  %is_null = icmp eq ptr %p, null
-  br i1 %is_null, label %ret, label %live
-live:
-  %tag = load i64, ptr %p, align 8
-  switch i64 %tag, label %dflt [
-    i64 0, label %arm_0
-  ]
-arm_0:
-  %b0 = and i64 %mask, 1
-  %s1 = icmp ne i64 %b0, 0
-  br i1 %s1, label %after_0_0, label %do_0_0
-do_0_0:
-  %a2 = getelementptr inbounds i8, ptr %p, i64 8
-  %v3 = load ptr, ptr %a2, align 8
-  call void @ailang_rc_dec(ptr %v3)
-  br label %after_0_0
-after_0_0:
-  br label %join
-dflt:
-  unreachable
-join:
-  call void @ailang_rc_dec(ptr %p)
-  br label %ret
-ret:
-  ret void
-}
-
 define i64 @ail_max3_max(i64 %arg_a, i64 %arg_b) {
 entry:
   %v1 = call i1 @ail_prelude_gt__Int(i64 %arg_a, i64 %arg_b)

crates/ail/tests/snapshots/sum.ll

@@ -22,8 +22,6 @@ declare ptr @ailang_str_clone(ptr)
 declare ptr @ailang_str_concat(ptr, ptr)
 declare i64 @llvm.fptosi.sat.i64.f64(double)
 
-@ail_kernel_stub_new_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_kernel_stub_new_adapter, ptr null }
-@ail_kernel_stub_answer_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_kernel_stub_answer_adapter, ptr null }
 @ail_prelude_float_eq_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_prelude_float_eq_adapter, ptr null }
 @ail_prelude_float_ne_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_prelude_float_ne_adapter, ptr null }
 @ail_prelude_float_lt_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_prelude_float_lt_adapter, ptr null }
@@ -35,84 +33,6 @@ declare i64 @llvm.fptosi.sat.i64.f64(double)
 @ail_prelude_print__Int_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_prelude_print__Int_adapter, ptr null }
 @ail_sum_sum_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_sum_sum_adapter, ptr null }
 @ail_sum_main_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_sum_main_adapter, ptr null }
-define ptr @ail_kernel_stub_new(i64 %arg_x) {
-entry:
-  %v1 = call ptr @ailang_rc_alloc(i64 16)
-  store i64 0, ptr %v1, align 8
-  %v2 = getelementptr inbounds i8, ptr %v1, i64 8
-  store i64 %arg_x, ptr %v2, align 8
-  ret ptr %v1
-}
-
-define ptr @ail_kernel_stub_new_adapter(ptr %_env, i64 %a0) {
-entry:
-  %r = call ptr @ail_kernel_stub_new(i64 %a0)
-  ret ptr %r
-}
-
-define i64 @ail_kernel_stub_answer() {
-entry:
-  ret i64 42
-}
-
-define i64 @ail_kernel_stub_answer_adapter(ptr %_env) {
-entry:
-  %r = call i64 @ail_kernel_stub_answer()
-  ret i64 %r
-}
-
-define void @drop_kernel_stub_StubT(ptr %p) {
-entry:
-  %is_null = icmp eq ptr %p, null
-  br i1 %is_null, label %ret, label %live
-live:
-  %tag = load i64, ptr %p, align 8
-  switch i64 %tag, label %dflt [
-    i64 0, label %arm_0
-  ]
-arm_0:
-  %a0 = getelementptr inbounds i8, ptr %p, i64 8
-  %v1 = load ptr, ptr %a0, align 8
-  call void @ailang_rc_dec(ptr %v1)
-  br label %join
-dflt:
-  unreachable
-join:
-  call void @ailang_rc_dec(ptr %p)
-  br label %ret
-ret:
-  ret void
-}
-
-define void @partial_drop_kernel_stub_StubT(ptr %p, i64 %mask) {
-entry:
-  %is_null = icmp eq ptr %p, null
-  br i1 %is_null, label %ret, label %live
-live:
-  %tag = load i64, ptr %p, align 8
-  switch i64 %tag, label %dflt [
-    i64 0, label %arm_0
-  ]
-arm_0:
-  %b0 = and i64 %mask, 1
-  %s1 = icmp ne i64 %b0, 0
-  br i1 %s1, label %after_0_0, label %do_0_0
-do_0_0:
-  %a2 = getelementptr inbounds i8, ptr %p, i64 8
-  %v3 = load ptr, ptr %a2, align 8
-  call void @ailang_rc_dec(ptr %v3)
-  br label %after_0_0
-after_0_0:
-  br label %join
-dflt:
-  unreachable
-join:
-  call void @ailang_rc_dec(ptr %p)
-  br label %ret
-ret:
-  ret void
-}
-
 define i1 @ail_prelude_float_eq(double %arg_x, double %arg_y) alwaysinline {
 entry:
   %v1 = fcmp oeq double %arg_x, %arg_y

crates/ail/tests/snapshots/ws_main.ll

@@ -22,8 +22,6 @@ declare ptr @ailang_str_clone(ptr)
 declare ptr @ailang_str_concat(ptr, ptr)
 declare i64 @llvm.fptosi.sat.i64.f64(double)
 
-@ail_kernel_stub_new_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_kernel_stub_new_adapter, ptr null }
-@ail_kernel_stub_answer_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_kernel_stub_answer_adapter, ptr null }
 @ail_prelude_float_eq_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_prelude_float_eq_adapter, ptr null }
 @ail_prelude_float_ne_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_prelude_float_ne_adapter, ptr null }
 @ail_prelude_float_lt_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_prelude_float_lt_adapter, ptr null }
@@ -34,84 +32,6 @@ declare i64 @llvm.fptosi.sat.i64.f64(double)
 @ail_prelude_print__Int_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_prelude_print__Int_adapter, ptr null }
 @ail_ws_lib_add_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_ws_lib_add_adapter, ptr null }
 @ail_ws_main_main_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_ws_main_main_adapter, ptr null }
-define ptr @ail_kernel_stub_new(i64 %arg_x) {
-entry:
-  %v1 = call ptr @ailang_rc_alloc(i64 16)
-  store i64 0, ptr %v1, align 8
-  %v2 = getelementptr inbounds i8, ptr %v1, i64 8
-  store i64 %arg_x, ptr %v2, align 8
-  ret ptr %v1
-}
-
-define ptr @ail_kernel_stub_new_adapter(ptr %_env, i64 %a0) {
-entry:
-  %r = call ptr @ail_kernel_stub_new(i64 %a0)
-  ret ptr %r
-}
-
-define i64 @ail_kernel_stub_answer() {
-entry:
-  ret i64 42
-}
-
-define i64 @ail_kernel_stub_answer_adapter(ptr %_env) {
-entry:
-  %r = call i64 @ail_kernel_stub_answer()
-  ret i64 %r
-}
-
-define void @drop_kernel_stub_StubT(ptr %p) {
-entry:
-  %is_null = icmp eq ptr %p, null
-  br i1 %is_null, label %ret, label %live
-live:
-  %tag = load i64, ptr %p, align 8
-  switch i64 %tag, label %dflt [
-    i64 0, label %arm_0
-  ]
-arm_0:
-  %a0 = getelementptr inbounds i8, ptr %p, i64 8
-  %v1 = load ptr, ptr %a0, align 8
-  call void @ailang_rc_dec(ptr %v1)
-  br label %join
-dflt:
-  unreachable
-join:
-  call void @ailang_rc_dec(ptr %p)
-  br label %ret
-ret:
-  ret void
-}
-
-define void @partial_drop_kernel_stub_StubT(ptr %p, i64 %mask) {
-entry:
-  %is_null = icmp eq ptr %p, null
-  br i1 %is_null, label %ret, label %live
-live:
-  %tag = load i64, ptr %p, align 8
-  switch i64 %tag, label %dflt [
-    i64 0, label %arm_0
-  ]
-arm_0:
-  %b0 = and i64 %mask, 1
-  %s1 = icmp ne i64 %b0, 0
-  br i1 %s1, label %after_0_0, label %do_0_0
-do_0_0:
-  %a2 = getelementptr inbounds i8, ptr %p, i64 8
-  %v3 = load ptr, ptr %a2, align 8
-  call void @ailang_rc_dec(ptr %v3)
-  br label %after_0_0
-after_0_0:
-  br label %join
-dflt:
-  unreachable
-join:
-  call void @ailang_rc_dec(ptr %p)
-  br label %ret
-ret:
-  ret void
-}
-
 define i1 @ail_prelude_float_eq(double %arg_x, double %arg_y) alwaysinline {
 entry:
   %v1 = fcmp oeq double %arg_x, %arg_y

crates/ailang-check/src/lib.rs

@@ -1083,7 +1083,7 @@ pub fn prepare_workspace_for_check(ws: &Workspace) -> Workspace {
             .collect();
     // raw-buf.4: per-module set of *monomorphic* (non-`Forall`)
     // top-level fn names. A type-scoped call `T.f` to a monomorphic
-    // op (e.g. the `kernel_stub.StubT.new` produced by the Term::New
+    // op (e.g. the `raw_buf.RawBuf.new` produced by the Term::New
     // desugar) is normalised to the module-qualified `<home>.f` form
     // by `qualify_workspace_term` — codegen recognises that spelling
     // directly. Polymorphic type-scoped ops stay in the `T.f` form so
@@ -1701,11 +1701,11 @@ pub fn build_check_env(ws: &Workspace) -> Env {
     // (`modules.filter(|m| m.kernel)`) that drives
     // `implicit_imports` into `build_workspace`. The pre-pass
     // `qualify_workspace_types` freely produces qualifiers like
-    // `kernel_stub.StubT`; without this injection the type-
+    // `raw_buf.RawBuf`; without this injection the type-
-    // validity check at ~line 1968 would reject `kernel_stub` as
+    // validity check at ~line 1968 would reject `raw_buf` as
     // an unknown module prefix. Fieldtest F3 surfaced the gap
     // (the previous code force-injected only `prelude`, leaving
-    // `kernel_stub` and any future kernel-tier module unreachable
+    // `raw_buf` and any future kernel-tier module unreachable
     // from consumers). The production prelude carries
     // `kernel: true`, so the two halves are idempotent for it; the
     // `"prelude"` literal stays so unit-test workspaces that
@@ -1865,7 +1865,7 @@ fn check_in_workspace(
     // explicit `import` of the same name is idempotent via
     // `entry`. A module is not auto-imported into its own body.
     // Fieldtest F3 surfaced that the previous code force-injected
-    // only `prelude`, leaving `kernel_stub` and any future
+    // only `prelude`, leaving `raw_buf` and any future
     // kernel-tier module unreachable from consumers even though
     // the pre-pass freely produces such qualifiers.
     if m.name != "prelude" {
@@ -2782,8 +2782,8 @@ pub struct FreeFnCall {
     /// substitution was fully pinned.
     pub metas: Vec<Type>,
     /// The TypeDef scope the call resolved through, when it was
-    /// spelled type-scoped (`T.f`, prep.1) — `Some("StubT")` for
+    /// spelled type-scoped (`T.f`, prep.1) — `Some("RawBuf")` for
-    /// `StubT.peek`, `Some("RawBuf")` for `RawBuf.get`. `None` for a
+    /// `RawBuf.new`, `Some("RawBuf")` for `RawBuf.get`. `None` for a
     /// bare / dot-qualified / local resolution. raw-buf.3: drives the
     /// scope-qualified mono symbol `T_f__<elem>` so two types' ops
     /// of the same name never collide.
@@ -4615,7 +4615,7 @@ pub(crate) fn qualify_workspace_term(
             // `T.f` to a *monomorphic* op into the module-qualified
             // `<home>.f` form. The Term::New desugar emits
             // `(app T.new …)` for every type; for a cross-module
-            // monomorphic `new` (e.g. kernel_stub's StubT.new) nothing
+            // monomorphic `new` (e.g. raw_buf's RawBuf.new) nothing
             // downstream rewrites the `T.new` callee, so codegen would
             // hit `unknown variable`. Three carve-outs:
             //  - a same-module type (`own_local_types`) keeps `T.f` —

crates/ailang-check/src/mono.rs

@@ -366,9 +366,9 @@ fn poly_free_fn_names_for_module(
     // local def, not the imported poly fn. Adding the bare name here
     // 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
+    // a kernel-tier type-scoped op collided with a fixture-local
-    // monomorphic `peek`). The dot-qualified / type-scoped spellings
+    // monomorphic fn of the same bare name). The dot-qualified /
-    // are unambiguous and stay unconditional.
+    // type-scoped spellings are unambiguous and stay unconditional.
     let local_global_names: BTreeSet<String> = env
         .module_globals
         .get(mname)
@@ -558,8 +558,8 @@ pub fn mono_symbol_n(base: &str, types: &[Type]) -> String {
 }
 
 /// raw-buf.3: the symbol base for a free-fn mono target. A
-/// type-scoped op (`scope = Some("StubT")`, name `"peek"`) bases on
+/// type-scoped op (`scope = Some("RawBuf")`, name `"get"`) bases on
-/// `"StubT_peek"`, so `mono_symbol_n` mints `StubT_peek__Int`; a
+/// `"RawBuf_get"`, so `mono_symbol_n` mints `RawBuf_get__Int`; a
 /// bare free fn (`scope = None`) keeps its bare base.
 pub fn scoped_base(scope: &Option<String>, name: &str) -> String {
     match scope {
@@ -622,7 +622,7 @@ pub enum MonoTarget {
         /// Module in which the polymorphic source `Def::Fn` is declared;
         /// the synthesised mono `Def::Fn` is appended there.
         defining_module: String,
-        /// The TypeDef scope (`Some("StubT")`) when the call resolved
+        /// The TypeDef scope (`Some("RawBuf")`) when the call resolved
         /// type-scoped; `None` for a bare free fn. Part of the dedup
         /// key and the minted symbol base.
         scope: Option<String>,

crates/ailang-codegen/src/intercepts.rs

@@ -164,27 +164,6 @@ pub(crate) static INTERCEPTS: &[Intercept] = &[
         wants_alwaysinline: true,
         emit: emit_ne_int,
     },
-    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,
-    },
     // raw-buf.4: the 12 scope-qualified RawBuf ops. Symbols are
     // `RawBuf_{new,get,set,size}__{Int,Float,Bool}` (raw-buf.3
     // scope-qualified mono mangling). Slab layout:
@@ -552,44 +531,6 @@ pub(crate) fn emit_ne_int(emitter: &mut Emitter<'_>) -> Result<()> {
         .map(|_| ())
 }
 
-/// 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(())
-}
-
 // ---------------------------------------------------------------
 // raw-buf.4: RawBuf op emits over an `@ailang_rc_alloc` slab.
 // Slab layout `[ size:i64 @0 ][ elem_0 @8 ][ elem_1 @8+w ]…`. The
@@ -808,13 +749,12 @@ mod tests {
         &["lt__Int", "le__Int", "gt__Int", "ge__Int", "ne__Int"];
 
     /// Collect the mangled name of every `(intrinsic)` marker reachable
-    /// in the kernel-tier source modules (prelude + kernel_stub — the
+    /// 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_kernel_stub(),
             ailang_surface::parse_raw_buf(),
         ] {
             for def in &module.defs {
@@ -848,7 +788,7 @@ mod tests {
                         }
                     }
                     // Top-level intrinsic fn: name is already the symbol
-                    // (float_eq, answer, ...).
+                    // (float_eq, ...).
                     Def::Fn(f) if matches!(f.body, Term::Intrinsic) => {
                         markers.insert(f.name.clone());
                     }

crates/ailang-codegen/src/lib.rs

@@ -1109,9 +1109,11 @@ impl<'a> Emitter<'a> {
                     // drop instead: a single rc-dec on the slab pointer
                     // (primitive elements carry no recursive drops).
                     // This distinguishes RawBuf (intrinsic `new`) from
-                    // StubT (real-body `new` → generic ADT drop), where
+                    // an ordinary param_in user ADT (real-body `new` →
-                    // a param_in heuristic would misclassify StubT
+                    // generic ADT drop), where a param_in heuristic
-                    // (also param_in). A matching flat partial-drop is
+                    // would misclassify the user ADT (also param_in).
+                    // The intrinsic-`new` test is the load-bearing
+                    // signal, not param_in. A matching flat partial-drop is
                     // emitted for symbol-resolution parity with the
                     // generic path (no carve-out site can actually
                     // target it — the sole field is a primitive).

crates/ailang-core/src/workspace.rs

@@ -306,10 +306,9 @@ pub enum WorkspaceLoadError {
 
     /// 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
+    /// The current built-in set is `prelude` and `raw_buf` (the
-    /// stub is injected unconditionally in all builds as the
+    /// `raw_buf` base extension is injected unconditionally in all
-    /// ratifying fixture for the kernel-extension mechanism;
+    /// builds; future base extensions may add more).
-    /// 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.

crates/ailang-core/tests/design_schema_drift.rs

@@ -733,48 +733,10 @@ fn typedef_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"));
-
-    // raw-buf.3: the type-scoped polymorphic intrinsic ratifier op
-    // round-trips and is an `(intrinsic)` marker.
-    let peek = recovered.defs.iter().find_map(|d| match d {
-        Def::Fn(f) if f.name == "peek" => Some(f),
-        _ => None,
-    }).expect("kernel_stub ships the peek ratifier op (raw-buf.3)");
-    assert!(matches!(peek.body, Term::Intrinsic), "peek is an (intrinsic) marker");
-}
-
 /// raw-buf.4: pin the JSON byte-shape of the raw_buf kernel-tier
-/// base-extension module. Mirror of `kernel_stub_module_round_trips`.
+/// base-extension module. Exercises all three additive schema items
+/// in a single fixture (`Module.kernel = true`, one TypeDef with
+/// `param-in`, one ctor).
 #[test]
 fn raw_buf_module_round_trips() {
     let m = ailang_surface::parse_raw_buf();

crates/ailang-core/tests/workspace_kernel.rs

@@ -11,7 +11,7 @@
 //! (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
+//! built-in `prelude` and `raw_buf` are always loaded because
 //! the loader injects them programmatically; user kernel-tier
 //! modules need a path from the entry.
 

crates/ailang-core/tests/workspace_pin.rs

@@ -49,14 +49,12 @@ fn loads_example_workspace_happy_path() {
     assert_eq!(ws.entry, "ws_main");
     assert!(ws.modules.contains_key("ws_main"));
     assert!(ws.modules.contains_key("ws_lib"));
-    // the loader auto-injects three built-in kernel-tier modules
+    // the loader auto-injects two built-in kernel-tier modules
-    // (`prelude`, `kernel_stub` — see prep.3 of the
+    // (`prelude` and `raw_buf`, the first real-payload kernel
-    // kernel-extension-mechanics milestone — and `raw_buf`, the
+    // extension, raw-buf.4), so the count is the user's two modules
-    // first real-payload kernel extension, raw-buf.4), so the count
+    // plus those two.
-    // is the user's two modules plus those three.
+    assert_eq!(ws.modules.len(), 4);
-    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"));
 }
 

crates/ailang-kernel/src/kernel_stub/mod.rs

@@ -1,16 +0,0 @@
-//! Kernel-stub submodule — minimal ratifying fixture for the
-//! kernel-extension-mechanics milestone (prep.3). The Form-A text
-//! lives in the sibling `source.ail`.
-//!
-//! No domain content. Retired when the `raw-buf` milestone lands
-//! its real kernel-tier consumer (raw-buf.4); until then it stays
-//! as the ratifying-fixture anchor.
-
-/// Source-of-truth Form-A text for the stub kernel module. Parsed
-/// by `ailang_surface::parse_kernel_stub` (and round-trip-pinned by
-/// `kernel_stub_module_round_trips` in `design_schema_drift.rs`).
-///
-/// Ships a `(fn new ...)` def so consumers can spell `(new StubT 42)`
-/// (Term::New end-to-end, per prep.3 fieldtest F4) and an `answer`
-/// `(intrinsic)` fn whose `INTERCEPTS` entry the bijection test pins.
-pub const SOURCE: &str = include_str!("source.ail");

crates/ailang-kernel/src/kernel_stub/source.ail

@@ -1,20 +0,0 @@
-(module kernel_stub
-  (kernel)
-  (data StubT (vars a)
-    (ctor Stub a)
-    (param-in (a Int Float)))
-  (fn new
-    (doc "Construct StubT<Int> 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)))
-  (fn answer
-    (doc "Ratifies the intrinsic mechanism end-to-end: codegen intercept answer emits ret i64 42.")
-    (type (fn-type (params) (ret (con Int))))
-    (params)
-    (intrinsic))
-  (fn peek
-    (doc "Ratifies the type-scoped polymorphic intrinsic mechanism: StubT.peek is polymorphic over a (param-in {Int,Float}) and type-scoped to StubT. Codegen intercepts StubT_peek__Int / StubT_peek__Float emit a load of the Stub payload. Retires with the stub in raw-buf.5.")
-    (type (forall (vars a) (fn-type (params (borrow (con StubT a))) (ret a))))
-    (params s)
-    (intrinsic)))

crates/ailang-kernel/src/lib.rs

@@ -5,11 +5,9 @@
 //!
 //! 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
+//! hops live in `ailang-surface` (`parse_raw_buf`, …) 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;

crates/ailang-surface/src/lib.rs

@@ -37,7 +37,7 @@ pub mod parse;
 pub mod print;
 
 pub use loader::{
-    load_module, load_workspace, parse_kernel_stub, parse_prelude, parse_raw_buf, PRELUDE_AIL,
+    load_module, load_workspace, parse_prelude, parse_raw_buf, PRELUDE_AIL,
 };
 pub use parse::{parse, parse_term, ParseError};
 pub use print::{print, term_to_form_a, type_to_form_a};

crates/ailang-surface/src/loader.rs

@@ -42,22 +42,8 @@ pub fn parse_prelude() -> Module {
     crate::parse(PRELUDE_AIL).expect("examples/prelude.ail must parse as a Module")
 }
 
-/// 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")
-}
-
 /// raw-buf.4: parse the embedded raw_buf kernel-tier base-extension
-/// module bytes into a `Module`. Mirror of [`parse_kernel_stub`].
+/// module bytes into a `Module`. Mirror of [`parse_prelude`].
 ///
 /// Source-of-truth: `ailang_kernel::RAW_BUF_AIL`. Declares the
 /// `RawBuf` TypeDef with `param-in (a Int Float Bool)` and the four
@@ -134,17 +120,6 @@ pub fn load_workspace(entry: &Path) -> Result<Workspace, WorkspaceLoadError> {
     }
     modules.insert("prelude".to_string(), parse_prelude());
 
-    // 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());
-
     // parse_raw_buf() injects the raw_buf kernel-tier base-extension
     // module — RawBuf, the first real-payload kernel extension. Its
     // source carries `(kernel)`, so the kernel-flag filter below

design/INDEX.md

@@ -109,4 +109,4 @@ is the default.
 | authoring-surface | onboarding / evolves | design/models/0001-authoring-surface.md |
 | prose-projection  | onboarding / evolves | design/models/0006-prose-projection.md |
 | pipeline          | onboarding / evolves | design/models/0003-pipeline.md |
-| 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 |
+| 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 |

design/models/0007-kernel-extensions.md

@@ -4,9 +4,10 @@
 (`kernel-extension-mechanics`; iterations prep.1, prep.2, prep.3
 landed). 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 module
+`param-in` — are shipped and ratified by the `raw_buf` base
-(`crates/ailang-kernel/src/kernel_stub/`). The base-extension and library-
+extension (`crates/ailang-kernel/src/raw_buf/`). The base-extension
-extension milestones (`raw-buf`, `series`) are pending. This
+milestone (`raw-buf`) has shipped; the library-extension milestone
+(`series`) is pending. This
 whitepaper describes the design as a coherent whole; the
 per-milestone specs in `docs/specs/` carry the implementation-
 level detail. Sections describing the now-shipped mechanisms read
@@ -220,7 +221,7 @@ generalised from a hardcoded single-name path (prelude only,
 pre-prep.3) to a flag-driven multi-module mechanism (since
 prep.3 of `kernel-extension-mechanics`). The loader at
 `crates/ailang-surface/src/loader.rs::load_workspace` injects
-`parse_prelude()` and `parse_kernel_stub()` programmatically,
+`parse_prelude()` and `parse_raw_buf()` programmatically,
 then derives the implicit-imports list from
 `modules.values().filter(|m| m.kernel)`. Every module in the
 workspace's modules map that carries `kernel: true` enters the
@@ -231,8 +232,8 @@ Prelude carries `kernel: true` in `examples/prelude.ail`. Its 12
 free fns (see `examples/prelude.ail:85-148`) remain callable bare
 in every consumer module — ratified by
 `crates/ail/tests/prelude_free_fns.rs` across the code-path
-migration. The ratifying stub kernel module
+migration. The `raw_buf` base-extension kernel module
-(`crates/ailang-kernel/src/kernel_stub/`) and any future kernel-tier
+(`crates/ailang-kernel/src/raw_buf/`) and any future kernel-tier
 consumers (Series, Matrix) auto-import through the same filter.
 
 Class-method dispatch (a separate mechanism — see

examples/fieldtest/kem_3_stub_consumer.ail

@@ -1,51 +0,0 @@
-; Fieldtest kem.3 (Axis 3, kernel-tier modules + auto-import) — a
-; consumer that references `kernel_stub`'s TypeDef without an
-; `(import kernel_stub)` declaration. Per spec § "Iteration prep.3":
-;
-;   - The module's top-level defs are accessible bare in every other
-;     module of the workspace, with no `(import ...)` declaration
-;     required.
-;   - The module's types are accessible bare in type position.
-;
-; Outcome: `ail check` fails with
-;
-;     [unknown-module] unwrap_int: unknown module prefix
-;     `kernel_stub` in qualified reference
-;
-; The workspace pre-pass rewrites bare `StubT` to qualified
-; `kernel_stub.StubT` (correct per prep.1's `qualify_workspace_term`);
-; but the resolver does not accept `kernel_stub` as a valid module
-; prefix because the consumer has no explicit `(import kernel_stub)`.
-; That is, the qualification pre-pass and the auto-import scope are
-; not cooperating — the auto-import does NOT add the kernel module
-; to the resolver's known-prefixes set.
-;
-; Workarounds attempted:
-;
-;   - Adding `(import kernel_stub)`: fails earlier with
-;     [module-not-found] expected at <sibling>/kernel_stub.ail.json
-;     — the kernel stub has no on-disk file, it is built into the
-;     compiler binary.
-;   - Bare `StubT` everywhere: same outcome as above (the pre-pass
-;     qualifies it before the resolver sees it).
-;
-; Prelude's bare fns (`print`, `lt`, etc.) DO work — prelude_free_fns
-; ratifies that. So the bug is specifically about TypeDefs in type
-; position for kernel-tier modules other than prelude. The shipped
-; kernel_stub TypeDef appears unreachable from any consumer in
-; practice.
-
-(module kem_3_stub_consumer
-
-  (fn unwrap_int
-    (doc "Project the Int back out of a StubT<Int>. Bare `StubT` in the type slot exercises the kernel-tier auto-import — and currently fails to resolve.")
-    (type (fn-type (params (con StubT (con Int))) (ret (con Int))))
-    (params s)
-    (body (match s (case (pat-ctor Stub x) x))))
-
-  (fn main
-    (type (fn-type (params) (ret (con Unit)) (effects IO)))
-    (params)
-    (body
-      (let s (term-ctor StubT Stub 7)
-        (seq (app print (app unwrap_int s)) (do io/print_str "\n"))))))

examples/fieldtest/kem_4_paramin_box_green.ail

@@ -6,7 +6,7 @@
 ; Per spec § "Iteration prep.3 — Kernel-tier modules + param-in":
 ; the param-in restriction is a generic, data-driven check; nothing
 ; in the checker mentions any specific extension. So a user TypeDef
-; can declare it just as the stub kernel_stub.StubT does.
+; can declare it just as the raw_buf.RawBuf base extension does.
 
 (module kem_4_paramin_box_green
 

examples/kernel_answer.ail

@@ -1,6 +0,0 @@
-(module kernel_answer
-  (fn main
-    (doc "E2E ratifier: prints the intrinsic answer (42).")
-    (type (fn-type (params) (ret (con Unit)) (effects IO)))
-    (params)
-    (body (app print (app kernel_stub.answer)))))

examples/new_stubt_smoke.ail

@@ -1,13 +0,0 @@
-(module new_stubt_smoke
-  (fn unwrap_int
-    (doc "Project the Int back out of a StubT<Int>.")
-    (type (fn-type (params (con StubT (con Int))) (ret (con Int))))
-    (params s)
-    (body (match s (case (pat-ctor Stub x) x))))
-  (fn main
-    (doc "raw-buf.4 desugar ratifier: (new StubT 42) desugars to (app StubT.new 42), builds, and prints 42.")
-    (type (fn-type (params) (ret (con Unit)) (effects IO)))
-    (params)
-    (body
-      (let s (new StubT 42)
-        (app print (app unwrap_int s))))))

examples/peek_mono_pin_smoke.ail

@@ -1,9 +0,0 @@
-(module peek_mono_pin_smoke
-  (fn at_int
-    (type (fn-type (params (own (con StubT (con Int)))) (ret (con Int))))
-    (params s)
-    (body (app StubT.peek s)))
-  (fn at_float
-    (type (fn-type (params (own (con StubT (con Float)))) (ret (con Float))))
-    (params s)
-    (body (app StubT.peek s))))