improvise/context/test-evidence/zset.md

Test evidence: zset

What each test guards, which rival it was run against, and where that rival failed. The entries are keyed by exact test name, and a rename orphans its entry, which scripts/check-comment-runs.py --check-evidence catches. The reasoning these tests defend is in context/code/zset.md. The decisions are ADR 009 clause 1's.

How the rivals are kept. Every property in crates/zset/tests/properties.rs is a checker that takes the implementation as a parameter (the Alg trait). The property's own test runs it on ZSet. A <property>_holds_on_the_model test runs it on Model(Fault::None), a second, correct implementation over a sorted vector, so a checker that rejects every implementation but ZSet is seen. A <property>_catches_<rival> test runs the same checker on a Model with one injected fault, with a deterministic seed, and asserts two things:

• the run fails;
• the failure message carries the property's own tag, so a rival that fails in setup, panics, or fails some other property does not count.

So each rival is watched failing on every run of the suite, not once by hand.

Injected in the source. Eight faults were also put into crates/zset/src/lib.rs one at a time, each run against the whole suite, each reverted and followed by a full rerun. The failing tests, by name:

• insert stores a zero weight: addition_is_associative, equal_sets_compare_equal, held_plus_target_minus_held_is_target, integrate_and_differentiate_invert_each_other, iteration_is_ascending_and_independent_of_insertion_order, map_is_a_homomorphism, no_zero_weight_is_ever_stored, scalar_multiplication_distributes;
• an insert that stores the sum without removing a zero one also fails addition_is_commutative, every_set_has_an_inverse and zero_is_the_identity;
• neg skips its first key: every_set_has_an_inverse, filter_is_linear, map_is_a_homomorphism, scalar_multiplication_distributes, subtraction_is_adding_the_negation;
• map overwrites: map_is_a_homomorphism;
• distinct does not clamp: distinct_clamps_positive_weights_to_one;
• filter also reads the weight: filter_is_linear;
• sub flipped: held_plus_target_minus_held_is_target, integrate_and_differentiate_invert_each_other, subtraction_is_adding_the_negation;
• integrate excludes the current delta: integrate_and_differentiate_invert_each_other.

The unit tests in src/lib.rs (the zero-weight, map, distinct and differentiate examples and the five overflow tests) also failed under the faults they cover. They are examples, so they carry no entry of their own, except the three at the end, which answer review findings.

Overflow is tested by example, not by property: the generators cannot reach it (sums of three weights stay below 2^43). The should_panic tests assert the message names the operation, so a panic from somewhere else does not pass them.

crates/zset/tests/properties.rs

addition_is_associative

(a + b) + c = a + (b + c) over three independently generated sets. Tag: [associativity].

associativity_holds_on_the_model

The same checker on the correct second implementation. It passes; it exists to show the checker is not specific to ZSet.

associativity_catches_an_add_that_clamps_weights

add clamps every result weight to +-10. A clamp is a saturating add, which is not associative: 10 + 10 + (-10) is 0 one way and 10 the other. The weights near +-3 and +-2^40 reach it at once.

addition_is_commutative

a + b = b + a. Tag: [commutativity].

commutativity_holds_on_the_model

The same checker on the correct second implementation. It passes; it exists to show the checker is not specific to ZSet.

commutativity_catches_an_add_that_keeps_the_left_weight

add is a left-biased union: a key present on both sides keeps the left weight. It is associative, so it escaped associativity when first tried there (the run reported the rival not caught, which is the failure the _catches_ shape exists to make loud), and the rival moved. It is caught here.

zero_is_the_identity

a + 0 = a and 0 + a = a, with zero built by build(&[]), the empty iterator, not by a constructor the rival could share. Tag: [identity].

identity_holds_on_the_model

The same checker on the correct second implementation. It passes; it exists to show the checker is not specific to ZSet.

identity_catches_an_add_that_keeps_only_shared_keys

add keeps only keys present on both sides. Then a + 0 is empty, not a. The first rival tried here, an add that keeps zero weights, passes identity (a canonical a has none to keep), so it was replaced; keeping zeros is caught by every_set_has_an_inverse and no_zero_weight_is_ever_stored.

every_set_has_an_inverse

a + (-a) = 0, a - a = 0 and --a = a. The sets include cancelling pairs and colliding keys. Tag: [inverse].

