docs(adr): ADR 009 aligns with ADRs 005, 006, 007 and 008 after the cross-read (improvise-felo.4)
Folds use the natural CellKey order and Seq is gone; no view action reorders the store; rollback joins the per-command snapshot; a notice per committed command, with a view-definitions flag; the non-finite wire change to ADR 005 is stated; the watermark is the whole stamp and corrections are restricted to the window; deltas cross a hop only after commit; the totals overlay is conditional on ADR 008; this ADR owns the text-width rule. 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
7ea88606e2
commit
5239d3b95a
@@ -3,7 +3,8 @@
|
||||
**Status:** proposed. ·
|
||||
**Ticket:** improvise-felo.4 (the record of this ADR; implementation goes to its own
|
||||
epic) ·
|
||||
**Relates to:** ADR 003, ADR 005, ADR 006, ADR 007, ADR 008
|
||||
**Relates to:** ADR 001 (the basis a write claims), ADR 002 (surrogates on the wire),
|
||||
ADR 003, ADR 005, ADR 006, ADR 007, ADR 008
|
||||
|
||||
## Problem
|
||||
|
||||
@@ -26,9 +27,8 @@ A problem-agnostic workspace crate with no dependencies beyond `std` (so it is
|
||||
wasm32-clean and serde-free). It provides:
|
||||
- `ZSet<K>`, a map from `K: Ord` to a non-zero `i64` weight, which is an abelian group;
|
||||
- a synchronous, single-threaded `Circuit` per process, with `delay`, `integrate`,
|
||||
`differentiate`,
|
||||
`map`, `filter`, `flat_map`, `index_by`, the bilinear delta join `join_indexed`,
|
||||
`distinct` and `aggregate`;
|
||||
`differentiate`, `map`, `filter`, `flat_map`, `index_by`, the bilinear delta join
|
||||
`join_indexed`, `distinct` and `aggregate`;
|
||||
- resumable rebuilds: building an operator from a snapshot is a `step(deadline)`, so it
|
||||
can run as a sliced job;
|
||||
- operator state behind one trace interface (look up, read a range, apply a delta), so
|
||||
@@ -54,18 +54,15 @@ is removed once its remaining uses are replaced (open question 3).
|
||||
|
||||
### 3. The cell delta
|
||||
|
||||
`DataStore::set` and `DataStore::remove` emit a `ZSet<(CellKey, CellValue, Seq)>`:
|
||||
- `+(k, v, s)` for a new cell;
|
||||
- `−(k, v₀, s) + (k, v₁, s)` for an overwrite;
|
||||
- `−(k, v₀, s)` for a removal;
|
||||
- a remove-then-set gets a fresh `s′`.
|
||||
`DataStore::set` and `DataStore::remove` emit a `ZSet<(CellKey, CellValue)>`:
|
||||
- `+(k, v)` for a new cell;
|
||||
- `−(k, v₀) + (k, v₁)` for an overwrite;
|
||||
- `−(k, v₀)` for a removal.
|
||||
|
||||
`Seq` is a per-cell sequence assigned at insertion, in `IndexMap` order, and kept by an
|
||||
overwrite. Value identity is bit identity (`f64::to_bits`), so an equal-value overwrite
|
||||
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
|
||||
natural order of ids (ADR 007 amendment 1, clause 4). A store reorder, such as entering
|
||||
records mode, reassigns `Seq` and rebuilds clause 5's per-record stage. The circuit steps
|
||||
once per model effect.
|
||||
natural order of ids (ADR 007 amendment 1, clause 4), the order eager folds in. The
|
||||
circuit steps once per model effect.
|
||||
|
||||
The record tier and the dirty flag read this delta instead of scanning the store. The
|
||||
dirty flag fires on a non-empty `(key, value)` delta, or when a fingerprint of the
|
||||
@@ -107,8 +104,8 @@ The affected pairs are evaluated in the formula graph's topological order.
|
||||
**An aggregate over an expression** (`SUM(Revenue * Price)`) is a pipeline:
|
||||
1. A per-record stage retracts and reinserts each touched record. It reads the record's
|
||||
previous cells as the store minus the delta, so it keeps no copy of the values.
|
||||
2. A map produces `(context, order key, expr)`. The order key is (context rank, minimum
|
||||
`Seq` of the record's live cells), which is eager's concatenation order.
|
||||
2. A map produces `(context, order key, expr)`. The order key is (context rank, record
|
||||
key in `CellKey` order), which is eager's concatenation order.
|
||||
3. The group aggregate, with an error channel that reads the first `Err` in order.
|
||||
|
||||
No cross product is built. A formula whose expression reads other records is evaluated
|
||||
@@ -150,9 +147,11 @@ changes no operator. The visible axis is a remap.
|
||||
- **Live keys are a cache.** A key is evicted after a period in which no request names
|
||||
it (the period is set by measurement), and every eviction is announced (clause 9).
|
||||
|
||||
**Column totals and hidden rows.** A total pools only the drawn rows, so a hidden row
|
||||
leaves it. The shape key is shared and a hide is one client's, so totals are kept over
|
||||
all rows. A read subtracts the request's H hidden cells as a temporary overlay:
|
||||
**Column totals and hidden rows.** This holds if hidden items travel in a request, which
|
||||
is ADR 008's open question. If they do not, totals are over all rows. A total pools only
|
||||
the drawn rows, so a hidden row leaves it. The shape key is shared and a hide is one
|
||||
client's, so totals are kept over all rows. A read subtracts the request's H hidden cells
|
||||
as a temporary overlay:
|
||||
- `Count` subtracts;
|
||||
- `Min` and `Max` skip keys whose whole count is hidden;
|
||||
- text counts the distinct keys left;
|
||||
@@ -192,12 +191,13 @@ 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 number never crosses as a JSON or JS double. A `numtower` `Num` crosses as its
|
||||
canonical text (ADR 005). An f64 crosses as its exact bits, which keeps `-0.0` and
|
||||
NaN payloads. That conflicts with today's `wire_f64` and with `numtower`'s `nan`
|
||||
token, which both drop the payload, so the edge carries bits for every non-finite
|
||||
value;
|
||||
- integers wider than 2⁵³, including positions and counts, cross as strings;
|
||||
- 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;
|
||||
- positions and counts below 2⁵³ are exact as JSON numbers. Wider integers cross as
|
||||
strings;
|
||||
- text crosses byte-exact, with no normalisation;
|
||||
- the delta is the unit that crosses, never `ExactSum`'s limbs. A receiver that needs
|
||||
a sum gets the host's exact read or rebuilds it from the exact deltas.
|
||||
@@ -206,11 +206,12 @@ an **edge adapter**. So every edge has the same semantics:
|
||||
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.
|
||||
- **Stamps compose end to end.** The host stamps each published batch (below), and an
|
||||
- **Stamps compose end to end.** The host stamps each committed command (below), and an
|
||||
intermediate edge forwards the stamp unchanged. So a loss anywhere on the path shows up
|
||||
downstream as a gap.
|
||||
- **One clock per process.** Each process runs its own synchronous sub-circuit. Across a
|
||||
hop, the stamped batches are the clock.
|
||||
hop, the stamped commands are the clock. A delta crosses a hop only after its command
|
||||
commits, so a remote operator never sees a delta that is later rolled back.
|
||||
- **Ordering and backpressure.** An edge delivers in order. A slow edge coalesces
|
||||
exactly: deltas are summed, and notices merged. A merged notice carries the range of
|
||||
publications it covers, `(from, to]`, so a downstream side sees no gap where nothing
|
||||
@@ -219,8 +220,9 @@ an **edge adapter**. So every edge has the same semantics:
|
||||
responses, for example several HTTP requests on one connection, as well as a socket.
|
||||
Every request can be retried, and a resync from a publication stamp is idempotent. A
|
||||
client asks for "notices since n", and the host answers from **one shared, bounded log
|
||||
of published notices**: a single log, not one per edge or client. A request older than
|
||||
the log's start is answered with a correction (below).
|
||||
of published notices**: a single log, not one per edge or client, holding the notices
|
||||
themselves (keys and flags, not values). A request older than the log's start is
|
||||
answered with a correction (below).
|
||||
- **Failure is local to a hop.** A hop may be a socket or a series of requests, and it is
|
||||
alive while its next message or request succeeds. Each hop keeps alive in both
|
||||
directions. A side that hears nothing within the timeout, or whose request fails,
|
||||
@@ -231,20 +233,23 @@ an **edge adapter**. So every edge has the same semantics:
|
||||
is the current state for the client's window and `held` is what the client holds.
|
||||
Applying it with ordinary Z-set addition gives `held + (target − held) = target`, so
|
||||
the group structure of `ZSet` provides it, with no separate machinery. The client's
|
||||
position is a **watermark**: the publication number up to which it has applied the
|
||||
stream, so everything at or before it is applied. There is one publication sequence,
|
||||
so a watermark is one number, held per shape key the client reads. The host and any
|
||||
position is a **watermark**: the whole stamp `(host instance, document_generation,
|
||||
publication)` up to which it has applied the stream, so everything at or before it is
|
||||
applied. A watermark from another host instance or generation is behind every current
|
||||
stamp. The client holds one per shape key it reads. The host and any
|
||||
gateway keep no watermarks: a client sends its own with each request.
|
||||
- where the shared log covers the watermark, the host sends the sum of the logged
|
||||
deltas after it;
|
||||
- otherwise the host sends `target`, and the client, which knows `held`, applies
|
||||
- where the shared log covers the watermark, the host sends the current values of the
|
||||
keys the log lists as moved since then, restricted to the client's window, and the
|
||||
client applies `target − held` over those keys. The log holds keys and flags; values
|
||||
are always read from the model's current state, so nothing per client is kept;
|
||||
- otherwise the host sends `target` for the whole window, and the client applies
|
||||
`target − held`;
|
||||
- a full refetch is `target − ∅`.
|
||||
|
||||
A correction is labelled with the publication range it covers, so it is applied only
|
||||
at the watermark it starts from, which makes it idempotent and resumable. It uses the same
|
||||
lossless delta form as a notice, so a client, a gateway or a worker applies it with the
|
||||
same code.
|
||||
A correction is labelled with the publication range it covers, so it is applied only at
|
||||
the watermark it starts from, which makes it idempotent and resumable. Its elements are
|
||||
`(key, value)` pairs with weights, in the lossless wire form, so a client, a gateway or a
|
||||
worker applies it with the same code.
|
||||
|
||||
Aggregation stays on the model side (ADR 008), so the operators that aggregate run on
|
||||
the model side, which may itself span a hop. Which other edges cross a wire is a
|
||||
@@ -269,12 +274,14 @@ either answer. If the client prunes, it prunes its window, fills forward with th
|
||||
query, and, when scrolling up or left, finds a new top-left by galloping backwards in
|
||||
doubling jumps (about 14 to 28 probes at density 10⁻⁴).
|
||||
|
||||
**The change notice.** After each accepted batch the host emits one notice to every
|
||||
client, addressed to none. It carries:
|
||||
**The change notice.** Each command commits on its own (ADR 006), and after each
|
||||
committed command the host emits one notice to every client, addressed to none. A frame
|
||||
whose later command fails keeps its earlier commands, and their notices, published. A
|
||||
notice carries:
|
||||
- the stamp `(host instance, document_generation, publication)`. The publication number
|
||||
increments once per published batch, and the host instance changes on restart;
|
||||
- axis changes, display relabels as `(id, display)`, and a flag when the formula set or
|
||||
`measure_agg` moved. A shared display's ` #2` suffix is never sent: the client computes
|
||||
increments once per committed command, and the host instance changes on restart;
|
||||
- axis changes, display relabels as `(id, display)`, and a flag when the formula set,
|
||||
`measure_agg`, the view definitions or the default view moved. A shared display's ` #2` suffix is never sent: the client computes
|
||||
it from the displays in scope;
|
||||
- the shape keys evicted since the last notice;
|
||||
- for each live shape key, the moved output keys (cells, formula cells and totals), as
|
||||
@@ -287,35 +294,41 @@ A notice whose key lists exceed a fixed size carries "correct" instead.
|
||||
maintained key, so it maps member keys through its own remap first. It then fetches what
|
||||
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 hop. 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.
|
||||
cannot read, or a dropped hop. 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.
|
||||
|
||||
**What this replaces.** Today's per-session mirrors and pushed diffs (`Sessions`,
|
||||
`ClientSession`, `grid_updates`, `Projection`, `Dirty`). The host keeps no per-client
|
||||
state, only the shared notice log. `GridExtent` is derived by the client, and in records mode the record count is
|
||||
fetched.
|
||||
state, only the shared notice log. `GridExtent` is derived by the client, and in records
|
||||
mode the record count is fetched. `Projection` also published the ADR 001 basis a write
|
||||
claims. Whether `project` returns it instead, and what replaces the layout tier, are
|
||||
ADR 008's questions.
|
||||
|
||||
**Edge adapters at the client.** Toward the circuit, a client's adapter is a sink for
|
||||
results and notices and a source of requests. Toward the client it is the mirror image.
|
||||
Each hop has an adapter at each end, and each end keeps only that hop's state: its
|
||||
liveness timer, and at the client end the watermark. A gateway hop (browser ⇄ gateway ⇄ host) may
|
||||
serve many clients behind one upstream connection, so the host sends one notice per
|
||||
gateway rather than one per client. In process, an edge is a function call.
|
||||
liveness timer, and at the client end the watermark. A gateway hop (browser ⇄ gateway ⇄
|
||||
host) may serve many clients behind one upstream connection, so the host sends one notice
|
||||
per gateway rather than one per client. In process, an edge is a function call.
|
||||
|
||||
### 10. Text column widths
|
||||
|
||||
The host maintains each text column's maximum display width as a histogram from width to
|
||||
count, per (shape key, column), fed by the delta of the column's text cells. Hidden rows
|
||||
come out through clause 7's overlay. Numeric widths stay with ADR 008's view-layer rule.
|
||||
This ADR owns the rule for text columns. The host maintains each text column's maximum
|
||||
display width as a histogram from width to count, per (shape key, column), fed by the
|
||||
delta of the column's text cells. Hidden rows come out through clause 7's overlay, where
|
||||
that applies. Numeric widths stay with ADR 008's view-layer rule.
|
||||
|
||||
### 11. Rollback and memory
|
||||
|
||||
- **Rollback.** The circuit's state joins the snapshot `Host::mutating_frame` takes. An
|
||||
inverse delta is not a rewind, because `delay` and `differentiate` keep history.
|
||||
- **Memory.** Resident state beside the store is the per-cell `Seq`, the multisets,
|
||||
`ExactSum` per summed group, occupancy per live shape, the successor-query index, the
|
||||
width histograms and the bounded notice log. The store itself is the integrated base and is never copied. It
|
||||
- **Rollback.** The circuit's state joins ADR 006's per-command snapshot, which is taken
|
||||
before a command's effects and restored if the command fails. An inverse delta is not
|
||||
a rewind, because `delay` and `differentiate` keep history. The requirement is that
|
||||
this snapshot does not cost O(cells) per command against ADR 008's 8 ms budget, and
|
||||
that writes do not block reads. How is for the implementation epic.
|
||||
- **Memory.** Resident state beside the store is the multisets, `ExactSum` per summed
|
||||
group, occupancy per live shape, the successor-query index, the width histograms and
|
||||
the bounded notice log. The store itself is the integrated base and is never copied. It
|
||||
is measured at ADR 008's fixture before the store-memory work begins.
|
||||
|
||||
## Alternatives rejected
|
||||
@@ -342,7 +355,7 @@ come out through clause 7's overlay. Numeric widths stay with ADR 008's view-lay
|
||||
- Integrated state is O(cells) beside the store.
|
||||
- `ExactSum` costs 568 bytes per summed group.
|
||||
- Every client receives every notice.
|
||||
- A mutating frame still clones the state for rollback.
|
||||
- Each command snapshots the circuit's state for rollback.
|
||||
|
||||
**Order** (each step is a ticket in the implementation epic, behind the differential
|
||||
test):
|
||||
@@ -356,13 +369,15 @@ test):
|
||||
8. delivery.
|
||||
|
||||
Step 8's required tests:
|
||||
- `[AddItem, SetCell]` publishes one notice, and no client asks for a correction;
|
||||
- a frame `[AddItem, SetCell]` publishes one notice per committed command, numbered
|
||||
consecutively, and no client asks for a correction;
|
||||
- a dropped notice is detected;
|
||||
- a reconnect after a host restart asks for a correction;
|
||||
- a corrected state equals the target, `held + (target − held) = target`, and
|
||||
correcting a state that is already correct is the zero Z-set (property tests over
|
||||
random edit sequences and losses);
|
||||
- a refused frame consumes no publication number;
|
||||
- a refused command consumes no publication number, and the commands before it in its
|
||||
frame stay published;
|
||||
- a dropped hop triggers a correction.
|
||||
|
||||
## Open questions
|
||||
|
||||
Reference in New Issue
Block a user