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 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VdfEGXA7aJ6ftMsCc9PJze
This commit is contained in:
committed by
Edward Langley
parent
a9ee6f00d0
commit
bb578d71e3
@@ -77,8 +77,11 @@ as `ExactSum` against rational sums, not against `Eager`.
|
|||||||
- `−(k, v₀) + (k, v₁)` for an overwrite;
|
- `−(k, v₀) + (k, v₁)` for an overwrite;
|
||||||
- `−(k, v₀)` for a removal.
|
- `−(k, v₀)` for a removal.
|
||||||
|
|
||||||
Value identity is bit identity (`f64::to_bits`), so an equal-value overwrite
|
Values compare by normal float rules, except that every NaN is one canonical value:
|
||||||
consolidates to nothing. `CellKey` gains `Ord`, which is its canonical order: the
|
`-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
|
natural order of ids (ADR 007 amendment 1, clause 4), the order eager folds in. The
|
||||||
circuit steps once per model effect.
|
circuit steps once per model effect.
|
||||||
|
|
||||||
@@ -203,9 +206,10 @@ backends:
|
|||||||
sums on 20,000 cases;
|
sums on 20,000 cases;
|
||||||
- 568 bytes per group, and about 1.3× the cost of an f64 add per update.
|
- 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
|
The sign of a zero sum follows IEEE rules for the same addends: it is `-0.0` only if
|
||||||
in their last bits, because they become correctly rounded, and a sum of `-0.0` reads
|
every addend is `-0.0`, and an exact cancellation gives `+0.0`. It lives in ADR 005's
|
||||||
`+0.0`.
|
`numtower` crate. **User-visible change:** displayed sums change in their last bits,
|
||||||
|
because they become correctly rounded.
|
||||||
|
|
||||||
### 9. Delivery
|
### 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.
|
tuple of ids, its position or an ADR 002 surrogate.
|
||||||
- **The wire form is lossless.** Nothing is lost in transport, numeric precision above
|
- **The wire form is lossless.** Nothing is lost in transport, numeric precision above
|
||||||
all:
|
all:
|
||||||
- a value never crosses as a JSON or JS double. A `numtower` `Num` crosses as its
|
- a value never crosses as a JSON or JS double. It crosses in ADR 005's canonical text:
|
||||||
canonical text (ADR 005), and an inexact finite value keeps its `#i` spelling, which
|
an inexact finite value as `#i` with its shortest round-trip spelling, which keeps
|
||||||
is already bit-exact, `-0.0` included. A non-finite value crosses as its bits, which
|
the sign of zero, infinities as `inf` and `-inf`, and every NaN as the one token
|
||||||
keeps NaN payloads. **That changes accepted ADR 005 clause 11**, whose wire spells
|
`nan`;
|
||||||
non-finite values as `inf`, `-inf` and `nan`, and it needs approval with this ADR;
|
|
||||||
- positions and counts below 2⁵³ are exact as JSON numbers. Wider integers cross as
|
- positions and counts below 2⁵³ are exact as JSON numbers. Wider integers cross as
|
||||||
strings;
|
strings;
|
||||||
- text crosses byte-exact, with no normalisation;
|
- 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
|
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
|
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
|
the identity for every value, including `-0.0`, infinities, 28-digit decimals and
|
||||||
`i128`-wide fractions.
|
`i128`-wide fractions. A NaN round-trips as the canonical NaN.
|
||||||
- **The clock is causal, never a wall clock.** Ordering, staleness and loss detection
|
- **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
|
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
|
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
|
`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
|
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
|
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`,
|
**What this replaces.** Today's per-session mirrors and pushed diffs (`Sessions`,
|
||||||
`ClientSession`, `grid_updates`, `Projection`, `Dirty`). The model store keeps no
|
`ClientSession`, `grid_updates`, `Projection`, `Dirty`). The model store keeps no
|
||||||
|
|||||||
Reference in New Issue
Block a user