docs(context): the reasoning and the evidence for delivery (improvise-z2vr)
Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VdfEGXA7aJ6ftMsCc9PJze
This commit is contained in:
committed by
Edward Langley
parent
0e6ad9e96a
commit
eb15df6c36
@@ -0,0 +1,198 @@
|
||||
# Delivery: the reasoning
|
||||
|
||||
ADR 009 step 8 (improvise-z2vr): notices per committed command, watermarks, corrections, the shared
|
||||
bounded log, the lossless wire and the edge adapters. The decisions are the ADR's clause 9
|
||||
(`context/adr/009-incremental-evaluation.md`). This file records how the code reads them, the places
|
||||
the ADR left a choice open, and the places it could not be satisfied yet. The evidence for each test is
|
||||
in `context/test-evidence/delivery.md`.
|
||||
|
||||
**What is built, and against what.** Neither the incremental backend nor ADR 008's render model
|
||||
exists. So the source of every target is the existing Eager path: the cells a `GridLayout` draws for a
|
||||
view. Everything below is correct against that source and does not depend on what replaces it. The
|
||||
circuit will supply "moved output keys" where `Delivery::commit` diffs two `Output`s today, and
|
||||
nothing else changes.
|
||||
|
||||
| piece | where |
|
||||
|---|---|
|
||||
| wire values, keys, Z-set elements | `improvise-protocol/src/delivery/wire.rs` |
|
||||
| stamp, range, notice, merge | `.../notice.rs` |
|
||||
| request, correction, `Edge` | `.../exchange.rs` |
|
||||
| the client end: watermark, held cells, when to ask | `.../client.rs` |
|
||||
| the publisher, the log, live shapes, answering | `improvise-command/src/ui/delivery.rs` |
|
||||
| `Host` integration, in-process and JSON edges | `ui/host.rs`, `ui/delivery.rs` |
|
||||
|
||||
## 1. The wire form
|
||||
|
||||
A number crosses as ADR 005's canonical text through `numtower::Num`: `#i0.1`, `#i-0.0`, `inf`,
|
||||
`-inf`, `nan`. `WireNum` accepts only text the tower itself writes (`parse` re-prints and compares),
|
||||
because a second spelling of one value would make textual equality wrong. Equality of wire values is
|
||||
textual, so `-0.0` and `+0.0` are different wire values. That is the opposite of the cell delta in
|
||||
clause 3, which makes them equal; the two do not meet, because the delta is a store-side signal and a
|
||||
correction is a value the client displays.
|
||||
|
||||
An integer is a JSON number below 2^53 and a decimal string at or above it (`wide`, `wide_weight`).
|
||||
That covers stamps, positions, window sizes and weights. Text is a JSON string, byte-exact.
|
||||
|
||||
`CellValue` is still an `f64`, so `WireValue::of` writes it through `Num::inexact` and
|
||||
`to_cell_value` narrows an exact number to `f64`. The round-trip properties therefore run over
|
||||
28-digit decimals and `i128`-wide fractions at the `WireNum` level, where they are lossless, and over
|
||||
`f64` at the `CellValue` level, where only the NaN payload is dropped.
|
||||
|
||||
`CellKey` is not `Serialize`, so a cell is named by `WireKey`, its `(category, item)` tuple. Under
|
||||
ADR 007 those become ids; nothing here reads the strings.
|
||||
|
||||
## 2. Stamps and notices
|
||||
|
||||
`Stamp` is `(host instance, document_generation, publication)`. A stamp from another host or
|
||||
generation is behind every current one (`Stamp::is_behind`). The publication number increments once
|
||||
per committed command, and it keeps counting across a document swap rather than restarting, so a
|
||||
number is never reused within one host instance.
|
||||
|
||||
**What "a committed command" is.** The host publishes one notice for each `Command::Model` that
|
||||
lands. A view command (cursor, mode, a view switch) publishes nothing: it is view-store state and
|
||||
the model store has no business announcing it. A write that changes nothing still publishes, with
|
||||
empty `moved`, because the contract is one notice per commit and a client counts them.
|
||||
|
||||
**A notice names moved keys per live shape**, plus axis changes, relabels, flags, evicted shapes. Axis
|
||||
changes are computed from the categories' item lists before and after (`axis_changes`): insert and
|
||||
remove by item, and a reorder when the surviving items changed order. `Relabel` exists and is never
|
||||
emitted: with names as identity a rename is a remove and an insert, and display writes arrive with
|
||||
ADR 007. Flags come from comparing the formula texts, `measure_agg`, the views and the default view.
|
||||
|
||||
`Notice::merge` joins two notices only when the second starts where the first ends (same epoch).
|
||||
Anything else returns both unchanged, so a merge cannot hide a loss. `Moved::Correct` absorbs key
|
||||
lists in a merge.
|
||||
|
||||
## 3. Requests and corrections
|
||||
|
||||
A request is a shape key, a window and one of three asks. `Ask::Correction` is "bring me up from my
|
||||
watermark"; `Ask::Fetch` is "the current values of these keys, covering the publications up to
|
||||
`through`"; `Ask::Notices` is "the notices after this stamp".
|
||||
|
||||
**A correction's elements are `target`, not `target - held`.** The host does not know what the client
|
||||
holds, so it sends the target restricted as the body says, and the client computes `target - held`
|
||||
with ordinary Z-set subtraction. A `Moved` body restricts both sides to the named keys, so a key the
|
||||
target no longer holds is removed. A `Window` body replaces everything held.
|
||||
|
||||
**`through` is not `at`.** `at` is the state the values were read at, always the latest committed one.
|
||||
`through` is how far the correction advances the client's watermark. They differ for a `Fetch`:
|
||||
the client named the keys of the notices it has seen, and a later commit may have moved other keys
|
||||
whose notice it has not seen yet. Advancing to `at` would make that notice look already applied, so
|
||||
the watermark advances only to `through` and the later notice refetches its keys. The values are
|
||||
at least as new as the watermark claims, never older.
|
||||
|
||||
**An axis change makes the correction a window refetch.** A moved key list says which values changed,
|
||||
not which keys sit in the client's window, and an insert or remove shifts cells into and out of it
|
||||
without moving them. The ADR has the client re-derive positions from the axis changes and fetch what
|
||||
it lacks. That needs ADR 008's render model, which this layer does not have. So the client records a
|
||||
notice that moved an axis (`restructured`), asks `Fetch { window: true }`, and the host answers with a
|
||||
`Window` body whose `carried` notice holds the axis changes, in order. This is a fetch, not a
|
||||
correction, so the required test "a frame `[AddItem, SetCell]` ... and no client asks for a correction"
|
||||
holds: it asserts no `Ask::Correction` was sent. When the render model exists the client can narrow
|
||||
the fetch to the cells that entered its window.
|
||||
|
||||
## 4. The client
|
||||
|
||||
`EdgeClient` holds, per shape: the window, the held cells (a `ZSet`), the **watermark** (applied
|
||||
through), `seen` (the last notice received), the notices received and not yet fetched, `restructured`
|
||||
and `stale`.
|
||||
|
||||
`on_notice` ignores a duplicate (`to <= seen`), treats a gap, another host or generation, a shape in the
|
||||
evicted list, or `Moved::Correct` as "ask for a correction", and otherwise queues the moved keys. The
|
||||
watermark advances over a notice only when nothing is owed, so it never claims a key it has not fetched.
|
||||
|
||||
`apply` takes a correction. It is a duplicate if the watermark already covers `through`; a `Moved`
|
||||
body is a gap unless it starts at or below the watermark. Otherwise `held += target - held`, the
|
||||
watermark becomes `through`, and the queued notices it covers are dropped. A late reply older than
|
||||
the watermark therefore cannot regress the state, which is what makes a retry safe.
|
||||
|
||||
`connection_lost`, `request_failed` and `unreadable` set `stale`, which `wants` turns into
|
||||
`Ask::Correction` from the watermark the client held. A duplicate whose `through` equals the watermark
|
||||
also clears `stale`: the host has said there is nothing newer.
|
||||
|
||||
**A lost final notice is invisible to a listener.** The next notice shows the gap, but if none comes the
|
||||
client never learns. `poll` is the answer: it asks `Ask::Notices { after: seen }`, which the host
|
||||
answers from the log. The property test ends every history with a `poll` for this reason.
|
||||
|
||||
`Event`s (`Axis`, `Relabel`, `Flags`, `Resync`) are what the shape's consumer applies to its
|
||||
structure. They are deduplicated by `events_through`, because an axis change is not idempotent.
|
||||
`Resync` means positions are unknown: re-derive them from what is held.
|
||||
|
||||
## 5. The Eager stand-in for a shape key
|
||||
|
||||
The real key is the circuit's: axes, None categories, filters, pages, `measure_agg`, in canonical id
|
||||
form. Here a shape key is `eager:view/<name>` (`shape_of_view`) and the output is that view's layout.
|
||||
That is finer than the real key, which is always safe: two views that would share state do not, and
|
||||
nothing else is lost. A view that no longer exists is announced as evicted.
|
||||
|
||||
`Output` is the shape's whole output, keyed by `WireKey` with the position attached. `target` restricts
|
||||
it to a window. `moved_since` compares two outputs by value and presence; a changed position is an axis
|
||||
change, not a key.
|
||||
|
||||
**This costs O(grid) per live shape per commit.** It stands in for the circuit's delta, and it is the
|
||||
reason the module exists beside, not instead of, the incremental work: nothing else in the host reads
|
||||
the whole grid per command.
|
||||
|
||||
## 6. The host
|
||||
|
||||
`Delivery` is one value per document, held by `Host`. `Host::handle` calls `Delivery::commit` after
|
||||
each `Command::Model` that lands, and `Host::deliver` answers a `Request`.
|
||||
|
||||
**Reads see only the last committed state.** `answer` reads `Live::output`, which `commit` refreshed,
|
||||
and never the workbook. A value a failed command wrote is not in it.
|
||||
|
||||
**Rollback.** `Host::mutating_frame` clones the `Delivery` beside the app snapshot and the session
|
||||
mirrors, and `undo_frame` puts it back. The clone is cheap (`Arc` for outputs, notices and structure,
|
||||
bounded by the log's capacity). So a refused frame consumes no publication number and publishes nothing.
|
||||
|
||||
**The ADR and ADR 001 disagree here, and ADR 001 wins until ADR 006 exists.** Clause 9 says a frame
|
||||
whose later command fails keeps its earlier commands and their notices, "each command commits on its own
|
||||
(ADR 006)". Today's host undoes the whole frame (ADR 001 clause 4, `Host::mutating_frame`), and ADR 006 is
|
||||
not in the tree. The required test "a refused command consumes no publication number, and the commands
|
||||
before it in its frame stay published" is split in two. The first half is tested. The second is
|
||||
tested as its opposite, `commands_before_a_refused_one_are_rolled_back_with_their_notices_under_adr_001`,
|
||||
which is the test to flip when per-command commit lands: the publisher already supports it, since it
|
||||
publishes whatever the host tells it committed.
|
||||
|
||||
**The host instance** is a random id, never a time (`Host::new` takes one from `RandomState`).
|
||||
`RandomState` has no entropy on `wasm32-unknown-unknown`, so a worker must pass a real one through
|
||||
`Host::with_instance`. A restarted host with the same id would accept a stale watermark as current.
|
||||
|
||||
**Eviction** (`evict_idle`) takes a local count and an idle length in the same unit, never a wall clock
|
||||
compared across machines. An evicted key is announced in the next notice and forgotten; naming it again
|
||||
revives it with `since` set to the current publication, so a watermark older than that is answered with
|
||||
a window.
|
||||
|
||||
## 7. Answering
|
||||
|
||||
`covered(shape, watermark)` is true when the watermark is in the current epoch, is not ahead of the
|
||||
host, and either equals the current publication or is no older than both the log's start and the time
|
||||
the shape went live. Only then are the moved keys of `(watermark, now]` complete.
|
||||
|
||||
- covered, only moved keys: a `Moved` body with those keys' current values in the window;
|
||||
- covered, with axis changes or relabels in range: a `Window` body with `carried`;
|
||||
- a `Moved::Correct` in range, or not covered: a `Window` body from `None`, which is `target - empty`.
|
||||
|
||||
A notice lists no keys for a shape whose list passed `MAX_KEYS`; it says `Moved::Correct` instead, and
|
||||
costs every reader a correction. `LOG_CAPACITY` bounds the single shared log. Both are set per host by
|
||||
`limit_delivery` so a test can reach them.
|
||||
|
||||
The token in a request is carried and echoed by the client and never read by the host.
|
||||
|
||||
## 8. Edge adapters
|
||||
|
||||
`Edge` is one end of a stream: `call(Request) -> Result<Reply, EdgeError>`. `InProcess` is the
|
||||
function call; `WireEdge` passes request and reply through JSON text, the adapter at a wire boundary,
|
||||
so the lossless properties are exercised by every test that uses it. Neither adds a `ClientFrame` or
|
||||
`ServerFrame` variant: the page does not read notices yet, and adding the frames means changing the
|
||||
browser and the worker together (ADR 008 replaces `Projection`). A transport pushes
|
||||
`Host::take_notices()`.
|
||||
|
||||
## Not done, and why
|
||||
|
||||
- **The notices are not sent by the socket or worker hosts.** They need frame variants and the page
|
||||
(above).
|
||||
- **A twin at the serving end** (a server-side watermark or filter) is not built; the ADR allows it and
|
||||
does not require it.
|
||||
- **A pushed filter** is the client's `window`, applied on every request.
|
||||
- **Hidden-item overlays, pruning queries and column widths** are ADR 008 and clause 10.
|
||||
@@ -0,0 +1,95 @@
|
||||
# Test evidence: delivery
|
||||
|
||||
What each delivery test guards and which injected fault it was seen to fail on. Keyed by test name.
|
||||
The reasoning is in `context/code/delivery.md`. Each fault was put into the source one at a time,
|
||||
the suite run, the fault reverted with `git checkout -- <file>`, and the suite run again.
|
||||
|
||||
The host-side tests are in `crates/improvise-command/src/ui/delivery_tests.rs`, the client's in
|
||||
`crates/improvise-protocol/src/delivery/client_tests.rs`, the wire's in `delivery/wire.rs`.
|
||||
|
||||
## The injected faults, by what failed
|
||||
|
||||
- **The host reports no moved keys** (`let keys = BTreeSet::new()` in `Delivery::commit`): seven
|
||||
host-side tests fail: `a_dropped_connection_or_a_failed_request_triggers_a_correction_and_the_session_resumes`,
|
||||
`a_pull_only_client_follows_the_log_without_a_correction`,
|
||||
`a_notice_names_the_moved_cells_including_a_formula_cell_it_did_not_write`,
|
||||
`values_keep_every_bit_from_the_cell_to_the_client`,
|
||||
`an_oversized_notice_says_correct_and_costs_every_reader_a_correction`,
|
||||
`a_dropped_notice_is_detected_and_a_correction_repairs_it` and the random property.
|
||||
`a_frame_of_two_commands_publishes_one_notice_each_and_no_client_asks_for_a_correction` still
|
||||
passes, on purpose: its `AddItem` makes the client refetch the window, which also fetches the write.
|
||||
- **The client treats every notice as contiguous** (`false => true` in `on_notice`):
|
||||
`a_dropped_notice_is_detected`, `a_dropped_notice_is_detected_and_a_correction_repairs_it` and the
|
||||
random property.
|
||||
- **A failed frame does not put the `Delivery` back** (`undo_frame` drops `published`):
|
||||
`a_refused_command_consumes_no_publication_number`,
|
||||
`commands_before_a_refused_one_are_rolled_back_with_their_notices_under_adr_001` and
|
||||
`a_refused_frame_is_never_read_back`.
|
||||
- **A moved correction replaces instead of subtracting held** (`target` for `target - held_there`):
|
||||
`a_moved_correction_applies_only_at_the_watermark_it_starts_from` and
|
||||
`a_moved_key_the_target_no_longer_holds_is_removed`. The same for a window correction (`target` for
|
||||
`target - held`): `a_correction_equals_the_target_and_a_second_one_is_the_zero_zset`,
|
||||
`a_correction_replaces_what_is_held_not_adds_to_it` and
|
||||
`a_correction_already_covered_is_idempotent_and_never_regresses`.
|
||||
- **A wire number loses the sign of zero** (`Num::inexact(x + 0.0)` in `WireNum::of_f64`):
|
||||
`a_float_crosses_in_canonical_text_with_the_sign_of_zero` and
|
||||
`a_float_keeps_every_bit_but_the_nan_payload`.
|
||||
- **`covered` ignores the log's start and the shape's liveness**:
|
||||
`a_watermark_the_log_covers_gets_the_moved_keys_and_one_it_does_not_gets_the_window` and
|
||||
`an_evicted_shape_is_announced_and_its_reader_corrects`.
|
||||
- **The client does not remember an axis change** (`restructured` never set):
|
||||
`an_axis_change_that_shifts_an_unmoved_cell_into_the_window_refetches_the_window`. The host's own
|
||||
`restructured` test alone fails only the random property, since the client's `window` flag also forces
|
||||
a window.
|
||||
- **`Stamp::same_epoch` ignores the host instance**:
|
||||
`a_notice_from_another_host_or_generation_asks_for_a_correction`,
|
||||
`a_stamp_from_another_epoch_is_behind_every_current_one`,
|
||||
`a_reconnect_after_a_host_restart_asks_for_a_correction_from_the_old_watermark` and
|
||||
`a_notice_from_a_restarted_host_asks_for_a_correction_too`.
|
||||
|
||||
## Entries
|
||||
|
||||
### a_refused_frame_is_never_read_back
|
||||
|
||||
The first fixture filled the document to the category limit and then refused the frame at its basis
|
||||
check, so the write never ran and the test passed with the `Delivery` not restored. A fixture that fails
|
||||
in a wider shape than the fault: the frame never reached `mutating_frame`. It now writes North, then
|
||||
loads a missing document, and asserts `Rejection::MutationRefused` so the write is known to have run. The
|
||||
rival above fails it with `77.0` held.
|
||||
|
||||
### a_corrected_state_is_the_target_and_correcting_it_again_is_the_zero_zset
|
||||
|
||||
The random property: histories of up to twelve single-command frames (writes of `0.0`, `-0.0`, both
|
||||
infinities, NaN and `0.1 + 0.2`, item adds and removes, a formula), a random window, notices delivered
|
||||
or dropped, connections lost, requests dropped, replies dropped and garbled. It ends with a `poll`, then
|
||||
asserts the client holds exactly what the grid draws in its window, and that `target - held` is the zero
|
||||
Z-set. The oracle (`drawn`) reads `GridLayout` itself and shares nothing with `Output`.
|
||||
|
||||
Without the closing `poll` a lost last notice is not detectable by a listener, and the property
|
||||
reported it as a stale client (minimal case: one `Remove`, notice dropped, no later notice).
|
||||
|
||||
The first version of the property also failed on a window of one cell after a remove, and that was a
|
||||
real gap in the correction, not in the test: the remove moved South into the window without moving its
|
||||
value. It is the reason for the `restructured` rule (`delivery.md` §3).
|
||||
|
||||
### a_frame_of_two_commands_publishes_one_notice_each_and_no_client_asks_for_a_correction
|
||||
|
||||
Step 8's first required test. The frame's first command carries one basis stating both records
|
||||
(`Host`'s frame rule: the first mutation's basis stands for the frame), which the test helper builds.
|
||||
|
||||
### commands_before_a_refused_one_are_rolled_back_with_their_notices_under_adr_001
|
||||
|
||||
Step 8 requires that the commands before a refused one stay published. Today's host undoes the whole
|
||||
frame (ADR 001 clause 4), so this test asserts the opposite and names the reason. Flip it when ADR 006
|
||||
makes each command commit on its own.
|
||||
|
||||
### a_dropped_connection_or_a_failed_request_triggers_a_correction_and_the_session_resumes
|
||||
|
||||
The three transport faults (request dropped, reply dropped, reply unreadable) each leave the client
|
||||
asking for `Ask::Correction` from the watermark it held, and the next request carries the same session
|
||||
token and that watermark.
|
||||
|
||||
### an_axis_change_that_shifts_an_unmoved_cell_into_the_window_refetches_the_window
|
||||
|
||||
A one-cell window, a remove that moves South into it. The notice lists only North, so a client that
|
||||
fetches moved keys alone ends with an empty window.
|
||||
@@ -69,6 +69,7 @@ const SECTIONS = [
|
||||
["context/code/gp.md", "code/gp", "gp-tree and improvise-gp"],
|
||||
["context/code/numtower.md", "code/numtower", "numtower, the numeric tower"],
|
||||
["context/code/zset.md", "code/zset", "zset, the Z-set group"],
|
||||
["context/code/delivery.md", "code/delivery", "delivery, notices and corrections"],
|
||||
["context/code/kb-tool.md", "code/kb-tool", "The kb tool"],
|
||||
["context/code/tooling.md", "code/tooling", "The repository's own checkers"],
|
||||
],
|
||||
@@ -89,6 +90,7 @@ const SECTIONS = [
|
||||
["context/test-evidence/gp.md", "test-evidence/gp", "gp-tree and improvise-gp"],
|
||||
["context/test-evidence/numtower.md", "test-evidence/numtower", "numtower"],
|
||||
["context/test-evidence/zset.md", "test-evidence/zset", "zset"],
|
||||
["context/test-evidence/delivery.md", "test-evidence/delivery", "delivery"],
|
||||
["context/test-evidence/tooling.md", "test-evidence/tooling", "The repository's own gates"],
|
||||
["context/test-evidence/layout-cost.md", "test-evidence/layout-cost", "Layout and keypress cost"],
|
||||
["context/test-evidence/scale-bisect.md", "test-evidence/scale-bisect", "Scale bisect"],
|
||||
|
||||
Reference in New Issue
Block a user