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, 4,096 cases, rust_decimal's to_f64 agrees with the text every time, as ADR 005 says (200,000 of 200,000). So a test whose generator stays in that range proves nothing about the conversion. This test is why the generator above spans 96 bits, and it is what fails, and should be re-read, if rust_decimal ever fixes its conversion.

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 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 small pool of denominators, so the exact grouped read is reached, and arbitrary fractions, so the K cutoff is too. ADR 005 clause 8's seed case, [0.30000000000000004, 1e12, −1e12], is one of the generator's arms and is also pinned exactly.

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

Inserting xs and ys, then retracting ys 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.

the_accumulator_reads_the_exact_sum_or_its_stated_roundings

This is the differential test of the read against the oracle. It is the only test that states every branch.

• 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 f64s are added and the result is rounded once more.
• Past K groups. Inexact.

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.

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.

---

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.