From caa3618c3e3a6970a169b053d372c7df0e3eec93 Mon Sep 17 00:00:00 2001 From: Brummel Date: Fri, 29 May 2026 17:46:50 +0200 Subject: [PATCH] =?UTF-8?q?iter=20intrinsic-bodies.2-migration-lock=20(DON?= =?UTF-8?q?E=204/4):=20prelude=20=E2=86=92=20(intrinsic)=20+=20bijection?= =?UTF-8?q?=20pin=20(refs=20#9)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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. --- crates/ail/tests/mono_hash_stability.rs | 19 ++- crates/ailang-codegen/src/intercepts.rs | 113 ++++++++++++------ crates/ailang-codegen/src/lib.rs | 18 +-- .../tests/prelude_module_hash_pin.rs | 9 +- examples/prelude.ail | 26 ++-- 5 files changed, 124 insertions(+), 61 deletions(-) diff --git a/crates/ail/tests/mono_hash_stability.rs b/crates/ail/tests/mono_hash_stability.rs index b1a0185..f213964 100644 --- a/crates/ail/tests/mono_hash_stability.rs +++ b/crates/ail/tests/mono_hash_stability.rs @@ -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 { diff --git a/crates/ailang-codegen/src/intercepts.rs b/crates/ailang-codegen/src/intercepts.rs index 2041b02..24974ed 100644 --- a/crates/ailang-codegen/src/intercepts.rs +++ b/crates/ailang-codegen/src/intercepts.rs @@ -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 { + 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 = + 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:?}" ); } } diff --git a/crates/ailang-codegen/src/lib.rs b/crates/ailang-codegen/src/lib.rs index 18cccfb..0caf910 100644 --- a/crates/ailang-codegen/src/lib.rs +++ b/crates/ailang-codegen/src/lib.rs @@ -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). diff --git a/crates/ailang-surface/tests/prelude_module_hash_pin.rs b/crates/ailang-surface/tests/prelude_module_hash_pin.rs index 622cb96..851230d 100644 --- a/crates/ailang-surface/tests/prelude_module_hash_pin.rs +++ b/crates/ailang-surface/tests/prelude_module_hash_pin.rs @@ -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." ); diff --git a/examples/prelude.ail b/examples/prelude.ail index 139f7ab..29ee981 100644 --- a/examples/prelude.ail +++ b/examples/prelude.ail @@ -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)))