AILang/design/contracts/float-semantics.md

# Float semantics

## Float semantics

`Float` is IEEE-754 binary64 (LLVM `double`). One float type ships;
no `f32` variant. The runtime / codegen contract:

**Guaranteed:**

- Every individual arithmetic builtin (`+`/`-`/`*`/`/`/`neg`) lowers
  to a single LLVM IR instruction on the Float arm: `fadd / fsub /
  fmul / fdiv double`, `fneg double`. Float comparison goes through
  the named prelude fns `float_eq` / `float_ne` / `float_lt` /
  `float_le` / `float_gt` / `float_ge` (Float has no Eq/Ord instance
  — see [Prelude (built-in) classes](prelude-classes.md)); each fn
  lowers to a single `fcmp` instruction (`oeq` / `une` / `olt` /
  `ole` / `ogt` / `oge` respectively) via the codegen intercept
  `try_emit_primitive_instance_body`, with the `alwaysinline`
  attribute on the generated `define` so the call folds to one
  instruction at every use site. 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 `float_eq` 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
  `float_eq` on Float.
- `float_eq` returns `false` whenever either operand is NaN
  (`fcmp oeq` is the ordered-equal predicate; ordered = both
  operands non-NaN).
- `float_ne` 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.
- The textual rendering of NaN through `float_to_str` (the runtime
  C helper that backs `instance Show Float` and every Float-typed
  `print` call). The libc `printf("%g", nan)`
  glue used by `float_to_str` is permitted to emit `nan` / `-nan`
  / `NaN` etc. depending on libc version and the NaN's sign bit;
  AILang does not normalise this, since the prose / surface-print
  paths render NaN as the explicit `"NaN"` spelling and Float
  rendering is for human-readable output, not round-trip.

The same libc-`%g` rendering applies to `show 1.5` / `show nan` /
`show inf` via `instance Show Float` (which calls `float_to_str`
internally — see [Prelude (built-in) classes](prelude-classes.md) for the Show ship).
The NaN-spelling caveat above is observable via `do print x` for
Float-typed `x`; the rendering is libc-version-dependent and
target-libc-specific. AILang does NOT canonicalise Float textual
representation; the LLM-author who needs deterministic Float
rendering for cross-platform test fixtures should bypass `show` /
`print` and emit a custom formatter.

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>"}` (see
[Data model](data-model.md) for the literal schema). 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.
This bits-hex encoding is what keeps Floats inside the
[Roundtrip Invariant](roundtrip-invariant.md).

**Pattern matching:** `Pattern::Lit` on `Literal::Float` (see
[Data model](data-model.md) for the pattern schema) is hard-
rejected at typecheck (`CheckError::FloatPatternNotAllowed`). IEEE
semantics make Float patterns semantically dubious — NaN never
matches via `float_eq` (its `fcmp oeq` lowering is `false` for
NaN), and bit-exact equality is rarely what an LLM-author wants.
Use the explicit comparison fns (`float_lt`, `float_gt`, ...) and
`is_nan` to discriminate Floats.

`float_to_str` (Float → Str) and `int_to_str` (Int → Str) are
fully wired through checker, codegen, and runtime. Both allocate
a fresh heap-Str slab at the call site (see [Str ABI](str-abi.md)
for the dual realisation) and carry `ret_mode: Own` so the let-binder
for the call result is RC-tracked and the slab is freed at scope
close.

Ratified by: `crates/ail/tests/eq_float_noinstance.rs`.