AILang/docs/specs/0055-intrinsic-bodies.md

Intrinsic bodies — Design Spec

Date: 2026-05-29 Status: Draft — awaiting user spec review Authors: orchestrator + Claude

Goal

Give Form-A a way to say "this definition's body is supplied by the compiler, not written in source" — and make that the single, honest representation for every definition whose real implementation lives in the codegen intercept registry (crates/ailang-codegen/src/intercepts.rs, shipped in raw-buf.1).

Today every such definition carries a dummy body that never runs. The prelude's eq Int instance method is

(module dummy_today
  (fn eq_int_like
    (doc "Real implementation is a codegen intercept; the body false never executes.")
    (type (fn-type (params (con Int) (con Int)) (ret (con Bool))))
    (params x y)
    (body false)))

The (body false) (and the eighteen siblings like it across the prelude) parses and type-checks, but codegen discards it and emits the intercept instead. The body is a structural lie: a reader who trusts the source is wrong about what runs. This is a standing infraction of the honesty rule (design/contracts/0007-honesty-rule.md), which the language has carried silently since the operator-routing milestone.

The lie is not merely cosmetic. It blocks the raw-buf milestone: a polymorphic kernel-tier function such as RawBuf's get : RawBuf a -> Int -> a needs a placeholder body that produces a value of type a — and AILang has no value of polymorphic type. There is no honest expression to write. The dummy-body requirement makes the function structurally impossible to author, which is what BLOCKED raw-buf.2 (see git log 4ad003d..647121c and the discarded .2 working tree).

The fix is a new Form-A surface affordance, (intrinsic), that replaces the (body ...) clause for compiler-supplied definitions. This is the same construct every systems language has: LLVM declare, Rust extern "rust-intrinsic" / #[rustc_intrinsic], Haskell foreign import prim, C compiler builtins. The intercept registry is AILang's compiler-supplied-body table; (intrinsic) is the surface declaration of membership in it.

Architecture

Three landing points, two iterations.

Iteration intrinsic-bodies.1 — the mechanism.

1. AST. A new leaf term variant Term::Intrinsic is the body of a compiler-supplied definition. FnDef.body and Term::Lam.body keep their existing types (Term / Box<Term>) — they are not made optional. A definition is intrinsic iff its body is Term::Intrinsic. The variant is strictly additive: a fixture that does not use it serialises bit-identically (the established additive-term-variant pattern — Term::New, Term::Loop, Term::Recur, Term::Clone, Term::ReuseAs all landed this way, design/contracts/0002-data-model.md). This is the load-bearing representation choice: it puts "this body is compiler-supplied" at the body position where it semantically belongs, keeps the ~150-site body-read/construct surface across six crates untouched (only exhaustive match-on-Term arms gain a case), and makes the illegal "body AND intrinsic" state unrepresentable rather than rejected — a body is either Term::Intrinsic or a real term, never both. (The rejected alternative, body: Option<Term> + an intrinsic: bool flag, splits one fact across two fields, admits that illegal state, and breaks every body consumer in the workspace.)
2. Form-A surface. For a top-level fn, the parser accepts (intrinsic) as a sibling clause where (body ...) would go and maps it to body = Term::Intrinsic; the printer emits (intrinsic) in that slot when the body is Term::Intrinsic. For a lambda, (intrinsic) sits at the positional body slot (where the body term goes today) and parses to Term::Intrinsic; the printer emits it there. Round-trip (parse ∘ print = id) holds by the standard fixture gate. The fn-vs-lam surface asymmetry mirrors the existing one (a fn carries a named (body X) clause; a lambda carries its body positionally) — (intrinsic) follows each form's existing body placement.
3. Checker. A definition whose body is Term::Intrinsic type-checks against its signature only — there is no body term to infer. One new reject: an intrinsic definition outside a (kernel)-tier module or the prelude is rejected with intrinsic-outside-kernel-tier. (There is no intrinsic-with-body reject — the representation makes that state impossible, see point 1.)
4. Codegen. A definition whose body is Term::Intrinsic routes through intercepts::lookup; if no intercept is registered for its mangled name, codegen emits the existing deferral diagnostic. The current "lower the body" path is not taken for these definitions — lower_term is never called on a Term::Intrinsic body (and a Term::Intrinsic reaching lower_term through any other path is a codegen-internal error, since an intrinsic body must be consumed by the intercept route).
5. Ratifier. One throwaway intrinsic in the kernel_stub fixture — a nullary answer : () -> Int whose intercept emits ret i64 42 — drives the mechanism end-to-end (parse → check → codegen → run). kernel_stub already exists precisely to ratify kernel-tier mechanisms.

