Brummel
8ad91e7f24
Positive-half completion of the DESIGN.md -> design/ split: design/
body cross-references are now formal, file-relative Markdown links
into the durable tier (design/ or source), and a new in-tree hard
gate (design_index_pin.rs clause-5,
design_body_links_are_durable_and_resolve) walks every
design/contracts/*.md + design/models/*.md, strips fenced code
(strip_fences toggles on ```/~~~ lines so a ]( inside a fence is not
treated as a link), extracts every ](path), and asserts the target
resolves file-relative to a real file under design/-or-crates/-or-
runtime/; never docs/, never an in-file #anchor.
RED-first via identity-stubbed strip_fences (four embedded synthetic
vectors -- first one FAILS); replacing the stub with the real
toggle-on-fence impl turns the test GREEN. clause-5 composes with
clause-3 into the complete invariant the milestone establishes:
every contract cross-reference is EITHER a resolving durable
file-link OR clause-3-forbidden decision-record prose.
Conversions (recon-and-corpus-verified closed set):
Task 2 (7 prose refs, 8 link tokens):
float-semantics.md:69 Prelude classes -> [..](typeclasses.md)
float-semantics.md:100 bare-path -> [Str ABI](str-abi.md)
embedding-abi.md:45 "Frozen value layout" -> [..](frozen-value-layout.md) (drop stale "below")
memory-model.md:44 Data model -> [..](data-model.md)
memory-model.md:105-106 Method dispatch -> [..](typeclasses.md) (drop stale "below"; the target heading lives in typeclasses.md:227, not in this file)
scope-boundaries.md:48 Str ABI -> [..](str-abi.md)
scope-boundaries.md:88 mixed split: ailang-core::desugar -> source link + Pipeline -> ../models/pipeline.md (drop stale "above")
Task 3 (2 disposition-(b) homeless removals):
pipeline.md:60-61 (see docs/PROSE_ROUNDTRIP.md) pointer removed, CLI prose preserved
authoring-surface.md:178-181 cross-tier pointer clause removed, ail merge-prose sentence preserved
Task 4: honesty-rule.md positive-half paragraph inserted between L14 and the existing L15-blank-L16; both docs_honesty_pin.rs-pinned phrases byte-identical at L14/L19 (now shifted to L19 -> L25 by the +6 lines).
Out of scope, preserved (asserted independently): every intra-file
"above/below"; embedding-abi.md:51 "frozen value layout below
specifies" (no quoted title, no (see) form); data-model.md
38/66/79/206/226 (in-fence ```jsonc schema annotations -- the inline
analog of the nominal-mention carve-out). INDEX.md and the
decision-records journal byte-unchanged; clauses 1-4 of
design_index_pin.rs source byte-unchanged (the only `-` lines in
the diff are the two-line //! header rewrite Task 1 Step 5 itself
delivers).
Boss-verified independently (not on agent report alone):
cargo test --workspace 647 passed / 0 failed
(+1 vs pre-milestone 646:
the new clause-5)
cargo test --test design_index_pin 5 / 5 passed
cargo test --test docs_honesty_pin 5 / 5 passed (additive
paragraph is pin-safe)
grep ](.../docs/.../) under design/ zero
grep ](#) under design/ zero
](-link count under design/ 8 (closed convert-set)
git diff --quiet design/INDEX.md ok
git diff --quiet decision-records ok
embedding-abi.md:48 pinned phrase byte-identical
One Concerns item: Task-5 Step-7's plan-predicted "`-` line count = 1"
was actually 2 because Task 1 Step 5 rewrote the //! header 5 -> 8
lines (removing the original L4 + L5, not just L5). Planner self-
review-item-8 miss on my part -- a verification-arithmetic error in
the plan, NOT an implementation defect. The substantive assertion
(clauses 1-4 source byte-unchanged) is fully satisfied; the
implementer correctly flagged it and proceeded. The plan stands as
written; the assertion's `1` should have been `2`. Lesson noted for
future header-rewrite tasks.
Spec: docs/specs/2026-05-19-design-ledger-formal-links.md
(grounding-check PASS x3 across two corpus-grounded amendments --
clause-6 + cross-ref definition; clause-5 fence-skip + closed
convert-set enumeration).
Next: mandatory milestone-close audit (no fieldtest -- zero
authoring-surface change, reasoned exclusion).
106 lines
5.1 KiB
Markdown
106 lines
5.1 KiB
Markdown
# 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 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.
|
|
- The textual rendering of NaN through `float_to_str` (the runtime
|
|
C helper that backs `instance Show Float` and, post-iter-rpe.1,
|
|
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](typeclasses.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>"}`. 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) 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`.
|