Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VdfEGXA7aJ6ftMsCc9PJze
12 KiB
zset: the reasoning
crates/zset is ADR 009 step 1 (improvise-tk51, epic improvise-bw4p): the Z-set group, first
and alone. Nothing depends on it yet, so it changes no behaviour. The decisions are the
ADR's (context/adr/009-incremental-evaluation.md, clause 1). This file records how the
crate reads them, where the ADR left a choice open, and the evidence discipline. The
evidence for each test is in context/test-evidence/zset.md.
The shape
| item | what it is |
|---|---|
ZSet<K: Ord> |
a map from K to a non-zero i64 weight; an abelian group within i64 (interpretation 5) |
+, -, unary -, * i64, scale |
the group operations and scalar multiplication |
new, singleton, insert, FromIterator, Extend |
construction; weights of equal keys sum |
weight, is_zero, len, iter, IntoIterator |
reads; iteration is ascending by key |
map, filter, distinct |
the three per-element operators |
integrate, differentiate |
the stream operators, over a slice |
There are no dependencies: not serde (clause 9 keeps the wire form in improvise-protocol),
not even the workspace's own crates. The crate is wasm32-clean by construction and is in
nix/ci.nix's wasmCrates.
Canonical form
A key with weight zero is never stored. insert removes a key whose sum reaches zero, and
singleton(k, 0) is the zero Z-set. Two Z-sets are therefore == exactly when every key has
the same weight, so the derived PartialEq, Hash and Ord are the group's equality. The
clause 9 correction target - held relies on it: a correct state gives == the zero Z-set,
and is_zero is len() == 0, not a scan.
The representation is a BTreeMap. Iteration order is the key order, the same in every
process and for every insertion order, which clause 3 needs (eager folds in CellKey order)
and which a HashMap would give up (context/code/core.md, gotcha 18's argument).
Interpretations
The ADR is one paragraph on the crate, and says more about what it is for than what it is. These are the readings this step takes.
-
Clause 1 lists a
Circuitand more operators; step 1 built the pure part, and "The circuit" below built the rest (improvise-bw4p.1). The ADR's list isdelay,integrate,differentiate,map,filter,flat_map,index_by,join_indexed,distinctandaggregate, run by a synchronousCircuit, plus resumable rebuilds and a trace interface. Step 1 as ticketed is the group and the operators that are functions of a Z-set or of a stream of them:map,filter,distinct,integrate,differentiate. The rest needs the circuit (a clock, state held between steps), or a second key type (index_by,join_indexed,aggregate), and is left to the steps that use it rather than designed without a caller.flat_mapismapinto several images and has no user yet either. -
integrateanddifferentiateare slice functions, not circuit nodes.integrate(&[d_0, d_1, ..])is the running sumsd_0 + .. + d_i;differentiateis its inverse,s_0thens_i - s_(i-1). The state before the first element is zero, as in DBSP.delayis not provided: over a slice it is a shift, and a circuit gives it meaning. -
distinctis not linear, and is not a group homomorphism. It keeps weight 1 on the keys whose weight is positive and drops every other key, negative included. That is the set-semantics operator of DBSP. The ADR says nothing about negative weights; dropping them is the standard reading, and the one that makesdistinctidempotent. -
Operators are methods on
&self, group operations arestd::opstraits.K: Cloneis required only where a result copies keys (filter,distinct,scale, the borrowed operators);mapand the by-value operators need onlyOrd. -
Overflow. Neither clause 1 nor clause 8 states a policy for weights (clause 8 is about
f64drift, which wrapping integers do not have). The crate currently useschecked_*on every weight operation, for the reason given below, and panics withzset: weight overflow in <op>, in debug and in release (checked_*does not depend onoverflow-checks). The operations areadd(includinginsert,Extend,FromIterator),sub,neg(soi64::MINpanics when it has to be negated) andscale. Scaling by zero cannot overflow and returns the zero Z-set. A panic, not aResult:Resultdoes not belong in the majority of the code (AGENTS.md), and a weight neari64::MAXis a defect in the caller, not an input to recover from. The weights clause 3 produces are small (one per cell).The group is partial, and that is the stated reading. The ADR calls a Z-set an abelian group. With
i64weights and no wrapping, the laws hold wherever no weight, intermediate ones included, leavesi64; outside that, an operation panics rather than return a different value. So associativity is order-dependent at the boundary:(MAX + 1) + (-1)panics whereMAX + (1 + (-1))isMAX. The result is never wrong, only sometimes refused. Wrapping arithmetic would make the type a true group (the integers mod 2^64), and(w + x) - x == wwould still hold exactly, so a retraction does cancel its insertion under wrapping. (An earlier version of this paragraph said otherwise; that was wrong.) What wrapping breaks is the intermediate reads.MAX + 1storesi64::MIN, sodistinctdrops a key whose true weight is positive andweight()has the wrong sign. A true weight of 2^64 stores as 0 (by the add path; ascaleproduct of 2^64 would store a zero too, which breaks canonical form), so the key vanishes andis_zero,lenand==report a set that does not exist. Those are wrong answers returned silently, which is why the crate panics instead. A wider weight (i128) moves the boundary and does not remove it. The ADR's "abelian group" wording needs amending whichever policy is chosen: checked-and-panic gives a group only within range, wrapping gives a group whose reads can be wrong, andi128is partial too. Which one is a ruling for the user, not for this step; the crate currently panics, andoverflow_depends_on_the_order_of_evaluation_and_never_gives_a_wrong_valuestates it.subis checked directly against the held weight, soa - ais zero for everya,i64::MINincluded, and only an absent key's0 - wcan overflow (wisi64::MIN). -
Stable error text. The panic message names the operation and both operands, so a failure in a long-running host is diagnosable from the log.
What the tests are
crates/zset/tests/properties.rs holds one checker per property, parameterised by an Alg
trait. The property's test runs it on ZSet. A companion runs it on Model(Fault::None), a
second implementation over a sorted vector, so the checker is shown not to reject a correct
implementation that is not ZSet. Each rival is Model(Fault::X), run through the same
checker with a deterministic seed, and the failure message must carry the property's tag
([inverse], [map], ..). A rival that fails for another reason does not count. The group
laws, canonical form, scalar distributivity, the map homomorphism, filter linearity,
distinct's definition, iteration order, the clause 9 correction identity and the
integrate/differentiate inverses are all properties; each runs at the default 256 cases
over keys from a range of six, so collisions and cancelling pairs are the common case.
Weights come from -3..=3, an explicit zero, and ±2^40, so sums of three cannot wrap.
The overflow policy is not a property over the generators (they cannot reach it by design)
and is tested by example in src/lib.rs, with should_panic(expected = ..).
The circuit (improvise-bw4p.1)
Clause 1's deferred scope, built without ADR 008. The ADR is not edited; this is how the crate reads it.
| item | what it is |
|---|---|
Circuit |
creation-order list of boxed nodes; step() runs each once |
Input<K>, Stream<ZSet<K>>, Output<K> |
push a delta in; the value on an edge; a sink that sums every step's delta until take() |
delay, integrate, differentiate, plus |
the stream operators as nodes |
map, filter, flat_map, index_by |
linear, per-element |
distinct |
incremental, state is the integrated input (DistinctState) |
join_indexed, join_indexed_in |
bilinear delta join of two ZSet<(K, _)> (JoinState) |
aggregate, aggregate_in |
group-by, re-folds only touched keys (AggregateState) |
Trace, MemTrace |
operator state behind lookup, range, apply |
Rebuild, Progress |
a snapshot loaded as a resumable job |
Decisions, where the ADR left a choice:
- Wiring is apart from logic.
circuit.rsis the only file withRc,RefCellandBox<dyn Node>.ops.rsholds each stateful operator as a plain struct with a purestep(delta) -> delta, testable and usable without a circuit. - Scheduling is creation order. A node is built from streams that already exist, so
creation order is a topological order, and the circuit has no cycles: the ADR has no
recursion operator, and
integrateis its own stateful node, not a delayed feedback loop.delayis a node with one held Z-set. NotSend; one thread per circuit (clause 1). - Incremental means the integral of the output is the operator of the integral of the
input. That is the property every operator is tested against, over random delta streams.
distinctandaggregateare not linear, so they keep the integrated input and emit the difference of the operator at the touched keys only. index_byismapto(key, element). A keyed stream is aZSet<(K, V)>; there is no separate indexed collection type, so the join and the aggregate read the same shape.- The join is
da x b_prev + a_prev x db + da x db, computed asdaagainst the right trace,daapplied to the left, thendbagainst the updated left (which holds the cross term), thendbapplied. Output weights are products and panic oni64overflow like every weight (interpretation 5).f(&K, &A, &B) -> Obuilds the output key. aggregate's fold gets the key and the group's(value, weight)pairs (owned, because a paged trace cannot lend references) and returnsOption<R>;Nonemeans the group has no row (an empty group, or aMinof nothing). Sum, count, min and max are closures; text unanimity and the ADR'sExactSumbelong to the caller (clause 4, 8), not this crate.- The trace interface is
apply(k, v, w),lookup(k)andrange(lo, hi), returning owned vectors.MemTraceis aBTreeMap<K, ZSet<V>>; the_inconstructors take anyTrace, which is the seam for paging or compression. An empty or inverted range reads nothing (BTreeMap::rangewould panic). - The resumable step takes a predicate, not an
Instant, and a load is one logical tick.Rebuild::step(circuit, expired)loadschunkkeys at a time and stops whenexpired()is true, always running at least one chunk first, so every call progresses. It reportsDoneas soon as the snapshot is exhausted, whateverexpired()would say.Instant::now()panics on wasm32 (web-timeis a dependency this crate refuses), so the host closes over its own clock. The first chunk isCircuit::step; the rest arestep_continue, which does not advance the clock. A circuit tick that arrives in pieces is exact for the incremental operators because their outputs are deltas. For the temporal ones the pieces are shaped so the outputs still sum to the one-step output: a continueddelayemits nothing and adds to what it holds, a continuedintegrateemits only its piece. An empty snapshot still takes its one tick; a finished job takes none. Deltas pushed to the same input between calls are absorbed into the next piece. Buffering live deltas during a rebuild (clause 7) is the host's. - Not built:
Circuitdoes not own a job runner (ADR 008's), and nothing here is serialised (clause 9,improvise-protocol).
The tests are crates/zset/tests/circuit.rs; the rivals and where they failed are in
context/test-evidence/zset.md.
A panic inside step (a weight overflow in an operator, say) leaves the circuit unusable:
nodes ahead of the panic have updated their state and the rest have not, and there is no
rollback. Drop the circuit and build another. ADR 009 clause 11's per-command snapshot and
restore is the host's job, not this crate's; zset-ffi poisons the circuit for this reason.