spec: intrinsic-bodies — correct .2 count + bijection split (refs #9)

Forward-fix on 5b66de7, prompted by plan-recon for intrinsic-bodies.2.
Two spec-vs-reality gaps in the .2 (migration + lock) sections, both
caught before the .2 plan was written:

1. Count. The spec said "18 dummy bodies" migrate to (intrinsic). That
   conflated the INTERCEPTS entry count with authored prelude bodies.
   Reality: examples/prelude.ail carries 13 authored dummy bodies — the
   7 Eq/Ord instance methods (eq Int/Bool/Str/Unit, compare
   Int/Bool/Str) + the 6 float_* free fns. The registry has 19 entries
   (18 legacy + the .1 `answer`); the other 6 are not prelude dummies.

2. The strict bijection cannot hold. lt__Int/le__Int/gt__Int/ge__Int/
   ne__Int (5 INTERCEPTS entries) intercept the monomorphised __Int
   specialisations of the polymorphic free fns lt/le/gt/ge/ne, which
   carry REAL bodies in the prelude (ne = (app not (app eq x y)); the
   four ordering helpers are (match (app compare x y) ...)). Those
   bodies are honest and live — lowered for every non-Int instantiation;
   only the Int specialisation is intercepted for a faster direct icmp.
   They are an optimisation class, not a compiler-supplied-body class:
   no lie, no source body to replace, no (intrinsic) marker. A strict
   bijection over all INTERCEPTS entries would be red for these 5.

Corrections:
- § Architecture point 6: 13 authored prelude sites (named), with the
  5 icmp-family + `answer` explicitly listed as non-prelude / not
  migrated and why.
- § Architecture point 7: the pin splits the registry into
  intrinsic-backed (13 prelude markers + answer = 14) and
  optimisation-only (the 5 *__Int, an explicit documented allowlist).
  The bijection holds over the intrinsic-backed class only; the pin
  loads the workspace + monomorphises to recover mangled names for the
  marker direction.
- § Architecture point 8: reframed from "dead-path removal" to
  "dead-path confirmation" — .1's intercept-by-name already bypasses
  the dummy body before lower_term sees it (committed reality at
  52ff873), so .2 confirms no path lowers an intercepted body and
  deletes stale comments; the .1 Term::Intrinsic escape-guards stay.
- § Components + § Testing: the two moving hash pins named
  (prelude_module_hash_pin.rs; mono_hash_stability.rs's 6 eq/compare
  pins move, its 4 show pins do not); hash_pin.rs carries no
  prelude-derived hash. IR snapshots do not change.

Grounding-check PASS on all five corrected .2 claims against the
shipped .1 baseline (count, the 5 real-bodied helpers, the three hash
pins' behaviour, the already-dead path, the bijection-pin pipeline
reachability). No ail/ail-json/ll fenced block changed — parse-gate a
documented no-op for this revision.

The deeper observation this surfaced — that INTERCEPTS conflates two
concepts (compiler-supplied bodies vs. optimisation of a real body) —
is noted but NOT resolved here; splitting the registry is out of scope
for intrinsic-bodies and would be its own milestone.

docs/specs/0055-intrinsic-bodies.md

@@ -106,21 +106,58 @@ Three landing points, two iterations.
 
 **Iteration `intrinsic-bodies.2` — the migration + the lock.**
 
-6. **Prelude migration.** All eighteen dummy bodies (the `eq__*`,
-   `compare__*`, and `lt|le|gt|ge|ne__*` instance methods enumerated
-   by `intercepts::INTERCEPTS`) swap their `(body <dummy>)` for
-   `(intrinsic)`.
-7. **Hard-lockstep pin.** A test asserts a **bijection** between
-   `INTERCEPTS` entries and `(intrinsic)` definitions reachable in
-   the loaded workspace (prelude + kernel-tier modules): every
-   registry entry has exactly one intrinsic marker and vice versa.
-   Drift in either direction is a red test. This extends the
+6. **Prelude migration.** The **thirteen authored dummy bodies** in
+   `examples/prelude.ail` swap their inner `(body <dummy>)` for
+   `(intrinsic)`: the seven Eq/Ord instance methods (`eq` for
+   Int/Bool/Str/Unit, `compare` for Int/Bool/Str) and the six `float_*`
+   free fns (`float_eq/ne/lt/le/gt/ge`). These are exactly the
+   `INTERCEPTS` entries that today carry a placeholder body a reader
+   would mistake for the implementation.
+
+   **Not migrated, and why** (the count reconciliation — the registry
+   has nineteen entries, not eighteen-all-dummies):
+   - `lt__Int`, `le__Int`, `gt__Int`, `ge__Int`, `ne__Int` (5) intercept
+     the *monomorphised* `__Int` specialisations of the polymorphic free
+     fns `lt/le/gt/ge/ne`, which carry **real bodies** in the prelude
+     (`(match (app compare x y) …)`, `(app not (app eq x y))`). Those
+     bodies are honest and live — they are lowered for every non-`Int`
+     instantiation; only the `Int` specialisation is intercepted for a
+     faster direct `icmp`. These are an **optimisation class**, not a
+     compiler-supplied-body class: there is no lie to fix and no source
+     body to replace, so they get **no** `(intrinsic)` marker.
+   - `answer` (1) is the `.1` ratifier, already `(intrinsic)` in
+     `STUB_AIL` — not a prelude site.
+
+   So: 13 prelude migrations + 5 optimisation-class entries + 1 already
+   migrated = 19 `INTERCEPTS` entries.
+7. **Hard-lockstep pin.** The registry splits into two classes: an
+   entry is **intrinsic-backed** when a `(intrinsic)` marker in the
+   loaded workspace resolves to its mangled name (the 13 prelude
+   migrations + `answer` = 14), or **optimisation-only** when it
+   intercepts a real-bodied fn's specialisation (the 5 `*__Int` icmp
+   family). The pin asserts a **bijection over the intrinsic-backed
+   class**: every workspace `(intrinsic)` marker has exactly one
+   `INTERCEPTS` entry, and every `INTERCEPTS` entry *not* on the
+   explicit optimisation-only allowlist has exactly one workspace
+   marker. The optimisation-only set is an explicit, documented
+   allowlist in the pin (the 5 names); adding a registry entry that is
+   neither marker-backed nor allowlisted is a red test, as is an
+   intrinsic marker with no entry. This extends the
    `registry_contains_all_legacy_arms` pin from raw-buf.1 from a
    one-directional name check to a two-directional source↔registry
    bijection.
