Forward-fix on 5b66de7, prompted by plan-recon for intrinsic-bodies.2.
Two spec-vs-reality gaps in the .2 (migration + lock) sections, both
caught before the .2 plan was written:
1. Count. The spec said "18 dummy bodies" migrate to (intrinsic). That
conflated the INTERCEPTS entry count with authored prelude bodies.
Reality: examples/prelude.ail carries 13 authored dummy bodies — the
7 Eq/Ord instance methods (eq Int/Bool/Str/Unit, compare
Int/Bool/Str) + the 6 float_* free fns. The registry has 19 entries
(18 legacy + the .1 `answer`); the other 6 are not prelude dummies.
2. The strict bijection cannot hold. lt__Int/le__Int/gt__Int/ge__Int/
ne__Int (5 INTERCEPTS entries) intercept the monomorphised __Int
specialisations of the polymorphic free fns lt/le/gt/ge/ne, which
carry REAL bodies in the prelude (ne = (app not (app eq x y)); the
four ordering helpers are (match (app compare x y) ...)). Those
bodies are honest and live — lowered for every non-Int instantiation;
only the Int specialisation is intercepted for a faster direct icmp.
They are an optimisation class, not a compiler-supplied-body class:
no lie, no source body to replace, no (intrinsic) marker. A strict
bijection over all INTERCEPTS entries would be red for these 5.
Corrections:
- § Architecture point 6: 13 authored prelude sites (named), with the
5 icmp-family + `answer` explicitly listed as non-prelude / not
migrated and why.
- § Architecture point 7: the pin splits the registry into
intrinsic-backed (13 prelude markers + answer = 14) and
optimisation-only (the 5 *__Int, an explicit documented allowlist).
The bijection holds over the intrinsic-backed class only; the pin
loads the workspace + monomorphises to recover mangled names for the
marker direction.
- § Architecture point 8: reframed from "dead-path removal" to
"dead-path confirmation" — .1's intercept-by-name already bypasses
the dummy body before lower_term sees it (committed reality at
52ff873), so .2 confirms no path lowers an intercepted body and
deletes stale comments; the .1 Term::Intrinsic escape-guards stay.
- § Components + § Testing: the two moving hash pins named
(prelude_module_hash_pin.rs; mono_hash_stability.rs's 6 eq/compare
pins move, its 4 show pins do not); hash_pin.rs carries no
prelude-derived hash. IR snapshots do not change.
Grounding-check PASS on all five corrected .2 claims against the
shipped .1 baseline (count, the 5 real-bodied helpers, the three hash
pins' behaviour, the already-dead path, the bijection-pin pipeline
reachability). No ail/ail-json/ll fenced block changed — parse-gate a
documented no-op for this revision.
The deeper observation this surfaced — that INTERCEPTS conflates two
concepts (compiler-supplied bodies vs. optimisation of a real body) —
is noted but NOT resolved here; splitting the registry is out of scope
for intrinsic-bodies and would be its own milestone.
Forward-fix on c42034b. plan-recon for intrinsic-bodies.1 surfaced
that the original AST representation — FnDef.body / Term::Lam.body
made Option<Term> plus an `intrinsic: bool` flag — has a ~150-site
blast radius across six crates: every body read/construct site breaks
when a mandatory public field goes optional. That blast radius is the
signal (CLAUDE.md design-rationale rule) that the representation was
wrong, not merely expensive.
The Form-A surface (user's chosen Approach 1) and the Local-Reasoning
semantics (Design X marker placement) are UNCHANGED. Only the internal
AST representation changes, which is orchestrator authority over AST
design.
New representation: a single new leaf Term variant, Term::Intrinsic
({ "t": "intrinsic" }), is the body of a compiler-supplied definition.
FnDef.body (Term) and Term::Lam.body (Box<Term>) keep their existing
types. A def is intrinsic iff matches!(body, Term::Intrinsic).
Three structural reasons (not effort):
1. Established pattern. The project adds new constructs as additive
Term variants — Term::New, Term::Loop, Term::Recur, Term::Clone,
Term::ReuseAs all landed this way, documented "strictly additive,
pre-existing fixtures hash bit-identically" in
design/contracts/0002-data-model.md. Term::Intrinsic follows it.
Option A introduced a brand-new pattern (mandatory field → optional)
absent from the schema.
2. Meaning at the right locus. "This body is compiler-supplied" is a
property of the body, not the container. Term::Intrinsic sits at the
body position — fn body, or instance-method lambda body (Design X
local-signature placement preserved exactly).
3. Illegal state unrepresentable. Option A admitted intrinsic:true with
body:Some(...), forcing an intrinsic-with-body reject. Under the
variant a body is either Term::Intrinsic or a real term, never both
— the reject is deleted, the state cannot occur. This is the same
make-illegal-states-unrepresentable discipline as the honesty theme
the milestone exists to serve.
Blast radius collapses from ~150 body-read/construct sites to the
exhaustive match-on-Term arms (canonical/hash/visit + schema_coverage),
which the no-wildcard Term match turns into compile errors until each
gains a Term::Intrinsic case — the project's normal new-variant
discipline.
Sections revised: § Architecture points 1/3/4, § Concrete code shapes
(Implementation shape now shows the leaf variant, not the
Option+flag), § Components, § Data flow, § Error handling (the
intrinsic-with-body row removed), § Testing strategy (the
both-body-and-intrinsic reject test removed; schema_coverage Term::Intrinsic
observation added). The scheme/ail surface examples are byte-unchanged.
Re-ran the brainstorm gates on the revision: Step-7 parse gate green
(both ail blocks exit 0, unchanged); Step-7.5 grounding-check PASS on
the four new load-bearing claims (additive-variant precedent +
contract wording, exhaustive-Term-match mechanism, mono.rs
synthesise_mono_fn destructure unchanged under preserved body type,
Term::Recur as non-reducing-leaf precedent).
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