a020ac669f
Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VdfEGXA7aJ6ftMsCc9PJze
79 lines
2.5 KiB
Rust
79 lines
2.5 KiB
Rust
//! `FloatSum`: ADR 009 clause 8's sign of a zero total, against IEEE addition.
|
|
//! Evidence: `context/test-evidence/numtower.md`.
|
|
|
|
use numtower::FloatSum;
|
|
use proptest::prelude::*;
|
|
|
|
/// Both zeros and small integers: totals that cancel, and every sum below 2^53 is exact.
|
|
fn addend() -> impl Strategy<Value = f64> {
|
|
prop_oneof![
|
|
Just(0.0),
|
|
Just(-0.0),
|
|
(-3i32..=3).prop_map(f64::from),
|
|
prop::sample::select(vec![0.5, -0.5]),
|
|
]
|
|
}
|
|
|
|
fn sum_of(values: &[f64]) -> FloatSum {
|
|
let mut sum = FloatSum::new();
|
|
for v in values {
|
|
sum.add(*v, 1);
|
|
}
|
|
sum
|
|
}
|
|
|
|
/// What adding the same addends in `f64` gives, starting from `-0.0` as `Sum for f64` does.
|
|
fn ieee(values: &[f64]) -> f64 {
|
|
values.iter().sum()
|
|
}
|
|
|
|
fn same_bits(a: f64, b: f64) -> bool {
|
|
a.to_bits() == b.to_bits()
|
|
}
|
|
|
|
#[test]
|
|
fn the_sign_of_a_zero_total_follows_ieee_for_the_cases_that_decide_it() {
|
|
assert!(same_bits(sum_of(&[-0.0, -0.0]).value(), -0.0));
|
|
assert!(same_bits(sum_of(&[-0.0, 0.0]).value(), 0.0));
|
|
assert!(same_bits(sum_of(&[0.0, 0.0]).value(), 0.0));
|
|
assert!(same_bits(sum_of(&[1.0, -1.0]).value(), 0.0));
|
|
assert!(same_bits(sum_of(&[-0.0, 1.0, -1.0]).value(), 0.0));
|
|
assert!(same_bits(sum_of(&[]).value(), -0.0), "as Sum for f64 is");
|
|
}
|
|
|
|
proptest! {
|
|
#[test]
|
|
fn a_sum_has_the_bits_ieee_gives_the_same_addends(
|
|
values in prop::collection::vec(addend(), 0..12),
|
|
) {
|
|
let (got, want) = (sum_of(&values).value(), ieee(&values));
|
|
prop_assert!(same_bits(got, want), "{got:?} for {want:?} over {values:?}");
|
|
}
|
|
|
|
#[test]
|
|
fn retracting_addends_leaves_the_sum_of_the_rest(
|
|
values in prop::collection::vec(addend(), 1..12),
|
|
keep in 0usize..12,
|
|
) {
|
|
let keep = keep.min(values.len());
|
|
let mut sum = sum_of(&values);
|
|
for v in &values[keep..] {
|
|
sum.add(*v, -1);
|
|
}
|
|
let (got, want) = (sum.value(), ieee(&values[..keep]));
|
|
prop_assert!(same_bits(got, want), "{got:?} for {want:?} over {values:?} keeping {keep}");
|
|
}
|
|
|
|
#[test]
|
|
fn absorbing_two_sums_is_adding_all_the_addends(
|
|
values in prop::collection::vec(addend(), 0..12),
|
|
cut in 0usize..12,
|
|
) {
|
|
let cut = cut.min(values.len());
|
|
let mut left = sum_of(&values[..cut]);
|
|
left.absorb(&sum_of(&values[cut..]));
|
|
let (got, want) = (left.value(), sum_of(&values).value());
|
|
prop_assert!(same_bits(got, want), "{got:?} for {want:?} over {values:?} cut at {cut}");
|
|
}
|
|
}
|