audit + close: operator-routing-eq-ord — drift_found → post-audit tidy applied inline; CLEAN

Single-iter milestone closing Gitea #1. Architect surfaced 4
honesty-rule drift items (2 high, 2 medium) — all post-Task-13
documentation drift, no codegen behaviour shift. Bench all three
scripts exit 0. Inline tidy applied under the CLAUDE.md trivial-
mechanical carve-out (4 documentation/comment edits on architect-
pre-named sites; no code surface change). No separate tidy iter.

Architect: drift_found → CLEAN-after-tidy.

The architect walked design/INDEX.md, the contracts touched by
the milestone (float-semantics, prelude-classes, str-abi,
scope-boundaries, authoring-surface, typeclasses, method-dispatch),
`git log 86dd7d7..HEAD --format=full` for the three milestone
commits (spec a68d7b6, plan 400ad7c, iter 5170b6a), and the
diff. The 4 drift items + per-item resolution:

  - [high] `design/contracts/prelude-classes.md` — Task-13
    direct-icmp intercept for `lt__Int`/`le__Int`/`gt__Int`/
    `ge__Int`/`ne__Int` was invisible. The Ord-class free-helper
    paragraph described them as routing via `compare` + `match`
    over Ordering, with no statement that at Int they short-
    circuit to direct `icmp`. The IR shape is actively pinned by
    `ord_int_intercept_ir_pin.rs` and load-bearing for
    `bench_closure_chain` perf. Tidy: new paragraph added naming
    the Int-direct family explicitly, the bench_closure_chain
    rationale, and the deliberate Int-only asymmetry (Bool/Str
    still go through compare→match because no current fixture
    exercises Ord-helpers there at hot-loop frequency).

  - [high] `crates/ailang-codegen/src/lib.rs:2777-2789` —
    rustdoc on `try_emit_primitive_instance_body` was three
    iterations stale: claimed "currently inhabited arms: `eq__Str`
    and `compare__Int/Bool/Str`" (= 4 arms, was correct as of
    iter 23.3), and claimed `eq__Int`/`eq__Bool` "ride the natural
    `lower_eq` dispatch via their lambda body `(== x y)`". Both
    claims are factually false post-milestone (the arm set is now
    14: 4 Eq + 3 compare + 5 lt/le/gt/ge/ne + 6 float_*; lower_eq
    is deleted; `==` is no longer a surface name). Tidy: rustdoc
    rewritten to enumerate the actual 14 arms, explain the
    alwaysinline-pairing, name the Int-direct optimization
    asymmetry, and cross-reference prelude-classes.md.

  - [medium] `crates/ail/tests/prelude_eq_alwaysinline_ir_pin.rs:19-21`
    — comment asserted the test could not use `eq_demo.ail`
    because "`eq_demo.ail` calls `(app == …)` directly which today
    uses the `lower_eq` direct-emit short-circuit and never
    references the prelude eq__Int symbol". Both factual claims
    became false the moment Task 4's fixture migration landed
    (eq_demo.ail now calls `(app eq …)`) and Task 7 deleted
    lower_eq. The test functions correctly but the rationale-
    comment lied about why the fixture choice mattered. Tidy:
    comment rewritten to describe the actual test path —
    `eq_ord_user_adt.ail` invokes `(app eq …)` on IntBox whose
    user-instance body internally calls `(app eq ai bi)` on Int,
    monomorphising `prelude.eq__Int` into the emitted IR where
    the alwaysinline attribute on the `define` line is the
    assertion target.

  - [medium] `design/contracts/typeclasses.md` — implicit-prelude-
    import was load-bearing at codegen for the new bare-prelude-
    fn surface (`(app float_eq …)` etc. without explicit
    `prelude.float_eq` qualifier) but no contract named it. The
    codegen extension (`lower_app::resolve_callee`,
    `is_static_callee`, `resolve_top_level_fn` each gained a
    parallel prelude-fallback during iter Task 2/3) was a
    silent dependency on a workspace invariant that lived only
    in typechecker-side comments. Tidy: invariant (4) added as a
    sibling to the existing three invariants on cross-module
    typeclass references, naming the source-level codegen
    fallback as the symmetric partner to invariant (2)'s post-
    mono fallback; the summary paragraph extended from "three
    invariants are lockstep partners" to four, with
    `float_compare_smoke_e2e.rs` named as the invariant-(4)
    ratifier.

