docs(zset): the circuit's reasoning and its test evidence (improvise-bw4p.1)
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
42ee9bac98
commit
a4dadae366
+57
-1
@@ -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<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:
|
||||
|
||||
1. **Wiring is apart from logic.** `circuit.rs` is the only file with `Rc`, `RefCell` and
|
||||
`Box<dyn Node>`. `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<R>`; `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<K, ZSet<V>>`; 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`.
|
||||
|
||||
@@ -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.
|
||||
|
||||
Reference in New Issue
Block a user