iter intrinsic-bodies.1-mechanism (DONE 8/8): Term::Intrinsic leaf + cross-crate wiring (refs #9)

First iteration of the intrinsic-bodies milestone. Introduces the
Form-A `(intrinsic)` body marker as a new leaf AST term and wires it
through surface, checker, codegen, and a kernel_stub ratifier. The
prelude migration + hard-lockstep pin + dead-path removal are .2.

What landed (8 tasks):

  Task 1 — Term::Intrinsic unit variant (ast.rs), tag "t":"intrinsic"
    via the enum's rename_all=lowercase. Additive: no existing fixture
    carries it, hashes bit-identical. In-core exhaustive-match arms
    (canonical/hash/visit/pretty/desugar/workspace) added as leaves.
  Task 2 — surface parse + print: (intrinsic) as a fn body-slot clause
    and a lambda positional body, mapped to/from Term::Intrinsic.
  Task 3 — cross-crate walker sweep (check/codegen/prose/ail-main):
    leaf no-op/identity arms at every no-wildcard Term match the
    compiler flagged.
  Task 4 — checker: new Env.current_module_kernel_tier flag (m.kernel
    || m.name=="prelude"), set alongside current_module. A def whose
    body is intrinsic (top-level fn OR instance-method lambda, via the
    shared is_intrinsic_body helper) is checked signature-only; an
    intrinsic body outside kernel-tier/prelude is rejected with
    intrinsic-outside-kernel-tier.
  Task 5 — codegen: an intrinsic-bodied fn routes through the existing
    try_emit_primitive_instance_body / intercepts::lookup path; if no
    intercept fired it is an internal error, never a lower_term
    fallthrough. lower_term and the synth walker get Term::Intrinsic
    internal-error arms (an intrinsic body reaching either is an
    escape bug).
  Task 6 — answer intercept (ret i64 42) registered in INTERCEPTS;
    the `answer : () -> Int` intrinsic added to STUB_AIL;
    examples/kernel_intrinsic_smoke.ail added so schema_coverage
    observes Term::Intrinsic in the examples/ corpus.
  Task 7 — E2E ratifier: examples/kernel_answer.ail calls
    kernel_stub.answer and prints 42; answer_intrinsic_builds_and_runs_printing_42
    asserts it end-to-end (source → native).
  Task 8 — design/contracts/0002-data-model.md gains the
    { "t": "intrinsic" } Term entry + fn/lam prose; form_a.md grammar
    note updated.

Verification:
  cargo test --workspace → 669 passed, 0 failed (baseline 667 +2:
    intrinsic_in_user_module_is_rejected, answer_intrinsic_builds_and_runs_printing_42).
  bench/check.py + bench/compile_check.py → 0 regressed.
  Reject E2E (subprocess ail check --json, exit 1, code
    intrinsic-outside-kernel-tier) GREEN.
  Round-trip + hash pins GREEN — Term::Intrinsic is additive, no
    existing fixture carries it, no hash moved.

Three implementation completions beyond the plan (all behaviour-
preserving, surfaced during execution):

1. The signature-only skip had to apply at the mono pass's two
   synth-on-body re-entry sites (collect_mono_targets,
   collect_residuals_ordered), not only check_fn — else an intrinsic
   body hits synth's Term::Intrinsic internal-error guard. Repaired by
   extracting the shared crate::is_intrinsic_body helper and applying
   it at all three synth-on-body paths. Not a representation surprise:
   the same signature-only treatment, more call sites.

2. The compiler-enumerated exhaustive-match set was broader than the
   plan's named grep set (the plan anticipated this and made the sweep
   compile-driven). Extra leaf arms in core desugar/workspace, check
   reuse-as + qualify_workspace_term, codegen synth_with_extras,
   ail/src/main.rs, and four test targets.

3. Fixture corrections: emit_answer needed the body-close
   (block terminator) the plan snippet omitted; kernel_answer.ail's
   main is (ret Unit)(effects IO) using (app print ...) since
   io/print_int does not exist (the plan flagged this for the
   implementer to resolve against real effect-op names).

IR snapshots (hello/sum/list/max3/ws_main.ll) refreshed: purely
additive @ail_kernel_stub_answer fn+adapter+closure, emitted into
every workspace exactly as the pre-existing @ail_kernel_stub_new
already was (kernel_stub is auto-injected; confirmed new was present
in the pre-iter hello.ll baseline). No user-fn IR changed.

The .2 iteration migrates the 18 prelude dummy bodies to (intrinsic),
upgrades registry_contains_all_legacy_arms to a source<->registry
bijection pin, and removes the dead body-lowering path.

crates/ail/src/main.rs

@@ -1585,6 +1585,7 @@ fn walk_term(
                 }
             }
         }
+        Term::Intrinsic => {}
     }
 }
 
