fix(zset): a - a is zero at i64::MIN, and the partial group is stated (improvise-tk51)
Answers Copilot (SubAssign negated before consulting the held weight) and Codex (checked arithmetic makes associativity order-dependent at the i64 boundary; documented as the intended policy and pinned by a test). Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VdfEGXA7aJ6ftMsCc9PJze
This commit is contained in:
committed by
Edward Langley
parent
1bb73cbe4f
commit
069d56bd9f
+20
-6
@@ -10,7 +10,7 @@ evidence for each test is in `context/test-evidence/zset.md`.
|
||||
|
||||
| item | what it is |
|
||||
|---|---|
|
||||
| `ZSet<K: Ord>` | a map from `K` to a non-zero `i64` weight; an abelian group |
|
||||
| `ZSet<K: Ord>` | 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 <op>`, 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.
|
||||
|
||||
|
||||
@@ -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.
|
||||
|
||||
+49
-6
@@ -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<K: Ord> ZSet<K> {
|
||||
|
||||
/// 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<K: Ord + Clone> Sub for &ZSet<K> {
|
||||
|
||||
impl<K: Ord> SubAssign for ZSet<K> {
|
||||
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::<u8>::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());
|
||||
|
||||
Reference in New Issue
Block a user