inverse_holds_on_the_model

The same checker on the correct second implementation. It passes; it exists to show the checker is not specific to ZSet.

inverse_catches_an_add_that_keeps_zero_weights

add and construction leave a key with weight 0 in the map. a + (-a) is then a map of zeros, not the empty one, and the equality says so.

inverse_catches_a_neg_that_forgets_a_key

neg skips the first key. a + (-a) keeps that key.

subtraction_is_adding_the_negation

a - b = a + (-b). Tag: [subtraction].

subtraction_holds_on_the_model

The same checker on the correct second implementation. It passes; it exists to show the checker is not specific to ZSet.

subtraction_catches_a_flipped_sub

sub(a, b) computes b - a.

no_zero_weight_is_ever_stored

After construction, +, -, unary -, scale (including by zero), map, filter and distinct, no stored weight is zero. It reads what the iterator yields, so a rival that hides a zero from the equality is still seen. Tag: [canonical-zero].

canonical_zero_holds_on_the_model

The same checker on the correct second implementation. It passes; it exists to show the checker is not specific to ZSet.

canonical_zero_catches_an_add_that_keeps_zero_weights

add and construction keep zero weights.

equal_sets_compare_equal

The same pairs in another order, and with a cancelling pair spliced in, build equal sets. Tag: [canonical-equality].

canonical_equality_holds_on_the_model

The same checker on the correct second implementation. It passes; it exists to show the checker is not specific to ZSet.

canonical_equality_catches_an_add_that_keeps_zero_weights

The spliced pair (9, 5), (9, -5) leaves a stored (9, 0), so the set is no longer equal to the one without it.

scalar_multiplication_distributes

(a + b) * n = an + bn, a*(m + n) = am + an, a * -1 = -a, a * 1 = a, a * 0 = 0. Tag: [scale].

scale_holds_on_the_model

The same checker on the correct second implementation. It passes; it exists to show the checker is not specific to ZSet.

scale_catches_a_scale_that_takes_the_absolute_value

scale multiplies by |n|. a*(m+n) differs from a*m + a*n as soon as m and n have different signs, and a * -1 is a.

scale_catches_a_scale_by_zero_that_keeps_zero_weights

scale(a, 0) keeps every key at weight 0.

map_is_a_homomorphism

map(a + b) = map(a) + map(b) and map(-a) = -map(a), with images k % m, so keys collide (m from 1 to 4). Tag: [map].

map_holds_on_the_model

The same checker on the correct second implementation. It passes; it exists to show the checker is not specific to ZSet.

map_catches_a_map_that_overwrites_colliding_keys

map inserts each image with =, so the last of several colliding keys wins instead of the weights summing.

filter_is_linear

filter(a + b) = filter(a) + filter(b) and filter(-a) = -filter(a). The predicate reads the key only. Tag: [filter].

filter_holds_on_the_model

The same checker on the correct second implementation. It passes; it exists to show the checker is not specific to ZSet.

filter_catches_a_filter_that_reads_the_weight

filter also requires a positive weight. That is not linear: a negated set loses everything, and a key whose weights cancel in a + b is judged on the sum.

distinct_clamps_positive_weights_to_one

distinct(a) is exactly the keys with a positive weight, each at weight 1, in the same order; and it is idempotent. Tag: [distinct].

distinct_holds_on_the_model

The same checker on the correct second implementation. It passes; it exists to show the checker is not specific to ZSet.

distinct_catches_a_distinct_without_clamping

distinct keeps the positive keys at their own weight.

iteration_is_ascending_and_independent_of_insertion_order

Iteration is strictly ascending by key, and the same pairs inserted in another order iterate identically. Tag: [order].

order_holds_on_the_model

The same checker on the correct second implementation. It passes; it exists to show the checker is not specific to ZSet.

order_catches_insertion_order_iteration

The rival stores keys in first-seen order. Its equality compares sorted copies, so every group law passes on it, and only this property sees the order.

held_plus_target_minus_held_is_target

ADR 009 clause 9: held + (target - held) = target, and correcting a state that is already correct is the zero Z-set. Tag: [correction].

correction_holds_on_the_model

The same checker on the correct second implementation. It passes; it exists to show the checker is not specific to ZSet.

