improvise/context/test-evidence/numtower.md

Test evidence: numtower

What each test guards, which rival it was run against, and where that rival failed. The entries are keyed by exact test name, and a rename orphans its entry, which scripts/check-comment-runs.py --check-evidence catches. The reasoning these tests defend is in context/code/numtower.md. The decisions are ADR 005's.

How the rivals are kept. Every property in crates/numtower/tests/properties.rs is a checker that takes the implementation as a parameter. The property's own test runs it on the real code. A companion test, named <property>_catches_<rival>, runs the same checker on the rival, with a deterministic seed, and asserts two things:

• the run fails;
• the failure message carries the property's own assertion text, so a rival that fails in setup, panics, or fails some other assertion does not count (assert_caught in tests/oracle/mod.rs).

So the rival is watched failing on every run of the suite, not once by hand. Two rivals were also injected into the crate's source, and the run was recorded. Those runs are noted under their entries.

The oracle is num-rational's BigRational, a dev-dependency feature. The crate itself never uses BigRational, so the oracle shares no rational type with the code under test. "Correctly rounded" is checked in the review's interval form (is_nearest). The exact value must lie inside the round-to-nearest-even interval of the returned f64, with the endpoints included only when the f64's mantissa is even. Comparing against BigRational::to_f64 would have been circular in the way ADR 005's option (d) section describes.

---

crates/numtower/tests/properties.rs

an_exact_result_is_never_a_rounded_one

Every exact pairing of arms and every operation (+ − × ÷) is checked against the oracle. When the result claims to be exact, its value must be the exact value. The generator spans 96-bit mantissas, scales 0–28 and i128 fractions. A fixed case pins ADR 005's own example, 1000 + 0.3333333333333333333333333333. rust_decimal returns that at scale 25, rounded, and the crate must not.

Injected in the source. In arith.rs::decimal_sum, the scale filter was deleted, so checked_add's result was trusted. Three tests failed: this one, contagion_is_total, and a_recomputed_result_keeps_the_stored_scale_clause_4_names. The revert was followed by a full rerun.

an_exact_result_is_never_a_rounded_one_catches_a_silently_rounding_add

The rival is rust_decimal's own checked_add, trusted as exact. That is the one outcome ADR 005 clause 4 exists to prevent.

contagion_is_total

Every pairing of the three arms, NaN and the infinities included, through + − × ÷:

• an inexact operand makes the result inexact;
• an exact pair gives an exact result iff the oracle value fits a stored arm, and otherwise the correctly rounded f64 of that value;
• division refuses iff the divisor is exactly zero, at either level.

"Total" means no pairing is missing. A pairing the code never handled would panic, and the runner reports a panic as a failure.

contagion_is_total_catches_an_integral_inexact_kept_exact

The rival is a "harmless" promotion: an integral f64 is treated as exact, so 2 + 3.0 is exact. It is caught on the seed pair (2, Inexact(3.0)). That pair is in the generator on purpose. Integral f64s are rare among random floats, so without the seed the rival was caught only by luck.

pow_is_exact_for_an_exact_base_and_integer_exponent_when_it_fits

Bases from every arm, exponents −6 to 6. An exact base gives an exact result iff the oracle's power fits, and otherwise the correctly rounded value. 0^-n refuses.

pow_decides_its_size_before_computing_and_honours_the_ceiling

• POW(1/3, 10^9) returns at once, inexact. Its lower bound is past the ceiling, so nothing is allocated. Without the size check the test does not finish.
• (1/3)^6000 is computed, but is 9,510 bits and demotes. That is the ceiling's exception.
• 1.05^28 is exact and 1.05^29 is not, the option (d) table's k = 29.
• Also pinned: (-1.0)^(10^20), 0^0, the scale of 1.50^2, and that a non-integer exponent is powf.

the_f64_conversion_agrees_with_parsing_the_decimal_text

