iter intrinsic-bodies.2-migration-lock (DONE 4/4): prelude → (intrinsic) + bijection pin (refs #9)
Second and final iteration of the intrinsic-bodies milestone. Migrates
the 13 authored prelude dummy bodies to (intrinsic), rebaselines the two
hash pins that move, and locks the registry to the source with a
bijection. Behaviour-preserving: the codegen intercepts emit identical
IR; the prelude placeholder bodies were already dead (intercepted by
name before lower_term, since raw-buf.1).
What landed (4 tasks):
Task 1 — examples/prelude.ail: 13 authored dummy bodies → (intrinsic).
7 Eq/Ord instance methods (eq Int/Bool/Str/Unit, compare
Int/Bool/Str) keep their lambda shell (params/ret = the method's
local signature, Design X); the inner (body false)/(body true)/
(body (term-ctor Ordering EQ)) becomes (intrinsic). 6 float_* fns
((body false) → (intrinsic) in the fn body slot). The honesty-rule
infraction the milestone exists to fix is now closed: no prelude
body lies about what runs.
Task 2 — hash rebaselines (the prelude bytes changed):
prelude module hash af372f28c726f29f → 2ea61ef21ebc1913
eq__Int 86ed4988438924d3 → cc7b99b63d1e44ae
eq__Bool d62d4d8c51f433f8 → fd0412f127986512
eq__Str 3d32f377c66b03e0 → fa269285754a52da
compare__Int 6d6c20520766368b → 0a02bd9effc9746c
compare__Bool 02b64e8fadc913eb → d0dc108dacf4e543
compare__Str 9645929d53cd3cc9 → d1419595dc52a456
The 4 show__* mono pins did NOT move (Show bodies are real).
Task 3 — intercepts.rs: registry_contains_all_legacy_arms (one-
directional, hardcoded 18-name list) replaced by
intercepts_bijection_with_intrinsic_markers. The in-source test
walks prelude + kernel_stub pre-mono for Term::Intrinsic markers,
recovers each marker's codegen symbol (mono_symbol(method, type) for
instance methods; the fn name for top-level float_*/answer), and
asserts a bijection over the intrinsic-backed class: (A) every
marker resolves to an INTERCEPTS entry, (B) every INTERCEPTS entry
not on the optimisation-only allowlist has a marker, plus a guard
that the allowlist names are themselves registered. The allowlist is
the 5 *__Int icmp-family entries, which intercept the monomorphised
specialisation of the real-bodied polymorphic lt/le/gt/ge/ne — an
optimisation, not a compiler-supplied body, so no marker. The pin
passing independently confirms Task 1 missed no prelude site.
Task 4 — confirmed no codegen path lowers an intercepted body (already
true since raw-buf.1: try_emit_primitive_instance_body matches by
name before f.body is inspected). Refreshed the now-accurate comment
at lib.rs:1310-1319. design/contracts/0007-honesty-rule.md needed NO
edit — it is a general present-tense rule and does not name the
prelude dummies (confirmed by grep), so editing it would have been
invented work.
Verification:
cargo test --workspace → 669 passed, 0 failed (post-.1 baseline held;
one test replaced net-0).
Behaviour-preservation ratifiers GREEN (the safety net):
eq_primitives_smoke_compiles_and_runs,
compare_primitives_smoke_prints_1_2_3_thrice (e2e.rs);
float_compare_smoke_prints_true_true_false (float_compare_smoke_e2e.rs);
eq_ord_polymorphic_runs_end_to_end (eq_ord_e2e.rs).
Bijection pin GREEN. Both hash pins GREEN at the new baselines.
bench/check.py + compile_check.py → 0 regressed.
Plan-text imprecision (no outcome impact, noted for the record): Task 1
Step 5 wrote `--test e2e` for all four ratifiers, but
float_compare_smoke_prints_true_true_false and
eq_ord_polymorphic_runs_end_to_end live in their own test targets
(float_compare_smoke_e2e.rs, eq_ord_e2e.rs). The verification-filter
self-review checked that the fn names exist, not that they sit in the
named target — a sharper form of the filter-zero discipline. The
implementer ran each in its real target; all four green.
Milestone intrinsic-bodies is now feature-complete (.1 mechanism +
.2 migration+lock). Audit + close follow.
This commit is contained in:
@@ -52,13 +52,20 @@ fn primitive_eq_ord_mono_symbol_hashes_stay_bit_identical() {
|
||||
// emits the actual `icmp` / `@ail_str_eq` call). The three
|
||||
// `compare__*` hashes were unchanged — those bodies were already
|
||||
// placeholder Ordering ctors.
|
||||
// 2026-05-29 intrinsic-bodies.2 re-pinned all six: the prelude
|
||||
// Eq/Ord instance-method bodies migrated from placeholder terms
|
||||
// ((body false)/(body true)/(term-ctor Ordering EQ)) to
|
||||
// Term::Intrinsic, so the mono-synthesised eq__T/compare__T body
|
||||
// bytes flip. Behaviour is unchanged — codegen intercepts these
|
||||
// by name; the body is signature-only. The four show__* pins
|
||||
// below do NOT move (Show instance bodies are real, unchanged).
|
||||
let pins: &[(&str, &str)] = &[
|
||||
("eq__Int", "86ed4988438924d3"),
|
||||
("eq__Bool", "d62d4d8c51f433f8"),
|
||||
("eq__Str", "3d32f377c66b03e0"),
|
||||
("compare__Int", "6d6c20520766368b"),
|
||||
("compare__Bool", "02b64e8fadc913eb"),
|
||||
("compare__Str", "9645929d53cd3cc9"),
|
||||
("eq__Int", "cc7b99b63d1e44ae"),
|
||||
("eq__Bool", "fd0412f127986512"),
|
||||
("eq__Str", "fa269285754a52da"),
|
||||
("compare__Int", "0a02bd9effc9746c"),
|
||||
("compare__Bool", "d0dc108dacf4e543"),
|
||||
("compare__Str", "d1419595dc52a456"),
|
||||
];
|
||||
|
||||
for (sym, pin) in pins {
|
||||
|
||||
@@ -460,47 +460,92 @@ pub(crate) fn emit_answer(emitter: &mut Emitter<'_>) -> Result<()> {
|
||||
|
||||
#[cfg(test)]
|
||||
mod tests {
|
||||
use super::lookup;
|
||||
use super::{lookup, INTERCEPTS};
|
||||
use ailang_check::mono::mono_symbol;
|
||||
use ailang_core::ast::{Def, Term};
|
||||
use std::collections::BTreeSet;
|
||||
|
||||
/// Pin: every name that was a match arm in the legacy
|
||||
/// `try_emit_primitive_instance_body` (before raw-buf.1)
|
||||
/// must resolve to a registered Intercept. If this test
|
||||
/// goes red, a name was dropped during migration AND/OR
|
||||
/// removed from the registry without the dispatch wrapper
|
||||
/// being audited to confirm no consumer still depends on
|
||||
/// it.
|
||||
/// INTERCEPTS entries that intercept the monomorphised `__Int`
|
||||
/// specialisation of a polymorphic free fn carrying a REAL body
|
||||
/// (`ne = not (eq x y)`; `lt/le/gt/ge = match compare ...`). These
|
||||
/// are an optimisation class, not a compiler-supplied body — they
|
||||
/// legitimately have no `(intrinsic)` marker. Any change here is a
|
||||
/// deliberate registry-policy decision, not drift.
|
||||
const OPTIMISATION_ONLY: &[&str] =
|
||||
&["lt__Int", "le__Int", "gt__Int", "ge__Int", "ne__Int"];
|
||||
|
||||
/// Collect the mangled name of every `(intrinsic)` marker reachable
|
||||
/// in the kernel-tier source modules (prelude + kernel_stub — the
|
||||
/// only modules where an intrinsic body is legal today).
|
||||
fn workspace_intrinsic_markers() -> BTreeSet<String> {
|
||||
let mut markers = BTreeSet::new();
|
||||
for module in [
|
||||
ailang_surface::parse_prelude(),
|
||||
ailang_surface::parse_kernel_stub(),
|
||||
] {
|
||||
for def in &module.defs {
|
||||
match def {
|
||||
// Top-level intrinsic fn: name is already the symbol
|
||||
// (float_eq, answer, ...).
|
||||
Def::Fn(f) if matches!(f.body, Term::Intrinsic) => {
|
||||
markers.insert(f.name.clone());
|
||||
}
|
||||
// Instance method whose lambda body is intrinsic:
|
||||
// the codegen symbol is mono_symbol(method, type).
|
||||
Def::Instance(inst) => {
|
||||
for m in &inst.methods {
|
||||
if let Term::Lam { body, .. } = &m.body {
|
||||
if matches!(**body, Term::Intrinsic) {
|
||||
markers.insert(mono_symbol(&m.name, &inst.type_));
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
_ => {}
|
||||
}
|
||||
}
|
||||
}
|
||||
markers
|
||||
}
|
||||
|
||||
/// Bijection over the intrinsic-backed class:
|
||||
/// (A) every workspace intrinsic marker resolves to an INTERCEPTS entry;
|
||||
/// (B) every INTERCEPTS entry not on the optimisation-only allowlist
|
||||
/// has a workspace intrinsic marker.
|
||||
#[test]
|
||||
fn registry_contains_all_legacy_arms() {
|
||||
let legacy_names = [
|
||||
"eq__Str",
|
||||
"compare__Int",
|
||||
"compare__Bool",
|
||||
"compare__Str",
|
||||
"eq__Int",
|
||||
"eq__Bool",
|
||||
"eq__Unit",
|
||||
"float_eq",
|
||||
"float_ne",
|
||||
"float_lt",
|
||||
"float_le",
|
||||
"float_gt",
|
||||
"float_ge",
|
||||
"lt__Int",
|
||||
"le__Int",
|
||||
"gt__Int",
|
||||
"ge__Int",
|
||||
"ne__Int",
|
||||
];
|
||||
fn intercepts_bijection_with_intrinsic_markers() {
|
||||
let markers = workspace_intrinsic_markers();
|
||||
let registry: BTreeSet<String> =
|
||||
INTERCEPTS.iter().map(|i| i.name.to_string()).collect();
|
||||
|
||||
let missing: Vec<&str> = legacy_names
|
||||
// (A) no intrinsic marker without a codegen intercept
|
||||
let orphan_markers: Vec<&String> =
|
||||
markers.iter().filter(|m| lookup(m).is_none()).collect();
|
||||
assert!(
|
||||
orphan_markers.is_empty(),
|
||||
"intrinsic markers with no INTERCEPTS entry: {orphan_markers:?}"
|
||||
);
|
||||
|
||||
// (B) no non-allowlisted intercept without an intrinsic marker
|
||||
let orphan_entries: Vec<&String> = registry
|
||||
.iter()
|
||||
.filter(|n| !OPTIMISATION_ONLY.contains(&n.as_str()))
|
||||
.filter(|n| !markers.contains(*n))
|
||||
.collect();
|
||||
assert!(
|
||||
orphan_entries.is_empty(),
|
||||
"INTERCEPTS entries with no intrinsic marker (and not optimisation-only): {orphan_entries:?}"
|
||||
);
|
||||
|
||||
// Guard: the allowlist names must actually be in the registry —
|
||||
// a stale allowlist entry (name removed from INTERCEPTS) is drift.
|
||||
let stale_allow: Vec<&&str> = OPTIMISATION_ONLY
|
||||
.iter()
|
||||
.copied()
|
||||
.filter(|n| lookup(n).is_none())
|
||||
.collect();
|
||||
|
||||
assert!(
|
||||
missing.is_empty(),
|
||||
"registry is missing legacy intercept names: {missing:?}"
|
||||
stale_allow.is_empty(),
|
||||
"optimisation-only allowlist names not in INTERCEPTS: {stale_allow:?}"
|
||||
);
|
||||
}
|
||||
}
|
||||
|
||||
@@ -1307,13 +1307,17 @@ impl<'a> Emitter<'a> {
|
||||
self.body.push_str(&sig);
|
||||
self.start_block("entry");
|
||||
|
||||
// primitive-instance body intercept. Returns true if
|
||||
// the body was emitted in full (including the closing `}\n\n`).
|
||||
// When that fires we skip the normal body-lowering block below
|
||||
// but still fall through to deferred-thunk flush + closure-pair
|
||||
// emission, so the intercepted fn participates in the same
|
||||
// post-body machinery as every other top-level fn (iter 23.2.2
|
||||
// fixup: previously this short-circuited past
|
||||
// primitive-instance body intercept. Returns true if the body
|
||||
// was emitted in full (including the closing `}\n\n`). A
|
||||
// compiler-supplied body is an `(intrinsic)` marker
|
||||
// (`Term::Intrinsic`) whose name resolves through the intercept
|
||||
// registry — the intercept is matched by name here, before the
|
||||
// body is ever inspected, so the marker is never lowered. When
|
||||
// the intercept fires we skip the normal body-lowering block
|
||||
// below but still fall through to deferred-thunk flush +
|
||||
// closure-pair emission, so the intercepted fn participates in
|
||||
// the same post-body machinery as every other top-level fn
|
||||
// (iter 23.2.2 fixup: previously this short-circuited past
|
||||
// `emit_adapter_and_static_closure`, leaving the fn without a
|
||||
// closure-pair symbol — a footgun the moment any caller
|
||||
// referenced it by value).
|
||||
|
||||
@@ -32,8 +32,15 @@ fn prelude_parse_yields_canonical_hash() {
|
||||
// protects (12 free fns callable bare in every consumer) is
|
||||
// unchanged — only the code path migrates from the hardcoded
|
||||
// `&["prelude"]` literal to the kernel-flag filter.
|
||||
// 2026-05-29 intrinsic-bodies.2 re-pinned (prior:
|
||||
// af372f28c726f29f): the 13 authored prelude dummy bodies
|
||||
// (7 Eq/Ord instance methods + 6 float_* fns) migrate from
|
||||
// placeholder terms ((body false)/(body true)/
|
||||
// (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).
|
||||
assert_eq!(
|
||||
h, "af372f28c726f29f",
|
||||
h, "2ea61ef21ebc1913",
|
||||
"prelude module hash drifted; if intentional, capture the new \
|
||||
hex below + record the why in the commit body."
|
||||
);
|
||||
|
||||
+13
-13
@@ -15,25 +15,25 @@
|
||||
(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.")
|
||||
(method eq
|
||||
(body (lam (params (typed x a) (typed y a)) (ret (con Bool)) (body false)))))
|
||||
(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.")
|
||||
(method eq
|
||||
(body (lam (params (typed x a) (typed y a)) (ret (con Bool)) (body false)))))
|
||||
(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.")
|
||||
(method eq
|
||||
(body (lam (params (typed x a) (typed y a)) (ret (con Bool)) (body false)))))
|
||||
(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`.")
|
||||
(method eq
|
||||
(body (lam (params (typed x a) (typed y a)) (ret (con Bool)) (body true)))))
|
||||
(body (lam (params (typed x a) (typed y a)) (ret (con Bool)) (intrinsic)))))
|
||||
(class Ord
|
||||
(param a)
|
||||
(superclass (class Eq) (type a))
|
||||
@@ -45,19 +45,19 @@
|
||||
(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.")
|
||||
(method compare
|
||||
(body (lam (params (typed x a) (typed y a)) (ret (con Ordering)) (body (term-ctor Ordering EQ))))))
|
||||
(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.")
|
||||
(method compare
|
||||
(body (lam (params (typed x a) (typed y a)) (ret (con Ordering)) (body (term-ctor Ordering EQ))))))
|
||||
(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.")
|
||||
(method compare
|
||||
(body (lam (params (typed x a) (typed y a)) (ret (con Ordering)) (body (term-ctor Ordering EQ))))))
|
||||
(body (lam (params (typed x a) (typed y a)) (ret (con Ordering)) (intrinsic)))))
|
||||
(class Show
|
||||
(param a)
|
||||
(doc "Producer of a human-readable Str representation. Ships in milestone 24 with primitive instances for Int/Bool/Str/Float; user types declare their own instance.")
|
||||
@@ -125,29 +125,29 @@
|
||||
(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.")
|
||||
(type (fn-type (params (con Float) (con Float)) (ret (con Bool))))
|
||||
(params x y)
|
||||
(body false))
|
||||
(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`.")
|
||||
(type (fn-type (params (con Float) (con Float)) (ret (con Bool))))
|
||||
(params x y)
|
||||
(body false))
|
||||
(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`.")
|
||||
(type (fn-type (params (con Float) (con Float)) (ret (con Bool))))
|
||||
(params x y)
|
||||
(body false))
|
||||
(intrinsic))
|
||||
(fn float_le
|
||||
(doc "IEEE Float less-than-or-equal. Lowered to `fcmp ole double`.")
|
||||
(type (fn-type (params (con Float) (con Float)) (ret (con Bool))))
|
||||
(params x y)
|
||||
(body false))
|
||||
(intrinsic))
|
||||
(fn float_gt
|
||||
(doc "IEEE Float strict greater-than. Lowered to `fcmp ogt double`.")
|
||||
(type (fn-type (params (con Float) (con Float)) (ret (con Bool))))
|
||||
(params x y)
|
||||
(body false))
|
||||
(intrinsic))
|
||||
(fn float_ge
|
||||
(doc "IEEE Float greater-than-or-equal. Lowered to `fcmp oge double`.")
|
||||
(type (fn-type (params (con Float) (con Float)) (ret (con Bool))))
|
||||
(params x y)
|
||||
(body false)))
|
||||
(intrinsic)))
|
||||
|
||||
Reference in New Issue
Block a user