correction_catches_a_flipped_sub

sub(a, b) computes b - a, so the correction applied to held gives 2*held - target.

integrate_and_differentiate_invert_each_other

integrate gives the running sums, differentiate(integrate(d)) = d and integrate(differentiate(s)) = s, element by element, including the empty stream. Tag: [stream].

stream_holds_on_the_model

The same checker on the correct second implementation. It passes; it exists to show the checker is not specific to ZSet.

stream_catches_an_integrate_that_excludes_the_current_delta

Element i is the sum of the deltas before i, so the stream is shifted by one.

stream_catches_a_differentiate_that_drops_the_first_state

Element 0 is zero instead of s_0.

crates/zset/src/lib.rs

tests::subtracting_a_set_from_itself_at_i64_min_is_zero

Found by Copilot on PR #341. SubAssign negated every right-hand weight before consulting the left, so a - a panicked for a weight of i64::MIN, as did differentiate over two equal states. Reproduced before the fix: the test failed at the sub call with weight overflow in neg. The fix subtracts a held weight with checked_sub and negates only the weight of an absent key. The test also checks the borrowed operator and differentiate.

tests::subtracting_i64_min_from_nothing_panics

The control for the one above: 0 - i64::MIN has no i64 value, so it must still panic. A fix that made a - a pass by swallowing the overflow would fail here.

tests::overflow_depends_on_the_order_of_evaluation_and_never_gives_a_wrong_value

Found by ChatGPT Codex on PR #341: checked arithmetic makes the group partial, so (MAX + 1) + (-1) panics where MAX + (1 + (-1)) is MAX. The behaviour is the intended policy, not a defect, and the test states it: one order gives the exact value, the other panics, and neither gives a different number. The argument is in context/code/zset.md, interpretation 5. A wrapping implementation would fail the catch_unwind half.

tests::subtracting_past_i64_max_panics

Found by the Opus review of PR #341: checked_sub in minus could be replaced with wrapping_sub and the suite stayed green, because no example reached sub's overflow branch. Injected: that replacement. These two (..._max_ and tests::subtracting_past_i64_min_panics) and near_the_limit_an_operation_is_exact_or_it_panics failed; the rest passed. Reverted, and the suite rerun.

tests::subtracting_past_i64_min_panics

The negative-side twin of the one above; it fails under the same injection.

tests::scaling_i64_min_by_minus_one_panics

i64::MIN * -1 is the one product of a small scalar that no generator reaches. Injected: checked_mul replaced by wrapping_mul. This test, tests::scaling_past_i64_panics and near_the_limit_an_operation_is_exact_or_it_panics failed.

crates/zset/tests/properties.rs: the boundary

near_the_limit_an_operation_is_exact_or_it_panics

The other properties keep weights at +-2^40 so the laws can be tested without overflow, which left the boundary to examples. This one draws weights from MAX-3..=MAX, MIN..=MIN+3 and -3..=3, and compares +, -, scale and unary - on a single key with an i128 oracle: the result must equal the exact value when it fits i64, and the operation must panic when it 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.

crates/zset/tests/circuit.rs: review of #345

The Opus review of PR #345 at ba17f92b found four defects; each test below failed before its fix. Injected afterwards, one at a time: Rebuild calling step for every chunk fails a_chunked_rebuild_is_one_logical_step_for_delay_integrate_and_differentiate and a_chunked_temporal_rebuild_equals_one_step; a continued integrate re-emitting its integral fails the same two; a continued delay emitting what it holds fails the first; folding empty groups (before or after) fails the two aggregate tests below; asking the deadline before checking the job is done fails the_last_chunk_is_done_even_when_the_deadline_has_expired.

a_chunked_rebuild_is_one_logical_step_for_delay_integrate_and_differentiate

Snapshot {1, 2} after one prior tick {9}, loaded in chunks of one with a deadline always expired, against chunks of five. The three sinks (delay, integrate, differentiate) must sum equal. Before the fix delay gave {1:1} where {9:1} was due, integrate {1:2, 2:1}.

a_chunked_temporal_rebuild_equals_one_step

The same property over random prior ticks, snapshots, chunk sizes and budgets, through a pipeline that combines all three temporal operators and ends in distinct.

an_empty_snapshot_is_still_one_tick

