From bb578d71e3e50f74c883e9861fce0f14db6e1d12 Mon Sep 17 00:00:00 2001 From: "Claude (adr9-steward)" Date: Fri, 9 Oct 2026 22:44:30 -0700 Subject: [PATCH] docs(adr): ADR 009 values compare by float rules, NaN canonical NaN payloads are not preserved: every NaN is one canonical value in the delta and crosses as ADR 005's `nan` token, so ADR 009 no longer changes ADR 005 clause 11. Zeros follow IEEE: -0.0 equals +0.0, and a zero sum takes the sign IEEE gives the same addends. The round-trip property test asserts a NaN comes back as the canonical NaN. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01VdfEGXA7aJ6ftMsCc9PJze --- context/adr/009-incremental-evaluation.md | 29 +++++++++++++---------- 1 file changed, 16 insertions(+), 13 deletions(-) diff --git a/context/adr/009-incremental-evaluation.md b/context/adr/009-incremental-evaluation.md index 36031e02..a791116a 100644 --- a/context/adr/009-incremental-evaluation.md +++ b/context/adr/009-incremental-evaluation.md @@ -77,8 +77,11 @@ as `ExactSum` against rational sums, not against `Eager`. - `−(k, v₀) + (k, v₁)` for an overwrite; - `−(k, v₀)` for a removal. -Value identity is bit identity (`f64::to_bits`), so an equal-value overwrite -consolidates to nothing. `CellKey` gains `Ord`, which is its canonical order: the +Values compare by normal float rules, except that every NaN is one canonical value: +`-0.0` equals `+0.0`, and an equal-value overwrite consolidates to nothing. NaN payloads +are not preserved, so nothing can be smuggled through them. Today's record tier compares +bits, so overwriting `0.0` with `-0.0` stops counting as a change. Multisets order values +by `f64::total_cmp` after mapping every NaN to the canonical one and `-0.0` to `+0.0`. `CellKey` gains `Ord`, which is its canonical order: the natural order of ids (ADR 007 amendment 1, clause 4), the order eager folds in. The circuit steps once per model effect. @@ -203,9 +206,10 @@ backends: sums on 20,000 cases; - 568 bytes per group, and about 1.3× the cost of an f64 add per update. -It lives in ADR 005's `numtower` crate. **User-visible changes:** displayed sums change -in their last bits, because they become correctly rounded, and a sum of `-0.0` reads -`+0.0`. +The sign of a zero sum follows IEEE rules for the same addends: it is `-0.0` only if +every addend is `-0.0`, and an exact cancellation gives `+0.0`. It lives in ADR 005's +`numtower` crate. **User-visible change:** displayed sums change in their last bits, +because they become correctly rounded. ### 9. Delivery @@ -229,11 +233,10 @@ an **edge adapter**. So every edge has the same semantics: tuple of ids, its position or an ADR 002 surrogate. - **The wire form is lossless.** Nothing is lost in transport, numeric precision above all: - - a value never crosses as a JSON or JS double. A `numtower` `Num` crosses as its - canonical text (ADR 005), and an inexact finite value keeps its `#i` spelling, which - is already bit-exact, `-0.0` included. A non-finite value crosses as its bits, which - keeps NaN payloads. **That changes accepted ADR 005 clause 11**, whose wire spells - non-finite values as `inf`, `-inf` and `nan`, and it needs approval with this ADR; + - a value never crosses as a JSON or JS double. It crosses in ADR 005's canonical text: + an inexact finite value as `#i` with its shortest round-trip spelling, which keeps + the sign of zero, infinities as `inf` and `-inf`, and every NaN as the one token + `nan`; - positions and counts below 2⁵³ are exact as JSON numbers. Wider integers cross as strings; - text crosses byte-exact, with no normalisation; @@ -242,8 +245,8 @@ an **edge adapter**. So every edge has the same semantics: The stamp rule detects lost messages, but nothing would detect a lossy encoding. So every element type has a round-trip property test, where encoding then decoding is - the identity for every value, including `-0.0`, NaN payloads, 28-digit decimals and - `i128`-wide fractions. + the identity for every value, including `-0.0`, infinities, 28-digit decimals and + `i128`-wide fractions. A NaN round-trips as the canonical NaN. - **The clock is causal, never a wall clock.** Ordering, staleness and loss detection use only the stamp sequence (below), a logical clock the host advances once per committed command. Each process runs its own synchronous sub-circuit, and across an @@ -355,7 +358,7 @@ moved. It asks for a correction when it sees a publication gap, a new `document_generation` or host instance, its shape in the eviction list, a notice it cannot read, or a dropped connection or failed request. A slow client may merge pending notices: the union of keys, the covered range of publications, and axis changes kept in order. Because the -wire is lossless, outputs keep the circuit's bit identity end to end. +wire is lossless, outputs keep the circuit's value identity end to end. **What this replaces.** Today's per-session mirrors and pushed diffs (`Sessions`, `ClientSession`, `grid_updates`, `Projection`, `Dirty`). The model store keeps no