The generator spans 96-bit mantissas and scales 0–28, as ADR 005 requires. The oracle text is built digit by digit, not by rust_decimal's Display, which is what the crate itself calls. So the test does not compare the crate's path with itself. The review's case 63294.607176721429540940386554 is pinned.

Injected in the source. num.rs::decimal_to_f64 was replaced with rust_decimal's ToPrimitive::to_f64, and three tests failed:

• this one, minimal case -0.10806611601966961 at scale 17;
• the_number_languages_gate_and_parse_agree, on 92240.01133710762224;
• exact_mixed_comparison_is_transitive.

The third was not expected. The comparison's fast path decides by the rounded value, and that is sound only if the rounding is correct.

the_f64_conversion_agrees_with_parsing_the_decimal_text_catches_rust_decimal_to_f64

The rival is rust_decimal's to_f64, which is not correctly rounded (ADR 005, B2). The test also asserts that the rival misses on the review's case, so the pinned case is known to discriminate.

rust_decimal_to_f64_agrees_on_fifteen_digit_mantissas_so_a_narrow_generator_is_vacuous

This test passes the rival on purpose. With mantissas of at most 15 digits, rust_decimal's to_f64 agrees with the text every time, at this test's 256 cases as in ADR 005's 200,000 of 200,000. So a test whose generator stays in that range proves nothing about the conversion, and this test is why the generator above spans 96 bits. It ran at 4,096 cases until Copilot pointed out, on PR #337, that the repository's budget is 256 (context/design-principles.md §7). The 200,000 is the ADR's measurement, and this test only pins its direction.

If rust_decimal ever fixes its conversion, this test still passes. What fails then is the_f64_conversion_agrees_with_parsing_the_decimal_text_catches_rust_decimal_to_f64, whose rival would agree. That is the signal to re-read both. An earlier version of this entry named this test instead, which was wrong.

a_fractions_conversion_lies_inside_the_round_to_nearest_even_interval

Reduced fractions with numerator and denominator widths from 20 to 126 bits, both signs: the review's independent form. It also checks the product of two such fractions, which reaches the bigint path and is stored. That covers ratio_to_f64 on values wider than i128.

a_fractions_conversion_lies_inside_the_round_to_nearest_even_interval_catches_an_f64_division

The rival is n as f64 / d as f64, which rounds three times.

exact_mixed_comparison_is_transitive

The generator is a crowd: values crowded around one f64 x.

• x itself, and its two neighbours;
• the shortest decimal that spells x, and that decimal ± k·10^-25;
• a third of the shortest decimal.

Every triple is checked for transitivity, and every pair for antisymmetry. Random values would almost never put two exacts and an inexact on one f64, which is exactly where the rival breaks.

exact_mixed_comparison_is_transitive_catches_comparing_through_f64

The rival is revision 1's rule: convert the exact operand to f64, then compare. It fails as ADR 005 clause 6 says it does. Exact(s) = Inexact(x) and Inexact(x) = Exact(s + 10^-25), while the two exacts differ. The marker is comparison: not transitive, so it is the transitivity assertion that fails, not antisymmetry.

comparison_agrees_with_the_oracle_at_every_pairing_of_arms

The differential half of comparison: the crowd, plus mixed random pools of decimals, fractions and finite f64s, against BigRational's order. NaN is unordered, and an infinity orders past every exact value.

min_and_max_prefer_the_exact_value_and_do_not_depend_on_order

Question 11's tie-break, plus the two the crate adds: the larger scale between equal decimals, and IEEE's -0.0 for MIN and 0.0 for MAX. Each pair is asserted in both argument orders, the order-independence property the tie-breaks exist for.

the_accumulator_is_independent_of_order

Random weighted term lists, from every arm, are summed in one order and in a shuffled order. The results must agree in arm, value and scale. The terms include fractions over a pool of fourteen non-decimal denominators, so groups receive several terms and lists often hold more than K of them, and arbitrary fractions too. ADR 005 clause 8's seed case, [0.30000000000000004, 1e12, −1e12], is one of the generator's arms and is also pinned exactly. It caught the review's F12 (a group's old f64 not retracted), where the stale values make the past-K read depend on the order of updates.

