floats iter 5.3: DESIGN.md — new §Float semantics subsection (A5 determinism contract)

docs/DESIGN.md

@@ -2003,6 +2003,89 @@ ail run       <module>                   — 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