Brummel/AILang
1
0
Fork 0
Code Issues 29 Pull Requests Actions Packages Projects Releases Wiki Activity

plan: intrinsic-bodies.2-migration-lock — 4-task prelude migration + bijection pin (refs #9)

Browse Source 
Decomposes intrinsic-bodies.2 (parent spec § Architecture points 6-8)
into 4 tasks + a final gate:

  Task 1 — migrate the 13 authored prelude dummy bodies to (intrinsic):
    7 Eq/Ord instance methods (inner (body false)/(body true)/
    (body (term-ctor Ordering EQ)) → (intrinsic), Design X lambda-body
    placement) + 6 float_* fns ((body false) → (intrinsic)). Gated by
    round-trip + the 4 eq/compare/float E2E ratifiers staying green
    (behaviour-preserving: the intercepts emit identical IR).
  Task 2 — rebaseline the two moving hash pins: prelude_module_hash_pin
    (prelude module hash) and mono_hash_stability's 6 eq/compare
    def-hashes (capture-from-failure, replace the constant). The 4
    show__* pins do NOT move.
  Task 3 — replace the one-directional registry_contains_all_legacy_arms
    pin with intercepts_bijection_with_intrinsic_markers: an in-source
    test that walks prelude + kernel_stub pre-mono for Term::Intrinsic
    markers, recovers mangled names (mono_symbol for instance methods,
    fn name for top-level), and asserts the bijection over the
    intrinsic-backed class (14) with the 5-name *__Int optimisation-only
    allowlist. Both directions + a stale-allowlist guard.
  Task 4 — confirm no codegen path lowers an intercepted body (already
    true post-.1: intercept-by-name precedes lower_term), delete the
    stale dummy-body comment at lib.rs:1310-1319, and conditionally edit
    0007-honesty-rule.md ONLY if it names the dummies (recon: it does
    not — a general rule; no forced edit).

Recon-driven plan decisions:

1. The bijection pin lives in intercepts.rs's in-source #[cfg(test)]
   mod tests, NOT a crates/ail/tests integration test. Visibility
   forces it: the pin needs INTERCEPTS (pub(crate) in codegen, in-source
   only) AND the parse hops (ailang-surface dev-dep). Verified
   ailang-surface does not dep ailang-codegen, so there is no
   dev-dep cycle blocking the in-source test from calling parse_prelude
   (the dev-dep-cycle hazard that bit pd.2.4/pd.3.1 does not apply
   here — that was the ailang-core <-> ailang-surface edge).
2. The pin walks PRE-mono (parse_prelude/parse_kernel_stub) and
   reconstructs mangled names via mono_symbol, rather than walking
   post-mono. Post-mono only synthesises USED mono symbols, so a
   post-mono walk would miss any instance method the pin's entry
   fixture does not exercise (e.g. eq__Unit). Pre-mono + mono_symbol
   sees all 14 markers unconditionally.
3. Task 2's hashes are capture-from-failure, not pre-computed — the new
   prelude bytes determine them. The old->new values get recorded in
   the iter commit body by the Boss.

All verification filter strings checked against the tree: the 4 E2E
ratifier fn names, the mono pin name, and the prelude pin target all
resolve to ≥1 real test. No ail/ail-json/ll fenced block in the plan
(the migrated-form snippets are scheme fragments — the (intrinsic) form
is already ratified by .1's kernel_intrinsic_smoke.ail), so the
parse-bytes gate is a documented no-op.

Handoff target: skills/implement on docs/plans/0107-intrinsic-bodies.2-migration-lock.md
This commit is contained in:
Brummel
2026-05-29 17:37:45 +02:00
parent 8301ca3ee8
commit 298fc2d36f
1 changed files with 363 additions and 0 deletions
Download Patch File Download Diff File Expand all files Collapse all files
docs/plans/0107-intrinsic-bodies.2-migration-lock.md
+363
View File
@@ -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 <dummy>)))`. Replace the
*inner* `(body <dummy>)` 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 <dummy>)` 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<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 intercepts_bijection_with_intrinsic_markers() {
let markers = workspace_intrinsic_markers();
let registry: BTreeSet<String> =
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).