diff --git a/docs/plans/0107-intrinsic-bodies.2-migration-lock.md b/docs/plans/0107-intrinsic-bodies.2-migration-lock.md new file mode 100644 index 0000000..d71dbfc --- /dev/null +++ b/docs/plans/0107-intrinsic-bodies.2-migration-lock.md @@ -0,0 +1,363 @@ +# intrinsic-bodies.2 — migration + lock — Implementation Plan + +> **Parent spec:** `docs/specs/0055-intrinsic-bodies.md` (committed 8301ca3; .1 shipped at 52ff873) +> +> **For agentic workers:** REQUIRED SUB-SKILL: use the `implement` +> skill to run this plan. Steps use `- [ ]` checkboxes for tracking. + +**Goal:** Migrate the 13 authored prelude dummy bodies to `(intrinsic)`, +rebaseline the two hash pins that move, and replace the one-directional +registry pin with a bijection over the intrinsic-backed class (with the +5-name optimisation-only allowlist) — closing the honesty-rule +infraction the milestone exists to fix. + +**Architecture:** The `(intrinsic)` mechanism shipped in .1; this +iteration is source migration + a stronger lock. The prelude's 7 Eq/Ord +instance-method bodies and 6 `float_*` fn bodies stop carrying +placeholder terms and become `Term::Intrinsic`. Behaviour is unchanged — +codegen already intercepts these by name before the body is inspected +(verified .1 reality), so the placeholder was already dead. Two hash +pins move (prelude module hash; the 6 post-mono eq/compare def-hashes) +and rebaseline. The registry pin upgrades from "the 18 legacy names +resolve" to a bijection: every workspace `(intrinsic)` marker has an +`INTERCEPTS` entry, and every non-allowlisted entry has a marker. + +**Tech Stack:** `examples/prelude.ail` (13 body edits), +`crates/ailang-surface/tests/prelude_module_hash_pin.rs` + +`crates/ail/tests/mono_hash_stability.rs` (rebaselines), +`crates/ailang-codegen/src/intercepts.rs` (bijection pin), +`crates/ailang-codegen/src/lib.rs` (stale-comment cleanup), +`design/contracts/0007-honesty-rule.md` (conditional). + +--- + +## Files this plan creates or modifies + +- Modify: `examples/prelude.ail` — 13 dummy bodies → `(intrinsic)` (lines 18,24,30,36,48,54,60 instance methods; 128,133,138,143,148,153 float fns). +- Modify: `crates/ailang-surface/tests/prelude_module_hash_pin.rs:36` — rebaseline prelude module hash. +- Modify: `crates/ail/tests/mono_hash_stability.rs:56-61` — rebaseline 6 eq/compare def-hashes. +- Modify: `crates/ailang-codegen/src/intercepts.rs:461-506` — replace the one-directional pin with the bijection pin. +- Modify: `crates/ailang-codegen/src/lib.rs:1310-1319` — delete the now-stale dummy-body comment; confirm no body-lowering of an intercepted def. +- Modify (conditional): `design/contracts/0007-honesty-rule.md` — only if it names the prelude dummies. + +--- + +## Task 1: Migrate the 13 authored prelude dummy bodies + +**Files:** +- Modify: `examples/prelude.ail` + +The migration rule by site kind: +- **Instance method** (Eq/Ord): the body is + `(body (lam (params ...) (ret ...) (body )))`. Replace the + *inner* `(body )` with `(intrinsic)`, leaving the lambda's + `(params ...)` and `(ret ...)` — the local signature — intact (Design X). +- **Top-level `float_*` fn**: the body clause is `(body false)`. Replace + the whole `(body false)` clause with `(intrinsic)` (a fn carries + `(intrinsic)` in the body slot, no `(body ...)` wrapper). + +- [ ] **Step 1: Migrate the 7 Eq/Ord instance methods** + +In `examples/prelude.ail`, at each of these inner-body sites, replace +the inner `(body )` with `(intrinsic)`: + +| line | def | inner clause today → becomes | +|---|---|---| +| 18 | Eq Int / eq | `(body false)` → `(intrinsic)` | +| 24 | Eq Bool / eq | `(body false)` → `(intrinsic)` | +| 30 | Eq Str / eq | `(body false)` → `(intrinsic)` | +| 36 | Eq Unit / eq | `(body true)` → `(intrinsic)` | +| 48 | Ord Int / compare | `(body (term-ctor Ordering EQ))` → `(intrinsic)` | +| 54 | Ord Bool / compare | `(body (term-ctor Ordering EQ))` → `(intrinsic)` | +| 60 | Ord Str / compare | `(body (term-ctor Ordering EQ))` → `(intrinsic)` | + +Each line becomes the shape (Eq Int shown): + +```scheme + (method eq + (body (lam (params (typed x a) (typed y a)) (ret (con Bool)) (intrinsic))))) +``` + +(The inner `(body false)` appears on the eq Int/Bool/Str lines AND on +the float lines — edit by the specific line number / surrounding +`(type (con Int|Bool|Str|Unit))` context so the right occurrence is +changed. The `(intrinsic)` form is already ratified by .1's +`examples/kernel_intrinsic_smoke.ail`; this only changes existing +bodies to that form.) + +- [ ] **Step 2: Migrate the 6 float_* fns** + +At each float fn, replace the `(body false)` clause with `(intrinsic)`: + +| line | def | +|---|---| +| 128 | float_eq | +| 133 | float_ne | +| 138 | float_lt | +| 143 | float_le | +| 148 | float_gt | +| 153 | float_ge | + +Each becomes the shape (float_eq shown): + +```scheme + (fn float_eq + (doc "IEEE Float equality. ...") + (type (fn-type (params (con Float) (con Float)) (ret (con Bool)))) + (params x y) + (intrinsic)) +``` + +- [ ] **Step 3: Parse + check the migrated prelude indirectly** + +Run: `cargo run -q -p ail --bin ail -- check examples/hello.ail` +Expected: `ok (...)` exit 0 — any consumer build auto-injects the +prelude, so a parse/check failure in the migrated prelude surfaces here. +(The prelude is embedded via `parse_prelude`; there is no standalone +`ail check examples/prelude.ail` path.) + +- [ ] **Step 4: Round-trip gate green** + +Run: `cargo test -p ailang-surface --test round_trip` +Expected: PASS — the migrated prelude bodies round-trip parse∘print=id. + +- [ ] **Step 5: Behaviour-preservation ratifiers green** + +Run: `cargo test -p ail --test e2e eq_primitives_smoke_compiles_and_runs compare_primitives_smoke_prints_1_2_3_thrice float_compare_smoke_prints_true_true_false eq_ord_polymorphic_runs_end_to_end` +Expected: all PASS — the intercepts emit the same IR; only the now-dead +source body changed. If any of these go red, the migration changed +behaviour and is wrong — STOP. + +--- + +## Task 2: Rebaseline the two moving hash pins + +**Files:** +- Modify: `crates/ailang-surface/tests/prelude_module_hash_pin.rs:36` +- Modify: `crates/ail/tests/mono_hash_stability.rs:56-61` + +The new hashes are not knowable in advance — they are determined by the +migrated prelude bytes. The procedure is: run the pin, read the captured +hash from the failure message, replace the pinned constant. This is +deterministic mechanics, not a placeholder. + +- [ ] **Step 1: Capture + rebaseline the prelude module hash** + +Run: `cargo test -p ailang-surface --test prelude_module_hash_pin` +Expected: FAIL with a message naming the new hash (the pin asserts +`== "af372f28c726f29f"`; it now reports the captured new hash). Replace +the constant at `prelude_module_hash_pin.rs:36` with the captured value. + +- [ ] **Step 2: Re-run the prelude hash pin green** + +Run: `cargo test -p ailang-surface --test prelude_module_hash_pin` +Expected: PASS. + +- [ ] **Step 3: Capture + rebaseline the 6 eq/compare mono def-hashes** + +Run: `cargo test -p ail --test mono_hash_stability primitive_eq_ord_mono_symbol_hashes_stay_bit_identical` +Expected: FAIL — each of `eq__Int/eq__Bool/eq__Str/compare__Int/compare__Bool/compare__Str` +reports a drifted hash (the synthesised body flipped from the dummy term +to `Term::Intrinsic`). For each `(sym, pin)` pair at lines 56-61, replace +the pinned hash with the captured value from the failure message. The +4 `show__*` pins (lines 100-103) are NOT touched — Show bodies are real +and unchanged. + +- [ ] **Step 4: Re-run the mono hash pin green** + +Run: `cargo test -p ail --test mono_hash_stability` +Expected: PASS (both `primitive_eq_ord_*` and `primitive_show_*`). + +--- + +## Task 3: Bijection pin over the intrinsic-backed class + +**Files:** +- Modify: `crates/ailang-codegen/src/intercepts.rs` (the `#[cfg(test)] mod tests`, currently 461-506) + +- [ ] **Step 1: Replace the one-directional pin with the bijection pin** + +In `crates/ailang-codegen/src/intercepts.rs`, the in-source +`#[cfg(test)] mod tests` currently holds `registry_contains_all_legacy_arms` +(uses only `super::lookup`). Replace that test with the bijection pin +below. It walks the two kernel-tier source modules (prelude + +kernel_stub) pre-mono for `Term::Intrinsic` markers, recovers each +marker's mangled name (`mono_symbol` for instance methods; the fn name +directly for top-level fns), and asserts the bijection against +`INTERCEPTS` modulo the optimisation-only allowlist. + +Dependencies used (all verified reachable from this in-source test: +`ailang-surface` is a dev-dep with no cycle back to codegen; +`ailang-check` is a normal dep with `pub mod mono`; `ailang-core` is a +normal dep): + +```rust +#[cfg(test)] +mod tests { + use super::{lookup, INTERCEPTS}; + use ailang_check::mono::mono_symbol; + use ailang_core::ast::{Def, Term}; + use std::collections::BTreeSet; + + /// 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 intercepts_bijection_with_intrinsic_markers() { + let markers = workspace_intrinsic_markers(); + let registry: BTreeSet = + INTERCEPTS.iter().map(|i| i.name.to_string()).collect(); + + // (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() + .filter(|n| lookup(n).is_none()) + .collect(); + assert!( + stale_allow.is_empty(), + "optimisation-only allowlist names not in INTERCEPTS: {stale_allow:?}" + ); + } +} +``` + +- [ ] **Step 2: Run the bijection pin** + +Run: `cargo test -p ailang-codegen --lib intercepts::tests::intercepts_bijection_with_intrinsic_markers` +Expected: PASS. After Task 1, the 13 prelude markers + `answer` (14 +intrinsic-backed) cover the 14 non-allowlisted INTERCEPTS entries, and +the 5 `*__Int` are allowlisted. If (B) reports an orphan entry, a +prelude site was missed in Task 1; if (A) reports an orphan marker, a +marker has no registered intercept (a real bug). + +- [ ] **Step 3: Confirm the old pin name is gone / no dangling reference** + +Run: `grep -rn "registry_contains_all_legacy_arms" crates/` +Expected: no matches (the test was replaced). If any doc comment or +other test referenced it by name, update that reference. + +--- + +## Task 4: Dead-path confirmation + stale-comment cleanup + +**Files:** +- Modify: `crates/ailang-codegen/src/lib.rs:1310-1319` +- Modify (conditional): `design/contracts/0007-honesty-rule.md` + +- [ ] **Step 1: Confirm no codegen path lowers an intercepted body** + +Read `crates/ailang-codegen/src/lib.rs:1310-1340`. Confirm the shape: +`try_emit_primitive_instance_body(&f.name, ...)` is called first +(name-based intercept), and `lower_term(&f.body)` is only reached under +`if !body_was_intercepted`. Since every migrated def's body is now +`Term::Intrinsic` AND its name is in INTERCEPTS, the intercept always +fires first and `lower_term` is never reached for it. No code change is +required for the path itself — this is the confirmation the spec +(§ Architecture point 8) calls for. + +- [ ] **Step 2: Delete the now-stale dummy-body comment** + +At `lib.rs:1310-1319`, the comment block describes skipping "the normal +body-lowering block below" for intercepted bodies and references the +historical dummy. Update it to state the current reality: an intrinsic +body is intercepted by name; a `Term::Intrinsic` reaching `lower_term` +is the internal-error guard (added in .1), not a body to lower. Remove +any sentence implying a live dummy body is lowered-then-discarded. + +- [ ] **Step 3: Check whether the honesty-rule contract names the dummies** + +Run: `grep -n "dummy\|placeholder\|body false\|intrinsic" design/contracts/0007-honesty-rule.md` +Expected: determine whether 0007 references the prelude dummy bodies +specifically. If it does NOT (recon's finding — it is a general +present-tense honesty rule), make NO edit and note in the iter that +0007 needed none. If it DOES name them, update that sentence to reflect +that the infraction is closed (the bodies are now `(intrinsic)`, +honestly compiler-supplied). Do not invent an edit where none is needed. + +- [ ] **Step 4: Build clean** + +Run: `cargo build --workspace` +Expected: compiles, 0 errors (Step 2 is a comment edit; no behavioural change). + +--- + +## Final gate + +- [ ] **Step F1: Full workspace test** + +Run: `cargo test --workspace` +Expected: all green. Baseline 669 (post-.1). This iteration replaces one +test (registry_contains_all_legacy_arms → intercepts_bijection_with_intrinsic_markers, +net 0) and rebaselines hashes (no count change). Expected ≈669 passing, +0 failed. The behaviour-preservation ratifiers (Task 1 Step 5) and both +hash pins (Task 2) are green. + +- [ ] **Step F2: Regression scripts** + +Run: `bench/check.py && bench/compile_check.py` +Expected: no regression versus baseline — the migration is +behaviour-preserving (identical emitted IR).