New milestone, triggered by the raw-buf.2 BLOCKED chain (the .2 work
was discarded; spec 4ad003d and plan 647121c stay 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
in a2698a8). 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).
Brummel
c42034b38d