From 6ccc756c0fbee3a289dd6ec4acf29be5881f98a9 Mon Sep 17 00:00:00 2001 From: Brummel Date: Fri, 29 May 2026 17:56:10 +0200 Subject: [PATCH] =?UTF-8?q?audit=20+=20close:=20intrinsic-bodies=20?= =?UTF-8?q?=E2=80=94=20honest=20prelude=20docs=20+=20lockstep=20table=20+?= =?UTF-8?q?=20stale-model=20fix=20(refs=20#9)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 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. --- CLAUDE.md | 1 + .../tests/prelude_module_hash_pin.rs | 9 ++++++- design/models/0007-kernel-extensions.md | 27 ++++++++++--------- examples/prelude.ail | 26 +++++++++--------- 4 files changed, 37 insertions(+), 26 deletions(-) diff --git a/CLAUDE.md b/CLAUDE.md index b3c1d38..6c8222a 100644 --- a/CLAUDE.md +++ b/CLAUDE.md @@ -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 ..HEAD --` on diff --git a/crates/ailang-surface/tests/prelude_module_hash_pin.rs b/crates/ailang-surface/tests/prelude_module_hash_pin.rs index 851230d..8c3d0d3 100644 --- a/crates/ailang-surface/tests/prelude_module_hash_pin.rs +++ b/crates/ailang-surface/tests/prelude_module_hash_pin.rs @@ -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." ); diff --git a/design/models/0007-kernel-extensions.md b/design/models/0007-kernel-extensions.md index b1e51b9..fb344be 100644 --- a/design/models/0007-kernel-extensions.md +++ b/design/models/0007-kernel-extensions.md @@ -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 diff --git a/examples/prelude.ail b/examples/prelude.ail index 29ee981..0d3aa16 100644 --- a/examples/prelude.ail +++ b/examples/prelude.ail @@ -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)))