@@ -2956,6 +2957,7 @@ fn rewrite_def(
                     }
                 }
             }
+            Term::Intrinsic => {}
         }
     }
 

crates/ail/tests/codegen_import_map_fallback_pin.rs

@@ -106,6 +106,7 @@ fn synthesised_print_uses_user_module_show_via_fallback() {
                 ailang_core::ast::NewArg::Type(_) => false,
             }),
             Term::Lit { .. } => false,
+            Term::Intrinsic => false,
         }
     }
 

crates/ail/tests/e2e.rs

@@ -82,6 +82,19 @@ 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");
+}
+
 #[test]
 fn loop_recur_sum_to_runs_to_value() {
     let stdout = build_and_run("loop_sum_to_run.ail");
@@ -1259,6 +1272,53 @@ fn check_json_unbound_var() {
     );
 }
 
+/// Property protected: an `(intrinsic)` body is rejected in a
+/// non-kernel-tier user module. `check_fn`'s honesty-rule guard fires
+/// `intrinsic-outside-kernel-tier` (Error) when a module that is
+/// neither kernel-tier nor the prelude declares a compiler-supplied
+/// body. Without the guard, user code could claim the compiler
+/// supplies a body it does not. The reject rides the subprocess
+/// `ail check --json` path so the diagnostic code is asserted as the
+/// machine consumer would see it; a temp file keeps the reject case
+/// out of the round-trip corpus.
+#[test]
+fn intrinsic_in_user_module_is_rejected() {
+    let tmp = std::env::temp_dir().join(format!(
+        "ailang_intrinsic_reject_{}",
+        std::process::id()
+    ));
+    std::fs::create_dir_all(&tmp).unwrap();
+    let src = tmp.join("intr_user.ail");
+    std::fs::write(
+        &src,
+        "(module intr_user (fn f (type (fn-type (params (con Int)) (ret (con Int)))) (params n) (intrinsic)))",
+    )
+    .unwrap();
+
+    let output = Command::new(ail_bin())
+        .args(["check", src.to_str().unwrap(), "--json"])
+        .output()
+        .expect("ail check --json failed to run");
+
+    let code = output.status.code().expect("process terminated by signal");
+    assert_eq!(
+        code, 1,
+        "expected exit 1, stderr: {}",
+        String::from_utf8_lossy(&output.stderr)
+    );
+    let stdout = String::from_utf8(output.stdout).expect("stdout utf8");
+    let diags: serde_json::Value =
+        serde_json::from_str(stdout.trim()).expect("stdout must be valid JSON");
+    let arr = diags.as_array().expect("diagnostics must be a JSON array");
+    assert!(
+        arr.iter().any(|d| {
+            d.get("severity").and_then(|v| v.as_str()) == Some("error")
+                && d.get("code").and_then(|v| v.as_str()) == Some("intrinsic-outside-kernel-tier")
+        }),
+        "expected an error with code intrinsic-outside-kernel-tier; got: {stdout}"
+    );
+}
+
 /// literal patterns at top level and inside Ctor
 /// sub-patterns. Property protected: the 16a desugar pass rewrites
 /// every `Pattern::Lit` to a `Term::If` against the scrutinee/field

crates/ail/tests/snapshots/hello.ll

@@ -26,6 +26,7 @@ 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 }
@@ -61,6 +62,17 @@ entry:
   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

crates/ail/tests/snapshots/list.ll

@@ -23,6 +23,7 @@ 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 }
@@ -48,6 +49,17 @@ entry:
   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

crates/ail/tests/snapshots/max3.ll

@@ -23,6 +23,7 @@ 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 }
@@ -51,6 +52,17 @@ entry:
   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

crates/ail/tests/snapshots/sum.ll

@@ -23,6 +23,7 @@ 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 }
@@ -49,6 +50,17 @@ entry:
   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

crates/ail/tests/snapshots/ws_main.ll

@@ -23,6 +23,7 @@ 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 }
@@ -48,6 +49,17 @@ entry:
   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

crates/ailang-check/src/lib.rs

@@ -270,6 +270,7 @@ pub(crate) fn substitute_rigids_in_term(t: &Term, mapping: &BTreeMap<String, Typ
                 })
                 .collect(),
         },
+        Term::Intrinsic => t.clone(),
     }
 }
 
@@ -755,6 +756,14 @@ pub enum CheckError {
         allowed: Vec<String>,
     },
 
+    /// An `(intrinsic)` body appears in a module that is neither
+    /// kernel-tier nor the prelude. User code may not declare a body as
+    /// compiler-supplied — the honesty-rule guard at the workspace
+    /// boundary (design/contracts/0007-honesty-rule.md).
+    /// Code: `intrinsic-outside-kernel-tier`.
+    #[error("def `{def}` in module `{module}` uses an `(intrinsic)` body, which is allowed only in a kernel-tier module or the prelude")]
+    IntrinsicOutsideKernelTier { def: String, module: String },
+
     /// an internal invariant in the typechecker / mono pass
     /// was violated — surfaced as an error so callers can propagate
     /// rather than abort, but in well-formed inputs (typecheck has
