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.