An empty snapshot ticks the clock once (a delay shows the prior input), and a finished job does not tick again.

the_last_chunk_is_done_even_when_the_deadline_has_expired

One chunk exhausts the snapshot with an always-expired deadline: Done, not Pending.

a_group_that_empties_leaves_no_phantom_row_for_a_count

A count closure, insert then delete then insert another: before the fix the delete step gave phantom (7, 0) rows for the empty group, e.g. {(7,0):-1, (7,1):1} where {(7,1):1} was due.

an_aggregate_that_returns_some_on_empty_input_matches_recompute

The same closure through the circuit against recompute-from-scratch. The earlier aggregate properties used closures that return None on empty input, which could not see the defect. aggregate_state_refolds_only_the_touched_keys now asserts both steps' fold counts and outputs.

crates/zset/tests/rebuild.rs: delta review of #345 (0849981a)

Injected, one at a time: a continued delay that replaces what it holds fails every_operator_chunked_equals_one_step_and_so_do_the_ticks_after; a continued integrate that does not accumulate fails that and a_chunked_temporal_rebuild_equals_one_step (which now pushes another delta after Done and steps twice, so the state left for later ticks is compared); a current() that reads the last piece fails current_after_a_chunked_rebuild_is_the_whole_ticks_value; an undetected split tick, or a step that does not count ticks, fails both should-panic tests below. Before these, the first two faults passed the whole suite.

every_operator_chunked_equals_one_step_and_so_do_the_ticks_after

One pipeline with every public operator (delay, integrate, differentiate, index_by, join, aggregate, distinct, flat_map), a prior tick, a chunked load, then two more ticks. The load tick [rebuild-tick], the next tick [next-tick] and the one after [tick-after] must equal the single-step run. From the reviewer's property.

current_after_a_chunked_rebuild_is_the_whole_ticks_value

integrate.current() after a load in chunks of one equals the one-chunk load.

a_host_step_between_rebuild_calls_is_refused_loudly

A Circuit::step between two Rebuild::step calls makes the second panic.

two_interleaved_rebuilds_are_refused_loudly

A second job's first chunk is a tick, so the first job's next call panics.

a_finished_rebuild_and_an_interrupted_check_do_not_trip_on_later_ticks

A finished job is never interrupted, and steps afterwards do not make it panic.

crates/zset/tests/{cost,rollback,rebuild}.rs: rollback, the borrowed piece, the bound rebuild (improvise-bw4p.5, .11, .12)

Every rival below was injected one at a time and watched fail by test name (and tag where one exists) before being reverted; the whole suite was re-run clean afterwards. Costs are counted in key clones and live keys of a Counted key type, never in time, so they hold on any machine.

an_eval_borrows_its_input_instead_of_cloning_it

bw4p.11. input -> map(|k| k.0) -> output over 100 keys makes 0 key clones in a step; before the change it made 200 (the source's whole-tick copy and piece()'s clone). Rival: Unary::eval clones the piece again fails [piece].

an_integrate_stream_holds_its_integral_twice_when_the_tick_is_whole

bw4p.11. After one step an input -> integrate pipeline holds 3N live keys (the input's piece, the integral, the integrate stream's piece), where it held 5N before: the whole-tick copy that duplicated the piece is kept only while a tick is split (Slot::whole is an Option). Rival: a publish that always stores whole = Some(v.clone()) fails [whole] (and the clone test).

a_transaction_costs_the_keys_a_step_touches_and_not_the_size_of_the_circuit

bw4p.5. A pipeline with distinct, delay, join_indexed, aggregate and three sinks is loaded with 10, then 300 keys, then given a two-key delta in each of two inputs. The extra key clones of begin; step; commit over the same step outside a transaction are 16 at both sizes (22 for rollback; the plain step is 20). Rival: DistinctState::begin clones what it holds (a snapshot of the world) fails [cost] with 28 against 318. A delay clones what it holds, the previous tick's input, so the test steps a small delta after the load. Review of #355: the pipeline now includes an integrate; a rival Acc::begin that clones the integral fails [cost]. (An integrate whose output is sunk is left out: its output is the integral, so the sink logs all of it, which is the delta and not an overhead.)

a_rolled_back_step_leaves_the_circuit_as_it_was_and_the_ticks_after_unchanged

