Merge adr009/zset (6de889a1) into adr009/derived

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

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.

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());

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<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")?;
+    }
+}