On weights (the review of 302594bf, B2). Until then every NumSum property called insert and retract only, so every weight was ±1. That was the cause the answer to Codex's P1 had itself named, and the generators had not changed. Two faults passed the whole suite: F7 (the decimal partition ignored the weight's magnitude) and F8 (a group multiplied by weight.signum()). Weights now come from weight():

• the units 1, −1 and 0;
• −3 to 3;
• magnitudes up to 2^40;
• ±i64::MAX and 2^30 − 1.

i64::MIN is left out so a weight always negates.

the_accumulator_is_independent_of_order_catches_decimal_addition

The rival is clause 8's own rival, a fold with Decimal's +, demoting to the tower where it overflows. On the seed case, one order rounds 0.30000000000000004 + 1e12 to scale 16 and the other does not.

the_accumulator_retracts_exactly

Adding weighted xs and ys, then adding each y again with its weight negated in reverse order, must equal a fresh sum of xs in arm, value and scale. A group whose numerator returns to zero must be dropped, or a retracted denominator would still count toward K. With weights it catches F7 and F12 as well.

the_accumulator_reads_the_exact_sum_or_its_stated_roundings

The differential test of the read against a BigRational oracle, over weighted terms. It states the value of all three branches:

• No inexact term, at most K live groups. The read is exact iff the exact total fits, and is then that total. Otherwise it is the total's correctly rounded f64.
• Inexact terms present. The exact total is rounded once, then the weighted f64s are added and the result is rounded once more.
• Past K groups. The nearest f64 of Σ round(live group) + round(decimal partition) + Σ w·f.

Until the review of 302594bf (B1) the past-K branch asserted only that the read was inexact, and this entry claimed the test stated every branch. Both were wrong. Three faults passed the whole suite:

• F12: a group's old f64 was not retracted from group_floats;
• F14: the past-K read dropped the decimal partition;
• F15: the past-K read dropped every inexact term.

The test now has the reviewer's oracle, at the repository's 256-case budget. 34ab0fc3 ran it at 512, and Copilot pointed out the budget. At 256, every fault in the table below still failed by name, and F7, F8, F12, F14 and F15 failed in four of four passes. Half the lists come from the fourteen-denominator pool, up to 40 terms long, so groups receive several terms and K is passed often. It also counts how many cases reach each branch and fails if any branch is reached fewer than 20 times, so a generator change cannot silently starve one.

The oracle counts live groups, those whose summed numerator is nonzero. The first version counted denominators ever seen, and that disagrees with the state-based count whenever terms cancel. Inexact presence is likewise per bit pattern, by net weight.

Every fault in the review's script, re-run after the fix. Each was injected into the source and cargo test -p numtower was run on a confirmed rebuild. Each failed by name:

fault	failed
F1 decimal sum's scale filter dropped	a_recomputed_result_keeps_the_stored_scale_clause_4_names, an_exact_result_is_never_a_rounded_one, contagion_is_total
F2 rust_decimal's to_f64	exact_mixed_comparison_is_transitive, comparison_agrees_with_the_oracle_at_every_pairing_of_arms, the_f64_conversion_agrees_with_parsing_the_decimal_text, the_number_languages_gate_and_parse_agree
F3 mixed comparison through f64	exact_mixed_comparison_is_transitive, comparison_agrees_with_the_oracle_at_every_pairing_of_arms, an_interim_compares_exactly_without_storing
F4 one net inexact count	the_accumulator_keeps_inexact_terms_whose_weights_cancel, the_accumulator_retracts_exactly, this test
F5 product, not lcm	sum::tests::the_grouped_read_combines_over_the_lcm_and_reduces_once
F6 ExactSum rounded per limb	exact_sum_is_the_exact_weighted_total_rounded_once, more_than_k_denominators_read_inexact_even_when_the_total_fits, the_accumulator_keeps_inexact_terms_whose_weights_cancel, this test
F7 decimal weight magnitude ignored	this test, the_accumulator_retracts_exactly
F8 group weight as its sign	this test
F9 decimal product's scale filter dropped	a_typed_value_and_the_same_value_computed_are_equally_exact, an_exact_result_is_never_a_rounded_one, contagion_is_total
F10 ExactSum's low weight digit only	exact_sum_is_the_exact_weighted_total_rounded_once, this test
F11 POW sign lost	a_huge_odd_exponent_keeps_the_sign_of_a_negative_base
F12 old group f64 kept	this test, the_accumulator_is_independent_of_order, the_accumulator_retracts_exactly
F13 mixed tie not checked exactly	comparison_agrees_with_the_oracle_at_every_pairing_of_arms, exact_mixed_comparison_is_transitive, an_interim_compares_exactly_without_storing
F14 past K, decimal partition dropped	this test
F15 past K, inexact terms dropped	this test

