test(zset): the edge over a hostile network, and the cases the review found

Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01VdfEGXA7aJ6ftMsCc9PJze
This commit is contained in:
Claude (dbsp-threads)
2026-10-10 21:33:21 -07:00
committed by Edward Langley
parent 5c577cddb1
commit 5344d287a9
9 changed files with 671 additions and 133 deletions
+1 -1
View File
@@ -243,4 +243,4 @@ pushes `Host::take_notices()`.
- **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.
**The same edge, generalised in `zset`.** `zset::edge` (`context/code/zset.md`, "Edges") carries Z-set deltas between two circuits with the rules of this file (stamps, coalescing by summing, `target - held`, left epochs) and no log; this layer is unchanged and does not use it.
**The same edge, generalised in `zset`.** The `zset` crate's edge module, `crates/zset/src/edge.rs` (`context/code/zset.md`, "Edges") carries Z-set deltas between two circuits with the rules of this file (stamps, coalescing by summing, `target - held`, token-matched answers) and no log; this layer is unchanged and does not use it.
+45 -24
View File
@@ -335,37 +335,58 @@ Nothing here spawns a thread; whoever owns each circuit calls `pump` and `poll`.
(`a_full_pipe_coalesces_exactly_and_keeps_the_range`).
4. **Order and gaps.** The receiver applies a delta only if it is in the epoch it joined and
`from == watermark`. `to <= watermark` is a duplicate and changes nothing. Anything else (a
gap, an overlap, an unjoined epoch, a frame that does not decode) sets `stale`, and `stale`
makes the next `poll` send a `Request`.
5. **A receiver always joins by correction, never by a delta.** A new `EdgeSource` is stale. The
sender answers a request with `Correction { epoch, through: seq, target: integral }` and the
receiver pushes `target - held` (delivery's rule), so the sender keeps its integral and the
receiver keeps what it has applied: two copies of the edge's state, one at each end. There is
no shared log as in delivery, so every answer is a full correction. Joining by a first delta
with `from == 0` was tried first, and the differential property found it wrong: a sender that
restarted with a non-empty integral at `seq 0` looks like a fresh one
(`two_circuits_on_an_edge_equal_one_circuit`, shrunk to a `RestartSink` after a rollback-free
history).
6. **A restart is a new epoch.** `EdgeSink::restart(epoch, seq, integral)` keeps the pipe and
codec. The receiver sees a delta from an epoch it has not joined, goes stale, and the answer
moves it onto the new epoch, adding the old one to `left` (the newest 16). Frames from a left
epoch change nothing, so a late reply from a dead sender cannot regress the receiver. A
receiver that restarts (`EdgeSource::restart`) is stale again.
7. **A lost final message is invisible to the receiver.** `connection_lost()` is the host's
gap, an overlap, a frame that does not decode) is a *mark*: `stale` is set and a counter of
troubles moves. `stale` makes the next `poll` send a `Request`.
5. **A receiver joins an incarnation only by the answer to its latest request.** A `Request`
carries a token (the receiver's counter, which `EdgeSource::restart` keeps), and the sender
echoes the token of the last request it read in its `Correction { epoch, through: seq, token,
target: integral }`. The receiver pushes `target - held` (delivery's rule). This carries over
delivery's third fix, "the host that answers a request is live" (`delivery.md` section 4): a
frame from an incarnation the receiver has not joined only marks it stale and never moves the
watermark, unless it is the answer to the request just sent. A reply to an older request, a
duplicate, or a late reply from a dead sender is therefore never a join. A correction from the
joined incarnation applies when it is ahead of the watermark, whoever asked. There is no shared
log as in delivery, so every answer is a full correction. Two earlier designs were wrong, each
found by a property: joining by a first delta with `from == 0` (a restarted sender with a
non-empty integral at `seq 0` looks fresh), and a `left` list of incarnations (a late reply
from an incarnation never joined sent the receiver back and shut the live sender out:
`a_late_reply_from_a_dead_incarnation_changes_nothing`). There is no `left` list now.
6. **What clears `stale`.** Only an answer, and only if it is not behind the watermark
(`an_answer_older_than_the_watermark_does_not_clear_stale`) and no mark has been made since
its request went out (`trouble_seen_after_a_request_keeps_its_answer_from_clearing_stale`);
an answer at the watermark says nothing newer exists
(`an_answer_at_the_watermark_says_nothing_newer_and_clears_stale`).
7. **A restart is a new epoch, and an epoch is never reused.** `EdgeSink::restart(epoch, seq,
integral)` keeps the pipe and codec. The first frame of an unjoined epoch makes the receiver
re-ask once for that epoch, because the request may have died with the sender that read it
(`a_new_epoch_frame_re_asks_once_after_a_lost_request`). A sender that reuses an epoch id at
a lower seq cannot be told from a reordered old frame, so the receiver ignores it as a
duplicate and is stranded until the sender restarts again: the caller must pass a fresh epoch.
A receiver that restarts (`EdgeSource::restart`) is stale again.
8. **A lost final message is invisible to the receiver.** `connection_lost()` is the host's
timeout: it marks the receiver stale and lets it ask again. The host calls it on its own local
monotonic timeout, never by comparing times across machines. It is also what retries a request
whose answer was lost. Requests carry the receiver's stamp and this sender does not read it.
8. **The wire form is a hook.** `EdgeCodec<K>` turns a `Frame<K>` into `Wire` and back, with
monotonic timeout, never by comparing times across machines, and it must be longer than the
round trip, or every answer is one request behind. Requests carry the receiver's stamp and
this sender does not read it.
9. **The wire form is a hook.** `EdgeCodec<K>` turns a `Frame<K>` into `Wire` and back, with
`CodecError` for what does not decode; `Direct` is the identity. `improvise-protocol` is to
implement it for its own key types in the lossless text of ADR 005, and `zset` stays free of
serde. The tests run every history through a hand-written text codec
(`the_same_histories_through_a_text_codec`).
9. **Threads.** `EdgeSink` and `EdgeSource` are `Send` when the pipe and codec are. The real
10. **Threads.** `EdgeSink` and `EdgeSource` are `Send` when the pipe and codec are. The real
two-thread test steps a producer on one thread and a consumer on another with a capacity-2 channel
(`a_circuit_on_each_of_two_threads_equals_one_circuit`). The property test simulates arbitrary
interleavings, losses and restarts by choosing the order of `commit`, `pump`, `poll` and step.
(`a_circuit_on_each_of_two_threads_equals_one_circuit`). Two properties simulate arbitrary
interleavings: `tests/edge.rs` over FIFO pipes that lose frames, and `tests/edge_net.rs` over a
network that drops, duplicates, garbles and reorders in-flight frames both ways, restarts either
end at any seq and times out (capacity 1 to 4). It checks after every action that the
receiver's applied state is the sender's integral at the stamp it claims, and that it never
moves to an older incarnation.
`poll` and `committed_from` panic inside a transaction: a rollback drops what a poll pushed,
and the stamps would not know (`a_poll_inside_a_transaction_is_refused`).
`committed` checks overflow before it changes anything, so a caught panic leaves the sink as
it was. `pump` clones the waiting delta each attempt against a full pipe; that is left.
Native threads are assumed; `mpsc` and `Send` compile on wasm32 and nothing runs there.
10. **Not built.** A sink with a log to answer a watermark with only the moved keys (delivery's
11. **Not built.** A sink with a log to answer a watermark with only the moved keys (delivery's
`Moved` correction). A pipe that blocks or notifies, because `try_send` and `try_recv` are
polling. Key-sharded data parallelism inside a circuit: its exchange step would be this same
edge, and nothing here forbids it.
+64 -3
View File
@@ -664,10 +664,71 @@ why that assertion is there.
A new epoch holding `{1, 2}` plus one command `9`: the receiver applies only `{9}` and stamps
`(2, 1)`. Rival R3 applies the whole target and fails.
### a_late_frame_from_an_epoch_the_receiver_left_changes_nothing
### a_late_reply_from_a_dead_incarnation_changes_nothing
After epoch 2 is joined, a correction from epoch 1 with a larger `through` and a delta of epoch 1
are ignored and ask for nothing. Rival R6 (no `left` check on corrections) fails it.
The reviewer's case: epoch 100's reply to the first request is delayed, the sender restarts as
1001, the receiver asks again and joins it, and then the late reply arrives. The first design
(a `left` list) went back to epoch 100 and then dropped every 1001 frame. Now the late reply is
not the answer to the latest request, so it only marks stale. Rival N2 (a foreign correction
accepted) fails it.
### an_unsolicited_correction_from_another_incarnation_only_marks_stale
A correction with a token nobody asked for, from another epoch, leaves the stamp as it was and
makes the receiver ask. Rival N2 fails it.
### only_the_reply_to_the_latest_request_may_join_a_new_incarnation
Two requests are out (a timeout between them); the reply to the first, from another epoch, does
not join, and the reply to the second does. Rival N1 (any reply while asked is the answer) fails
it.
### an_answer_older_than_the_watermark_does_not_clear_stale
An answer through 1 to a receiver at 3 neither moves it back nor says it is current. Rival N6
(`<=` where `==` belongs) fails it.
### an_answer_at_the_watermark_says_nothing_newer_and_clears_stale
A repeat answer at the watermark clears `stale`; without the line the receiver asks for ever.
### trouble_seen_after_a_request_keeps_its_answer_from_clearing_stale
A gap seen after the request went out, then an answer through the old watermark: still stale.
Rival N5 (no comparison of marks) fails it.
### a_new_epoch_frame_re_asks_once_after_a_lost_request
The sender read a request and restarted before answering. Five frames from the new epoch cause
exactly one more request. Rival N3 (no re-ask) fails the first half and rival N4 (a re-ask for
every foreign frame) the second.
### a_poll_inside_a_transaction_is_refused
A poll outside a transaction followed by a rolled-back consumer step loses nothing; a poll inside
one panics. The reviewer's sequence stranded the receiver at `(1, 1)` holding nothing. Rival N8
(the assertion removed) fails it.
### a_zero_capacity_pipe_is_refused
`channel_pipes(0)` made a rendezvous channel that `try_send` could never use. Rival N10 fails it.
### a_committed_that_overflows_leaves_the_sink_as_it_was
A weight overflow in `committed` no longer leaves a bumped `seq` or half an integral behind.
Rival N9 (mutating first) fails it.
### the_receiver_is_never_wrong_over_a_hostile_network
The reviewer's generator as a permanent property: dropped, duplicated, garbled and reordered
frames in both directions, restarts at any seq, timeouts and receiver restarts, capacity 1 to 4.
After every action the receiver's applied state equals the sender's integral at the stamp it
claims and its epoch never goes down; after the network is reliable it catches up. Run at 20,000
cases three times, all green. Rivals N4 and N7 (a foreign delta moves the receiver) fail it.
### the_reviewers_late_reply_case_is_a_history
The late-reply sequence as a fixed history through the same World.
### an_unreadable_frame_asks_for_a_correction