diff --git a/context/code/zset.md b/context/code/zset.md index 76df1f00..37c78fa1 100644 --- a/context/code/zset.md +++ b/context/code/zset.md @@ -10,7 +10,7 @@ evidence for each test is in `context/test-evidence/zset.md`. | item | what it is | |---|---| -| `ZSet` | a map from `K` to a non-zero `i64` weight; an abelian group | +| `ZSet` | a map from `K` to a non-zero `i64` weight; an abelian group within `i64` (interpretation 5) | | `+`, `-`, unary `-`, `* i64`, `scale` | the group operations and scalar multiplication | | `new`, `singleton`, `insert`, `FromIterator`, `Extend` | construction; weights of equal keys sum | | `weight`, `is_zero`, `len`, `iter`, `IntoIterator` | reads; iteration is ascending by key | @@ -63,11 +63,25 @@ These are the readings this step takes. to show it, which is the failure the ADR's exactness argument is against. So every weight operation uses `checked_*` and **panics** with `zset: weight overflow in `, in debug and in release (`checked_*` does not depend on `overflow-checks`). The operations are - `add` (including `insert`, `Extend`, `FromIterator`), `neg` (so `i64::MIN` panics) and - `scale`. Scaling by zero cannot overflow and returns the zero Z-set. A panic, not a - `Result`: `Result` does not belong in the majority of the code (`AGENTS.md`), and a weight - near `i64::MAX` is a defect in the caller, not an input to recover from. The weights - clause 3 produces are small (one per cell). + `add` (including `insert`, `Extend`, `FromIterator`), `sub`, `neg` (so `i64::MIN` panics + when it has to be negated) and `scale`. Scaling by zero cannot overflow and returns the + zero Z-set. A panic, not a `Result`: `Result` does not belong in the majority of the code + (`AGENTS.md`), and a weight near `i64::MAX` is a defect in the caller, not an input to + recover from. The weights clause 3 produces are small (one per cell). + + **The group is partial, and that is the stated reading.** The ADR calls a Z-set an abelian + group. With `i64` weights and no wrapping, the laws hold wherever no weight, intermediate + 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). + `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 failure in a long-running host is diagnosable from the log. diff --git a/context/test-evidence/zset.md b/context/test-evidence/zset.md index 986647cb..b283d1e8 100644 --- a/context/test-evidence/zset.md +++ b/context/test-evidence/zset.md @@ -38,7 +38,7 @@ failing tests, by name: 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. +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 @@ -225,3 +225,26 @@ 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. diff --git a/crates/zset/src/lib.rs b/crates/zset/src/lib.rs index 38825939..7d4a20b4 100644 --- a/crates/zset/src/lib.rs +++ b/crates/zset/src/lib.rs @@ -1,5 +1,5 @@ -//! Z-sets: maps from keys to non-zero `i64` weights, an abelian group (ADR 009 clause 1). -//! Reasoning and the overflow policy: `context/code/zset.md`. +//! Z-sets: maps from keys to non-zero `i64` weights (ADR 009 clause 1). An abelian group +//! wherever no weight leaves `i64`; past that it panics. See `context/code/zset.md`. use std::collections::BTreeMap; use std::collections::btree_map::Entry; @@ -22,6 +22,10 @@ fn plus(a: i64, b: i64) -> i64 { a.checked_add(b).unwrap_or_else(|| overflow("add", a, b)) } +fn minus(a: i64, b: i64) -> i64 { + a.checked_sub(b).unwrap_or_else(|| overflow("sub", a, b)) +} + fn negated(a: i64) -> i64 { a.checked_neg().unwrap_or_else(|| overflow("neg", a, 0)) } @@ -76,14 +80,24 @@ impl ZSet { /// Adds `weight` to `key`'s, dropping the key at zero. Panics on `i64` overflow. pub fn insert(&mut self, key: K, weight: i64) { + self.adjust(key, weight, false); + } + + fn adjust(&mut self, key: K, weight: i64, subtract: bool) { match self.weights.entry(key) { Entry::Vacant(e) => { - if weight != 0 { - e.insert(weight); + let from_zero = if subtract { negated(weight) } else { weight }; + if from_zero != 0 { + e.insert(from_zero); } } Entry::Occupied(mut e) => { - let sum = plus(*e.get(), weight); + let held = *e.get(); + let sum = if subtract { + minus(held, weight) + } else { + plus(held, weight) + }; if sum == 0 { e.remove(); } else { @@ -241,7 +255,9 @@ impl Sub for &ZSet { impl SubAssign for ZSet { fn sub_assign(&mut self, other: Self) { - self.extend(other.into_iter().map(|(k, w)| (k, negated(w)))); + for (k, w) in other { + self.adjust(k, w, true); + } } } @@ -338,6 +354,33 @@ mod tests { let _ = ZSet::singleton(1, i64::MAX).scale(2); } + #[test] + fn subtracting_a_set_from_itself_at_i64_min_is_zero() { + let a = ZSet::singleton(1, i64::MIN); + assert!(a.clone().sub(a.clone()).is_zero()); + assert!((&a - &a).is_zero()); + assert!(differentiate(&[a.clone(), a]).pop().unwrap().is_zero()); + } + + #[test] + #[should_panic(expected = "weight overflow in neg")] + fn subtracting_i64_min_from_nothing_panics() { + let _ = ZSet::::new() - ZSet::singleton(1, i64::MIN); + } + + #[test] + fn overflow_depends_on_the_order_of_evaluation_and_never_gives_a_wrong_value() { + let (max, one, minus) = ( + ZSet::singleton(1, i64::MAX), + ZSet::singleton(1, 1), + ZSet::singleton(1, -1), + ); + let right = max.clone() + (one.clone() + minus.clone()); + assert_eq!(right, max); + let left = std::panic::catch_unwind(|| (max.clone() + one.clone()) + minus.clone()); + assert!(left.is_err()); + } + #[test] fn scaling_by_zero_never_overflows() { assert!(ZSet::singleton(1, i64::MAX).scale(0).is_zero());