@@ -815,6 +824,7 @@ impl CheckError {
             CheckError::NewTypeNotConstructible { .. } => "new-type-not-constructible",
             CheckError::NewArgKindMismatch { .. } => "new-arg-kind-mismatch",
             CheckError::ParamNotInRestrictedSet { .. } => "param-not-in-restricted-set",
+            CheckError::IntrinsicOutsideKernelTier { .. } => "intrinsic-outside-kernel-tier",
             CheckError::Internal(_) => "internal",
         }
     }
@@ -1844,6 +1854,7 @@ fn check_in_workspace(
     }
     env.imports = import_map;
     env.current_module = m.name.clone();
+    env.current_module_kernel_tier = m.kernel || m.name == "prelude";
 
     for def in &m.defs {
         match check_def(def, &env, out_warnings) {
@@ -2092,6 +2103,20 @@ fn check_type_well_formed(t: &Type, env: &Env) -> Result<()> {
     }
 }
 
+/// `true` when `f`'s body is an `(intrinsic)` marker: either the body
+/// is `Term::Intrinsic` directly (a top-level intrinsic fn) or it is a
+/// `Term::Lam` whose inner body is `Term::Intrinsic` (a synthesised
+/// instance method). Such a body is signature-only — the typechecker
+/// validates the signature and skips body inference, and the mono pass
+/// collects no targets from it. Shared by `check_fn` and the mono
+/// pass's `synth`-re-entry sites (`mono::collect_mono_targets`,
+/// `mono::collect_residuals_ordered`) so every synth-on-body path
+/// applies the same skip.
+pub(crate) fn is_intrinsic_body(f: &FnDef) -> bool {
+    matches!(f.body, Term::Intrinsic)
+        || matches!(&f.body, Term::Lam { body, .. } if matches!(**body, Term::Intrinsic))
+}
+
 fn check_fn(f: &FnDef, env: &Env, out_warnings: &mut Vec<Diagnostic>) -> Result<()> {
     // Peel an outer Forall (Iter 12a). The vars become rigid in the
     // inner env so they pass `check_type_well_formed` and unify only
@@ -2138,6 +2163,23 @@ fn check_fn(f: &FnDef, env: &Env, out_warnings: &mut Vec<Diagnostic>) -> Result<
     }
     check_type_well_formed(&ret_ty, &env)?;
 
+    // An `(intrinsic)` body is signature-only: the signature is already
+    // validated above; codegen supplies the implementation via the
+    // intercept registry. The body is `Term::Intrinsic` directly (a
+    // top-level intrinsic fn) or a `Term::Lam` whose inner body is
+    // `Term::Intrinsic` (a synthesised instance method). Skip body
+    // inference, but first gate the honesty rule: an intrinsic body is
+    // legal only in a kernel-tier module or the prelude.
+    if is_intrinsic_body(f) {
+        if !env.current_module_kernel_tier {
+            return Err(CheckError::IntrinsicOutsideKernelTier {
+                def: f.name.clone(),
+                module: env.current_module.clone(),
+            });
+        }
+        return Ok(());
+    }
+
     // Embedding-ABI gate (M1 scalars / M2 ctx / M3 record): an
     // `(export …)` fn is the C call boundary. Its signature must be
     // C-ABI-permitted — `Int`/`Float`, or a single-constructor
@@ -3000,6 +3042,7 @@ pub fn verify_tail_positions(t: &Term, is_tail: bool) -> Result<()> {
             }
             Ok(())
         }
+        Term::Intrinsic => Ok(()),
     }
 }
 
@@ -3105,6 +3148,7 @@ fn verify_loop_body(t: &Term, in_loop_tail: bool) -> Result<()> {
             }
             Ok(())
         }
+        Term::Intrinsic => Ok(()),
     }
 }
 
@@ -4073,6 +4117,7 @@ pub(crate) fn synth(
                         Term::Loop { .. } => "loop",
                         Term::Recur { .. } => "recur",
                         Term::New { .. } => "new",
+                        Term::Intrinsic => "intrinsic",
                         Term::Ctor { .. } | Term::Lam { .. } => unreachable!(),
                     };
                     return Err(CheckError::ReuseAsNonAllocatingBody {
@@ -4331,6 +4376,14 @@ pub(crate) fn synth(
             }
             Ok(substitute_rigids(&ret_ty, &mapping))
         }
+        // An intrinsic body is signature-only: the per-fn body check
+        // (`check_fn`) validates the signature from `f.ty` and never
+        // calls `synth` on a `Term::Intrinsic`. Reaching here means the
+        // skip-guard was bypassed — a checker-internal invariant break.
+        Term::Intrinsic => unreachable!(
+            "synth reached Term::Intrinsic; an intrinsic body is signature-only and must be \
+             skipped by check_fn before synth runs"
+        ),
     }
 }
 