• F13's text now occurs twice. Interim's comparison added a second copy of the replaced line, so the review's script refuses to inject it. It was injected at its original site, in cmp.rs::mixed.
• The five former survivors were run twice and failed both times. F12's set varied between runs: the_accumulator_retracts_exactly failed in one run and not the other, and this test failed in both.

more_than_k_denominators_read_inexact_even_when_the_total_fits

1/3 + 1/7 + … + 1/31 is nine distinct denominators. The exact total fits an i128 fraction, yet the read is inexact. That is question 13's second exception, the K cutoff overriding representability. Eight of them read as an exact Fraction. The read past K is asserted to be each group rounded, then the total rounded once. The first version asserted one rounding of the exact total, and it failed: clause 8's maintained f64 accumulator of group values rounds twice by design.

exact_sum_is_the_exact_weighted_total_rounded_once

ADR 009's ExactSum against the oracle. Weights are drawn from small values, from the whole i64 range and up to 2^40. A whole-range weight exercises all three base-2^30 digits, which ADR 009's chunk loop could not reach in reasonable time. Values include subnormals.

division_decides_fit_directly

ADR 005 clause 5's three seed cases, as both property inputs and pinned assertions:

• 1 / 2^40 and 1 / 5^30 are fractions;
• 1e-28 / 0.5 is the exact decimal 2e-28.

Random decimal pairs must also be an exact decimal iff the quotient fits one, an exact fraction iff it fits only that, and otherwise inexact. The test also pins AVG's example (70/3), 1/3 × 3 = 1, and division by an inexact -0.0.

division_decides_fit_directly_catches_multiplying_back

The rival is multiplying back with revision 6's scale test (demote on the hint). It fails on 1e-28 / 0.5, as ADR 005 says. An experiment, not committed, ran multiplying back with Num's own *, which carries revision 7's recompute. It agreed with the direct test on all 5,120 random cases and the seeds. The ADR's argument that multiplying back is incomplete holds only under the earlier rule (context/code/numtower.md, "Division").

the_number_languages_gate_and_parse_agree

The generated lexemes have four sources:

• structured lexemes: an optional sign, up to 40 digits, an optional fraction, and an optional exponent of up to 4 digits, so the empty parts give 1., .5 and .;
• junk over the alphabet of digits, eE+-._/aifnIN and space;
• n/d lexemes;
• the named spellings: inf, NaN, Infinity, 1_000, +.5, e5.

For each lexeme, the parse succeeds iff f64::from_str reads a finite value. The exact value parsed must round to the f64 f64::from_str reads. is_number and parse_number must agree in both typings.

the_number_languages_gate_and_parse_agree_catches_from_str_exact

The rival is rust_decimal's from_str_exact. ADR 005 clause 3 names it as the parse whose language differs from the gate's: it rejects 1.5e3 and accepts 1_000.

the_number_language_seed_cases

Every seed case ADR 005's migration step 1 lists:

