From 47b32bff3d0672789d5a382008930e4da9b52798 Mon Sep 17 00:00:00 2001 From: Brummel Date: Sun, 10 May 2026 16:38:24 +0200 Subject: [PATCH] =?UTF-8?q?floats=20iter=205.3:=20DESIGN.md=20=E2=80=94=20?= =?UTF-8?q?new=20=C2=A7Float=20semantics=20subsection=20(A5=20determinism?= =?UTF-8?q?=20contract)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- docs/DESIGN.md | 83 ++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 83 insertions(+) diff --git a/docs/DESIGN.md b/docs/DESIGN.md index 02d7aae..46e89e7 100644 --- a/docs/DESIGN.md +++ b/docs/DESIGN.md @@ -2003,6 +2003,89 @@ ail run — build + execute (tempdir), passthro Fixing a rustdoc warning is part of the iteration that introduced it, not a follow-up. +## 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 + `0x7ff8000000000000` 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`. + ## What is not (yet) supported Snapshot of the current boundary. Items move out of this list