From a4dadae36616f4803b8c8bff375f0b55f1bb0252 Mon Sep 17 00:00:00 2001 From: "Claude (dbsp-circuit)" Date: Sat, 10 Oct 2026 11:45:56 -0700 Subject: [PATCH] docs(zset): the circuit's reasoning and its test evidence (improvise-bw4p.1) Co-Authored-By: Claude Sonnet 5.5 Claude-Session: https://claude.ai/code/session_01VdfEGXA7aJ6ftMsCc9PJze --- context/code/zset.md | 58 +++++++++++++++++++++++++- context/test-evidence/zset.md | 76 +++++++++++++++++++++++++++++++++++ 2 files changed, 133 insertions(+), 1 deletion(-) diff --git a/context/code/zset.md b/context/code/zset.md index b3b551da..18928337 100644 --- a/context/code/zset.md +++ b/context/code/zset.md @@ -38,7 +38,7 @@ and which a `HashMap` would give up (`context/code/core.md`, gotcha 18's argumen 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. -1. **Clause 1 lists a `Circuit` and more operators; this step builds the pure part.** The +1. **Clause 1 lists a `Circuit` and more operators; step 1 built the pure part, and "The circuit" below built the rest (improvise-bw4p.1).** The ADR's list is `delay`, `integrate`, `differentiate`, `map`, `filter`, `flat_map`, `index_by`, `join_indexed`, `distinct` and `aggregate`, run by a synchronous `Circuit`, plus resumable rebuilds and a trace interface. Step 1 as ticketed is the group and the @@ -108,3 +108,59 @@ Weights come from `-3..=3`, an explicit zero, and `±2^40`, so sums of three can 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`, `Stream>`, `Output` | 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: + +1. **Wiring is apart from logic.** `circuit.rs` is the only file with `Rc`, `RefCell` and + `Box`. `ops.rs` holds each stateful operator as a plain struct with a pure + `step(delta) -> delta`, testable and usable without a circuit. +2. **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 `integrate` is its own stateful node, not a delayed feedback loop. + `delay` is a node with one held Z-set. Not `Send`; one thread per circuit (clause 1). +3. **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. + `distinct` and `aggregate` are not linear, so they keep the integrated input and emit the + difference of the operator at the touched keys only. +4. **`index_by` is `map` to `(key, element)`.** A keyed stream is a `ZSet<(K, V)>`; there is no + separate indexed collection type, so the join and the aggregate read the same shape. +5. **The join** is `da x b_prev + a_prev x db + da x db`, computed as `da` against the right + trace, `da` applied to the left, then `db` against the updated left (which holds the cross + term), then `db` applied. Output weights are products and panic on `i64` overflow like + every weight (interpretation 5). `f(&K, &A, &B) -> O` builds the output key. +6. **`aggregate`'s fold gets the key and the group's `(value, weight)` pairs** (owned, because + a paged trace cannot lend references) and returns `Option`; `None` means the group has no + row (an empty group, or a `Min` of nothing). Sum, count, min and max are closures; text + unanimity and the ADR's `ExactSum` belong to the caller (clause 4, 8), not this crate. +7. **The trace interface** is `apply(k, v, w)`, `lookup(k)` and `range(lo, hi)`, returning + owned vectors. `MemTrace` is a `BTreeMap>`; the `_in` constructors take any + `Trace`, which is the seam for paging or compression. An empty or inverted range reads + nothing (`BTreeMap::range` would panic). +8. **The resumable step takes a predicate, not an `Instant`.** `Rebuild::step(circuit, + expired)` loads `chunk` keys per circuit step and stops when `expired()` is true, always + running at least one chunk first, so every call progresses. `Instant::now()` panics on + wasm32 (`web-time` is a dependency this crate refuses), so the host closes over its own + clock. Outputs of the chunks sum to what one delta would give, which the test states. + Buffering live deltas during a rebuild (clause 7) is the host's: push them to the same input + after the job is done, or to a second input merged with `plus`. +9. **Not built:** `Circuit` does 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`. diff --git a/context/test-evidence/zset.md b/context/test-evidence/zset.md index c2890257..d2e03476 100644 --- a/context/test-evidence/zset.md +++ b/context/test-evidence/zset.md @@ -278,3 +278,79 @@ the result must equal the exact value when it fits `i64`, and the operation must does not. **Injected**, one at a time, `wrapping_add`, `wrapping_sub`, `wrapping_mul` and `wrapping_neg` in place of the checked calls: this test failed under every one, and the example tests named above failed under the matching one. + +## `crates/zset/tests/circuit.rs`: the circuit + +Each operator is checked against recomputing from scratch: a random stream of deltas goes in, +one circuit step each, and after every step the sum of the outputs so far must equal the +operator applied to the sum of the inputs so far. The failure message carries `[incremental]`, +`[join]`, `[rebuild]` and so on. Keys come from a range of six (four by three for the keyed +ones) and weights from `-3..=3`, so cancelling deltas and re-insertions are the common case. + +**Injected in the source**, one at a time, each reverted and the suite rerun. The failing +tests, by name (a build that printed `Running` was confirmed each time; the first attempt at +the `delay` fault did not compile and was redone): +- `DistinctState` does not update its held set: `distinct_matches_recompute`, + `a_composed_pipeline_matches_recompute`, `a_resumable_rebuild_equals_an_uninterrupted_step`; +- the join applies `da` to the left trace after reading it for `db` (drops the `da x db` + term): `join_matches_recompute`, `join_is_bilinear`, + `the_join_reads_state_through_the_trace_it_was_given`; +- the join drops `da x b_prev`: `join_matches_recompute`, `join_is_bilinear`; +- `aggregate` does not retract the old result: `aggregate_sum_matches_recompute`, + `aggregate_max_matches_recompute`, `aggregate_state_refolds_only_the_touched_keys`; +- `delay` passes the current input: `delay_is_the_previous_step`, and both identities; +- `integrate` forgets history (`acc = d`): `integrate_after_differentiate_is_the_identity`, + `differentiate_after_integrate_is_the_identity`; +- `Rebuild` stops after the first chunk: `a_rebuild_that_is_out_of_time_reports_pending_after_one_chunk`, + `a_resumable_rebuild_equals_an_uninterrupted_step`; +- `Rebuild` checks the deadline before running any chunk (no progress is possible): + the same two; +- `MemTrace::range` ignores the upper bound, and `MemTrace` keeps an emptied key: + `a_trace_reads_what_was_applied`; +- `flat_map` gives every image weight 1: `flat_map_matches_recompute`. + +### map_matches_recompute + +`map`, `filter`, `index_by` and the pipeline test below are linear or compositions of +linear and `distinct`; they pin the circuit's wiring (the input node, the output sink, +creation-order scheduling) as much as the operators, which are `ZSet` methods tested in +`properties.rs`. No fault in them separates from the wiring faults above, and none was +needed. + +### join_is_bilinear + +Three tags. `[bilinear-left]` and `[bilinear-right]` check the reference join is bilinear, so +the oracle itself is a legitimate one; `[bilinear-circuit]` checks the incremental join: one +step of `a1 + a2` and two steps `a1` then `a2` (same `b`) sum to the same output. A join that +drops the `da x db` term fails the first-step, one-delta case, which is why the cross term is +exercised at all. + +### a_resumable_rebuild_equals_an_uninterrupted_step + +The snapshot enters a pipeline (`map` then `distinct`) in chunks of 1 to 3, and the deadline +predicate expires after 1 to 3 chunks per call, so the job is interrupted at varied points. +The sum of the outputs must equal one uninterrupted step over the whole snapshot. The loop is +bounded at 100 calls, so a job that never finishes is the named failure `[rebuild]`, not a hang. + +### a_rebuild_that_is_out_of_time_reports_pending_after_one_chunk + +A predicate that is always expired still lets exactly one chunk through (two of six keys), +then `Pending`; the rest completes on the next call; an exhausted job answers `Done` even +when out of time. This is the progress guarantee the property cannot see, because its budget +is never zero. + +### aggregate_state_refolds_only_the_touched_keys + +Fifty groups are loaded, then one delta touches one key: `f` is called twice (before and +after), not once per group. It is the O(delta) claim, in the one place a count can show it. + +### an_unbounded_range_that_is_empty_reads_nothing + +`range(Excluded(1), Included(1))` and an inverted range are empty. `BTreeMap::range` panics +on those; the trace guards it first. Not from the property, whose `lo > hi` draws are +covered by the same guard, but the equal-bounds corner is rare there. + +### the_join_reads_state_through_the_trace_it_was_given + +A counting `Trace` handed to `join_indexed_in` is looked up, so the join's state really is +behind the trace interface and not a private map beside it.