-8. **Dead-path removal.** The dummy-body-execution path for
-   intercepted definitions is removed; nothing emits it once the
-   migration lands.
+8. **Dead-path confirmation.** `.1` already routes every intercepted
+   def by name (`try_emit_primitive_instance_body` consults
+   `intercepts::lookup` on the fn name *before* the body is inspected),
+   so a prelude dummy body is bypassed before it could reach
+   `lower_term` — the dummy is already dead, not lowered-then-discarded.
+   After migration the dummy is gone entirely (replaced by
+   `Term::Intrinsic`). This point is therefore a **verification, not a
+   removal**: confirm no codegen path lowers an intercepted body, and
+   delete now-stale comments that reference the discarded dummy. The
+   `Term::Intrinsic` internal-error guards in `lower_term` / the synth
+   walker (added in `.1`) STAY — they guard against an intrinsic body
+   escaping its definition slot, which is a different concern.
 
 ## Concrete code shapes
 
@@ -272,11 +309,13 @@ all move in the same iteration as the variant.
 | `crates/ailang-check/src/mono.rs` | .1 | `synthesise_mono_fn` lambda-destructure unchanged; an inner `Term::Intrinsic` body flows through to an intrinsic synthesised `FnDef`. |
 | `crates/ailang-codegen/src/lib.rs` | .1 | A def whose body is `Term::Intrinsic` routes through `intercepts::lookup`; `lower_term` is never called on it. |
 | `crates/ailang-kernel-stub` + `ailang-surface` parse hop | .1 | `answer` smoke intrinsic added to the stub fixture; its intercept registered. |