bw4p.5, the property. A rig with every stateful operator (integrate, delay, differentiate, distinct, join, aggregate, plus and eight sinks) runs a random prefix, then a key preloaded at i64::MAX - 1. The failing step adds (0,0): 1 and then BIG: 5, so operators have applied the first key when the second overflows (the test asserts the step panicked iff it was meant to). After rollback, every stream's current() and every sink equal what they were ([rollback]), and the ticks after equal a reference circuit that never saw the step ([post]). The same test rolls back a step that succeeds. carry is pending at begin and must stay pending. Rivals, each failing this test: rollback that skips every node ([rollback], and an_operator_built_inside_a_transaction_goes_back_to_empty); an integrate log not undone ([post]); a stream slot not restored ([rollback]); a delay's held value not restored ([post]); a source's pending delta not restored ([post]); a sink not undone ([rollback]); DistinctState not undone ([post]); a trace not undone ([post]); an undo that drops the sign ([post]); a log that records nothing ([rollback], [built]).

a_committed_transaction_equals_the_same_steps_outside_one

bw4p.5. A circuit that commits some of its steps equals one that never opened a transaction, state and output, tick by tick. Rival: commit rolls back fails [commit].

rollback_undoes_the_clock

bw4p.5. A rolled-back step does not count as a tick. Rival: ticks not restored fails [ticks].

an_operator_built_inside_a_transaction_goes_back_to_empty

bw4p.5. An integrate built after begin, stepped, then rolled back, forgets the step ([built]). Without the "a node built in a transaction starts recording" rule it kept it.

rollback_undoes_newest_first_so_no_undo_leaves_i64

bw4p.5. A key at i64::MAX lowered by one and raised by one in one transaction. Undone oldest first the first undo would reach MAX + 1 and panic; undone newest first nothing leaves i64. Rival: the log replayed oldest first fails this test (and no other: the property above cannot see it, since its keys never sit at the boundary).

a_minimum_weight_applied_to_every_kind_of_state_is_taken_back

bw4p.5. i64::MIN has no negation, so a trace undoes it as i64::MAX then 1. Rival: the second application dropped fails [min].

a_second_begin_is_refused_loudly

bw4p.5, with a_rollback_with_nothing_open_is_refused_loudly and a_commit_with_nothing_open_is_refused_loudly: misuse panics, as an overflow does.

a_rebuild_stepped_on_a_foreign_circuit_is_refused_loudly

bw4p.12. A job made from circuit A's input, stepped on circuit B, used to report Done and land its chunk in B's next tick. It now panics. Rival: the check removed fails this test.

a_rebuild_knows_the_circuit_its_input_came_from

bw4p.12. Rebuild::belongs_to, the question a host asks before the panic. Rival: always true fails [owner].

an_interrupted_rebuild_stays_interrupted_and_a_new_job_loads_the_snapshot

bw4p.12. Documents, and pins, that an interrupted job can never finish: later steps never clear it, and a new job over the same snapshot loads it. It did not fail before: the behaviour was right and unstated.

Review of #355 at 51438911 (improvise-bw4p.5, .12)

An adversarial review found a rebuild across a rollback losing data, a panicking Clone mutating unlogged state, and two cost claims that did not hold. Its reproductions are adopted as tests; each rival below was injected and watched fail by name.

r1_rebuild_begun_before_txn_continued_inside_then_rolled_back_reports_interrupted

A job begun outside a transaction and continued inside, then rolled back, was not interrupted; finishing it gave {1,3,4} for the snapshot {1,2,3,4}. Rival: rollback does not count the undone step fails this and r2 to r4.

r2_rebuild_finished_inside_a_rolled_back_txn_is_reported_done_with_nothing_loaded

A job that finished inside a rolled-back transaction was Done with an empty integral and not interrupted.

r3_an_interrupted_rebuild_resurrects_after_rollback_and_a_later_step

rollback rewinds ticks, so a later step made a dead job's recorded tick current again and it continued without its first chunk.

r4_rebuild_whose_first_chunk_panics_in_a_txn_then_rolled_back

A first chunk that panicked left began_at unset, and the job resumed without it. The count is now recorded before the chunk runs. Rival: recording it never (the get_or_insert removed) fails all four; a rival recording it after the chunk was not run separately.