• 1.5e3 is the exact 1500;
• 1_000 is text;
• -0.0 is the exact 0.0, with no sign;
• 3/4 is text when the type is inferred, and 0.75 when it is forced;
• 1e999, -1e999, nan, inf and Infinity are text;
• 1e-999 is an inexact zero;
• 1e-30 is the exact 1/10^30;
• 0.12345678901234567890123456789 is an exact fraction, not a rounded decimal;
• 2^120 is an exact n/1;
• 1e-40 is inexact.

a_typed_value_and_the_same_value_computed_are_equally_exact

For random decimal pairs (and the seed 1e-15 × 1e-15), the exact product is spelled as <integer>e-<k> and parsed. The parse must have the arm and the value of the computed product. An earlier draft built the text only when the reduced denominator was a power of ten, and rejected most cases. A reduced decimal product's denominator is 2^a·5^b, so the text now scales by the smallest power of ten that makes the product an integer.

a_typed_value_and_the_same_value_computed_are_equally_exact_catches_demoting_on_the_hint

The rival is revision 6's multiplication, which demotes whenever the returned scale drops. 1e-15 × 1e-15 then becomes an f64, while the typed 1e-30 is the exact fraction. That is the asymmetry revision 6's N2 was about.

a_recomputed_result_keeps_the_stored_scale_clause_4_names

ADR 005 clause 4's example: 1.2500000000000000 × 4.0000000000000000 is 5 at scale 28, not scale 0 and not 32. The test also pins that a common-path sum keeps its returned scale (12.50 + 1.5 = 14.00), that 1000 + 0.333… goes to the fraction arm, and that an exact zero result has no sign.

an_intermediate_beyond_i128_comes_back_exact

The point of question 13 (b). a = 10^30/7; a × a does not fit i128, yet (a × a) / a through Interim is a, exactly. The same product stored through Num is inexact and correctly rounded.

the_canonical_text_reads_back_as_the_same_number

Every arm's Display text reads back through from_canonical as the same arm, value and scale. The test pins the four spellings ADR 005 clause 11 tabulates, and that canonical exact text never reads back as an inexact value.

the_accumulator_keeps_inexact_terms_whose_weights_cancel

ChatGPT Codex, P1 on PR #337, against edbb50c4. NumSum decided "is an inexact term present" from the net inexact weight. Adding 1.0 with weight 1 and 2.0 with weight −1 nets to zero while the accumulator holds −1.0. So read() took the exact branch and returned the exact partition alone, dropping the inexact term silently.

This test failed at edbb50c4, on its first assertion: the read of [1.0 ×1, 2.0 ×−1, 0.5] claimed to be exact. Two things made the bug invisible to the existing properties:

• every generated term was inserted with weight +1;
• the retraction test retracts the very values it inserted, so per-value presence and net presence agree there by construction.

The test also asserts that retracting both inexact terms returns the exact 0.5, so the fix cannot simply make every sum that ever saw an f64 inexact.

a_huge_odd_exponent_keeps_the_sign_of_a_negative_base

Copilot on PR #337, against edbb50c4. When the size check demotes a power to powf, the exponent becomes an f64. Above 2^53 it rounds to an even value, so (-2)^(2^53 + 1) returned +inf where the sign must be negative, and the negative exponent gave +0.0. This test failed at edbb50c4 on its first assertion. It also checks a fraction base, and that an even exponent stays positive, so a fix that always negates cannot pass.

i128_min_is_an_exact_fraction_numerator

Copilot on PR #337, against edbb50c4. Num::fit rejected i128::MIN as a numerator because to_i128 filtered it for both halves, so Num::ratio(i128::MIN, 1) became inexact although Ratio<i128> holds it. This test failed at edbb50c4 on its first assertion. The oracle's fits had the same symmetric-range assumption, so no property could see the bug. Both are fixed, and fraction() now generates i128::MIN / d.