Iteration intrinsic-bodies.2 — the migration + the lock.

6. Prelude migration. All eighteen dummy bodies (the eq__*, compare__*, and lt|le|gt|ge|ne__* instance methods enumerated by intercepts::INTERCEPTS) swap their (body <dummy>) for (intrinsic).
7. Hard-lockstep pin. A test asserts a bijection between INTERCEPTS entries and (intrinsic) definitions reachable in the loaded workspace (prelude + kernel-tier modules): every registry entry has exactly one intrinsic marker and vice versa. Drift in either direction is a red test. This extends the registry_contains_all_legacy_arms pin from raw-buf.1 from a one-directional name check to a two-directional source↔registry bijection.
8. Dead-path removal. The dummy-body-execution path for intercepted definitions is removed; nothing emits it once the migration lands.

Concrete code shapes

North-star: what a kernel author writes (proposed surface)

The surface this milestone delivers. These blocks are labelled scheme (not ail) on purpose — the (intrinsic) attribute does not parse against the pre-feature tool, so they are proposals, not ratified current behaviour. (Verified: see the must-fail transcript below.)

The raw-buf north-star — a polymorphic kernel-tier function with no honest body, the case that motivated the milestone:

(fn get
  (doc "Indexed read. Codegen intercept get__RawBuf__<T> emits a getelementptr + load.")
  (type (forall (vars a) (fn-type (params (borrow (con RawBuf a)) (con Int)) (ret (con a)))))
  (params b i)
  (intrinsic))

The prelude eq Int instance method after migration (the lie, fixed). The marker sits on the lambda body; the lambda's typed shell (params/ret) stays — it is the method's local signature, and intrinsic drops the body, not the signature (see the rationale under "Implementation shape" below):

(instance
  (class Eq)
  (type (con Int))
  (doc "Eq Int. Codegen intercept eq__Int emits icmp eq i64 with alwaysinline.")
  (method eq
    (body (lam (params (typed x a) (typed y a)) (ret (con Bool)) (intrinsic)))))

The intrinsic-bodies.1 ratifier — the throwaway smoke intrinsic in the kernel_stub fixture:

(fn answer
  (doc "Ratifies the intrinsic mechanism end-to-end. Intercept answer emits ret i64 42.")
  (type (fn-type (params) (ret (con Int))))
  (params)
  (intrinsic))

Current-state evidence (parses today)

The dummy-body lie exactly as the prelude carries it now — a body that parses, type-checks, and never runs:

(module dummy_today
  (fn forty_two
    (doc "Real implementation is a codegen intercept. The body 0 never executes.")
    (type (fn-type (params (con Int)) (ret (con Int))))
    (params n)
    (body 0)))

Must-fail evidence (rejected today)

(intrinsic) is not yet a surface attribute, so the proposed forms above are rejected by the pre-feature tool. This is the baseline the milestone moves off — the parser reject is what intrinsic-bodies.1 turns into an accept (inside kernel-tier / prelude) and a different reject (intrinsic-outside-kernel-tier, for user modules):

$ cat intr.ail
(module intr
  (fn new (type (fn-type (params (con Int)) (ret (con Int)))) (params n) (intrinsic)))
$ ail check intr.ail
error: [surface-parse-error] parse error in fn-def: unknown fn attribute
  `intrinsic`; expected `doc`, `export`, `suppress`, `type`, `params`,
  or `body` at byte 86

Implementation shape (secondary — the AST delta)

The change is one new leaf Term variant. Exact bytes are the planner's job; this fixes the shape only.

Term::Intrinsic (crates/ailang-core/src/ast.rs):