@@ -4614,6 +4667,7 @@ pub(crate) fn qualify_workspace_term(
                 }
             }
         }
+        Term::Intrinsic => {}
     }
 }
 
@@ -4828,6 +4882,11 @@ pub struct Env {
     /// treat self-references (module name == own name) as local globals,
     /// without touching the `imports` channel.
     pub current_module: String,
+    /// `true` when the currently checked module is kernel-tier
+    /// (`module.kernel`) or the prelude. An `(intrinsic)` body is legal
+    /// only here; the per-fn body check reads this to gate
+    /// `IntrinsicOutsideKernelTier`. Set alongside `current_module`.
+    pub current_module_kernel_tier: bool,
     /// Rigid type vars in scope (Iter 12a). Populated by `check_fn` when
     /// it peels an outer `Forall` from the def's type. Inside the body,
     /// these names are legal as `Type::Var { name }` and unify only

crates/ailang-check/src/lift.rs

@@ -689,6 +689,7 @@ impl<'a> Lifter<'a> {
                     args: new_args?,
                 })
             }
+            Term::Intrinsic => Ok(t.clone()),
         }
     }
 
@@ -780,6 +781,7 @@ fn contains_any_letrec(m: &Module) -> bool {
                 NewArg::Value(v) => term_has_letrec(v),
                 NewArg::Type(_) => false,
             }),
+            Term::Intrinsic => false,
         }
     }
     for def in &m.defs {

crates/ailang-check/src/linearity.rs

@@ -626,6 +626,7 @@ impl<'a> Checker<'a> {
                     }
                 }
             }
+            Term::Intrinsic => {}
         }
     }
 
@@ -813,6 +814,7 @@ fn make_reuse_as_source_not_bare_var(def: &str, source: &Term, body: &Term) -> D
         Term::Loop { .. } => "loop",
         Term::Recur { .. } => "recur",
         Term::New { .. } => "new",
+        Term::Intrinsic => "intrinsic",
     };
     let replacement = term_to_form_a(body);
     Diagnostic::error(
@@ -974,6 +976,7 @@ fn any_sub_binder_consumed_for(
             NewArg::Value(v) => any_sub_binder_consumed_for(v, pname, uniq, def_name, ctors),
             NewArg::Type(_) => false,
         }),
+        Term::Intrinsic => false,
     }
 }
 
@@ -1111,6 +1114,7 @@ fn ctor_uses_any_binder(t: &Term, binders: &[String]) -> bool {
             NewArg::Value(v) => ctor_uses_any_binder(v, binders),
             NewArg::Type(_) => false,
         }),
+        Term::Intrinsic => false,
     }
 }
 
@@ -1165,6 +1169,7 @@ fn term_mentions_any_binder(t: &Term, binders: &[String]) -> bool {
             NewArg::Value(v) => term_mentions_any_binder(v, binders),
             NewArg::Type(_) => false,
         }),
+        Term::Intrinsic => false,
     }
 }
 

crates/ailang-check/src/mono.rs

@@ -692,6 +692,13 @@ pub fn collect_mono_targets(
     module_name: &str,
     env: &crate::Env,
 ) -> Result<Vec<MonoTarget>> {
+    // An `(intrinsic)` body is signature-only — codegen supplies it via
+    // the intercept registry, so it carries no mono targets. Skip the
+    // synth re-entry (which would hit synth's `Term::Intrinsic`
+    // unreachable guard), matching `check_fn`'s body-check skip.
+    if crate::is_intrinsic_body(f) {
+        return Ok(Vec::new());
+    }
     // Build the per-def env exactly as `check_fn` does — install
     // rigid vars, set the current module, etc. This mirrors
     // `crate::check_fn` minus the diagnostic emission.
@@ -1289,6 +1296,7 @@ fn rewrite_mono_calls(
             }
         }
         Term::Lit { .. } => {}
+        Term::Intrinsic => {}
     }
 }
 
@@ -1347,6 +1355,10 @@ pub(crate) fn collect_residuals_ordered(
     poly_free_fns: &BTreeSet<String>,
     poly_free_fn_ccounts: &BTreeMap<String, usize>,
 ) -> Result<Vec<Option<MonoTarget>>> {
+    // Intrinsic bodies carry no mono slots — see `collect_mono_targets`.
+    if crate::is_intrinsic_body(f) {
+        return Ok(Vec::new());
+    }
     let (rigids, inner_ty): (Vec<String>, Type) = match &f.ty {
         Type::Forall { vars, constraints: _, body } => (vars.clone(), (**body).clone()),
         other => (vec![], other.clone()),
@@ -1671,6 +1683,7 @@ fn interleave_slots(
             }
         }
         Term::Lit { .. } => {}
+        Term::Intrinsic => {}
     }
 }
 