Allowing the value exposes a second hazard: it cannot be negated in i128, and the old negate computed -n, which panics in a debug build. So the test also negates i128::MIN / 3 (an inexact, correctly rounded result), takes it through Interim twice and back, divides it, compares it and reads its canonical text.

a_negative_power_has_its_minimal_scale

Copilot on PR #337, and B3 of the review of 302594bf. The unit-base arm of POW padded every result to s·|n|, so 1.0^-2 was 1.00 and (-1.0)^-3 was -1.000, while 2.0^-2 was 0.25. context/code/numtower.md already said "a negative power … has its minimal scale", so the code contradicted the crate's stated rule. This test failed at 302594bf on its first assertion. It also pins that a positive power keeps s·n ((-1.0)^3 = -1.000), so a fix that stripped every scale cannot pass.

The broader guard is the scale assertion now in pow_is_exact_for_an_exact_base_and_integer_exponent_when_it_fits, which had checked value and exactness but never scale. Its oracle, power_scale, is the rule restated:

• start from the minimal scale;
• pad toward min(s·k, 28) for a decimal base with k > 0 only, while the mantissa fits 96 bits.

Unit bases (1.0, -1.0, 1.000, -1, 0.00) are among its seeds. It failed at 302594bf with the minimal case 1.0^-1 = 1.0. The injection G1 (a negative power keeps the base's scale) fails both tests.

exact_sums_are_equal_when_their_values_are

Copilot on PR #337, and B3 of the review. ExactSum derived PartialEq over its raw limbs and its pending carry counter. This test failed at 302594bf on its first assertion, 0.5 + 0.5 == 1.0. It also asserts:

• insert then retract equals an empty sum;
• weights (2^30 − 1, 2) added in either order are equal;
• different values are unequal, and a counted NaN is part of the value, so an == that always answers true cannot pass.

Injection G2, equality back on the representation, fails it.

a_forced_fraction_never_reads_as_infinity

A should-fix from the review of 302594bf. A forced n/d with a 400-digit n read as Inexact(inf), though clause 3 says a finite lexeme never reads as infinity. This test failed at 302594bf. It also asserts:

• is_number agrees with the parse;
• a negative one is text too;
• an underflowing 1/9…9 is still the inexact zero, so a fix that refused every inexact forced fraction cannot pass.

Injection G3 fails it.

an_interim_compares_exactly_without_storing

New API, from a should-fix in the review: Interim had no comparison and no zero test while step 3 is told to evaluate through it. For two wide products a, it compares a against:

• another wide product;
• a ± 1/(3·10^30);
• a itself;
• the f64 nearest a, and that f64's upper neighbour.

Each comparison is made in both directions, against the BigRational order. It also asserts a − a is zero and a is not. Injection G4, storing before comparing, fails it, and so do F3 and F13, because the stored arms delegate to Num::cmp_exact.

an_interim_compares_exactly_without_storing_catches_storing_first

The rival is the comparison the review warned step 3 would otherwise have to make: store both operands, then compare. a and a ± 1/(3·10^30) store to one f64, so the rival calls them equal.

---

crates/numtower/src/sum.rs

sum::tests::the_grouped_read_combines_over_the_lcm_and_reduces_once

The combine must return the lcm as its denominator, and the reduced result must equal the BigRational sum. Group numerators are up to i128 × i64, and the denominators share factors (3, 77, 2^20, 3^40), so the lcm and the product differ.

sum::tests::the_grouped_read_combines_over_the_lcm_and_reduces_once_catches_the_product

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.

a_sum_that_is_not_zero_never_reads_as_negative_zero

The first version of the sign rule returned -0.0 whenever the -0.0 count was positive and the other count was nil, without checking that the finite total was zero. The weights here (+5.0 and -7.0 net to one "other" addend, and the -0.0 is held) make the counts say "negative zero" over a total of -2. Found by the existing the_accumulator_reads_the_exact_sum_or_its_stated_roundings, which read #i-0.0 for a nonzero sum; the rival is that version.