From a4c309642f964a2b9ef4d5f8d6dc37c56a5aced4 Mon Sep 17 00:00:00 2001 From: "Claude (dbsp-delivery)" Date: Sat, 10 Oct 2026 11:54:51 -0700 Subject: [PATCH] fix(numtower): a zero ExactSum has the sign IEEE gives its addends (improvise-z2vr) Co-Authored-By: Claude Sonnet 5.5 Claude-Session: https://claude.ai/code/session_01VdfEGXA7aJ6ftMsCc9PJze --- context/test-evidence/numtower.md | 19 +++++ crates/numtower/src/sum.rs | 25 +++++- .../tests/zero_sign.proptest-regressions | 10 +++ crates/numtower/tests/zero_sign.rs | 80 +++++++++++++++++++ 4 files changed, 132 insertions(+), 2 deletions(-) create mode 100644 crates/numtower/tests/zero_sign.proptest-regressions create mode 100644 crates/numtower/tests/zero_sign.rs diff --git a/context/test-evidence/numtower.md b/context/test-evidence/numtower.md index c57949a3..3e04045f 100644 --- a/context/test-evidence/numtower.md +++ b/context/test-evidence/numtower.md @@ -466,3 +466,22 @@ factors (3, 77, 2^20, 3^40), so the lcm and the product differ. The rival combines over the product of the denominators. Its value is right, so only the lcm assertion can see it. That is why the property asserts the denominator before the value. + +### a_sum_of_negative_zeros_is_negative_zero + +`ExactSum` kept only limbs, so every zero sum read `+0.0` and a lone `-0.0` addend lost its sign +(ADR 009 clause 8 asks for IEEE's). Injected fault: `negative_zero()` always false. This test, the +property below and the retraction property all fail, each by name. + +### a_zero_sum_has_the_sign_ieee_gives_the_same_addends + +The oracle is an IEEE fold from `-0.0` over the same addends. The generator builds zero sums on +purpose (zeros of either sign plus cancelling pairs, shuffled), because filtering random addends +for a zero sum rejected nearly every case. Rival: the sign rule without the `others` count +(`neg_zeros > 0` alone) fails `one_positive_zero_makes_the_zero_positive_and_so_does_a_cancellation` +and both properties, since one `+0.0` or one cancelling pair must make the zero positive. + +### a_retracted_addend_leaves_the_sign_of_the_rest + +Adds `keep` and `gone`, then retracts `gone`; the read and the sum itself must equal a fresh sum +of `keep`. It is why both counters are net weights and why `PartialEq` compares the sign. diff --git a/crates/numtower/src/sum.rs b/crates/numtower/src/sum.rs index 366edbb5..63f7a97a 100644 --- a/crates/numtower/src/sum.rs +++ b/crates/numtower/src/sum.rs @@ -27,6 +27,10 @@ pub struct ExactSum { nan: i128, pos_inf: i128, neg_inf: i128, + /// Net weight of the `-0.0` addends, and of every other finite one: a zero sum is + /// `-0.0` only when the first is positive and the second is nil (IEEE). + neg_zeros: i128, + others: i128, } /// Equal sums, not equal representations: carries propagated, `pending` ignored. @@ -36,7 +40,9 @@ impl PartialEq for ExactSum { propagate(&mut mine); propagate(&mut theirs); let counts = |s: &ExactSum| (s.nan, s.pos_inf, s.neg_inf); - mine == theirs && counts(self) == counts(o) + mine == theirs + && counts(self) == counts(o) + && self.negative_zero() == o.negative_zero() } } @@ -50,6 +56,8 @@ impl Default for ExactSum { nan: 0, pos_inf: 0, neg_inf: 0, + neg_zeros: 0, + others: 0, } } } @@ -66,6 +74,10 @@ impl ExactSum { (false, true, true) => self.pos_inf += weight as i128, (false, true, false) => self.neg_inf += weight as i128, (false, false, _) => { + match x == 0.0 && x.is_sign_negative() { + true => self.neg_zeros += weight as i128, + false => self.others += weight as i128, + } let magnitude = weight.unsigned_abs(); for j in 0..3 { let digit = (magnitude >> (30 * j)) & (CHUNK - 1); @@ -122,6 +134,12 @@ impl ExactSum { self.nan += o.nan; self.pos_inf += o.pos_inf; self.neg_inf += o.neg_inf; + self.neg_zeros += o.neg_zeros; + self.others += o.others; + } + + fn negative_zero(&self) -> bool { + self.neg_zeros > 0 && self.others == 0 } /// The exact sum rounded to the nearest f64, ties to even. @@ -130,7 +148,10 @@ impl ExactSum { (true, _, _) | (false, true, true) => f64::NAN, (false, true, false) => f64::INFINITY, (false, false, true) => f64::NEG_INFINITY, - (false, false, false) => ratio_to_f64(&self.total(), &(BigInt::one() << 1074)), + (false, false, false) => match self.negative_zero() { + true => -0.0, + false => ratio_to_f64(&self.total(), &(BigInt::one() << 1074)), + }, } } diff --git a/crates/numtower/tests/zero_sign.proptest-regressions b/crates/numtower/tests/zero_sign.proptest-regressions new file mode 100644 index 00000000..671a5deb --- /dev/null +++ b/crates/numtower/tests/zero_sign.proptest-regressions @@ -0,0 +1,10 @@ +# Seeds for failure cases proptest has generated in the past. It is +# automatically read and these particular cases re-run before any +# novel cases are generated. +# +# It is recommended to check this file in to source control so that +# everyone who runs the test benefits from these saved cases. +cc 7c90e519b344ca86376f5a0b214d39873c790abd54bb140d369dac66bf4157dd # shrinks to mut addends = [], pairs = [] +cc 05e479a0606a42e8b9d31945d9ee2c548bff3b487f85189dff10c750ca1a2708 # shrinks to keep = [-3.0, 1e-300, 3.0], gone = [] +cc ba72a5a0e795ac7bb6f0833b21286f9da2cd9ec82c20224550e0fe030791e906 # shrinks to addends = [-0.0] +cc 1b8f452c472f86228458b4a4ce0e904c63335d40d3aaab9c0e7606a98b54d771 # shrinks to keep = [-0.0], gone = [] diff --git a/crates/numtower/tests/zero_sign.rs b/crates/numtower/tests/zero_sign.rs new file mode 100644 index 00000000..18c7e06f --- /dev/null +++ b/crates/numtower/tests/zero_sign.rs @@ -0,0 +1,80 @@ +//! ADR 009 step 8's last test: the sign of a zero sum is IEEE's. Evidence: `context/test-evidence/numtower.md`. + +use numtower::ExactSum; +use proptest::prelude::*; + +fn addend() -> impl Strategy { + prop_oneof![ + Just(-0.0), + Just(0.0), + Just(0.5), + Just(-0.5), + Just(3.0), + Just(-3.0), + ] +} + +/// IEEE addition from `-0.0`, the identity that keeps a `-0.0` addend's sign. +fn ieee(addends: &[f64]) -> f64 { + addends.iter().fold(-0.0, |sum, x| sum + x) +} + +fn exact(addends: &[f64]) -> f64 { + let mut sum = ExactSum::new(); + addends.iter().for_each(|x| sum.add(*x, 1)); + sum.value() +} + +#[test] +fn a_sum_of_negative_zeros_is_negative_zero() { + assert_eq!(exact(&[-0.0, -0.0]).to_bits(), (-0.0f64).to_bits()); + assert_eq!(exact(&[-0.0]).to_bits(), (-0.0f64).to_bits()); +} + +#[test] +fn one_positive_zero_makes_the_zero_positive_and_so_does_a_cancellation() { + assert_eq!(exact(&[-0.0, 0.0]).to_bits(), 0.0f64.to_bits()); + assert_eq!(exact(&[0.5, -0.5]).to_bits(), 0.0f64.to_bits()); + assert_eq!(exact(&[-0.0, 0.5, -0.5]).to_bits(), 0.0f64.to_bits()); +} + +#[test] +fn an_empty_sum_is_positive_zero() { + assert_eq!(ExactSum::new().value().to_bits(), 0.0f64.to_bits()); +} + +/// Addends whose exact sum is zero: some zeros of either sign, and cancelling pairs. +fn zero_sum() -> impl Strategy> { + let zeros = proptest::collection::vec(prop_oneof![Just(-0.0), Just(0.0)], 0..5); + let pairs = proptest::collection::vec(prop_oneof![Just(0.5), Just(-3.0)], 0..3); + (zeros, pairs) + .prop_map(|(mut all, pairs)| { + all.extend(pairs.iter().flat_map(|p| [*p, -*p])); + all + }) + .prop_filter("non-empty", |all| !all.is_empty()) + .prop_shuffle() +} + +proptest! { + #[test] + fn a_zero_sum_has_the_sign_ieee_gives_the_same_addends(addends in zero_sum()) { + let want = ieee(&addends); + prop_assert_eq!(want, 0.0, "the generator must build zero sums"); + prop_assert_eq!(exact(&addends).to_bits(), want.to_bits()); + } + + #[test] + fn a_retracted_addend_leaves_the_sign_of_the_rest( + keep in zero_sum(), + gone in proptest::collection::vec(addend(), 0..6), + ) { + let mut sum = ExactSum::new(); + keep.iter().chain(&gone).for_each(|x| sum.add(*x, 1)); + gone.iter().for_each(|x| sum.add(*x, -1)); + prop_assert_eq!(sum.value().to_bits(), ieee(&keep).to_bits()); + let mut fresh = ExactSum::new(); + keep.iter().for_each(|x| fresh.add(*x, 1)); + prop_assert_eq!(sum, fresh); + } +}