diff --git a/docs/specs/0055-intrinsic-bodies.md b/docs/specs/0055-intrinsic-bodies.md new file mode 100644 index 0000000..5a1ef26 --- /dev/null +++ b/docs/specs/0055-intrinsic-bodies.md @@ -0,0 +1,333 @@ +# 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 + +```ail +(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.** `FnDef.body` and `Term::Lam.body` become *optional*; a + new `intrinsic: bool` flag rides each. `intrinsic: true` ⟺ + `body` absent. The flag is additive and `skip_serializing_if`-gated, + so every existing fixture's canonical-JSON hash stays bit-identical + (the standard additive-schema pattern, `design/contracts/0002-data-model.md`). +2. **Form-A surface.** Parser accepts `(intrinsic)` as a sibling + attribute to `(body ...)` inside both `fn-def` and `lam`; the + printer emits it. Round-trip (`parse ∘ print = id`) holds by the + standard fixture gate. +3. **Checker.** An `(intrinsic)` definition type-checks against its + *signature only* — there is no body to check. Two new rejects: + (a) a definition carrying **both** a body and `intrinsic` is + malformed; (b) an `(intrinsic)` definition outside a `(kernel)`-tier + module or the prelude is rejected with `intrinsic-outside-kernel-tier`. +4. **Codegen.** An `(intrinsic)` definition 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 simply not taken for these + definitions. +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 )` 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: + +```scheme +(fn get + (doc "Indexed read. Codegen intercept get__RawBuf__ 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): + +```scheme +(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: + +```scheme +(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: + +```ail +(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): + +```console +$ 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) + +Before → after on the two load-bearing structs. Exact bytes are the +planner's job; this fixes the shape only. + +`FnDef` (`crates/ailang-core/src/ast.rs`): + +```jsonc +// before +{ "kind": "fn", "name": "...", "type": Type, "params": [...], "body": Term, ... } + +// after — body optional, intrinsic flag additive +{ "kind": "fn", "name": "...", "type": Type, "params": [...], + "body": Term, // present ⟺ intrinsic absent/false + "intrinsic": true, // optional; omitted when false (hash-stable when omitted). + // When true: body MUST be absent; the def is legal only in a + // (kernel)-tier module or the prelude; codegen routes through + // intercepts::lookup on the mangled name. + ... } +``` + +`Term::Lam` (same crate) takes the symmetric pair: `body` becomes +optional, `intrinsic: bool` is added. An instance method whose body +is a lambda (every `eq`/`compare` instance) carries the marker on the +*lambda body*, **not** on 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 replaces the lambda's *body*, 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; the +intrinsic marker rides where the dummy body sits today, so that path +is unchanged. + +Serde note: `Option` serialises `Some(t)` as `t` (not as a +tagged wrapper), so a non-intrinsic def's `"body": {...}` is +byte-identical before and after. `None` is `skip_serializing_if`-omitted. +This is what keeps every existing fixture's hash stable; the +`design_schema_drift.rs` schema mirror and the `0002-data-model.md` +contract move in the same iteration as the struct change. + +## Components + +| Component | Iteration | Change | +|---|---|---| +| `crates/ailang-core/src/ast.rs` | .1 | `FnDef.body` / `Lam.body` → optional; `intrinsic: bool` added to both. | +| `crates/ailang-core` canonical/hash/visit | .1 | Visitors gain an explicit intrinsic arm (no body to walk). Schema-coverage corpus extended. | +| `crates/ailang-surface` (lex/parse/print) | .1 | `(intrinsic)` attribute parsed + printed in `fn-def` and `lam`; round-trip gated. | +| `crates/ailang-check/src/lib.rs` | .1 | Intrinsic def checks signature-only; rejects body+intrinsic; rejects intrinsic outside kernel-tier/prelude (`intrinsic-outside-kernel-tier`). | +| `crates/ailang-codegen/src/lib.rs` | .1 | Intrinsic def routes through `intercepts::lookup`; body-lowering path not taken for 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 | `fn` + `lam` schema gain `intrinsic`; `body` documented optional. | +| `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; +the intrinsic flag is read at three of those stations: + +1. **Parse.** `(intrinsic)` sets `intrinsic = true`, leaves `body = None`. + A `fn-def`/`lam` carrying both `(body ...)` and `(intrinsic)` is a + parse-level malformation (or a check-level one — planner picks the + station; the reject must exist). +2. **Check.** Intrinsic def: 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.** Intrinsic def: `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)` and `(body ...)` on the same def | `intrinsic-with-body` (malformed) | parse or check | +| `(intrinsic)` in a non-kernel, non-prelude module | `intrinsic-outside-kernel-tier` | check | +| Intrinsic def with no registered intercept | existing codegen deferral | codegen | + +The middle 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. + +## 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`. +- Check reject (malformed): a def with both body and intrinsic is rejected. +- 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`. + +**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).