crates/ailang-check/src/pre_desugar_validation.rs

@@ -144,6 +144,7 @@ fn walk_term(t: &Term) -> Result<(), CheckError> {
             }
             Ok(())
         }
+        Term::Intrinsic => Ok(()),
     }
 }
 

crates/ailang-check/src/reuse_shape.rs

@@ -278,6 +278,7 @@ impl<'a> Checker<'a> {
                     }
                 }
             }
+            Term::Intrinsic => {}
         }
     }
 

crates/ailang-check/src/uniqueness.rs

@@ -358,6 +358,7 @@ impl<'a> Walker<'a> {
                     }
                 }
             }
+            Term::Intrinsic => {}
         }
     }
 

crates/ailang-codegen/src/escape.rs

@@ -213,6 +213,7 @@ fn walk(t: &Term, out: &mut NonEscapeSet) {
             }
         }
         Term::Lit { .. } | Term::Var { .. } => {}
+        Term::Intrinsic => {}
     }
 }
 
@@ -420,6 +421,7 @@ fn escapes(t: &Term, tainted: &BTreeSet<String>, in_tail: bool) -> bool {
             }
             false
         }
+        Term::Intrinsic => false,
     }
 }
 
@@ -552,6 +554,7 @@ fn collect_free_vars(t: &Term, bound: &mut BTreeSet<String>, out: &mut BTreeSet<
                 }
             }
         }
+        Term::Intrinsic => {}
     }
 }
 

crates/ailang-codegen/src/intercepts.rs

@@ -164,6 +164,13 @@ 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,
+    },
 ];
 
 pub(crate) fn lookup(name: &str) -> Option<&'static Intercept> {
@@ -440,6 +447,17 @@ 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(())
+}
+
 #[cfg(test)]
 mod tests {
     use super::lookup;

crates/ailang-codegen/src/lambda.rs

@@ -502,6 +502,7 @@ impl<'a> Emitter<'a> {
                     }
                 }
             }
+            Term::Intrinsic => {}
         }
     }
 

crates/ailang-codegen/src/lib.rs

@@ -1320,6 +1320,21 @@ impl<'a> Emitter<'a> {
         let body_was_intercepted =
             self.try_emit_primitive_instance_body(&f.name, &llvm_param_tys, &llvm_ret)?;
 
+        // An `(intrinsic)` body is supplied entirely by the intercept
+        // registry. `try_emit_primitive_instance_body` already consults
+        // `intercepts::lookup(&f.name)`; if it fired, the body is fully
+        // emitted. If it did NOT fire, the intrinsic has no registered
+        // implementation — surface that as an internal error rather than
+        // falling through to `lower_term`, which cannot lower a
+        // `Term::Intrinsic` (it is signature-only, not an expression).
+        if !body_was_intercepted && matches!(f.body, Term::Intrinsic) {
+            return Err(CodegenError::Internal(format!(
+                "intrinsic fn `{}` has no registered intercept; an `(intrinsic)` body must \
+                 resolve through the intercept registry",
+                f.name
+            )));
+        }
+
         if !body_was_intercepted {
             let (val, val_ty) = self.lower_term(&f.body)?;
         if !self.block_terminated {
@@ -2076,6 +2091,11 @@ impl<'a> Emitter<'a> {
                 "Term::New requires the type's `new` def to be desugared first; \
                  codegen does not yet support Term::New directly — milestone raw-buf".into(),
             )),
+            Term::Intrinsic => Err(CodegenError::Internal(
+                "Term::Intrinsic must be consumed by the intercept route in fn-body \
+                 emission, not lowered as an expression; reaching lower_term means an \
+                 intrinsic body escaped its definition slot".into(),
+            )),
         }
     }
 
@@ -3273,6 +3293,11 @@ impl<'a> Emitter<'a> {
                 "Term::New cannot be synthed at codegen — must be desugared first; \
                  codegen support lands in the raw-buf milestone".into(),
             )),
+            Term::Intrinsic => Err(CodegenError::Internal(
+                "Term::Intrinsic cannot be synthed at codegen — an intrinsic body is \
+                 signature-only and routed through the intercept registry, never an expression"
+                    .into(),
+            )),
         }
     }
 }

crates/ailang-core/specs/form_a.md

