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.