audit + close: intrinsic-bodies — honest prelude docs + lockstep table + stale-model fix (refs #9)

Milestone close for intrinsic-bodies (.1 mechanism 52ff873 + .2
migration/lock caa3618). Architect drift review over c42034b^..caa3618
plus the regression scripts. Both gates assessed; four drift items
resolved (3 fixed inline here, 1 filed to backlog).

Regression: both scripts exit 0.
  bench/check.py        → 34 metrics, 0 regressed, 2 improved beyond
                          tolerance (bench_hof_pipeline.bump_s -10.76%,
                          bench_list_sum_explicit.bump_s -12.27%), 32 stable.
  bench/compile_check.py → 24 metrics, 0 regressed, 24 stable.
  The milestone is behaviour-preserving; the two throughput improvements
  are noise within the bench's run-to-run band, not a milestone effect.

Drift items (architect):

1. [FIXED] examples/prelude.ail — the 13 migrated defs' doc strings
   still said "Body is placeholder for round-trip stability" and named
   `try_emit_primitive_instance_body` (the pre-raw-buf.1 dispatch fn).
   Post-migration the body IS an honest (intrinsic) marker, not a
   placeholder, and dispatch is `intercepts::lookup`. The docs lied
   about the very artefact the milestone exists to de-lie — an active
   honesty-rule infraction on main. Rewritten to present-tense
   "compiler-supplied (intrinsic) body; codegen emits <IR> via the
   intercept registry" across all 13 (7 Eq/Ord instance methods +
   6 float_* fns).

2. [FIXED] design/models/0007-kernel-extensions.md — claimed the
   `try_emit_primitive_instance_body` hardcoded list is "not yet
   migrated into a plugin registry ... deferred to the Series
   milestone". Stale since raw-buf.1 (the registry shipped) and
   intrinsic-bodies (the (intrinsic) marker + bijection pin). Rewritten
   to the present state: the registry exists, (intrinsic) declares
   membership, the bijection pin locks marker<->entry, and the
   optimisation-only class is named.

3. [FIXED] CLAUDE.md "Lockstep-invariant pairs" — added the third pair:
   INTERCEPTS entries <-> (intrinsic) markers, guarded by
   intercepts_bijection_with_intrinsic_markers, with the
   optimisation-only allowlist carve-out. Same class as the two existing
   tabled pairs; ships silently broken if one side moves without the
   other.

