diff --git a/context/code/zset.md b/context/code/zset.md index 37c78fa1..46461e07 100644 --- a/context/code/zset.md +++ b/context/code/zset.md @@ -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 diff --git a/context/test-evidence/zset.md b/context/test-evidence/zset.md index b283d1e8..c2890257 100644 --- a/context/test-evidence/zset.md +++ b/context/test-evidence/zset.md @@ -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. diff --git a/crates/zset/src/lib.rs b/crates/zset/src/lib.rs index 7d4a20b4..8d60c65a 100644 --- a/crates/zset/src/lib.rs +++ b/crates/zset/src/lib.rs @@ -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()); diff --git a/crates/zset/tests/properties.rs b/crates/zset/tests/properties.rs index 25b35cfe..f921f880 100644 --- a/crates/zset/tests/properties.rs +++ b/crates/zset/tests/properties.rs @@ -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 { + 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, 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")?; + } +}