@@ -297,6 +297,7 @@ Parenthesised forms:
 (loop (NAME TYPE INIT)* BODY-TERM+)     ; strict iteration block (loop-recur)
 (recur ARG*)                            ; re-enter enclosing loop (loop-recur)
 (new TYPE-NAME ARG+)                    ; functional construction (kernel-extension prep.2)
+(intrinsic)                             ; compiler-supplied body (kernel-tier only; fills a fn/lam body slot)
 ```
 
 Notes:
@@ -337,6 +338,12 @@ Notes:
   `new-type-not-constructible` (T's home module has no `new` def),
   `new-arg-kind-mismatch` (arg's kind disagrees with the sig at that
   position). Codegen lands in the raw-buf milestone.
+- `(intrinsic)` fills the single body slot of a `fn` def (in place of
+  `(body TERM)`) or a `lam`. It marks the definition as
+  compiler-supplied: the typechecker validates only the signature and
+  codegen routes the body through the intercept registry. It is legal
+  only in a `(kernel)`-tier module or the prelude — elsewhere it is
+  rejected with `intrinsic-outside-kernel-tier`.
 
 ## Patterns
 

crates/ailang-core/src/ast.rs

@@ -604,6 +604,18 @@ pub enum Term {
         type_name: String,
         args: Vec<NewArg>,
     },
+    /// The body of a compiler-supplied ("intrinsic") definition. Legal
+    /// only as the body of a `FnDef` or a `Term::Lam`, and only in a
+    /// `(kernel)`-tier module or the prelude (enforced at typecheck,
+    /// `IntrinsicOutsideKernelTier`). Never reduces to a value: codegen
+    /// consumes it via `intercepts::lookup` on the def's mangled name;
+    /// the typechecker treats a def with this body as signature-only.
+    /// A def is intrinsic iff `matches!(body, Term::Intrinsic)`. Additive
+    /// `"t":"intrinsic"` tag (unit variant via the enum's
+    /// `rename_all = "lowercase"`); pre-existing fixtures hash
+    /// bit-identically — none carry the tag. Precedent: `Term::Recur`
+    /// (a non-reducing control-transfer leaf).
+    Intrinsic,
 }
 
 /// One positional arg to a `(new T args...)` call. Either a `Type`

crates/ailang-core/src/desugar.rs

@@ -366,6 +366,7 @@ fn collect_used_in_term(t: &Term, used: &mut BTreeSet<String>) {
                 }
             }
         }
+        Term::Intrinsic => {}
     }
 }
 
@@ -932,6 +933,7 @@ impl Desugarer {
                     })
                     .collect(),
             },
+            Term::Intrinsic => t.clone(),
         }
     }
 
@@ -1250,6 +1252,7 @@ pub fn free_vars_in_term(t: &Term, bound: &BTreeSet<String>, out: &mut BTreeSet<
                 }
             }
         }
+        Term::Intrinsic => {}
     }
 }
 
@@ -1440,6 +1443,7 @@ pub fn subst_var(t: &Term, from: &str, to: &str) -> Term {
                 })
                 .collect(),
         },
+        Term::Intrinsic => t.clone(),
     }
 }
 
@@ -1590,6 +1594,7 @@ pub fn subst_call_with_extras(t: &Term, name: &str, lifted: &str, extras: &[Stri
                 })
                 .collect(),
         },
+        Term::Intrinsic => t.clone(),
     }
 }
 
@@ -1655,6 +1660,7 @@ pub fn find_non_callee_use(t: &Term, name: &str) -> Option<Term> {
             NewArg::Value(v) => find_non_callee_use(v, name),
             NewArg::Type(_) => None,
         }),
+        Term::Intrinsic => None,
     }
 }
 
@@ -1705,6 +1711,7 @@ mod tests {
                 NewArg::Value(v) => any_nested_ctor(v),
                 NewArg::Type(_) => false,
             }),
+            Term::Intrinsic => false,
         }
     }
 
@@ -1738,6 +1745,7 @@ mod tests {
                 NewArg::Value(v) => any_let_rec(v),
                 NewArg::Type(_) => false,
             }),
+            Term::Intrinsic => false,
         }
     }
 
@@ -2893,6 +2901,7 @@ mod tests {
                 NewArg::Value(v) => any_lit_pattern(v),
                 NewArg::Type(_) => false,
             }),
+            Term::Intrinsic => false,
         }
     }
 

crates/ailang-core/src/workspace.rs

@@ -1291,6 +1291,7 @@ where
             }
             Ok(())
         }
+        Term::Intrinsic => Ok(()),
     }
 }
 
@@ -1434,6 +1435,7 @@ where
             }
             Ok(())
         }
+        Term::Intrinsic => Ok(()),
     }
 }
 

crates/ailang-core/tests/design_schema_drift.rs

@@ -167,6 +167,7 @@ fn design_md_anchors_every_term_variant() {
                 args: vec![],
             },
         ),
+        (r#""t": "intrinsic""#, Term::Intrinsic),
     ];
 
     for (anchor, term) in exemplars {
@@ -189,6 +190,7 @@ fn design_md_anchors_every_term_variant() {
             Term::Loop { .. } => "loop",
             Term::Recur { .. } => "recur",
             Term::New { .. } => "new",
+            Term::Intrinsic => "intrinsic",
         };
         assert!(
             anchor_in_jsonc_block(DATA_MODEL, anchor),

crates/ailang-core/tests/schema_coverage.rs

@@ -49,6 +49,7 @@ enum VariantTag {
     TermReuseAs,
     TermLoop,
     TermRecur,
+    TermIntrinsic,
     // Pattern
     PatternWild,
     PatternVar,
@@ -96,6 +97,7 @@ const EXPECTED_VARIANTS: &[VariantTag] = &[
     VariantTag::TermReuseAs,
     VariantTag::TermLoop,
     VariantTag::TermRecur,
+    VariantTag::TermIntrinsic,
     VariantTag::PatternWild,
     VariantTag::PatternVar,
     VariantTag::PatternLit,
@@ -261,6 +263,9 @@ fn visit_term(t: &Term, observed: &mut HashSet<VariantTag>) {
                 }
             }
         }
+        Term::Intrinsic => {
+            observed.insert(VariantTag::TermIntrinsic);
+        }
     }
 }
 

crates/ailang-core/tests/spec_drift.rs

@@ -136,6 +136,7 @@ fn spec_mentions_every_term_variant() {
                 })],
             },
         ),
+        ("(intrinsic", Term::Intrinsic),
     ];
 
     for (anchor, term) in exemplars {
@@ -160,6 +161,7 @@ fn spec_mentions_every_term_variant() {
             Term::Loop { .. } => "loop",
             Term::Recur { .. } => "recur",
             Term::New { .. } => "new",
+            Term::Intrinsic => "intrinsic",
         };
         assert!(
             FORM_A_SPEC.contains(anchor),

crates/ailang-kernel-stub/src/lib.rs

@@ -33,5 +33,10 @@ pub const STUB_AIL: &str = r#"(module kernel_stub
     (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))))
+    (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)))
 "#;

crates/ailang-prose/src/lib.rs

@@ -954,6 +954,7 @@ fn write_term_prec(out: &mut String, t: &Term, level: usize, parent_prec: u8, ow
             }
             out.push(')');
         }
+        Term::Intrinsic => out.push_str("compiler-supplied (intrinsic)"),
     }
 }
 
@@ -1154,6 +1155,7 @@ fn count_free_var(name: &str, t: &Term) -> usize {
                 NewArg::Type(_) => 0,
             })
             .sum(),
+        Term::Intrinsic => 0,
     }
 }
 
@@ -1314,6 +1316,7 @@ fn subst_var_with_term(t: &Term, name: &str, replacement: &Term) -> Term {
                 })
                 .collect(),
         },
+        Term::Intrinsic => t.clone(),
     }
 }
 

crates/ailang-surface/src/parse.rs

@@ -614,12 +614,18 @@ impl<'a> Parser<'a> {
                     }
                     body = Some(self.parse_body_attr()?);
                 }
+                Some("intrinsic") => {
+                    if body.is_some() {
+                        return Err(self.duplicate_clause_err("fn-def", &format!("fn `{name}`"), "body"));
+                    }
+                    body = Some(self.parse_intrinsic_attr()?);
+                }
                 Some(other) => {
                     let pos = self.peek().map(|t| t.span.start).unwrap_or(0);
                     return Err(ParseError::Production {
                         production: "fn-def",
                         message: format!(
-                            "unknown fn attribute `{other}`; expected `doc`, `export`, `suppress`, `type`, `params`, or `body`"
+                            "unknown fn attribute `{other}`; expected `doc`, `export`, `suppress`, `type`, `params`, `body`, or `intrinsic`"
                         ),
                         pos,
                     });
@@ -640,7 +646,7 @@ impl<'a> Parser<'a> {
         })?;
         let body = body.ok_or_else(|| ParseError::Production {
             production: "fn-def",
-            message: format!("fn `{name}` is missing required `(body ...)` attribute"),
+            message: format!("fn `{name}` is missing required `(body ...)` or `(intrinsic)` attribute"),
             pos: 0,
         })?;
         Ok(FnDef {
@@ -767,6 +773,17 @@ impl<'a> Parser<'a> {
         Ok(t)
     }
 
+    /// Parse an `(intrinsic)` body clause into [`Term::Intrinsic`]. It
+    /// fills the same single body slot a `(body ...)` clause fills; a
+    /// def carrying it is compiler-supplied (signature-only at
+    /// typecheck, routed through the intercept registry at codegen).
+    fn parse_intrinsic_attr(&mut self) -> Result<Term, ParseError> {
+        self.expect_lparen("intrinsic-attr")?;
+        self.expect_keyword("intrinsic")?;
+        self.expect_rparen("intrinsic-attr")?;
+        Ok(Term::Intrinsic)
+    }
+
     // ---- const def ------------------------------------------------------
 
     fn parse_const(&mut self) -> Result<ConstDef, ParseError> {
@@ -1526,8 +1543,12 @@ impl<'a> Parser<'a> {
         if let Some("effects") = self.peek_head_ident() {
             effects = self.parse_effects_clause()?;
         }
-        // (body term)
+        // (body term) — or (intrinsic) for a compiler-supplied body
-        let body = self.parse_body_attr()?;
+        let body = if let Some("intrinsic") = self.peek_head_ident() {
+            self.parse_intrinsic_attr()?
+        } else {
+            self.parse_body_attr()?
+        };
         self.expect_rparen("lam-term")?;
         Ok(Term::Lam {
             params,

crates/ailang-surface/src/print.rs

@@ -209,9 +209,13 @@ fn write_fn_def(out: &mut String, fd: &FnDef, level: usize) {
     out.push(')');
     out.push('\n');
     indent(out, level + 1);
-    out.push_str("(body ");
+    if matches!(fd.body, Term::Intrinsic) {
-    write_term(out, &fd.body, level + 2);
+        out.push_str("(intrinsic)");
-    out.push(')');
+    } else {
+        out.push_str("(body ");
+        write_term(out, &fd.body, level + 2);
+        out.push(')');
+    }
     out.push(')');
 }
 
@@ -549,9 +553,13 @@ fn write_term(out: &mut String, t: &Term, level: usize) {
                 }
                 out.push(')');
             }
-            out.push_str(" (body ");
+            if matches!(**body, Term::Intrinsic) {
-            write_term(out, body, level);
+                out.push_str(" (intrinsic))");
-            out.push_str("))");
+            } else {
+                out.push_str(" (body ");
+                write_term(out, body, level);
+                out.push_str("))");
+            }
         }
         Term::Seq { lhs, rhs } => {
             out.push_str("(seq ");
@@ -636,6 +644,11 @@ fn write_term(out: &mut String, t: &Term, level: usize) {
             }
             out.push(')');
         }
+        // A general term-printer only reaches Term::Intrinsic via a
+        // fn/lam body slot, which the fn-def and lam printers above
+        // already special-case; emitting `(intrinsic)` here keeps the
+        // exhaustive match correct.
+        Term::Intrinsic => out.push_str("(intrinsic)"),
     }
 }
 

design/contracts/0002-data-model.md

@@ -191,6 +191,14 @@ narrative — defaults, superclasses, diagnostics — lives in
 { "t": "new",
   "type": "<TypeName>",
   "args": [ NewArg, ... ] }
+
+// intrinsic: the body of a compiler-supplied definition. Legal only as
+// a FnDef/Lam body, only in a (kernel)-tier module or the prelude
+// (typecheck: intrinsic-outside-kernel-tier). Never reduces to a value;
+// codegen consumes it via the intercept registry. A def is intrinsic
+// iff its body is this term. Strictly additive (no skip_serializing_if;
+// pre-existing fixtures hash bit-identically — none carry the tag).
+{ "t": "intrinsic" }
 ```
 
 **`NewArg`** (one positional arg to a `(new T args...)` call):
