Claude (dbsp-delivery)
e3f5cee29a
Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VdfEGXA7aJ6ftMsCc9PJze
90 lines
2.7 KiB
Rust
90 lines
2.7 KiB
Rust
//! 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);
|
|
}
|
|
}
|
|
|
|
#[test]
|
|
fn a_sum_that_is_not_zero_never_reads_as_negative_zero() {
|
|
let mut sum = ExactSum::new();
|
|
sum.add(-0.0, 1);
|
|
sum.add(5.0, 1);
|
|
sum.add(7.0, -1);
|
|
assert_eq!(sum.value(), -2.0);
|
|
}
|