-| `examples/prelude.ail` | .2 | 18 dummy bodies → `(intrinsic)`. |
-| `crates/ailang-codegen/src/intercepts.rs` (pin) | .2 | `registry_contains_all_legacy_arms` upgraded to a source↔registry bijection pin. |
-| codegen dummy-body path | .2 | Removed. |
+| `examples/prelude.ail` | .2 | 13 authored dummy bodies → `(intrinsic)` (7 Eq/Ord instance methods + 6 `float_*` fns). The 5 `*__Int` icmp-family and `answer` are NOT prelude sites. |
+| `crates/ailang-codegen/src/intercepts.rs` (pin) | .2 | `registry_contains_all_legacy_arms` upgraded to a bijection over the intrinsic-backed class + an explicit 5-name optimisation-only allowlist. Pin loads the workspace + monomorphises to recover mangled names for the marker direction. |
+| `crates/ailang-surface/tests/prelude_module_hash_pin.rs` | .2 | Rebaseline the prelude module hash (13 bodies change). |
+| `crates/ail/tests/mono_hash_stability.rs` | .2 | Rebaseline the 6 post-mono `eq__*`/`compare__*` def-hashes (body flips to `Term::Intrinsic`). The 4 `show__*` pins do NOT move. |
+| codegen dummy-body path | .2 | Already dead post-`.1` (intercept-by-name precedes body inspection); `.2` confirms + deletes stale comments, no behavioural removal. |
 | `design/contracts/0002-data-model.md` | .1 | New `{ "t": "intrinsic" }` Term entry; note in `fn`/`lam` that the body may be `Term::Intrinsic`. |
-| `design/contracts/0007-honesty-rule.md` | .2 | The prelude-dummy infraction is closed; note its resolution if the contract references it. |
+| `design/contracts/0007-honesty-rule.md` | .2 | Edit only if it names the prelude dummies; recon found it is a general rule that may not reference them — flag honestly, no forced edit. |
 
 ## Data flow
 
@@ -328,16 +367,27 @@ unrepresentable, not diagnosed.)
 
 **intrinsic-bodies.2:**
 
-- Hard-lockstep pin: bijection between `INTERCEPTS` and workspace
-  intrinsic markers. Add a marker without an entry → red; add an
-  entry without a marker → red; drop either → red.
+- Hard-lockstep pin: bijection over the intrinsic-backed class. Add an
+  intrinsic marker with no `INTERCEPTS` entry → red; add a
+  non-allowlisted `INTERCEPTS` entry with no marker → red; drop either
+  → red. The 5-name optimisation-only allowlist is explicit in the pin;
+  the pin loads the workspace, monomorphises, and walks post-mono
+  `FnDef` bodies for `Term::Intrinsic` to recover mangled names for the
+  marker direction.
 - All pre-existing E2E ratifiers stay green (the eq/compare/float
-  smoke suite named in raw-buf.1's commit body) — the migration is
-  behaviour-preserving by construction.
-- Prelude hash: the prelude module's hash *changes* in .2 (the dummy
-  bodies are gone); the `prelude_module_hash_pin.rs` baseline is
-  rebaselined in the same iteration, with the old→new hash recorded
-  in the commit body.
+  smoke suite named in raw-buf.1's commit body:
+  `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`) — the migration is
+  behaviour-preserving (the intercepts emit the same IR; only the
+  now-dead source body changes).
+- Hash rebaselines (both move; both recorded old→new in the commit
+  body): `prelude_module_hash_pin.rs` (prelude module hash; 13 bodies
+  change) and `mono_hash_stability.rs` (the 6 post-mono
+  `eq__*`/`compare__*` def-hashes flip to `Term::Intrinsic`; the 4
+  `show__*` pins do NOT move). IR snapshots do NOT change (no prelude
+  instance method is codegen'd into the user-program snapshots).
 
 ## Acceptance criteria