// new leaf term — the body of a compiler-supplied definition.
// Strictly additive (no skip_serializing_if needed; a fixture that
// does not carry it hashes bit-identically — the same additive-variant
// pattern as Term::New / Term::Loop / Term::Recur / Term::Clone).
// Never reduces to a value: codegen consumes it via intercepts::lookup,
// the typechecker treats a def with this body as signature-only.
{ "t": "intrinsic" }

FnDef.body (currently Term) and Term::Lam.body (currently Box<Term>) are unchanged in type — they simply may now hold Term::Intrinsic. A top-level intrinsic fn is FnDef { body: Term::Intrinsic, .. }; an intrinsic instance-method lambda is Term::Lam { body: Box::new(Term::Intrinsic), .. }. "Is this definition intrinsic?" is matches!(body, Term::Intrinsic).

The marker sits at the body position — for a top-level fn that is the fn body; for an instance method that is the lambda body, not the method as a whole — and this placement is load-bearing, not incidental.

The reason is local reasoning (design/INDEX.md § Goal: "every definition carries its full type and effect set, so a signature can be trusted without reading the body"). An intrinsic is a signature without a body, never nothing — exactly as LLVM declare i64 @llvm.foo(i64, i64), Rust extern "rust-intrinsic" { fn foo(x: i32) -> i32; }, and Haskell foreign import prim all keep the full signature and drop only the body. For a top-level fn the signature is the (type ...) clause, which stays beside the (intrinsic) marker. For an instance method the signature-bearing structure is the lambda itself: its (params (typed x a) (typed y a)) and (ret (con Bool)) are the parameter types and return type, readable at the definition site. Hoisting the marker to the method ((method eq (intrinsic))) would erase that local signature — a reader would have to climb to the Eq class declaration and substitute a := Int mentally to recover it. So the marker is the lambda's body (Term::Intrinsic), leaving the lambda's typed shell — the local signature — in place. The mono pass (crates/ailang-check/src/mono.rs::synthesise_mono_fn) already reads the method's parameter names and inner body out of this lambda (Term::Lam { params, body, .. } => (params, *body)); with the inner body being Term::Intrinsic, the synthesised FnDef carries body: Term::Intrinsic and is itself intrinsic. The destructure itself is unchanged — only what the inner body is differs.

Hash-stability note: Term::Intrinsic is a new enum variant, not a new field, so a fixture that does not use it serialises exactly as before — the same mechanism that kept hashes stable when Term::New, Term::Loop, and Term::Recur were added. The design_schema_drift.rs schema mirror, the schema_coverage.rs variant corpus (a fixture must now exercise Term::Intrinsic), and the 0002-data-model.md contract all move in the same iteration as the variant.

Components

Component	Iteration	Change
crates/ailang-core/src/ast.rs	.1	New leaf variant Term::Intrinsic. FnDef.body / Lam.body types unchanged.
crates/ailang-core canonical/hash/visit	.1	Exhaustive match-on-Term arms gain a Term::Intrinsic case (leaf, no sub-terms to walk). Schema-coverage corpus extended to exercise it.
crates/ailang-surface (lex/parse/print)	.1	(intrinsic) parsed + printed: as a body-slot clause in fn-def, at the positional body slot in lam; maps to/from Term::Intrinsic; round-trip gated.
crates/ailang-check/src/lib.rs	.1	A def whose body is Term::Intrinsic checks signature-only; rejects intrinsic outside kernel-tier/prelude (intrinsic-outside-kernel-tier). No intrinsic-with-body reject — the representation forbids that state.
crates/ailang-check/src/mono.rs	.1	synthesise_mono_fn lambda-destructure unchanged; an inner Term::Intrinsic body flows through to an intrinsic synthesised FnDef.
crates/ailang-codegen/src/lib.rs	.1	A def whose body is Term::Intrinsic routes through intercepts::lookup; lower_term is never called on it.
crates/ailang-kernel-stub + ailang-surface parse hop	.1	answer smoke intrinsic added to the stub fixture; its intercept registered.
examples/prelude.ail	.2	18 dummy bodies → (intrinsic).
crates/ailang-codegen/src/intercepts.rs (pin)	.2	registry_contains_all_legacy_arms upgraded to a source↔registry bijection pin.
codegen dummy-body path	.2	Removed.
design/contracts/0002-data-model.md	.1	New { "t": "intrinsic" } Term entry; note in fn/lam that the body may be Term::Intrinsic.
design/contracts/0007-honesty-rule.md	.2	The prelude-dummy infraction is closed; note its resolution if the contract references it.