@@ -209,7 +217,14 @@ narrative — defaults, superclasses, diagnostics — lives in
 In the MVP, `do` is only a direct call to a built-in effect op (no
 handler); the effect system is described in [effects](../models/0002-effects.md).
 A `lam` term constructs an anonymous function value; free
-variables of its body are captured from the enclosing scope.
+variables of its body are captured from the enclosing scope. A `lam`
+body may be `{ "t": "intrinsic" }`, in which case the lambda is
+compiler-supplied (the synthesised-instance-method form).
+
+A `fn` def's `body` may be `{ "t": "intrinsic" }`, in which case the
+def is compiler-supplied: the typechecker validates only its signature
+and codegen routes it through the intercept registry. Such a body is
+legal only in a `(kernel)`-tier module or the prelude.
 
 Loop binders are alloca-resident: typecheck binds them in the
 ordinary local scope plus a positional `loop_stack`, and codegen

examples/kernel_answer.ail

@@ -0,0 +1,6 @@
+(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/kernel_intrinsic_smoke.ail

@@ -0,0 +1,7 @@
+(module kernel_intrinsic_smoke
+  (kernel)
+  (fn smoke
+    (doc "Schema-coverage fixture: exercises Term::Intrinsic in a kernel-tier module.")
+    (type (fn-type (params) (ret (con Int))))
+    (params)
+    (intrinsic)))