The four fixes are pure-docs/comment work (no `.rs` code path
changed, no IR shape changed); the workspace passing-test count
is unchanged (640 still GREEN, 0 FAILED). No code regression
risk; therefore inline-apply rather than dispatching a separate
planner+implement cycle was the right cost-benefit call.

Bench: 0/0/0.

  - bench/check.py exit 0 — 36 metrics, 0 regressed (full
    bench_closure_chain healed by Task 13's direct-icmp
    intercept arms — bump_s -6.05% rc_s -2.67% bump_rss_kb
    -0.77% rc_rss_kb +0.46%, all four previously-regressed
    metrics back inside tolerance).
  - bench/compile_check.py exit 0 — 24 metrics, 0 regressed.
    Largest delta build_O0_ms.bench_list_sum_explicit +11.04%
    (within 20% tolerance — operator-routing adds two extra
    intercept-arm matches on the compile hot-path, marginal).
  - bench/cross_lang.py exit 0 — 25 metrics, 0 regressed.

No baseline updates needed; no `--update-baseline` invoked. The
intercept-arm extension in Task 13 explicitly aimed at restoring
the pre-milestone baseline; bench data ratifies that the aim was
met.

Pipeline this milestone followed:

  brainstorm (one-question-at-a-time Q&A, three design forks
              resolved: operator-names die from surface; Float
              keeps named fns; codegen via always-call +
              alwaysinline pre-emptive mitigation; grounding-
              check PASS over 11 load-bearing assumptions, after
              one BLOCK → spec defect about desugar.rs:2414
              mischaracterisation fixed)
  -> planner (recon DONE_WITH_CONCERNS, 4 substantive spec gaps
              absorbed inline: 60 fixtures not ≈10, 8 in-source
              AST-literal sites not 3, 5 contract files not 3,
              alwaysinline mechanism new to crate; plus 2 self-
              review items absorbed inline: north-star RED-first
              via Unit-eq line; lockstep edits at codegen/lib.rs:2529)
  -> implement (DONE 12/12 from orchestrator; Boss reclassified
                as PARTIAL via acceptance-#8-fail after independent
                bench re-run; iter scope extended to Task 13 via
                SendMessage to same orchestrator-context; final
                DONE 13/13)
  -> audit (drift_found, 4 items inline-tidy applied: prelude-
            classes.md paragraph + codegen rustdoc refresh + test
            comment rewrite + typeclasses.md invariant-(4)
            addition; bench 0/0/0; CLEAN-after-tidy)

Closing Gitea #1. The `closes #1` trailer lived on the iter
commit `5170b6a` and fired on push.

Spec: docs/specs/2026-05-20-operator-routing-eq-ord.md
Plan: docs/plans/operator-routing-eq-ord.1.md

crates/ail/tests/prelude_eq_alwaysinline_ir_pin.rs