4. [BACKLOG #41, label idea] INTERCEPTS conflates two concepts —
   intrinsic-backed (compiler-supplied body) vs optimisation-of-a-
   real-body (the 5 *__Int icmp family). The .2 bijection pin contains
   it with a hardcoded OPTIMISATION_ONLY allowlist + a stale-allowlist
   guard; a structural split (an Intercept kind field) is the
   forward direction but is its own focused change, out of scope here.

What holds (architect confirmed): data-model contract matches the
shipped Term::Intrinsic (design_schema_drift gates it); no INDEX row
needed (data-model addition, not a new contract); both existing
lockstep pairs untouched (answer lowers via the ordinary qualified-fn
path, no new lower_app arm; no Pattern::Lit reject); 0007-honesty-rule
correctly needed no edit (general rule, never named the dummies).

RATIFY — baseline move: the prelude module hash pin
(crates/ailang-surface/tests/prelude_module_hash_pin.rs) moves
2ea61ef21ebc1913 -> b1373a2c69e70a3f. Cause: this tidy's 13 doc-string
rewrites (item 1). doc is part of the canonical JSON, so the module
hash shifts; behaviour is unchanged. The 6 mono eq/compare def-hashes
do NOT move (synthesise_mono_fn sets doc: None, so instance-method docs
never reach the synthesised symbol). Full workspace test green
post-rebaseline.

Milestone intrinsic-bodies is closed. It unblocks the raw-buf.2 redo
(the polymorphic kernel-tier fns RawBuf needs now have an honest body
form). raw-buf (#7) remains parked; resuming it is a fresh decision.
This commit is contained in:
2026-05-29 17:56:10 +02:00
parent caa3618c3e
commit 6ccc756c0f
4 changed files with 37 additions and 26 deletions
+1
View File
@@ -309,6 +309,7 @@ the cross-references column of a file-map.
|---|---|
| `Pattern::Lit::*` typecheck rejects in `crates/ailang-check/src/lib.rs` ↔ pre-desugar walkers in `crates/ailang-check/src/pre_desugar_validation.rs` | A reject arm placed AFTER `desugar_module` in the call chain is unreachable through the public `check` API if the desugar pass rewrites that pattern shape first (e.g. `desugar::build_eq` rewrites `Pattern::Lit::Float` into `(== scrut lit)` before typecheck runs). New rejects on a `Pattern::Lit::*` shape MUST live in `pre_desugar_validation.rs`, or be paired with a written guarantee that no desugar pass eats the shape. |
| `lower_app` arms in `crates/ailang-codegen/src/lib.rs::lower_app` (line ~1749) ↔ name recognition in `crates/ailang-codegen/src/lib.rs::is_static_callee` (line ~2189) | A name lowered by a direct `lower_app` arm but unrecognised by `is_static_callee` falls through to the indirect-call path with `UnknownVar` (`UnknownVar` panic in worst case). Every new builtin lowering arm in `lower_app` must have a matching `is_static_callee` entry. |
| `INTERCEPTS` entries in `crates/ailang-codegen/src/intercepts.rs``(intrinsic)` markers (`Term::Intrinsic` bodies) in the kernel-tier sources (`examples/prelude.ail`, `crates/ailang-kernel-stub/src/lib.rs::STUB_AIL`) | A registry entry without a marker is a compiler-supplied body no source declares; a marker without an entry is an `(intrinsic)` fn codegen cannot emit. The bijection (modulo the optimisation-only allowlist — registry entries that intercept the monomorphised `__Int` specialisation of a real-bodied polyfn) is enforced by `intercepts::tests::intercepts_bijection_with_intrinsic_markers`. Every new intrinsic-backed intercept needs both an `INTERCEPTS` entry and an `(intrinsic)` marker; every new optimisation-only intercept needs an `OPTIMISATION_ONLY` allowlist entry. |
Walk procedure: for each milestone-scope commit-range arm
landed in these files (use `git diff <prev-close>..HEAD --` on
@@ -39,8 +39,15 @@ fn prelude_parse_yields_canonical_hash() {
// (body (term-ctor Ordering EQ))) to Term::Intrinsic. The
// canonical-JSON byte stream changes; behaviour is unchanged
// (codegen intercepts by name before the body is inspected).
// 2026-05-29 intrinsic-bodies audit-tidy re-pinned (prior:
// 2ea61ef21ebc1913): the same 13 defs' doc strings were
// rewritten from the stale "placeholder / try_emit_primitive_instance_body"
// wording to honest "compiler-supplied (intrinsic)" wording.
// doc is part of the canonical JSON, so the module hash moves;
// the synthesised mono def-hashes do NOT (synthesise_mono_fn
// sets doc: None).
assert_eq!(
h, "2ea61ef21ebc1913",
h, "b1373a2c69e70a3f",
"prelude module hash drifted; if intentional, capture the new \
hex below + record the why in the commit body."
);
+15 -12
View File
@@ -568,18 +568,21 @@ Concrete state after the mechanisms milestone closed (2026-05-28):
regression pin); the code path no longer hardcodes any module
name as special.
- Codegen intercepts: the pre-existing `try_emit_primitive_instance_body`
hardcoded list is **not yet** migrated into a plugin registry
that migration is deferred to the Series milestone, when there
is the first real external consumer and the mechanism can
graduate from "hardcoded for one case" to "registry for many
cases". Single-consumer registries are premature mechanism.
The reason migration cost is not a decision driver: there is
nothing to break externally, and rewrites inside the workspace
are cheap. Choosing the right design now is the priority; cost
of refactoring tests and fixtures is the project's own problem
and is amortised over zero external consumers.
- Codegen intercepts: the compiler-supplied implementations of the
prelude's primitive Eq/Ord/Float operations live in a registry,
`crates/ailang-codegen/src/intercepts.rs::INTERCEPTS`. A
kernel-tier or prelude definition whose body is the `(intrinsic)`
marker (`Term::Intrinsic`) declares membership in that registry;
codegen routes it through `intercepts::lookup` on its mangled
name. The pairing is locked by
`intercepts_bijection_with_intrinsic_markers`: every intrinsic
marker reachable in the loaded workspace resolves to a registry
entry, and every registry entry not on the optimisation-only
allowlist has a marker. The registry also carries an
optimisation-only class — entries that intercept the
monomorphised `__Int` specialisation of a real-bodied polymorphic
free fn (`lt/le/gt/ge/ne`) for a faster direct `icmp`; those have
a real source body and no marker.
## Coexistence with existing mechanisms
+13 -13
View File
@@ -13,25 +13,25 @@
(instance
(class Eq)
(type (con Int))
(doc "Eq Int. Body is placeholder for round-trip stability; codegen intercept try_emit_primitive_instance_body::eq__Int emits `icmp eq i64` with the alwaysinline attribute.")
(doc "Eq Int. Compiler-supplied (intrinsic) body; codegen emits `icmp eq i64` with the alwaysinline attribute via the intercept registry.")
(method eq
(body (lam (params (typed x a) (typed y a)) (ret (con Bool)) (intrinsic)))))
(instance
(class Eq)
(type (con Bool))
(doc "Eq Bool. Body is placeholder for round-trip stability; codegen intercept try_emit_primitive_instance_body::eq__Bool emits `icmp eq i1` with the alwaysinline attribute.")
(doc "Eq Bool. Compiler-supplied (intrinsic) body; codegen emits `icmp eq i1` with the alwaysinline attribute via the intercept registry.")
(method eq
(body (lam (params (typed x a) (typed y a)) (ret (con Bool)) (intrinsic)))))
(instance
(class Eq)
(type (con Str))
(doc "Eq Str. Body is placeholder for round-trip stability; codegen intercept try_emit_primitive_instance_body::eq__Str overrides it with a call to `@ail_str_eq` and attaches the alwaysinline attribute.")
(doc "Eq Str. Compiler-supplied (intrinsic) body; codegen emits a call to `@ail_str_eq` with the alwaysinline attribute via the intercept registry.")
(method eq
(body (lam (params (typed x a) (typed y a)) (ret (con Bool)) (intrinsic)))))
(instance
(class Eq)
(type (con Unit))
(doc "Eq Unit. Unit is single-inhabitant so all values compare equal. Body is placeholder; codegen intercept try_emit_primitive_instance_body::eq__Unit emits `ret i1 1`.")
(doc "Eq Unit. Unit is single-inhabitant so all values compare equal. Compiler-supplied (intrinsic) body; codegen emits `ret i1 1` via the intercept registry.")
(method eq
(body (lam (params (typed x a) (typed y a)) (ret (con Bool)) (intrinsic)))))
(class Ord
@@ -43,19 +43,19 @@
(instance
(class Ord)
(type (con Int))
(doc "Ord Int. The lambda body shape is a placeholder for round-trip stability; the codegen intercept `try_emit_primitive_instance_body::\"compare__Int\"` emits a three-way `icmp slt` / `icmp eq` branch ladder constructing LT / EQ / GT.")
(doc "Ord Int. Compiler-supplied (intrinsic) body; codegen emits a three-way `icmp slt` / `icmp eq` branch ladder constructing LT / EQ / GT via the intercept registry.")
(method compare
(body (lam (params (typed x a) (typed y a)) (ret (con Ordering)) (intrinsic)))))
(instance
(class Ord)
(type (con Bool))
(doc "Ord Bool. Body lowered via `try_emit_primitive_instance_body::\"compare__Bool\"` — `icmp ult i1` LT-test, `icmp eq i1` EQ-test, GT default.")
(doc "Ord Bool. Compiler-supplied (intrinsic) body; codegen emits `icmp ult i1` LT-test, `icmp eq i1` EQ-test, GT default, via the intercept registry.")
(method compare
(body (lam (params (typed x a) (typed y a)) (ret (con Ordering)) (intrinsic)))))
(instance
(class Ord)
(type (con Str))
(doc "Ord Str. Body lowered via `try_emit_primitive_instance_body::\"compare__Str\"` — `call i32 @ail_str_compare(ptr, ptr)` then branch on slt-0 / eq-0 against the normalised {-1, 0, +1} return.")
(doc "Ord Str. Compiler-supplied (intrinsic) body; codegen emits `call i32 @ail_str_compare(ptr, ptr)` then branches on slt-0 / eq-0 against the normalised {-1, 0, +1} return, via the intercept registry.")
(method compare
(body (lam (params (typed x a) (typed y a)) (ret (con Ordering)) (intrinsic)))))
(class Show
@@ -122,32 +122,32 @@
(params x)
(body (let s (app show x) (do io/print_str s))))
(fn float_eq
(doc "IEEE Float equality. `float_eq x y` returns true iff both operands are non-NaN and bit-equal. Lowered to `fcmp oeq double` via try_emit_primitive_instance_body::float_eq with alwaysinline. Replaces the milestone-deleted polymorphic `==` on Float.")
(doc "IEEE Float equality. `float_eq x y` returns true iff both operands are non-NaN and bit-equal. Compiler-supplied (intrinsic) body; codegen emits `fcmp oeq double` with alwaysinline via the intercept registry. Replaces the milestone-deleted polymorphic `==` on Float.")
(type (fn-type (params (con Float) (con Float)) (ret (con Bool))))
(params x y)
(intrinsic))
(fn float_ne
(doc "IEEE Float disequality. `float_ne nan nan` returns true (unordered-or-not-equal per IEEE-754). Lowered to `fcmp une double`.")
(doc "IEEE Float disequality. `float_ne nan nan` returns true (unordered-or-not-equal per IEEE-754). Compiler-supplied (intrinsic) body; codegen emits `fcmp une double`.")
(type (fn-type (params (con Float) (con Float)) (ret (con Bool))))
(params x y)
(intrinsic))
(fn float_lt
(doc "IEEE Float strict less-than. `float_lt nan x` returns false for any x (unordered). Lowered to `fcmp olt double`.")
(doc "IEEE Float strict less-than. `float_lt nan x` returns false for any x (unordered). Compiler-supplied (intrinsic) body; codegen emits `fcmp olt double`.")
(type (fn-type (params (con Float) (con Float)) (ret (con Bool))))
(params x y)
(intrinsic))
(fn float_le
(doc "IEEE Float less-than-or-equal. Lowered to `fcmp ole double`.")
(doc "IEEE Float less-than-or-equal. Compiler-supplied (intrinsic) body; codegen emits `fcmp ole double`.")
(type (fn-type (params (con Float) (con Float)) (ret (con Bool))))
(params x y)
(intrinsic))
(fn float_gt
(doc "IEEE Float strict greater-than. Lowered to `fcmp ogt double`.")
(doc "IEEE Float strict greater-than. Compiler-supplied (intrinsic) body; codegen emits `fcmp ogt double`.")
(type (fn-type (params (con Float) (con Float)) (ret (con Bool))))
(params x y)
(intrinsic))
(fn float_ge
(doc "IEEE Float greater-than-or-equal. Lowered to `fcmp oge double`.")
(doc "IEEE Float greater-than-or-equal. Compiler-supplied (intrinsic) body; codegen emits `fcmp oge double`.")
(type (fn-type (params (con Float) (con Float)) (ret (con Bool))))
(params x y)
(intrinsic)))