b1 (a closure reading a stream during an eval; the test is removed)

Superseded by the arena (PR dbsp/zset-send): a stream is read through Circuit::current, so a closure cannot read one during a step, and the case no longer compiles. It used to check that the borrowed piece() did not conflict with a closure that read streams, including its own source, inside a transaction. It passed before and after.

c1_a_clone_panic_anywhere_in_a_step_is_rolled_back

Sweeps a panic over every key clone of one transactional step through integrate, distinct, join, delay, aggregate and sinks; 138 panic points left state that differed after the rollback. The post-rollback tick now pushes the keys the failed step touched, because a leaked key is only visible when it is touched again (a rival that mutated DistinctState before cloning its entry survived the first version). Rivals, each failing it: add_logged, DistinctState::step and Undoable::apply each mutating before cloning the entry.

a_panicking_value_clone_leaves_a_memtrace_unchanged

MemTrace::apply inserted an empty group before cloning the value. Rival: that order restored fails [c2].

reviewer_rollback_matches_a_circuit_that_never_ran_the_step

The reviewer's model-based property (random circuits over every public operator, a custom panicking trace, random push/step/continue/begin/commit/rollback histories, operators built in a transaction), at the default 256 cases here (30,000 passed in review). Rival: the continued path saving the slot without its whole fails it.

a_rollback_across_a_split_tick_restores_the_whole_value

The tick is split before the transaction opens, so every edge holds a whole when the first continued piece saves it. Rival: that save dropping whole fails [split] (an earlier version split the tick inside the transaction and never reached the save).

a_split_tick_in_a_transaction_costs_the_size_of_the_edge

Pins the limit zset.md states: a first continued piece in a transaction clones the edge's whole value, growing with the state.

p1_a_chunk_whose_push_panics_in_a_txn_is_counted

Delta review of #355 at b2445fed. Rebuild::step takes the chunk from its iterator and pushes it before stepping; a push that overflows the pending delta panicked with no step run, so undone was not bumped and the resumed job silently dropped the chunk (key 1's +1). The step is now marked before the push. Rival: that mark removed fails [p1].

a_circuit_and_every_handle_it_hands_out_is_send

The Rc/RefCell graph made Circuit !Send. Rival: an Rc<()> field on Circuit fails the build of tests/threads.rs with three Rc<()> cannot be sent between threads safely errors, so the file never runs; the same file's other tests move a circuit for real.

a_circuit_built_on_one_thread_steps_on_another_and_returns

A circuit moved to a new thread for each of nine ticks equals one that never moved, over a pipeline with integrate, distinct, aggregate, filter and delay. It would fail if a node kept state outside the circuit (a thread-local, say), which would not move with it.

a_transaction_begun_on_one_thread_is_rolled_back_on_another

begin and a step on one thread, rollback on another: the stream, the sink and ticks are as at begin. The undo log lives in the nodes, which move with the circuit.

every_call_that_takes_a_handle_refuses_a_foreign_one

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_reply_from_a_dead_incarnation_changes_nothing

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

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.

a_poll_reads_at_most_the_frames_it_is_given

Three corrections waiting, poll(c, 2) reads two and the next reads one, so a unit's turn is bounded by its budget. Rival: the bound removed from the loop fails the first assertion.

Ids index an arena, so a foreign handle from a circuit of the same shape reads or wires the other circuit's slot. Ten cases (current, take, push, a unary operator, both operands of a binary one, output, delay, integrate, distinct) each need the panic text "handle from another circuit". The first draft pinned one site in nine. Rivals, each failing it: the check removed from current, take, push, unary_with, binary_with (each operand), output, delay or integrate.

a_circuit_is_not_sync

The ambiguous-impl trick: the test does not build (E0283) if Circuit implements Sync. Rival: unsafe impl Sync for Circuit {} fails the build of tests/threads.rs.

a_sink_adds_its_input_with_one_clone_per_key

A sink over Counted keys clones each key once (the insert into its sum). Rival: a sink that clones its input piece first, as the reviewer injected, makes N more.

traffic_never_goes_down_across_a_restart_of_either_end

EdgeSink::restart and EdgeSource::restart kept the frame counters at 0 (they rebuilt the struct), which could make a unit read "no progress" and lose a kick. Rival: either restart resetting its counter fails it.