test(zset): reach the overflow branches of sub and scale, and correct the policy's reason (improvise-tk51)

Adds sub and scale(-1) overflow examples and an i128-oracle property over
near-limit weights; injecting wrapping_{add,sub,mul,neg} now fails named
tests. context/code/zset.md no longer claims wrapping breaks retraction.

Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01VdfEGXA7aJ6ftMsCc9PJze
This commit is contained in:
Claude (adr009-zset)
2026-10-09 23:57:04 -07:00
committed by Edward Langley
parent 069d56bd9f
commit 6de889a116
4 changed files with 93 additions and 6 deletions
+13 -6
View File
@@ -74,12 +74,19 @@ These are the readings this step takes.
ones included, leaves `i64`; outside that, an operation panics rather than return a
different value. So associativity is order-dependent at the boundary:
`(MAX + 1) + (-1)` panics where `MAX + (1 + (-1))` is `MAX`. The result is never wrong,
only sometimes refused. Wrapping arithmetic would make the type a true group (the integers
mod 2^64) and give up exactly the property the ADR argues for in clause 8, that a
retraction cancels its insertion, since a wrapped weight is a different weight. A wider
weight (`i128`) moves the boundary and does not remove it. This is the one place the crate
departs from the ADR's wording. It is a ruling for the user, not for this step
(`overflow_depends_on_the_order_of_evaluation_and_never_gives_a_wrong_value` states it).
only sometimes refused. Wrapping arithmetic would make the type a true group (the integers mod 2^64), and
`(w + x) - x == w` would still hold exactly, so a retraction does cancel its insertion
under wrapping. (An earlier version of this paragraph said otherwise; that was wrong.) What
wrapping breaks is the intermediate reads. `MAX + 1` stores `i64::MIN`, so `distinct`
drops a key whose true weight is positive and `weight()` has the wrong sign. A true weight
of 2^64 stores as 0, so the key vanishes and `is_zero`, `len` and `==` report a set that
does not exist. Those are wrong answers returned silently, which is why the crate panics
instead. A wider weight (`i128`) moves the boundary and does not remove it. The ADR's
"abelian group" wording needs amending whichever policy is chosen: checked-and-panic gives
a group only within range, wrapping gives a group whose reads can be wrong, and `i128` is
partial too. Which one is a ruling for the user, not for this step; the crate currently
panics, and
`overflow_depends_on_the_order_of_evaluation_and_never_gives_a_wrong_value` states it.
`sub` is checked directly against the held weight, so `a - a` is zero for every `a`, `i64::MIN`
included, and only an absent key's `0 - w` can overflow (`w` is `i64::MIN`).
6. **Stable error text.** The panic message names the operation and both operands, so a
+30
View File
@@ -248,3 +248,33 @@ Found by ChatGPT Codex on PR #341: checked arithmetic makes the group partial, s
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.
+18
View File
@@ -381,6 +381,24 @@ mod tests {
assert!(left.is_err());
}
#[test]
#[should_panic(expected = "weight overflow in sub")]
fn subtracting_past_i64_max_panics() {
let _ = ZSet::singleton(1, i64::MAX) - ZSet::singleton(1, -1);
}
#[test]
#[should_panic(expected = "weight overflow in sub")]
fn subtracting_past_i64_min_panics() {
let _ = ZSet::singleton(1, i64::MIN) - ZSet::singleton(1, 1);
}
#[test]
#[should_panic(expected = "weight overflow in scale")]
fn scaling_i64_min_by_minus_one_panics() {
let _ = ZSet::singleton(1, i64::MIN).scale(-1);
}
#[test]
fn scaling_by_zero_never_overflows() {
assert!(ZSet::singleton(1, i64::MAX).scale(0).is_zero());
+32
View File
@@ -707,3 +707,35 @@ property!(
IntegrateExcludesCurrent => stream_catches_an_integrate_that_excludes_the_current_delta,
DifferentiateDropsFirst => stream_catches_a_differentiate_that_drops_the_first_state
);
fn near_limit() -> impl Strategy<Value = i64> {
prop_oneof![
(0i64..4).prop_map(|d| i64::MAX - d),
(0i64..4).prop_map(|d| i64::MIN + d),
-3i64..=3,
]
}
fn probe(f: &dyn Fn() -> ZSet<u8>, wide: i128, what: &str) -> Result<(), TestCaseError> {
let got = std::panic::catch_unwind(std::panic::AssertUnwindSafe(f));
match (i64::try_from(wide).ok(), got) {
(Some(w), Ok(z)) => prop_assert_eq!(z.weight(&1), w, "{} gave the wrong weight", what),
(None, Err(_)) => {}
(Some(_), Err(_)) => prop_assert!(false, "{} panicked within range", what),
(None, Ok(z)) => prop_assert!(false, "{} returned {:?} past i64", what, z),
}
Ok(())
}
proptest! {
#[test]
fn near_the_limit_an_operation_is_exact_or_it_panics(
(a, b, n) in (near_limit(), near_limit(), -3i64..=3)
) {
let (x, y) = (ZSet::singleton(1u8, a), ZSet::singleton(1u8, b));
probe(&|| &x + &y, i128::from(a) + i128::from(b), "add")?;
probe(&|| &x - &y, i128::from(a) - i128::from(b), "sub")?;
probe(&|| x.scale(n), i128::from(a) * i128::from(n), "scale")?;
probe(&|| -&x, -i128::from(a), "neg")?;
}
}