diff --git a/context/code/numtower.md b/context/code/numtower.md new file mode 100644 index 00000000..cb794e83 --- /dev/null +++ b/context/code/numtower.md @@ -0,0 +1,284 @@ +# `numtower`: the reasoning + +`crates/numtower` is ADR 005 migration step 1 (improvise-59nw.1): the numeric tower, +first and alone. Nothing in improvise depends on it yet, so it changes no behaviour. +The decisions are the ADR's (`context/adr/005-exact-decimal-arithmetic.md`). This file +records how the crate reads them, the places the ADR left a choice open or said two +things, and the measurements. The evidence for each test is in +`context/test-evidence/numtower.md`. + +## The shape + +| type | what it is | ADR | +|---|---|---| +| `Num` | the stored value: an exact `Decimal`, an exact `Ratio`, or an `f64` | clauses 1, 2 | +| `NumRef` | a borrowed view of a `Num`'s arm, for exhaustive matching | — | +| `Interim` | a value inside one evaluation; exact intermediates widen to a bigint rational | question 13 (b) | +| `NumSum` | a retractable, order-free `SUM` over any `Num` | clause 8, question 16 | +| `ExactSum` | ADR 009's f64 superaccumulator | question 15 (a) | +| `parse_number`, `is_number`, `Typing` | clause 3's number language, gate and parse | clause 3, question 12 | +| `Display` / `Num::from_canonical` | the canonical text: `12.50`, `10/3`, `#i0.1`, `inf`, `-inf`, `nan` | clauses 10, 11, 14 | +| `Num::round_to_places` | display rounding, the mode a parameter | clause 12 "Format" | + +**`Num` is a struct with private arms, not the ADR's `pub enum`.** The ADR's sketch +(clause 2) shows `pub enum Num { Exact(Decimal), Fraction(Box>), +Inexact(f64) }`. A public enum would let any caller build values the tower never +produces: `Fraction(1/2)` (which must be the decimal `0.5`), an unreduced fraction, or an +exact `-0`. Each would break exact equality or the fingerprint of clause 9. So the arms +are private, every constructor normalizes, and callers match on `NumRef`. That is +`context/design-principles.md` §3, smart constructors. It is also what clause 14's table +asks for, since improvise calls "`Num`'s accessors for exactness, mantissa, scale and +fraction parts". The `Box` lives in one constructor, as `AGENTS.md` asks. `Num` is 24 +bytes, as the ADR measured, and `a_num_is_24_bytes` pins it. + +**The normal form.** An exact zero has no sign. A fraction is reduced and has a positive +denominator. A value whose reduced denominator is `2^p·5^q`, with `k = max(p, q) <= 28` +and a mantissa that fits 96 bits, is always the `Decimal`, never a `Fraction`. So +`Fraction(n/1)` exists only when `n` does not fit 96 bits, as with `10^35/1`. + +## Arithmetic + +### Why there are two types: `Num` and `Interim` + +Question 13 (b) bounds only the **stored** result: "every intermediate inside one formula +evaluation is unbounded up to the ceiling". The bounded `Num` cannot be such an +intermediate, so `Interim` is the widened type. It is either a stored `Num` or an exact +`BigQ` (a reduced `BigInt` fraction) that does not fit `i128`. `Interim::store` applies +the stored bound. The operators on `&Num` are one-operation evaluations: each builds the +`Interim`, applies the operation and stores the result. So `(a * a) / a` returns +`a` exactly when computed through `Interim`, and is inexact when computed through `Num` +(`an_intermediate_beyond_i128_comes_back_exact`). That difference is (b)'s whole point. +Step 3's evaluators should evaluate through `Interim` and store once per cell. + +### Contagion, and how many roundings a demotion has + +An inexact operand makes the result inexact. Each exact operand is converted by the +correctly rounded conversion, and then the f64 operation runs. That is two roundings, +which is clause 4's "computed in f64". + +**An exact ∘ exact result that does not fit is rounded once.** It is the correctly rounded +f64 of the exact value. Clause 4 still says a demoted sum or product is "rounded twice, +once per operand and once in the operation". That text predates option (d). Option (d)'s +"Operations" and question 13 (b) both say that a result failing the stored bound is "the +correctly rounded f64 of the exact fraction", and under (b) the exact value is always in +hand. The crate follows (d), because (d) is decided and later. Both texts cannot hold for +one operation, so this is a reading, and it is flagged. + +### Clause 4: the hint, the recompute, the stored scale + +`Decimal + Decimal` and `Decimal × Decimal` first try `rust_decimal`'s checked operation. +The result is trusted only when its scale equals the nominal one (`max(sa, sb)` for `+` +and `−`, `sa + sb` for `×`). A lower scale is the **hint**, and so is a `None`. On the +hint the exact integer result is recomputed in a 256-bit integer, and its trailing zeros +are stripped. If the stripped mantissa fits 96 bits at a scale of at most 28, the result +is a decimal at the **stored scale**, `min(nominal, 28)`, padded back with zeros while the +mantissa fits. Otherwise the result goes to the fraction arm, then to a wide `Interim`. +The ADR's own example holds: `1.2500000000000000 × 4.0000000000000000` is `5` at scale 28 +(`a_recomputed_result_keeps_the_stored_scale_clause_4_names`). A `None` counts as the +hint, so that an overflow `rust_decimal` reports is never mistaken for an exact result. + +### Division: the direct test, one implementation + +Clause 5 is normative: write the quotient as a reduced `n / (2^p·5^q)`, then it is a +decimal iff `k <= 28` and the padded mantissa fits. The crate does this the same way for +every exact pairing, not only for decimals. It reduces the quotient (in `i128` when that +cannot overflow, and in a bigint otherwise), then normalizes. `small_ratio` and +`decimal_of` are the one normalization, so a decimal reached through any path has the +same representation. Multiplying back is never used. + +**A quotient carries its minimal scale** (`10.00 / 2` is `5`, `1 / 4` is `0.25`). The ADR +does not say what scale a quotient has. A quotient's scale is not a function of its +operands' scales (clause 5), and a result that passed through the fraction arm carries +its minimal scale (option (d)), so the minimal scale is the consistent choice. It is a +reading, and it is flagged. + +**The ADR's argument against multiplying back is weaker than it says.** Clause 5 rejects +it as incomplete, on `1e-28 / 0.5`: `q × 0.5` "needs scale 29, so the check flags it". +That holds under revision 6's rule, which demotes on the hint +(`division_decides_fit_directly_catches_multiplying_back` keeps that rival). But under +revision 7's recompute the product `1e-28` is found exact after its zeros are stripped. +So multiplying back by `Num`'s own `*` accepts the ADR's counterexample. In 20 runs of the +division property (5,120 random cases plus the three seeds), it agreed with the direct +test every time. That was an experiment and is not committed. The direct test stays the +rule, because the ADR decided it and because it needs no second division. + +### `POW` + +- **The exponent.** It is exact when it is an exact **integer value**, so `2.0` counts. +- **The size, decided before any multiplication.** The result's numerator has at least + `|n|·(bits(num) − 1)` bits, and likewise its denominator. If either lower bound passes + the ceiling, the result is `powf`, inexact, with nothing allocated. So + `POW(1/3, 10^9)` costs nothing. Inside the bound the result is computed exactly, and it + can still exceed the ceiling (`3^6000` is 9,510 bits). It then demotes, which is the + ceiling's stated exception. +- **The scale.** A positive power of a decimal takes clause 4's stored scale with nominal + `s·n`, the scale repeated multiplication would give, so `1.50^2` is `2.2500`. A + negative power is a division and has its minimal scale. +- **The edge values.** `0^0` is `1`. `0^-n` is `div/0`. `±1^n` is `±1` for any `n`, + including one too large to compute. + +### The ceiling + +`CEILING_BITS = 8,192`. It applies to the bit length of an intermediate's numerator *or* +denominator. The ADR states the ceiling as a width, not as which of the two it measures. +Past it, the intermediate becomes the correctly rounded f64 of its exact value. + +## Comparison + +- **Exact with exact.** Cross-multiplication in 256 bits. A decimal is `m / 10^s` with + `10^28 < 2^94`, so every product fits. +- **Exact with inexact.** The ADR's method: convert the exact operand, and the rounded + value decides unless it lands on the f64 itself. A tie is resolved against the f64's + exact binary value, in a bigint. +- **That fast path is sound only because the conversion is correctly rounded.** Injecting + `rust_decimal`'s `to_f64` failed `exact_mixed_comparison_is_transitive` as well as the + conversion test. A future integer conversion (clause 4 allows one) must keep that. + +`MIN` and `MAX` skip NaN. Equal values break their tie as follows. Only the first rule is +the ADR's (question 11); the other two are this crate's, and they make the result +independent of argument order: +- the exact value is preferred to the inexact one (question 11); +- of two equal decimals, the larger scale is kept, for the same reason: it keeps more of + what was typed; +- of `0.0` and `-0.0`, `MIN` takes `-0.0` and `MAX` takes `0.0`, as IEEE 754's + `minimum` and `maximum` do. + +## The number language + +**The gate is literally `f64::from_str` reading a finite value.** The parse is the +crate's own lexer, and it never goes through an f64 on an exact path. The property test +checks that the two agree, and that the exact value read rounds to the f64 +`f64::from_str` reads. + +- **A lexeme's scale.** It is the scale the lexeme implies (`1.50` → 2, `1.5e3` → 0). When + the implied scale is above 28 but the value fits a decimal (`0.1` written with 29 + places), clause 4's stored-scale rule applies: strip the zeros, then pad toward 28. + The ADR only says "with the scale the lexeme implies", which cannot exceed 28. +- **Zero.** It is exact, unsigned, at the implied scale clamped to 0–28, so + `0e99999999999999999999` is `0`. +- **An exponent too long to read** saturates, because no exact arm can reach it. A + significand of more than 180 digits, or a leading digit outside 10^-130 to 10^40, goes + straight to f64. Those bounds are wider than the fraction arm can reach (a reduced + denominator `10^k / 2^a` is at least `2^k`, so `k < 127`). +- **The forced `n/d` arm.** Its value is a decimal, then a fraction, then **the nearest + f64**. The ADR says `n/d` "is a fraction or, once normalized, a decimal", and does not + say what a forced `n/d` too large for `i128` becomes. The crate applies clause 3's order + to it, as it does to every other spelled number. This is a reading, and it is flagged. + +**The canonical text is `Display`.** An inexact finite value is `#i` followed by Rust's +`{:?}` spelling, which is the shortest that reads back (`#i1e300`, `#i0.1`). +`from_canonical` reads all six spellings back, and reads an exact spelling only as an +exact value. Clause 14's list puts "`#i…`" in the crate, while its table says "the `#i` +prefix and the grammar are improvise's". Those two contradict each other. The crate +holds the prefix, because the wire and the file both need the one spelling, and step 7 +may move the prefix out if the grammar wants it. + +## Rounding to places + +Every arm goes through one exact path: the value as a bigint fraction, +`n·10^places / d`, then rounded by the caller's mode (`HalfAwayFromZero` or `HalfEven`). +An inexact value is first read exactly from its shortest round-trip spelling, which is +improvise-felo.9's fix, so a typed-then-computed `1.005` shows `1.01`. A result that +rounds to zero has no sign (`-0.001` at two places is `0.00`). The ADR does not decide +that, and today's f64 path would print `-0.00`. + +## Sums + +`NumSum` keeps four things, and every one is an abelian group, so the state is a function +of the multiset of terms and not of their order. + +| part | holds | width | +|---|---|---| +| the decimal partition | every decimal, and every fraction whose denominator is `2^p·5^q` with `k <= 28`, as an integer at scale 28 | 320 bits | +| the groups | per other reduced denominator, the summed numerator | 256 bits each, in a `BTreeMap` | +| `group_floats` | an `ExactSum` of each group's correctly rounded value | ADR 009's | +| `inexact` | an `ExactSum` of the f64 terms, plus their net weight | ADR 009's | + +**The read.** It is exact when the net inexact weight is zero and at most K = 8 groups +remain. The groups and the decimal partition are then combined **over the lcm of their +denominators, and reduced once**, and the stored bound applies to the result. Past K the +read is the f64 accumulators: `group_floats`, the decimal partition converted once, and +the inexact terms. That reading rounds each group, then the total. With inexact terms and +at most K groups, the exact total is converted once and added to the inexact terms. A +group whose numerator returns to zero is dropped, so "how many groups" is a function of +state. The K cutoff overrides representability: nine denominators whose exact total fits +still read inexact (`more_than_k_denominators_read_inexact_even_when_the_total_fits`). +That is question 13's second exception, and the ADR's flagged reading. + +**`ExactSum` is ADR 009's prototype**, from `crates/improvise-core/examples/retraction_drift.rs` +on PR #309. It has three changes: +- it splits a weight into base-2^30 digits, as ADR 009 says the `numtower` version must, + instead of looping per chunk; +- it holds 70 limbs, not 67, because a digit's shift adds up to 60 bits; +- it reads through the crate's one rational-to-f64 rounding. + +It counts NaN and the infinities, so they can be retracted. A count that is nonzero in +either direction is treated as present. + +**For ADR 009's seam crate.** `NumSum` and `ExactSum` both have the shape a Z-set group +needs: `add(&Num, i64)` / `add(f64, i64)`, `insert`, `retract`, `read`/`value`, `Clone`. +`ExactSum` also has `absorb`, to merge two accumulators. Neither implements a group trait +yet, because `zset` does not exist yet. The newtype of question 15 is where that goes. + +## The wide integers + +`Fixed` is a two's-complement integer of `N` 64-bit limbs that never allocates. It is +used for the clause 4 recompute (256 bits), exact comparison (256 bits), the decimal +partition (320 bits) and the group numerators (256 bits). Clause 14 also names "256-bit +helpers for the division reduction". Division reduces in `i128` when the products cannot +overflow, and otherwise in a bigint. It does not have a hand-rolled 256-bit gcd. That +path is the slow path, and it is measured below. + +## Dependencies + +The normal edges are `rust_decimal` 1.43.0 (std only), `num-rational` 0.4.2 (no default +features), `num-bigint` 0.4.8, `num-integer` 0.1.47 and `num-traits` 0.2.19. The last two +are direct dependencies, used for `gcd`/`lcm` and the numeric traits. They were already +in the tree through `num-rational` and `num-bigint`, so they add no crate. The ADR names +only the first three. There is no serde, and `cargo tree --edges normal` shows no +`borsh`. `BigRational` is a **dev**-dependency feature only, for the oracle, so the +oracle and the implementation do not share a rational type. + +## Measured + +On an Apple M4 Max (64 GB), rustc 1.98.1, `cargo run --release -p numtower --example +bench`. Each range is two runs. + +| what | figure | +|---|---| +| SUM, 18k and 90k typed two-place values, ns per element | f64 0.53; `rust_decimal` fold 2.7–3.0; `Num` `+` fold 7.8–8.2; `NumSum` insert and read 7.9–8.1 | +| per operation over 18,000 typed pairs, ns | `Num` add 3.1–3.3, mul 3.0–3.2, div 146–153; `rust_decimal` checked add 1.4–1.5, mul 1.2, div 24.7–25.3 | +| `(Rev − Cost) / Rev`, ns per record | 151–153 | +| `to_f64` of a decimal (the text path), ns | 36.7–37.1 | +| `round_to_places(2)`, ns | 370–382 | +| `NumSum` read, K distinct 126-bit denominators, numerators of about 190 bits | K = 2: 5.2–5.4 µs; K = 8: 41.4–42.0 µs | +| `ExactSum`, 1M values | 1.78–1.81 ns per insert, 0.29 µs per read | + +Here is how these sit against the ADR: +- **The grouped read.** At K = 8 it is inside the ADR's 52–127 µs. The ADR measured + 250-bit numerators, and these are about 190 bits, because `NumSum` can only reach a + group's numerator through its public `add`. +- **`ExactSum`.** It agrees with ADR 009's 2.0 ns per update and 0.58 µs per read. +- **Division.** At about 150 ns it is above the ADR's *estimate* of 60–110 ns. Most + quotients of typed values do not terminate, so each one pays two `i128` gcds and the + `Box` of a `Fraction`. +- **The rest.** The ADR's whole-recompute measurement at 18k and 90k cells waits for + step 3, as the ADR says. + +**The wasm32 cost** comes from a probe outside the repository, built exactly as the +ADR's appendix builds one: a `cdylib`, `opt-level = "s"`, LTO, `wasm-opt -Oz +--enable-bulk-memory --enable-nontrapping-float-to-int`, `gzip -9`. The baseline already +parses and prints an f64. + +| probe | after `wasm-opt -Oz` | gzipped | +|---|---|---| +| f64 only | 48,331 B | 29,162 B | +| the ADR's five operations (parse, `+`, `−`, `/`, print) through `numtower` | +89,375 B | **+36,714 B** | +| plus `NumSum`, `cmp_exact` and `round_to_places` | +119,277 B | **+48,221 B** | + +The narrow figure confirms the ADR's estimate of "up to about +36 KB together". The full +surface is about +47 KB gzipped. That is what the bundle pays once step 4 sums through +the crate and step 6 rounds through it. It is more than the +15.4 KB the user answered +question 8 against, and the ADR says question 8 "reopens" if the figure changes the +answer. Neither figure is the real bundle, which shares allocator and formatting code +with everything else. diff --git a/context/test-evidence/numtower.md b/context/test-evidence/numtower.md new file mode 100644 index 00000000..7938728d --- /dev/null +++ b/context/test-evidence/numtower.md @@ -0,0 +1,302 @@ +# 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 `_catches_`, 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 +`e-` 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. diff --git a/crates/numtower/examples/bench.rs b/crates/numtower/examples/bench.rs index f328e4d9..809a3be0 100644 --- a/crates/numtower/examples/bench.rs +++ b/crates/numtower/examples/bench.rs @@ -1 +1,187 @@ -fn main() {} +//! ADR 005 migration step 1's benchmark: `cargo run --release -p numtower --example bench`. +//! A microbenchmark, not the evaluator; what it does and does not show is in `context/code/numtower.md`. + +use std::hint::black_box; +use std::time::Instant; + +use numtower::{Decimal, ExactSum, Num, NumSum, Rounding, Typing, parse_number}; + +struct SplitMix64(u64); + +impl SplitMix64 { + fn next(&mut self) -> u64 { + self.0 = self.0.wrapping_add(0x9E37_79B9_7F4A_7C15); + let mut z = self.0; + z = (z ^ (z >> 30)).wrapping_mul(0xBF58_476D_1CE4_E5B9); + z = (z ^ (z >> 27)).wrapping_mul(0x94D0_49BB_1331_11EB); + z ^ (z >> 31) + } +} + +/// Typed two-place values from 0.01 to 999,999.99, as the ADR's appendix draws them. +fn typed_texts(seed: u64, n: usize) -> Vec { + let mut rng = SplitMix64(seed); + (0..n) + .map(|_| { + let cents = 1 + rng.next() % 99_999_999; + format!("{}.{:02}", cents / 100, cents % 100) + }) + .collect() +} + +fn nums(texts: &[String]) -> Vec { + texts + .iter() + .map(|t| parse_number(t, Typing::Inferred).unwrap()) + .collect() +} + +/// The best of `runs`, in nanoseconds per item. +fn best(runs: usize, items: usize, mut f: impl FnMut()) -> f64 { + (0..runs) + .map(|_| { + let t = Instant::now(); + f(); + t.elapsed().as_nanos() as f64 / items as f64 + }) + .fold(f64::INFINITY, f64::min) +} + +fn sums() { + println!("SUM over typed two-place values, ns per element, best of 20"); + for n in [18_000, 90_000] { + let texts = typed_texts(1, n); + let floats: Vec = texts.iter().map(|t| t.parse().unwrap()).collect(); + let decimals: Vec = texts.iter().map(|t| t.parse().unwrap()).collect(); + let values = nums(&texts); + let f64_fold = best(20, n, || { + black_box(black_box(&floats).iter().sum::()); + }); + let decimal_fold = best(20, n, || { + let s = black_box(&decimals) + .iter() + .fold(Decimal::ZERO, |a, b| a.checked_add(*b).unwrap()); + black_box(s); + }); + let num_fold = best(20, n, || { + let zero = Num::exact(Decimal::ZERO); + black_box(black_box(&values).iter().fold(zero, |a, b| &a + b)); + }); + let accumulator = best(20, n, || { + let mut s = NumSum::new(); + black_box(&values).iter().for_each(|v| s.insert(v)); + black_box(s.read()); + }); + println!( + " {n:>6} cells: f64 {f64_fold:.2}, rust_decimal {decimal_fold:.2}, Num + fold {num_fold:.2}, NumSum {accumulator:.2}" + ); + } +} + +fn operations() { + println!("Per operation over 18,000 typed pairs, ns, best of 20"); + let (a, b) = ( + nums(&typed_texts(21, 18_000)), + nums(&typed_texts(22, 18_000)), + ); + let decimal = + |v: &[Num]| -> Vec { v.iter().map(|n| n.to_string().parse().unwrap()).collect() }; + let (da, db) = (decimal(&a), decimal(&b)); + let pairs = a.len(); + let rd_add = best(20, pairs, || { + da.iter().zip(&db).for_each(|(x, y)| { + black_box(x.checked_add(*y)); + }) + }); + let rd_mul = best(20, pairs, || { + da.iter().zip(&db).for_each(|(x, y)| { + black_box(x.checked_mul(*y)); + }) + }); + let rd_div = best(20, pairs, || { + da.iter().zip(&db).for_each(|(x, y)| { + black_box(x.checked_div(*y)); + }) + }); + let add = best(20, pairs, || { + a.iter().zip(&b).for_each(|(x, y)| drop(black_box(x + y))) + }); + let mul = best(20, pairs, || { + a.iter().zip(&b).for_each(|(x, y)| drop(black_box(x * y))) + }); + let div = best(20, pairs, || { + a.iter() + .zip(&b) + .for_each(|(x, y)| drop(black_box(x.checked_div(y)))) + }); + let margin = best(20, pairs, || { + a.iter() + .zip(&b) + .for_each(|(rev, cost)| drop(black_box((rev - cost).checked_div(rev)))); + }); + let to_f64 = best(20, pairs, || { + a.iter().for_each(|x| { + black_box(x.to_f64()); + }) + }); + let places = best(20, pairs, || { + a.iter() + .for_each(|x| drop(black_box(x.round_to_places(2, Rounding::HalfAwayFromZero)))); + }); + println!(" rust_decimal checked: add {rd_add:.1}, mul {rd_mul:.1}, div {rd_div:.1}"); + println!(" Num: add {add:.1}, mul {mul:.1}, div {div:.1}"); + println!( + " Num (Rev - Cost) / Rev {margin:.1}, to_f64 {to_f64:.1}, round_to_places(2) {places:.1}" + ); +} + +/// K groups of near-`i128` denominators: the ADR's worst case for the exact read. +fn grouped_read() { + println!("NumSum read over K distinct 126-bit denominators, us per read, best of 200"); + for k in [2usize, 8] { + let mut rng = SplitMix64(0x5EED); + let mut sum = NumSum::new(); + for _ in 0..k { + let den = ((rng.next() as i128) << 62 | rng.next() as i128 >> 2) | 1 | (1 << 125); + let num = (rng.next() as i128) << 60 ^ rng.next() as i128; + let term = Num::ratio(num, den).unwrap(); + sum.add(&term, i64::MAX); + sum.add(&term, i64::MAX); + } + assert_eq!(sum.groups(), k); + let read = best(200, 1, || drop(black_box(sum.read()))); + println!( + " K = {k}: {:.1} us (exact: {})", + read / 1000.0, + sum.read().is_exact() + ); + } +} + +fn exact_sum() { + println!("ExactSum (f64 superaccumulator), best of 20"); + let floats: Vec = typed_texts(1, 1_000_000) + .iter() + .map(|t| t.parse().unwrap()) + .collect(); + let mut acc = ExactSum::new(); + let insert = best(20, floats.len(), || { + acc = ExactSum::new(); + floats.iter().for_each(|x| acc.add(*x, 1)); + }); + let read = best(20, 1, || { + black_box(acc.value()); + }); + println!( + " {insert:.2} ns per insert, {:.2} us per read", + read / 1000.0 + ); +} + +fn main() { + println!("numtower bench (release); name the machine when you quote these"); + sums(); + operations(); + grouped_read(); + exact_sum(); +} diff --git a/crates/numtower/src/sum.rs b/crates/numtower/src/sum.rs index 5276a50f..65401366 100644 --- a/crates/numtower/src/sum.rs +++ b/crates/numtower/src/sum.rs @@ -165,23 +165,31 @@ impl NumSum { /// Adds `x` with a Z-set `weight`. Exact and associative: the order cannot matter. pub fn add(&mut self, x: &Num, weight: i64) { - match (x.kind(), x.exact_parts()) { - (NumRef::Inexact(f), _) => { + match x.kind() { + NumRef::Inexact(f) => { self.inexact.add(f, weight); self.inexact_weight += weight as i128; } - (_, Some((n, d))) => match at_scale_28(d) { - Some(unit) => self.add_scaled(n, unit, weight), - None => self.add_to_group(n, d, weight), + NumRef::Exact(d) => { + let unit = pow10(MAX_SCALE - d.scale()) as u128; + self.add_scaled(d.mantissa(), unit, weight); + } + NumRef::Fraction(r) => match at_scale_28(*r.denom()) { + Some(unit) => self.add_scaled(*r.numer(), unit, weight), + None => self.add_to_group(*r.numer(), *r.denom(), weight), }, - (_, None) => unreachable!("an exact value has parts"), } } fn add_scaled(&mut self, n: i128, unit: u128, weight: i64) { - let term = I320::from_i128(n) - .checked_mul_u128(unit) - .and_then(|t| t.checked_mul_u128(weight.unsigned_abs() as u128)) + let magnitude = weight.unsigned_abs() as u128; + let scaled = match unit.checked_mul(magnitude) { + Some(both) => I320::from_i128(n).checked_mul_u128(both), + None => I320::from_i128(n) + .checked_mul_u128(unit) + .and_then(|t| t.checked_mul_u128(magnitude)), + }; + let term = scaled .and_then(|t| if weight < 0 { t.checked_neg() } else { Some(t) }) .expect("a weighted term is below 2^284"); self.decimals = self diff --git a/crates/numtower/tests/properties.rs b/crates/numtower/tests/properties.rs index 68cc76e5..43043a46 100644 --- a/crates/numtower/tests/properties.rs +++ b/crates/numtower/tests/properties.rs @@ -219,6 +219,8 @@ fn pow_decides_its_size_before_computing_and_honours_the_ceiling() { assert!(dec("0").pow(&dec("-1")).is_err()); assert!(!dec("2").pow(&dec("0.5")).unwrap().is_exact()); assert!(same(&dec("2").pow(&dec("-2")).unwrap(), &dec("0.25"))); + assert!(same(&dec("1.50").pow(&dec("2.0")).unwrap(), &dec("2.2500"))); + assert!(same(&dec("0").pow(&dec("0")).unwrap(), &dec("1"))); } // --------------------------------------------------------------------------- diff --git a/nix/ci.nix b/nix/ci.nix index ceb4f384..f8a56de9 100644 --- a/nix/ci.nix +++ b/nix/ci.nix @@ -46,6 +46,8 @@ "improvise-wasm-client" "improvise-worker-server" "improvise-gp" + # ADR 005 clause 14: nothing depends on it yet, and improvise-core will. + "numtower" ]; pFlags = crates: lib.concatMapStringsSep " " (c: "-p ${c}") crates; diff --git a/scripts/build-doc-site.mjs b/scripts/build-doc-site.mjs index 3ae5941d..3e7f5d87 100644 --- a/scripts/build-doc-site.mjs +++ b/scripts/build-doc-site.mjs @@ -63,6 +63,7 @@ const SECTIONS = [ ["context/code/tui.md", "code/tui", "The TUI"], ["context/code/cli.md", "code/cli", "The headless CLI"], ["context/code/gp.md", "code/gp", "gp-tree and improvise-gp"], + ["context/code/numtower.md", "code/numtower", "numtower, the numeric tower"], ["context/code/kb-tool.md", "code/kb-tool", "The kb tool"], ["context/code/tooling.md", "code/tooling", "The repository's own checkers"], ], @@ -81,6 +82,7 @@ const SECTIONS = [ ["context/test-evidence/tui.md", "test-evidence/tui", "The TUI"], ["context/test-evidence/cli.md", "test-evidence/cli", "The headless CLI"], ["context/test-evidence/gp.md", "test-evidence/gp", "gp-tree and improvise-gp"], + ["context/test-evidence/numtower.md", "test-evidence/numtower", "numtower"], ["context/test-evidence/tooling.md", "test-evidence/tooling", "The repository's own gates"], ["context/test-evidence/layout-cost.md", "test-evidence/layout-cost", "Layout and keypress cost"], ["context/test-evidence/scale-bisect.md", "test-evidence/scale-bisect", "Scale bisect"],