Data flow

Authoring → parse → AST → check → codegen, unchanged in topology; Term::Intrinsic is recognised at three of those stations:

1. Parse. (intrinsic) in a fn body slot or a lambda body slot produces a Term::Intrinsic body. There is no "both body and intrinsic" surface form to reject — the grammar offers one body slot, and (intrinsic) either fills it or it does not.
2. Check. A def whose body is Term::Intrinsic: validate the signature, skip body inference. Enforce the kernel-tier/prelude scope. The module's kernel: true flag (or prelude identity) is already available to the checker via the loaded workspace.
3. Codegen. A def whose body is Term::Intrinsic: intercepts::lookup(mangled_name). Hit → emit the intercept. Miss → the existing deferral diagnostic (same one raw-buf.2 reuses for unregistered RawBuf ops).

Error handling

Condition	Diagnostic	Station
(intrinsic) in a non-kernel, non-prelude module	intrinsic-outside-kernel-tier	check
Intrinsic def with no registered intercept	existing codegen deferral	codegen

The first row is the honesty-rule guard at the workspace boundary: user code cannot mark a body as compiler-supplied, so the lie cannot re-enter through user modules. (There is deliberately no "body-and-intrinsic" row — Term::Intrinsic is a body, so a def either has it or has a real body, never both. The illegal state is unrepresentable, not diagnosed.)

Testing strategy

intrinsic-bodies.1:

• Round-trip: a kernel-tier fixture carrying (intrinsic) on both a top-level fn and a lambda parses → prints → re-parses to canonical-byte equality (rides the existing round_trip.rs corpus gate).
• Check accept: the kernel_stub answer intrinsic checks clean.
• Check reject (scope): a user module with an (intrinsic) fn is rejected with intrinsic-outside-kernel-tier.
• E2E: answer builds and runs, exit/print observing 42 — the mechanism works from source to native.
• Schema drift: design_schema_drift.rs green against the new 0002-data-model.md; schema_coverage.rs observes Term::Intrinsic in the fixture corpus.

intrinsic-bodies.2:

• Hard-lockstep pin: bijection between INTERCEPTS and workspace intrinsic markers. Add a marker without an entry → red; add an entry without a marker → red; drop either → red.
• All pre-existing E2E ratifiers stay green (the eq/compare/float smoke suite named in raw-buf.1's commit body) — the migration is behaviour-preserving by construction.
• Prelude hash: the prelude module's hash changes in .2 (the dummy bodies are gone); the prelude_module_hash_pin.rs baseline is rebaselined in the same iteration, with the old→new hash recorded in the commit body.

Acceptance criteria

Applied prospectively (design/contracts/0004-feature-acceptance.md):

• An LLM author naturally reaches for it. A kernel author writing RawBuf.get has no honest body to write — there is no value of type a. Faced with the dummy-body requirement, the natural move is to declare "the compiler supplies this", which is exactly (intrinsic). The north-star block above is that program; it is the empirical evidence, not a prose assertion.
• Measurably improves correctness / removes redundancy. Closes a standing honesty-rule infraction (eighteen bodies that lie about what runs); removes the dead body-lowering path for intercepted defs; removes the structural impossibility blocking polymorphic kernel-tier functions.
• Reintroduces no eliminated failure class. Machine-readability, local reasoning, provability, hallucination-robustness all hold or improve: a reader of an (intrinsic) def now knows from the source alone that the body is compiler-supplied, instead of having to read the codegen table to discover the source was lying.

Out of scope: a user-facing plugin API for registering custom intercepts (the scope guard explicitly forbids (intrinsic) in user modules); any change to the intercept dispatch mechanism shipped in raw-buf.1; the raw-buf redo itself (a separate milestone that consumes this one).