fix(numtower): a zero ExactSum has the sign IEEE gives its addends (improvise-z2vr)

Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01VdfEGXA7aJ6ftMsCc9PJze

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.

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)),
+            },
         }
     }
 

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 = []

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<Value = f64> {
+    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<Value = Vec<f64>> {
+    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);
+    }
+}