@@ -14,13 +14,15 @@ use std::process::Command;
 fn prelude_eq_int_carries_alwaysinline_attribute_in_emitted_ir() {
     let manifest_dir = env!("CARGO_MANIFEST_DIR");
     let repo_root = PathBuf::from(manifest_dir).join("../..");
-    // Use a fixture that already invokes the class-method `eq` path
+    // Use a fixture that invokes the class-method `eq` path so
-    // (so prelude.eq__Int gets monomorphised into the emitted IR).
+    // `prelude.eq__Int` gets monomorphised into the emitted IR.
-    // `eq_demo.ail` calls `(app == …)` directly which today uses the
+    // `eq_ord_user_adt.ail` calls `(app eq …)` on an IntBox whose
-    // `lower_eq` direct-emit short-circuit and never references the
+    // user instance body internally calls `(app eq ai bi)` on Int —
-    // prelude eq__Int symbol; `eq_ord_user_adt.ail` calls `(app eq …)`
+    // class-dispatch resolves both the outer (Eq IntBox) and inner
-    // on an IntBox whose user instance internally calls `(app eq ai bi)`
+    // (Eq Int) calls. The inner Eq Int path is the one we pin here:
-    // on Int, monomorphising `eq__Int` into the IR.
+    // its `define i1 @ail_prelude_eq__Int(...) alwaysinline { ... }`
+    // must carry `alwaysinline` so the call folds to a single
+    // `icmp eq i64` at every use site under -O0.
     let fixture = repo_root.join("examples/eq_ord_user_adt.ail");
 
     let out = Command::new(env!("CARGO_BIN_EXE_ail"))

crates/ailang-codegen/src/lib.rs

@@ -2774,19 +2774,30 @@ impl<'a> Emitter<'a> {
     /// top-level fn gets so it is reachable as a `Term::Var` value).
     /// `Ok(false)` lets `emit_fn` continue with normal body lowering.
     ///
-    /// Currently inhabited arms: `eq__Str` (ships in 23.2.2) and
+    /// Currently inhabited arms (post-operator-routing-eq-ord
-    /// `compare__Int`, `compare__Bool`, `compare__Str` (this iter
+    /// milestone): the `Eq` instance bodies `eq__Int`, `eq__Bool`,
-    /// 23.3). The two eq Int/Bool primitives (`eq__Int`, `eq__Bool`)
+    /// `eq__Str`, `eq__Unit`; the `Ord` instance bodies `compare__Int`,
-    /// ride the natural `lower_eq` dispatch via their lambda body
+    /// `compare__Bool`, `compare__Str`; the Int-direct short-circuits
-    /// `(== x y)` and do not need a hand-rolled body. The three
+    /// for the Ord-class free helpers `lt__Int`, `le__Int`, `gt__Int`,
-    /// `compare` arms must be hand-rolled because there is no
+    /// `ge__Int`, `ne__Int`; and the six Float-named comparison fns
-    /// type-polymorphic primitive that returns an Ordering ADT
+    /// `float_eq`, `float_ne`, `float_lt`, `float_le`, `float_gt`,
-    /// value (Decision: `builtin_binop_typed` covers Int and Float
+    /// `float_ge`. Fourteen arms total; every arm pairs with an
-    /// only — Bool is missing — so a surface-level
+    /// `alwaysinline` attribute on the generated `define` line (via
-    /// `if x < y { LT } else if x == y { EQ } else { GT }` body
+    /// `intercept_emit_wants_alwaysinline`) so the call folds to a
-    /// would fail at codegen for `compare__Bool`). Hand-rolling all
+    /// single instruction at every use site under -O0 as well as
-    /// three keeps the family consistent and the IR shape
+    /// -O2. The eq/compare/Float arms exist because there is no
-    /// predictable.
+    /// type-polymorphic builtin that would lower to the right
+    /// per-type instruction (`lower_eq` was deleted in the
+    /// operator-routing-eq-ord milestone — `==` is no longer a
+    /// language identifier; the class-method dispatch through
+    /// `prelude.Eq` / `prelude.Ord` is the only path). The `lt/le/gt/
+    /// ge/ne` Int-direct arms exist as an asymmetric optimization
+    /// (Int-only) — without them the source-level body of `lt`/etc.
+    /// allocates an `Ordering` ctor per call via the
+    /// `compare__Int` → `match` path, which surfaces as a
+    /// `bench_closure_chain` regression. See
+    /// `design/contracts/prelude-classes.md` for the full surface
+    /// and the Int-only asymmetry rationale.
     fn try_emit_primitive_instance_body(
         &mut self,
         fn_name: &str,

design/contracts/prelude-classes.md

@@ -14,6 +14,26 @@ them with single-instruction bodies (`icmp eq i64` for `eq__Int`,
 `LT`/`EQ`/`GT` for `compare__T`) and attaches `alwaysinline` so
 the call folds to the single instruction at every use site.
 
+The five Ord-class free helpers (`ne`/`lt`/`le`/`gt`/`ge`) have
+source-level bodies that route through `eq` / `compare` plus
+`match` over `Ordering` — written that way so the surface form is
+LLM-natural and so user-ADT instances of `Eq`/`Ord` automatically
+pick up working helpers without any per-type opt-in. At Int the
+codegen intercept short-circuits this indirection: `lt__Int`,
+`le__Int`, `gt__Int`, `ge__Int`, and `ne__Int` are intercept-
+overridden to emit `icmp slt i64` / `sle i64` / `sgt i64` /
+`sge i64` / `ne i64` directly, bypassing the `compare__Int` →
+`Ordering`-ctor → `match` path. Without this short-circuit the
+`Ordering` ctor allocates per call inside hot loops — a real
+cost surfaced by the `bench_closure_chain` regression at the
+operator-routing-eq-ord milestone and pinned by
+`crates/ail/tests/ord_int_intercept_ir_pin.rs`. The short-circuit
+is *Int-only* by deliberate asymmetry: no current bench or
+example fixture exercises Ord-`lt`/`le`/`gt`/`ge` at Bool or
+Str at sufficient call frequency to justify the intercept-arm
+maintenance; the symmetric extensions are mechanical when the
+first such workload appears.
+
 Float has neither `Eq` nor `Ord` instance per [Float semantics](
 float-semantics.md); a polymorphic helper invoked at Float fires
 `NoInstance` at typecheck with a Float-aware diagnostic that names

design/contracts/typeclasses.md

@@ -135,15 +135,39 @@ Three invariants make this work:
    `unknown variable: show` from codegen instead of the right
    typecheck-phase NoInstance Show.
 
-The three invariants are lockstep partners: invariant (1) creates the
+4. **Bare-prelude-fn calls resolve via implicit-prelude-import at
+   typecheck AND at codegen.** A user-module source-level call
+   `(app float_eq 1.5 1.5)` writes the bare name `float_eq`, not
+   the qualified form `prelude.float_eq`. The typechecker resolves
+   this via the auto-injected prelude import (see invariant (2)
+   for the one-way auto-injection rule); codegen's
+   `lower_app::resolve_callee` + `is_static_callee` + `resolve_top_level_fn`
+   each carry a parallel prelude-fallback: when the bare name does
+   not resolve in the caller-module's symbol table, fall back to
+   `prelude.<name>`. This is the source-level counterpart to
+   invariant (2)'s post-mono fallback — both make the implicit-
+   prelude-import a workspace invariant rather than a typechecker-
+   only feature. The fallback is load-bearing for the surface
+   `(app float_eq …)` / `(app float_lt …)` / etc. of the
+   operator-routing-eq-ord milestone; without it the LLM-author
+   must write `prelude.float_eq` explicitly, which is exactly the
+   syntactic noise the implicit import exists to eliminate.
+
+The four invariants are lockstep partners: invariant (1) creates the
 cross-module reference, invariant (2) makes codegen able to resolve
-it, invariant (3) makes the typecheck-time discharge fire correctly
+post-mono references, invariant (3) makes the typecheck-time
-when no instance exists. A future refactor that loosens any one of
+discharge fire correctly when no instance exists, invariant (4)
-the three breaks the user-ADT trajectory; the test pins at
+makes bare prelude-fn names resolve from user modules at the source
+level. A future refactor that loosens any one of the four breaks
+the user-ADT trajectory or the Float-named-fn surface; the test
+pins at
 `crates/ail/tests/codegen_import_map_fallback_pin.rs` (invariant 2),
 `crates/ail/tests/polyfn_dot_qualified_branch_pin.rs` (invariant 3
-+ lockstep), and the existing `crates/ail/tests/show_user_adt`
++ lockstep), `crates/ail/tests/float_compare_smoke_e2e.rs`
-fixture (full trajectory) collectively protect the contract.
+(invariant 4 — drives `(app float_eq …)` end-to-end across the
+implicit-prelude-import boundary), and the existing
+`crates/ail/tests/show_user_adt` fixture (full trajectory)
+collectively protect the contract.
 
 ## Defaults and superclasses