spec: intrinsic-bodies — (intrinsic) Form-A body marker (refs #9)
New milestone, triggered by the raw-buf.2 BLOCKED chain (the .2 work was discarded; spec4ad003dand plan647121cstay on main per the forward-only rule). The Form-A surface currently forces every fn / instance-method to carry a (body ...) clause, which produces three problems the marker resolves: 1. Prelude dummy-body lies. The eq/compare/ne/lt/le/gt/ge instance methods ship placeholder bodies — (body false), (body (term-ctor Ordering EQ)) — that parse and type-check but never run; codegen discards them and emits the intercept (registry shipped in raw-buf.1, intercepts.rs). A standing honesty-rule infraction (design/contracts/0007-honesty-rule.md): a reader who trusts the source is wrong about what runs. 2. Polymorphic kernel-tier fns are structurally impossible. RawBuf's get : RawBuf a -> Int -> a needs a placeholder body producing a value of type a, and AILang has no value of polymorphic type. The dummy-body requirement made the fn unauthorable — what BLOCKED raw-buf.2. 3. No surface affordance for "compiler supplies this body". Every systems language has one (LLVM declare, Rust extern "rust-intrinsic", Haskell foreign import prim, C builtins). The intercept registry IS AILang's compiler-supplied-body table; (intrinsic) is the surface declaration of membership. Decomposition (2 iterations, full cut): intrinsic-bodies.1 — the mechanism. FnDef.body / Term::Lam.body become optional; an additive intrinsic: bool rides each (skip_serializing_if, hash-stable when omitted). Form-A parses + prints (intrinsic); round-trip gated. Checker checks signature-only, rejects body+intrinsic, rejects intrinsic outside kernel-tier / prelude (intrinsic-outside-kernel-tier). Codegen routes intrinsic defs through intercepts::lookup. Ratified by a throwaway `answer` smoke intrinsic in the kernel_stub fixture, end-to-end to native. intrinsic-bodies.2 — migration + lock. The dummy bodies swap for (intrinsic); a hard-lockstep pin asserts a bijection between INTERCEPTS entries and intrinsic markers reachable in the loaded workspace (extends raw-buf.1's registry_contains_all_legacy_arms from a one-way name check to a two-way source<->registry bijection). Dead body-lowering path for intercepted defs removed. Design decisions locked during brainstorm: - Marker placement (Design X). For a top-level fn, (intrinsic) replaces the (body ...) clause directly — the (type ...) signature stays beside it. For an instance method, the marker sits on the lambda BODY, not the method: the lambda's typed shell (params / ret) IS the method's local signature, and intrinsic drops the body, not the signature — exactly as LLVM declare / Rust extern-intrinsic keep the full signature. Hoisting the marker to (method eq (intrinsic)) would erase the local signature (a reader would have to climb to the Eq class decl and substitute a := Int), violating local reasoning (design/INDEX.md § Goal). The mono pass (mono.rs::synthesise_mono_fn) reads params + inner body out of this lambda today, so the placement keeps that path unchanged. The Design Y alternative was considered and rejected on this signature-locality ground. - Scope guard. (intrinsic) is legal only in (kernel)-tier modules and the prelude; user modules are rejected. This 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. Process note: first spec under the hardened brainstorm pipeline (Skills issue #1 fixes + the spec_validation parse gates retrofitted ina2698a8). The Step-7 parse-every-block gate caught a real defect in the spec's own ail examples on first run (an invalid module-level (doc ...) head) — the defense line that was absent on raw-buf.2 and let its unparseable spec bytes through to implement. Grounding-check PASS on 12 load-bearing assumptions, each ratified by a named green test. Out of scope: a user-facing plugin API for custom intercepts (the scope guard forbids user-module intrinsics); any change to the raw-buf.1 dispatch mechanism; the raw-buf.2 redo itself (milestone #7, parked behind this one).
This commit is contained in:
@@ -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 <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:
|
||||
|
||||
```scheme
|
||||
(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):
|
||||
|
||||
```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<Term>` 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).
|
||||
Reference in New Issue
Block a user