plan: floats iter 5 — prose + DESIGN.md + milestone close

2026-05-10 16:33:35 +02:00
parent 73d65baa81
commit fd287c9740
1 changed files with 699 additions and 0 deletions
@@ -0,0 +1,699 @@
+# Floats Iteration 5 — Prose + DESIGN.md + Milestone Close (Implementation Plan)
+
+> **Parent spec:** `docs/specs/2026-05-10-floats.md` (committed
+> `e37366f`, approved 2026-05-10) — section A5 (determinism
+> contract) + the `crates/ailang-prose/` Components subsection.
+>
+> **For agentic workers:** REQUIRED SUB-SKILL: use `skills/implement`
+> to run this plan. Steps use `- [ ]` checkboxes for tracking.
+
+**Goal:** Replace the iter-1 prose `unimplemented!("Floats milestone
+iter 5: prose")` arm with a Float renderer matching the surface-print
+shape from iter 2; add §"Float semantics" to DESIGN.md per spec A5;
+update DESIGN.md's "supported primitive types" line and the builtins
+list to include Float entries; mark Floats `[x]` in roadmap; write
+the milestone-close JOURNAL entry.
+
+**Architecture:** Prose render is one-way (Form-A AST → Form-B text).
+The Float arm in `write_lit` reuses the same `to_string + .0-suffix-
+fallback` shape as `crates/ailang-surface/src/print.rs::write_float_lit`
+from iter 2 — except non-finite bits render as the Mainstream-language
+spellings `NaN` / `+Inf` / `-Inf` rather than panicking, because prose
+is a one-way render and CAN handle Form-A values that surface lex
+cannot produce. DESIGN.md additions sit alongside the existing
+"What is supported" list and add a new §"Float semantics" subsection.
+
+**Tech Stack:** `crates/ailang-prose/src/lib.rs`, `docs/DESIGN.md`,
+`docs/roadmap.md`, `docs/JOURNAL.md`. No code outside the prose
+crate.
+
+**No-regression invariant:** `cargo test --workspace` GREEN. The
+iter-1 spec_drift / design_schema_drift anchors for `Float`
+(`` `FLOAT` `` in form_a.md, `"kind": "float"` in DESIGN.md JSON-
+schema block) are already in place since iter 1.1 — they stay
+unchanged. The new DESIGN.md additions do not perturb the existing
+anchors.
+
+---
+
+## Files this plan creates or modifies
+
+- Modify: `crates/ailang-prose/src/lib.rs` — replace the
+  `Literal::Float { .. } => unimplemented!(...)` arm at line 917
+  with a real renderer; add `mod tests` Float coverage.
+- Modify: `docs/DESIGN.md` — line 2034 (primitive types list) +
+  lines 2038-2059 (builtins list) + insert new §"Float semantics"
+  subsection before §"What is not (yet) supported".
+- Modify: `docs/roadmap.md` — flip Floats `[~]` → `[x]`; drop
+  `depends on: Floats` from Post-22 Prelude.
+- Modify: `docs/JOURNAL.md` — append iter-5 close entry AND
+  separate milestone-close entry summarising the whole 5-iteration
+  arc.
+
+No file outside this list is touched.
+
+---
+
+## Task 1: Prose renderer for `Literal::Float`
+
+**Files:**
+- Modify: `crates/ailang-prose/src/lib.rs:911-919` (write_lit) +
+  add a private helper `write_float_lit(out, bits)`; add a `mod
+  tests` block (or extend the existing one — verify which).
+
+- [ ] **Step 1: Find the test mod or confirm absence**
+
+Run: `grep -n "^#\[cfg(test)\]\|^mod tests" crates/ailang-prose/src/lib.rs`
+Determine where to add the test. If a `mod tests` already exists at
+EOF, append to it. If not, create one.
+
+- [ ] **Step 2: Write the RED test**
+
+In the test mod, append:
+
+```rust
+/// Floats milestone iter 5.1: prose renders Float literals as
+/// surface-style decimal text. Finite values use shortest
+/// round-trippable decimal with `.0` suffix when neither `.` nor
+/// `e`/`E` is in the rendered string (parallel to surface print).
+/// Non-finite (NaN, ±Inf) render as the Mainstream-language
+/// spellings — `NaN`, `+Inf`, `-Inf` — because prose is a one-way
+/// render and the surface lex grammar's no-NaN/Inf restriction
+/// does not apply to it.
+#[test]
+fn renders_float_literal_finite() {
+    use ailang_core::ast::*;
+    let t = Term::Lit { lit: Literal::Float { bits: 0x3ff8_0000_0000_0000u64 } };
+    let s = render_term(&t);
+    assert_eq!(s, "1.5");
+
+    let t = Term::Lit { lit: Literal::Float { bits: 0x4024_0000_0000_0000u64 } };
+    let s = render_term(&t);
+    assert_eq!(s, "10.0");
+}
+
+#[test]
+fn renders_float_literal_signed_zero() {
+    use ailang_core::ast::*;
+    let pos = Term::Lit { lit: Literal::Float { bits: 0x0u64 } };
+    assert_eq!(render_term(&pos), "0.0");
+    let neg = Term::Lit { lit: Literal::Float { bits: 0x8000_0000_0000_0000u64 } };
+    assert_eq!(render_term(&neg), "-0.0");
+}
+
+#[test]
+fn renders_float_literal_non_finite() {
+    use ailang_core::ast::*;
+    let nan = Term::Lit { lit: Literal::Float { bits: 0x7ff8_0000_0000_0000u64 } };
+    assert_eq!(render_term(&nan), "NaN");
+    let pos_inf = Term::Lit { lit: Literal::Float { bits: 0x7ff0_0000_0000_0000u64 } };
+    assert_eq!(render_term(&pos_inf), "+Inf");
+    let neg_inf = Term::Lit { lit: Literal::Float { bits: 0xfff0_0000_0000_0000u64 } };
+    assert_eq!(render_term(&neg_inf), "-Inf");
+}
+```
+
+If `render_term` is private or absent, look for the equivalent
+helper at the top of `mod tests` (the existing tests use it per
+the `grep` from earlier surveying — `render_term(&Term::Lit { lit:
+Literal::Int { value: 42 } })` returned `"42"`).
+
+- [ ] **Step 3: Verify RED**
+
+Run: `cargo test -p ailang-prose --lib renders_float_literal`
+Expected: PANIC at the iter-1 `unimplemented!("Floats milestone
+iter 5: prose")` arm in `write_lit`.
+
+- [ ] **Step 4: Add the `write_float_lit` helper + replace the arm**
+
+In `crates/ailang-prose/src/lib.rs`, immediately BEFORE `write_lit`
+(around line 911), add:
+
+```rust
+/// Floats milestone iter 5: render a Float literal's bit pattern
+/// as surface-style decimal text. Finite values use Grisu3
+/// (`f64::to_string`) with a `.0` suffix when neither `.` nor
+/// `e`/`E` appears, parallel to
+/// `crates/ailang-surface/src/print.rs::write_float_lit`. Non-finite
+/// values render as `NaN` / `+Inf` / `-Inf` — these are valid in
+/// Form-A (the canonical bytes carry the bit pattern) but cannot
+/// be expressed in surface lex; prose is one-way render, so naming
+/// them after the Mainstream-language spellings is more useful
+/// than a panic or a `(float-bits hex)` placeholder.
+fn write_float_lit(out: &mut String, bits: u64) {
+    let f = f64::from_bits(bits);
+    if f.is_nan() {
+        out.push_str("NaN");
+        return;
+    }
+    if f == f64::INFINITY {
+        out.push_str("+Inf");
+        return;
+    }
+    if f == f64::NEG_INFINITY {
+        out.push_str("-Inf");
+        return;
+    }
+    let s = f.to_string();
+    out.push_str(&s);
+    if !s.contains('.') && !s.contains('e') && !s.contains('E') {
+        out.push_str(".0");
+    }
+}
+```
+
+Then replace the iter-1 arm at `write_lit` (line 917):
+
+```rust
+        Literal::Float { bits } => write_float_lit(out, *bits),
+```
+
+- [ ] **Step 5: Verify RED tests now GREEN**
+
+Run: `cargo test -p ailang-prose --lib renders_float_literal`
+Expected: all 3 tests PASS.
+
+- [ ] **Step 6: Verify no `unimplemented!` arm with the iter-5 string remains**
+
+Run: `grep -rn "Floats milestone iter 5: prose" crates/`
+Expected: zero hits.
+
+- [ ] **Step 7: Verify no workspace regression**
+
+Run: `cargo test --workspace`
+Expected: all 402+ tests pass (= 402 prior + 3 new), 0 failed.
+
+- [ ] **Step 8: Commit**
+
+```bash
+git add crates/ailang-prose/src/lib.rs
+git commit -m "floats iter 5.1: prose renders Float literals (finite + NaN/Inf)"
+```
+
+---
+
+## Task 2: DESIGN.md — extend supported primitives + builtins lists
+
+**Files:**
+- Modify: `docs/DESIGN.md:2034` (primitive types list) +
+  lines 2038-2059 (builtins list).
+
+- [ ] **Step 1: Update line 2034 to include Float**
+
+In `docs/DESIGN.md`, line 2034, replace:
+
+```
+- Int, Bool, Unit, **Str** as primitive types.
+```
+
+with:
+
+```
+- Int, Bool, Unit, **Str**, **Float** as primitive types.
+```
+
+- [ ] **Step 2: Refresh the builtins list at lines 2038-2059**
+
+In `docs/DESIGN.md`, replace the `**Builtins.**` block at lines
+2038-2059 with the post-Floats current shape:
+
+```
+- **Builtins.** Arithmetic operators (`+`, `-`, `*`, `/`) of type
+  `forall a. (a, a) -> a` (codegen-restricted to `{Int, Float}`);
+  `%` of type `(Int, Int) -> Int` (Int-only — `fmod` semantics for
+  Float deferred); ordering operators and `!=` (`!=`, `<`, `<=`,
+  `>`, `>=`) of type `forall a. (a, a) -> Bool` (codegen-restricted
+  to `{Int, Float}`); polymorphic `neg : forall a. (a) -> a`
+  (codegen-restricted to `{Int, Float}`; Float arm uses LLVM
+  `fneg double` for correct `-0.0` handling); logical
+  `not : (Bool) -> Bool`; conversions
+  `int_to_float : (Int) -> Float`,
+  `float_to_int_truncate : (Float) -> Int` (saturating, NaN → 0),
+  `float_to_str : (Float) -> Str` (codegen lowering deferred —
+  symbol installed but errors at codegen pending runtime Str
+  allocation); inspection `is_nan : (Float) -> Bool` (LLVM
+  `fcmp uno`); Float bit-pattern constants `nan : Float`,
+  `inf : Float`, `neg_inf : Float` (resolved as bare values, lower
+  to direct hex-float `double` SSA constants at use site); the IO
+  effect ops (`io/print_int|bool|str|float`); **`==` : forall a.
+  (a, a) -> Bool**; and **`__unreachable__ : forall a. a`**.
+  - **`==` is polymorphic.** The typechecker accepts
+    `==` at any type whose two sides agree (the rigid `a` of the
+    `Forall` is unified by HM at the use site). Codegen
+    monomorphises and dispatches on the resolved AIL arg type:
+    `Int` → `icmp eq i64`; `Bool` → `icmp eq i1`;
+    `Str` → `call @strcmp(ptr, ptr)` then `icmp eq i32 0`
+    (`@strcmp` is declared in the LLVM IR header alongside
+    `@printf` / `@GC_malloc`); `Unit` → constant `i1 true`
+    (Unit has a single inhabitant; both sides are still
+    evaluated for any side effects); `Float` → `fcmp oeq double`.
+    ADT and `Fn` arg types are rejected at codegen with a
+    `CodegenError::Internal` mentioning `==` and the offending
+    type — neither has a canonical structural-equality scheme
+    yet, and the language deliberately does not silently elide
+    the check. **`!=` for Float uses `fcmp UNE double` (NOT
+    `one`)** — `one` is "ordered and not equal" and would return
+    false for `nan != nan`, violating IEEE-`!=`.
+  - **`__unreachable__`** is a polymorphic bottom value: a use of
+    `__unreachable__` typechecks against any expected type at
+    the use site and codegens to the LLVM `unreachable`
+    instruction (UB if ever executed). It is the chain
+    machinery's deepest fall-through for matches that the
+    typechecker proved exhaustive, and it is available to user
+    code as an explicit panic primitive
+    (`(if cond __unreachable__ ...)` for assertions or
+    impossible branches). Reference site is
+    `Term::Var { name = "__unreachable__" }` / form-A bare
+    `__unreachable__`.
+```
+
+The widening + new entries are folded in; the existing prose about
+`==` polymorphism gains a `Float → fcmp oeq double` line; the
+`!=` UNE-not-one note is added; the existing `__unreachable__`
+prose is preserved verbatim.
+
+- [ ] **Step 3: Verify DESIGN.md still parses (markdown render)**
+
+Run: `cargo test -p ailang-core --test design_schema_drift`
+Expected: GREEN — the `"kind": "float"` anchor (added in iter 1)
+is still present in the JSON-schema block, unchanged. The new
+prose only adds; nothing is removed.
+
+- [ ] **Step 4: Commit**
+
+```bash
+git add docs/DESIGN.md
+git commit -m "floats iter 5.2: DESIGN.md — Float in primitive types + refreshed builtins list"
+```
+
+---
+
+## Task 3: DESIGN.md — add §"Float semantics" subsection
+
+**Files:**
+- Modify: `docs/DESIGN.md` — insert new top-level section
+  immediately BEFORE `## What is not (yet) supported` (line 2006).
+
+- [ ] **Step 1: Insert the new subsection**
+
+In `docs/DESIGN.md`, immediately before `## What is not (yet) supported`
+(line 2006), insert:
+
+```markdown
+## Float semantics
+
+`Float` is IEEE-754 binary64 (LLVM `double`). One float type ships;
+no `f32` variant. The runtime / codegen contract:
+
+**Guaranteed:**
+
+- Every individual builtin (`+`/`-`/`*`/`/`/`neg`/`<`/`==`/...) lowers
+  to a single LLVM IR instruction on the Float arm:
+  `fadd/fsub/fmul/fdiv double`, `fneg double`, `fcmp olt/ole/ogt/oge
+  double`, `fcmp oeq double`, `fcmp une double` (for `!=`). On a
+  fixed `(target triple, LLVM version)` pair, the bit pattern of
+  the result of any single op is reproducible.
+- NaN and ±Inf propagate per IEEE 754 — no silent collapse to zero,
+  no trap. Arithmetic on a NaN operand produces NaN; division by
+  zero produces ±Inf; `0.0 / 0.0` produces NaN.
+- `-0.0` and `+0.0` are distinct bit patterns at the canonical-JSON
+  hash level (`{"bits":"0000000000000000",...}` vs
+  `{"bits":"8000000000000000",...}` — distinct `def_hash`s) but
+  compare equal via `==` per IEEE (`fcmp oeq double` returns true
+  for `+0 == -0`). This asymmetry is the correct IEEE behaviour;
+  it does mean `def_hash`-equality is finer than `==`-equality on
+  Float.
+- `==` returns `false` whenever either operand is NaN
+  (`fcmp oeq` is the ordered-equal predicate; ordered = both
+  operands non-NaN).
+- `!=` returns `true` whenever either operand is NaN (`fcmp une`
+  is the unordered-or-not-equal predicate). This matches Rust
+  `f64::ne` and IEEE-`!=` exactly.
+- `is_nan` (`fcmp uno double %x, %x`) returns `true` iff `x` is
+  NaN. Bit-pattern-based NaN detection without dependence on the
+  payload bits.
+- `int_to_float` (`sitofp`) is exact for `|n| < 2^53`,
+  round-to-nearest-even otherwise.
+- `float_to_int_truncate` (`@llvm.fptosi.sat.i64.f64`) is total:
+  NaN → 0, +Inf → i64::MAX, -Inf → i64::MIN, finite-out-of-range
+  saturates, finite-in-range truncates toward zero. Matches Rust
+  `as i64` semantics (since 1.45).
+
+**Unspecified:**
+
+- FMA contraction. LLVM may fold `fadd (fmul a b) c` into
+  `fma a b c`. Bit results may differ between an op-emitted-in-
+  isolation pattern and an op-folded-into-FMA pattern.
+- Reassociation. The compiler may reorder a chain like
+  `(a + b) + c` into `a + (b + c)`, producing a bit-different
+  result on numerically sensitive inputs.
+- Subnormal flushing modes. If the target enables FTZ (flush-to-
+  zero) or DAZ (denormals-are-zero), subnormal results round to
+  zero; AILang does not enable these flags but does not forbid the
+  target from doing so.
+- The exact NaN bit pattern produced by an op. Any quiet NaN bit
+  pattern is conformant; `0.0 / 0.0` may produce `0x7ff8_0000_
+  0000_0000` on one target and a different qNaN on another.
+
+These are the Rust / Swift / standard-LLVM defaults — not
+research-grade reproducibility guarantees. The stronger guarantee
+(e.g. Pythonic `float.fromhex`-level bit reproducibility across
+ops) would require `-ffp-contract=off` plus per-op intrinsic
+selection — out of scope for the milestone; revisit only if a real
+use case appears.
+
+**Form-A serialisation:** Float literals carry the IEEE-754
+bit pattern as a 16-character lowercase hex string in the canonical
+JSON: `{"kind":"float","bits":"<16-hex>"}`. Routing through the
+JSON *string* path (not `serde_json::Number`) preserves bit
+stability across `serde_json` versions and lets NaN / ±Inf
+round-trip through Form-A — JSON numbers cannot represent them.
+
+**Pattern matching:** `Pattern::Lit` on `Literal::Float` is hard-
+rejected at typecheck (`CheckError::FloatPatternNotAllowed`). IEEE
+semantics make Float patterns semantically dubious — NaN never
+matches via IEEE-`==`, and bit-exact equality is rarely what an
+LLM-author wants. Use ordering operators (`<`, `>`, ...) and
+`is_nan` to discriminate Floats.
+
+`float_to_str` (Float → Str) is **type-installed but codegen-
+deferred** to a follow-up milestone: it requires runtime-allocated
+`Str` (the current Str path uses only static `@.str_*` globals;
+no malloc-backed dynamic-Str infrastructure). Calling it
+typechecks but produces a structured `CodegenError::Internal`.
+```
+
+- [ ] **Step 2: Verify markdown still parses cleanly**
+
+Run: `cargo doc --no-deps -p ailang-core 2>&1 | head -10`
+Expected: no new warnings (rustdoc doesn't see DESIGN.md, but the
+test sweeps any markdown-formatting glitches that might have been
+introduced; a clean output here is reassurance, not a hard test).
+
+- [ ] **Step 3: Verify the drift test still passes**
+
+Run: `cargo test -p ailang-core --test design_schema_drift`
+Expected: GREEN. The new section adds prose; no anchor is removed.
+
+- [ ] **Step 4: Commit**
+
+```bash
+git add docs/DESIGN.md
+git commit -m "floats iter 5.3: DESIGN.md — new §Float semantics subsection (A5 determinism contract)"
+```
+
+---
+
+## Task 4: Roadmap — mark Floats `[x]`, drop Post-22 Prelude dependency
+
+**Files:**
+- Modify: `docs/roadmap.md` — Floats entry P0 → mark `[x]`;
+  Post-22 Prelude P1 → drop `depends on: Floats` line.
+
+- [ ] **Step 1: Mark the Floats milestone done**
+
+In `docs/roadmap.md`, line 36 currently reads:
+
+```
+- [~] **\[milestone\]** Floats — introduce `Float` as IEEE-754
+```
+
+Change to:
+
+```
+- [x] **\[milestone\]** Floats — introduce `Float` as IEEE-754
+```
+
+(Just the `~` → `x` swap; the rest of the entry stays for now —
+will be removed in a follow-up tidy once the milestone-close
+JOURNAL entry is enough context.)
+
+- [ ] **Step 2: Drop the Post-22 Prelude dependency line**
+
+In `docs/roadmap.md`, locate the Post-22 Prelude entry (P1, around
+line 53). Remove the lines:
+
+```
+  - depends on: Floats (the partial-Eq/Ord story for Float must be
+    settled before the Prelude classes ship, so the Prelude can
+    decide what's instanced and what isn't)
+```
+
+The Prelude is now unblocked; the Floats commitment (no `Eq` /
+`Ord` for Float, only `Show`) is settled and documented in DESIGN.md
+§"Float semantics".
+
+- [ ] **Step 3: Commit**
+
+```bash
+git add docs/roadmap.md
+git commit -m "floats iter 5.4: roadmap — mark Floats [x] + unblock Post-22 Prelude"
+```
+
+---
+
+## Task 5: JOURNAL — iter-5 close + milestone-close
+
+**Files:**
+- Modify: `docs/JOURNAL.md` — append TWO entries: iter-5 close
+  (small, mirrors per-task subjects), and a separate milestone-
+  close summary covering the whole 5-iteration arc.
+
+- [ ] **Step 1: Append the iter-5 close entry**
+
+In `docs/JOURNAL.md`, append at file end:
+
+```markdown
+## 2026-05-10 — Iteration Floats.5: prose + DESIGN.md + milestone close
+
+Replaced the iter-1 prose `unimplemented!("Floats milestone iter 5:
+prose")` arm with `write_float_lit` — finite values render as
+shortest round-trippable decimal with `.0` suffix (parallel to
+surface print); non-finite values render as `NaN` / `+Inf` /
+`-Inf` (Mainstream-language spellings) because prose is one-way
+render and CAN handle Form-A NaN / ±Inf bits that surface lex
+cannot produce.
+
+DESIGN.md gained a new top-level §"Float semantics" subsection per
+spec section A5: IEEE-754 binary64 commitment, per-op bit stability
+on fixed (target, LLVM), NaN / ±Inf propagation, `-0`/`+0` hash-vs-
+equality asymmetry, FMA-contraction / reassociation / subnormal
+flushing UNSPECIFIED, conversions semantics, Form-A serialisation
+shape, Pattern::Lit::Float rejection rationale, and the
+`float_to_str` deferred-codegen note. The "What is supported"
+bullet list at line 2034 was extended to mention `Float` as a
+primitive type; the builtins list was refreshed to include the
+widened ops (`forall a. (a, a) -> a`), the 5 new fn builtins, the
+3 Float constants, and the 4th IO effect op (`io/print_float`).
+
+Roadmap flipped Floats from `[~]` to `[x]`; Post-22 Prelude is
+unblocked (the `depends on: Floats` line dropped — the partial-
+Eq/Ord-for-Float story is now settled and documented in
+§"Float semantics", so the Prelude milestone can decide what's
+instanced without bouncing back to Float design).
+
+Per-task commits:
+
+- `<sha-5.1>` floats iter 5.1: prose renders Float literals (finite + NaN/Inf)
+- `<sha-5.2>` floats iter 5.2: DESIGN.md — Float in primitive types + refreshed builtins list
+- `<sha-5.3>` floats iter 5.3: DESIGN.md — new §Float semantics subsection (A5 determinism contract)
+- `<sha-5.4>` floats iter 5.4: roadmap — mark Floats [x] + unblock Post-22 Prelude
+```
+
+Replace each `<sha-5.N>` with the actual commit SHA at write time.
+
+- [ ] **Step 2: Append the milestone-close entry**
+
+In `docs/JOURNAL.md`, immediately AFTER the iter-5 close section,
+append:
+
+```markdown
+## 2026-05-10 — Milestone close: Floats
+
+The Floats milestone is closed. `Float` is a fully supported
+primitive type in AILang, end-to-end. `examples/floats.ail.json`
+builds via `ail build`, runs, and produces predictable stdout —
+the milestone-acceptance gate landed first try in iter 4.6.
+
+**Five-iteration arc:**
+
+- **Iter 1 (schema).** `Literal::Float { bits: u64 }` AST variant
+  with private `hex_u64` serde helper (16-char lowercase hex string
+  in canonical JSON; bypasses `serde_json::Number` for bit
+  stability + NaN/Inf representability). `Float` registered as
+  primitive name. 8 downstream `match Literal` sites wired with
+  permanent semantic arms or named-iteration `unimplemented!`
+  placeholders. Drift-test anchors added to `spec_drift.rs` /
+  `design_schema_drift.rs` / `form_a.md` / DESIGN.md JSON-schema
+  block. Bit-stability tests pin A1 / A5 properties.
+- **Iter 2 (surface).** Lex `<digits>.<digits>(e[+-]?<digits>)?`
+  and `<digits>e[+-]?<digits>` per spec A2; reject bare leading /
+  trailing dots, missing fraction-after-dot, missing / sign-only
+  exponents. Parser accepts `Tok::Float` in atom + pat-lit
+  positions (typecheck rejects pat-lit Float in iter 3). Surface
+  print emits shortest-round-trippable decimal with `.0` suffix
+  fallback; non-finite bits panic per spec (cannot reach printer
+  via well-formed surface input). Round-trip property
+  `lex(print(L)) == L` pinned for 6 representative bit patterns.
+- **Iter 3 (typecheck + builtins).** Widened `+`/`-`/`*`/`/` and
+  `!=`/`<`/`<=`/`>`/`>=` from monomorphic `(Int, Int) -> {Int, Bool}`
+  to polymorphic `forall a. (a, a) -> {a, Bool}` (same shape `==`
+  already had). `%` stays Int-only. 5 new builtins installed:
+  `neg` (poly), `int_to_float`, `float_to_int_truncate`,
+  `float_to_str`, `is_nan`. 3 bit-pattern constants installed as
+  bare-value globals: `nan`, `inf`, `neg_inf`. 1 new effect op:
+  `io/print_float`. `Pattern::Lit::Float` typecheck-rejected via
+  new `CheckError::FloatPatternNotAllowed`.
+- **Iter 4 (codegen + E2E).** Float literals lower as LLVM hex-
+  float `double` constants. `synth::builtin_binop` replaced by
+  3-tuple-returning `builtin_binop_typed(name, &Type)` —
+  `fadd/fsub/fmul/fdiv double` and `fcmp olt/ole/ogt/oge/oeq/UNE
+  double` arms (note `UNE`, not `one`). `lower_eq` Float arm.
+  5 new fn-builtin lowering arms (`neg` poly with `fneg double`;
+  `int_to_float` `sitofp`; `float_to_int_truncate`
+  `@llvm.fptosi.sat.i64.f64`; `is_nan` `fcmp uno`; `float_to_str`
+  deferred via structured `CodegenError`). 3 Float constants
+  intercepted at `Term::Var` arm. `io/print_float` via inline
+  `printf("%g\n", v)`. `examples/floats.ail.json` E2E fixture +
+  `crates/ail/tests/floats_e2e.rs` E2E test — milestone gate.
+- **Iter 5 (prose + DESIGN.md).** Prose renderer for Float
+  literals (finite + NaN/Inf). DESIGN.md §"Float semantics" + line-
+  2034 + builtins-list refresh. Roadmap mark + Prelude unblock.
+
+**Key design decisions (rationale):**
+
+- **One float type only — `f64`, named `Float`** (no `f32`). LLM
+  authors don't reach for `f32` unprompted; shipping both would
+  surface a per-op type-pun question that adds friction without
+  measurable correctness gain.
+- **IEEE-conformant equality** — `==` returns `false` for `nan ==
+  nan`, no `Eq` instance for `Float` in the eventual prelude. The
+  partial-equality reality is real and surfaces through builtins
+  (`is_nan`, ordering ops returning `false` for NaN-involved
+  comparisons) rather than through a lying total typeclass
+  instance.
+- **Polymorphic operators over `{Int, Float}` via codegen-dispatch**
+  — the same mechanism `==` already used. Mainstream alignment
+  beats the explicit-naming purity of the earlier `(fadd 1.5 2.5)`
+  draft. The hardcoded `{Int, Float}` filter is transitional;
+  cleanly replaceable by a `Num a` constraint when typeclasses
+  ship in 22c.
+- **Form-A bit-pattern hex string** — bypasses `serde_json::Number`
+  (not bit-stable across versions for floats; cannot represent
+  NaN / ±Inf). Routing through the string path preserves bit-exact
+  determinism + lets non-finite Floats round-trip through
+  canonical JSON.
+- **Pattern::Lit::Float hard-reject at typecheck** — IEEE semantics
+  make Float patterns semantically dubious (NaN never matches;
+  bit-exact equality is rarely the LLM-author's intent). Surface
+  lex / parser accept the syntax to keep the diagnostic at the
+  correct layer (typecheck, not parser).
+- **`fcmp UNE` for `!=`, NOT `fcmp one`** — `one` is "ordered and
+  not equal" and returns false for `nan != nan`, violating IEEE-
+  `!=` and the user-fixed constraint #2. Caught during the
+  pre-implementation LLVM IR audit; documented in iter-4 codegen
+  arm + DESIGN.md §"Float semantics".
+- **`fneg double` for `neg`, NOT `fsub double 0.0, x`** — IEEE
+  `0.0 - 0.0 = +0.0`, so the `fsub`-from-zero desugar would
+  wrongly produce `+0.0` for `neg(+0.0)` instead of `-0.0`. LLVM 8+
+  intrinsic; clang 22 always available.
+- **`@llvm.fptosi.sat.i64.f64` for `float_to_int_truncate`** —
+  saturating fp-to-int intrinsic exactly matches Rust `as i64`
+  semantics (NaN → 0, ±Inf → i64::{MIN,MAX}, saturating). Total,
+  no Maybe wrapper.
+
+**Process notes (orchestration lessons):**
+
+- **Drift tests are part of the schema layer.** The original 5-iter
+  plan put DESIGN.md anchor edits in iter 5; iter 1's drift-test
+  break revealed they belong in iter 1 (where they get added
+  together with the AST variant they document). The exhaustive-
+  match drift tests are *the enforcement mechanism* of the schema
+  invariant — adding a new `Literal` variant without their anchors
+  IS a schema-layer break.
+- **Plan inconsistencies caught by the reviewer chain.** Iter 4.2
+  shipped a plan that would have stranded comparison ops (Step 4
+  said `builtin_binop_typed` returns None for them; Step 5
+  narrowed the dispatch matches!). Implementer caught it; pulled
+  forward Task 3 Steps 3-4 as minimal repair; orchestrator
+  endorsed; Task 3's residual scope was narrowed accordingly. The
+  two-stage review (spec + quality) caught two more issues:
+  the dual-meaning `(instr, ll_ty)` 2-tuple → fixed via 3-tuple
+  return; the `unimplemented!()` panic for `float_to_str` →
+  fixed via structured `CodegenError::Internal`.
+- **`is_static_callee` companion-edit.** Any new lowering arm in
+  `lower_app` MUST also be recognised by `is_static_callee`
+  (otherwise App dispatch falls through to indirect-call →
+  UnknownVar). This bit twice (iter 4.2 for `==`, iter 4.4 for
+  the 5 new fn-builtins). Both pulled forward as minimal repairs.
+- **The `synth_term` test helper does not exist.** Iter 3 plan
+  named it; the actual fn is `crate::synth(...)` with 8 args. The
+  implementer flagged this; future plans should specify the
+  adapter pattern explicitly.
+
+**Workspace at milestone close:** 405+ tests passing, 0 failed.
+Iter-1-baseline rustdoc warnings preserved (1 warning on `desugar`
+private link, pre-existing). `def_hash` regression hashes
+(`db33f57cb329935e` for `sum.sum`, `b082192bd0c99202` for
+`IntList`) preserved bit-identical — adding a Literal variant
+does not perturb pre-existing canonical bytes.
+
+**Known debt deferred beyond this milestone:**
+
+- `float_to_str` codegen lowering — requires runtime-allocated Str
+  (the current Str path uses only static `@.str_*` globals;
+  no malloc-backed dynamic-Str infrastructure). Symbol is
+  type-installed and surface-callable, but lowering errors with a
+  structured `CodegenError::Internal`. Future milestone wires the
+  runtime Str-allocator path; revisit then.
+- Float-typed container slot layout — mono pass produces
+  `List_Fl` etc. naturally per the iter-1 `type_descriptor` `Fl`
+  arm, but no current fixture exercises a Float-typed container.
+  Verify when a future use case surfaces.
+- Pattern-matching on Float ranges (e.g. `(0.0..1.0)`) — out of
+  scope; would need a different Pattern variant entirely.
+- Float-aware ADT layout for Float-only ADT fields — same
+  monomorphisation guarantee as `List<Float>` would extend; not
+  exercised by current corpus.
+
+**Roadmap effects:** Floats `[x]`. Post-22 Prelude unblocked (was
+`depends on: Floats`); the Prelude milestone can now ship `Show`
+for `Float` and decide-against `Eq` / `Ord` for Float (both
+reflecting the partial-equality reality settled in this milestone).
+
+Next dispatch (orchestrator): `audit` skill — milestone-close
+drift review + bench-regression diagnostics + rustdoc audit.
+After audit closes clean: `fieldtest` skill — 2-4 `.ailx`
+real-world examples exercising the new Float surface.
+```
+
+- [ ] **Step 3: Commit**
+
+```bash
+git add docs/JOURNAL.md
+git commit -m "floats iter 5: JOURNAL — iter-5 close + Floats milestone close"
+```
+
+---
+
+## Iteration acceptance
+
+- [ ] `cargo build --workspace` is clean.
+- [ ] `cargo test --workspace` is GREEN — pre-existing 402 tests
+  stay GREEN; the 3 new prose tests PASS (= 405+).
+- [ ] No `unimplemented!("Floats milestone iter 5: prose")` arm
+  remains anywhere in `crates/`.
+- [ ] DESIGN.md §"Float semantics" present.
+- [ ] DESIGN.md line 2034 lists Float as a supported primitive.
+- [ ] `crates/ailang-core/tests/design_schema_drift.rs` and
+  `tests/spec_drift.rs` GREEN (the iter-1 anchors are unchanged).
+- [ ] Roadmap shows Floats `[x]`; Post-22 Prelude has no
+  `depends on: Floats` line.
+- [ ] JOURNAL has BOTH the iter-5 close entry AND the separate
+  milestone-close summary.
+- [ ] No file touched outside the four listed in the file map.
+
+When all five tasks are committed and the acceptance checklist is
+green, hand back to the orchestrator. The orchestrator dispatches
+`audit` next (milestone-close drift review + bench regression),
+followed by `fieldtest` (2-4 real-world `.ailx` examples).