feat(zset): a stamped, coalescing delta edge between two circuits

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 20:50:07 -07:00
committed by Edward Langley
parent 5d7a3423c2
commit c2598f0c60
8 changed files with 1260 additions and 0 deletions
+2
View File
@@ -242,3 +242,5 @@ pushes `Host::take_notices()`.
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.
**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.
+58
View File
@@ -305,3 +305,61 @@ threads are out of scope, and nothing in `zset` spawns one. `Send` and `mpsc` co
still holds.
6. **Handing a circuit to a thread is the host's business** (`std::thread` lives in host crates).
Whoever owns the circuit pushes, steps and takes; a handle is a number and needs no thread.
## Edges (user ruling 2026-10-11; ADR 009 section 9)
`crates/zset/src/edge.rs`, std only. An edge joins two circuits that share nothing: the
producer's `Output` feeds an `EdgeSink`, the consumer's `Input` is fed by an `EdgeSource`, and a
`Pipe` carries `Frame`s between them. A channel and a network are the same kind of edge: the
channel edge is `Direct` over `ChannelPipe`, a network edge is a codec over a socket pipe.
Nothing here spawns a thread; whoever owns each circuit calls `pump` and `poll`.
1. **The clock is a counter the sender increments per committed command.** `Stamp { epoch, seq }`:
`epoch` names the sender's incarnation and is passed in, never read from a clock (the host
uses a random id, as `Host::with_instance` does). `delivery`'s `(host instance,
document_generation, publication)` maps to `(epoch, seq)` with the first two folded into
`epoch`; a delta is a notice with its `(from, to]` range. Delivery is not changed.
2. **Only committed deltas cross.** `EdgeSink::committed_from(circuit, &output)` takes the output
after `Circuit::commit` and panics inside a transaction (`Circuit::in_transaction`). A rolled
back command is never taken, so it consumes no stamp
(`a_rolled_back_command_does_not_cross`). An empty command is still a stamp, as in delivery.
3. **Backpressure coalesces exactly.** The sink keeps one waiting delta `(sent, seq]`. A command
adds to it (Z-set sum) and moves its `to`; `pump` sends it and, if the pipe says `Full`, leaves
it to grow. Nothing is dropped and the range has no gap
(`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
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
`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
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.
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
`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.
+70
View File
@@ -619,3 +619,73 @@ as at `begin`. The undo log lives in the nodes, which move with the circuit.
Ids index an arena, so a foreign handle used to be an out-of-range or mistyped slot. It is now
refused by name ("handle from another circuit"); `should_panic(expected)` pins the message,
so a downcast panic does not satisfy it.
### two_circuits_on_an_edge_equal_one_circuit
Random histories of commit, rolled-back command, pump, poll, consumer step, a lost frame in
either direction, a sender restart, a receiver restart and a timeout, at capacity 1 to 3, settle
to the output of one circuit running both graphs. It found a real bug: a receiver that joined on a
delta with `from == 0` took a restarted sender's first delta for a fresh stream and ended with
`(1, 1)` where the combined circuit had nothing; joining only by correction fixed it. Rivals, each
failing it (and the text-codec twin): coalescing that keeps only the last delta (R1), accepting a
delta across a gap (R2), a correction applied as `target` instead of `target - held` (R3), joining
by a first delta (R7). R1 also fails the two-thread test.
### the_same_histories_through_a_text_codec
The same property with a string wire form, so a frame is encoded and decoded on every hop. The
rivals above fail it as well; it would also fail if the codec lost a weight or a stamp.
### a_full_pipe_coalesces_exactly_and_keeps_the_range
Capacity 1: a first frame fills the pipe, four more commands pile up, and the next frame is one
delta `(1, 5]` with their exact sum. Rival R1 (the waiting delta replaced, not summed) fails it on
the sum.
### an_empty_command_is_still_a_stamp
Two commands that change nothing still move the receiver to `seq 2`. Rival R8 (stamp only a
non-empty delta) fails it.
### a_lost_delta_is_seen_in_the_stamps_and_corrected
Capacity 8: the second delta is dropped by the pipe, so the third starts at 2 while the receiver
is at 1. The receiver goes stale, asks, and `target - held` brings it to `{1, 2, 3}`. Rivals R2
(apply across the gap) and R3 fail it.
### a_duplicate_delta_is_applied_once
The same delta twice after a join: applied once, and the receiver is not stale. Rival R5 (a
duplicate treated as a gap) leaves the output right and fails only the `stale` assertion, which is
why that assertion is there.
### a_restarted_sender_is_corrected_not_trusted
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
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.
### an_unreadable_frame_asks_for_a_correction
A frame that does not decode sets `stale`. A delta before the join is ignored and a correction
joins.
### a_rolled_back_command_does_not_cross
A producer step inside `begin`/`rollback` consumes no stamp and leaves nothing waiting; the
retry that commits is stamp 1.
### taking_a_delta_inside_a_transaction_is_refused
`committed_from` panics while a transaction is open. Rival R9 (the assertion removed) fails it
with "did not panic".
### a_circuit_on_each_of_two_threads_equals_one_circuit
Three hundred commands on a producer thread, a consumer on another, capacity 2, the producer
yielding at uneven points and pumping on only two of three commands. The consumer's output equals
the combined circuit's. Rival R1 fails it.