BLOCK D2: option (d)'s grouped sum keeps a parallel f64 accumulator per group and reads exactly only with at most K = 32 non-decimal groups, with its costs stated; rules for dropping zeroed groups and for decimal-denominator fractions. Should-fix: 1-based overflow counting (5th-6th, i64 3rd-4th), the independent interval check replaces the circular to_f64 one, may-overflow wording for checked_add, display beyond 38 places, CellValue stays 32 bytes, plain examples of changed formulas and the version-skew cost, the review's signed large-N figures. CSV measures parse their verbatim text with from_str_exact and keep scale; shortest spelling is for JSON only. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VdfEGXA7aJ6ftMsCc9PJze
This commit is contained in:
committed by
Edward Langley
parent
73ff08318c
commit
87ae21caec
@@ -41,7 +41,9 @@ them if the user answers (d). Question 12 is new.
|
||||
direction: "I think ADR 005 should implement the math operations in a separate crate".
|
||||
That is new clause 14. Clause 2 and the migration now place `Num` there, not in
|
||||
`improvise-core`. It also adds questions 13–15: where the fraction bound applies (13),
|
||||
the crate's name (14), and where ADR 009's `ExactSum` lives (15).
|
||||
the crate's name (14), and where ADR 009's `ExactSum` lives (15). The same revision
|
||||
answers the review of `e4acf643` (BLOCK D1 and D2, and its should-fix list) and Codex's
|
||||
P2 on aligning CSV entry with PR #321.
|
||||
|
||||
## The decision this ADR writes down
|
||||
|
||||
@@ -173,8 +175,13 @@ so two distributions were measured. The first is positive two-place values unifo
|
||||
| 3 | 10,000 | **1,621** (16%) | **3,836** (38%) | 2,683 (27%) |
|
||||
| 10 | 10,000 | **752** (7.5%) | **3,950** (40%) | 4,039 (40%) |
|
||||
| 100 | 10,000 | **250** (2.5%) | **4,018** (40%) | 7,944 (79%) |
|
||||
| 18,000 | 8 seeds | **0** | not measured | (all 8: see above) |
|
||||
| 90,000 | 8 seeds | **0** | not measured | (all 8) |
|
||||
| 18,000 | 8 seeds | **0** | **5 of 8** seeds (the review) | (all 8: see above) |
|
||||
| 90,000 | 8 seeds | **0** | **2 of 8** seeds (the review) | (all 8) |
|
||||
|
||||
The signed column's large-N cells were measured by the review of `e4acf643`, with the
|
||||
same generator and stand-in. It also measured signed N = 1,000: 84 of 200 trials
|
||||
(42%). At 18k it found 16 of 40 trials with seed 7, and 5 of 8 across seeds 1–8. So
|
||||
"about 40% at every length" holds out to 18k.
|
||||
|
||||
**The accumulator helps only where the total is large beside its terms.** With positive
|
||||
values the total grows with the count, its ulp grows with it, and the input rounding
|
||||
@@ -332,8 +339,9 @@ spelling of `0.1_f64` is `0.1`, not `0.1000000000000000055…`. With `float_roun
|
||||
enabled workspace-wide, that recovers the *value* the file spelled whenever the literal
|
||||
had at most 15 significant digits, though not its trailing zeros (clause 12). A longer
|
||||
literal may come back different in its last digits. Enabling `serde_json`'s
|
||||
`arbitrary_precision` instead is question 6. The import pipeline carries CSV fields as
|
||||
`serde_json` numbers too, so the same rule reads them.
|
||||
`arbitrary_precision` instead is question 6. **CSV fields are not JSON numbers and do
|
||||
not take this rule** (clause 12): they are parsed from their own text with
|
||||
`from_str_exact`.
|
||||
|
||||
### 4. How exactness propagates
|
||||
|
||||
@@ -687,20 +695,26 @@ f32 rounding of a threshold. That boundary difference already exists between f32
|
||||
f64. `scoring_known_answers.rs`'s bit patterns (gotcha 37c) are untouched, because
|
||||
gp-tree never sees a `Num`.
|
||||
|
||||
**Import.** The import pipeline carries every record as a `serde_json::Value`, CSV
|
||||
included: `parse_csv_field` (`csv_parser.rs:167-186`) turns a field into an `i64` or an
|
||||
`f64` `Number`, and the pipeline reads measures back with `as_f64` (`wizard.rs:425`). A
|
||||
`Value` has no decimal. So the one change is at that read. A measure that is an integer
|
||||
`Number` is read with `as_i64` or `as_u64` first: `parse_csv_field` already holds an
|
||||
integer of up to 19 digits exactly as an `i64`, and `as_f64` is what drops it today, so
|
||||
this keeps it exact at no cost. Any other number becomes a `Num` by clause 3's
|
||||
shortest-spelling rule, for CSV and JSON alike. A CSV field of at most 15 significant
|
||||
digits is recovered exactly. Carrying the field's text through the pipeline
|
||||
instead would restructure the analyzer for digits no CSV of money carries. One thing is
|
||||
lost and stated: the **scale**. A CSV `12.50` becomes the f64 `12.5`, whose shortest
|
||||
spelling is `12.5`, so an imported value's editor opens on `12.5`. Its value is exact.
|
||||
Only typed and `.improv` values keep their trailing zeros. The collision "sum" policy
|
||||
(`wizard.rs:307`) then sums exactly, by clause 8.
|
||||
**Import.** Two sources, two rules. This follows Codex's P2 on `962d7f90`, which
|
||||
aligns the contract with PR #321.
|
||||
|
||||
- **CSV.** PR #321 keeps every non-empty CSV field as its verbatim text
|
||||
(`Value::String`, carried as `Scalars::Text`). It does so to preserve numeric-looking
|
||||
category identifiers. So a CSV measure is parsed **from that text** with
|
||||
`numtower`'s `from_str_exact`. It keeps its significant digits and its **scale**, so
|
||||
a CSV `12.50` opens in the editor as `12.50`. It falls back to the nearest f64 only
|
||||
when it does not fit a `Decimal`.
|
||||
- Revision 3's description of `parse_csv_field` (`csv_parser.rs:167-186`: an `i64`,
|
||||
else an `f64` `Number`) is today's code at `b639266b`, and #321 replaces it. The
|
||||
ADR does not reintroduce that normalization.
|
||||
- If this ADR lands before #321, the same contract holds by reading the field's text
|
||||
before `parse_csv_field` turns it into a number.
|
||||
- **JSON.** A JSON number arrives already as an f64, so clause 3's shortest-spelling
|
||||
rule applies. An integer `Number` is read with `as_i64`/`as_u64` first, which keeps a
|
||||
19-digit integer exact where `as_f64` (`wizard.rs:425`) drops it today. A JSON
|
||||
value's trailing zeros are lost, because the f64 never had them.
|
||||
|
||||
The collision "sum" policy (`wizard.rs:307`) then sums exactly, by clause 8.
|
||||
|
||||
**Format.** `format_f64` stays for inexact values and gains a decimal twin. `FormatPlan`
|
||||
is unaffected: it chooses a format, not a value.
|
||||
@@ -821,7 +835,7 @@ An exact non-decimal value is a **reduced fraction `n/d` with `n` and `d` each a
|
||||
|
||||
| what stops being exact | `i64` | `i128` | `rust_decimal` |
|
||||
|---|---|---|---|
|
||||
| running sum of 18k or 90k margins `(Rev − Cost) / Rev`, first overflowing term, 8 seeds | 2nd–3rd | **4th–5th** | not exact (a non-terminating quotient) |
|
||||
| running sum of 18k or 90k margins `(Rev − Cost) / Rev`, first overflowing term (1-based: the term whose addition overflows), 8 seeds | 3rd–4th | **5th–6th** | not exact (a non-terminating quotient) |
|
||||
| `1.05^k` (5% compound growth) | k = 15 | **k = 29** | k = 15 |
|
||||
|
||||
`i128` doubles every horizon, for 2–3× the cost of `i64` (below). A value is 32 bytes.
|
||||
@@ -863,11 +877,19 @@ pub enum Num {
|
||||
this bullet applies at the store rather than per operation. Every operation uses
|
||||
checked `i128` arithmetic after the gcd
|
||||
reduction (`num-rational`'s `checked_add`/`checked_mul`/`checked_div` do exactly
|
||||
this). A `None` means the reduced result does not fit, and the value demotes to
|
||||
`Inexact`. The demotion is the correctly rounded f64 of the exact fraction.
|
||||
`Ratio<i128>::to_f64` agreed with `BigRational`'s conversion on 200,000 of 200,000
|
||||
random fractions, but its correct rounding was not independently proved here.
|
||||
Migration step 1's property test covers it.
|
||||
this). A `None` **may** mean the reduced result does not fit. It may also mean an
|
||||
intermediate overflowed while the reduced result would have fitted, because
|
||||
`checked_add` goes through the lcm of the denominators. Either way the value demotes
|
||||
to `Inexact`. That is safe, because it only demotes, and it is deterministic. The
|
||||
demotion is the correctly rounded f64 of the exact fraction.
|
||||
|
||||
Revision 3 cited `Ratio<i128>::to_f64` agreeing with `BigRational`'s conversion. That
|
||||
was **circular**: both share `num-rational`'s one `ratio_to_f64` routine. The review
|
||||
ran an independent check instead. It took 200,000 random reduced `Ratio<i128>`s, with
|
||||
numerator and denominator widths from 20 to 126 bits and both signs. For each, it
|
||||
asked whether the exact `BigRational` lies inside the round-to-nearest-even interval
|
||||
of the returned f64. There were **0 failures**. That is evidence, not proof, and
|
||||
migration step 1's property test uses this interval form.
|
||||
- **Contagion is unchanged.** Exact ∘ fraction is a fraction (or a decimal after
|
||||
normalization, or f64 on overflow). Anything with an inexact operand is inexact.
|
||||
- **`POW`** with an integer exponent is exact while it fits. That is why `1.05^k`
|
||||
@@ -876,8 +898,10 @@ pub enum Num {
|
||||
(an `i128` times an `i128` fits). A fraction against an f64 follows clause 6's exact
|
||||
rule.
|
||||
- **Display** rounds the exact fraction to the view's places, half away from zero,
|
||||
exactly: `n · 10^places / d`, computed in 256 bits, then rounded. So `10/3` at two
|
||||
places shows `3.33`, and `2/3` shows `0.67`.
|
||||
exactly: `n · 10^places / d`, then rounded. So `10/3` at two places shows `3.33`, and
|
||||
`2/3` shows `0.67`. In 256 bits that holds up to about 38 places, because `places` is
|
||||
a `u8` (`parse_number_format`) and `n · 10^places` passes 2²⁵⁵ above that. Beyond 38
|
||||
places the computation takes the bigint path. That is display only, and rare.
|
||||
|
||||
### Sums: the one real design choice
|
||||
|
||||
@@ -903,11 +927,50 @@ There are three ways to sum one:
|
||||
3. **Demote the whole sum on mixed denominators.** Rejected. Whether two denominators
|
||||
ever met depends on nothing a user can see.
|
||||
|
||||
**Recommendation: (2).** It is the only one of the three that keeps
|
||||
`SUM(v / 3) = SUM(v) / 3` exact, which the measurement confirmed (below). And it costs
|
||||
nothing where it cannot help. The sum of margins has one denominator per record: 17,996
|
||||
to 17,999 distinct at 18k, and 89,923 to 89,956 at 90k. The read's combination
|
||||
overflows by the fifth, so the result is inexact exactly as under (a).
|
||||
**Two rules the grouping needs.**
|
||||
- **A group whose numerator returns to 0 is dropped.** A retracted denominator then
|
||||
cannot affect the read, and "the current groups" is a function of state alone.
|
||||
- **A `Fraction` whose denominator is `2^p · 5^q` joins the decimal partition when its
|
||||
exact scale `k = max(p, q)` is at most 28.** An example is one born from a decimal
|
||||
overflow with denominator `10^17`. At scale 28 its value is an exact integer, which
|
||||
the 320-bit accumulator holds. With `k > 28` (for example `1/2^40`) it is a group of
|
||||
its own, keyed by its denominator like any other.
|
||||
|
||||
**Recommendation: (2), with a bound on the exact read** (revision 4, answering review
|
||||
BLOCK D2). Revision 3 said (2) "costs nothing where it cannot help", and that was
|
||||
false in exactly that case. The sum of margins has one denominator per record: 17,996 to
|
||||
17,999 distinct at 18k, and 89,923 to 89,956 at 90k. So its state is O(records), and
|
||||
so is every read. Under ADR 009 a maintained `SUM` whose read is O(records) is no longer
|
||||
incremental: every one-cell edit would re-read 90k groups, where (a) holds a 40-byte
|
||||
integer and reads in O(1). The review proposed a mitigation, and it is adopted:
|
||||
|
||||
- **Beside the groups, keep one ADR 009 f64 accumulator of each group's correctly
|
||||
rounded value.** Updating a group retracts its old f64 and inserts its new one, so it
|
||||
stays order-free and retractable.
|
||||
- **Read exactly only when the current number of non-decimal groups is at most
|
||||
K = 32.** Otherwise read the f64 accumulator, and the result is inexact. The count is
|
||||
a function of the current state, not of history, so the choice is independent of
|
||||
order.
|
||||
|
||||
**What that costs.**
|
||||
- **Update:** O(log D) for the group map, plus one correctly rounded conversion of the
|
||||
group's new value. That conversion is a 320-bit numerator over an `i128` denominator,
|
||||
estimated at about 1 µs through a bigint rational. Plus two accumulator updates at
|
||||
2.0–3.6 ns (ADR 009's figures).
|
||||
- **Exact read:** at most 32 checked combinations. At the measured 313–457 ns per
|
||||
`Ratio<i128>` add on unrelated denominators, that is at most about 15 µs.
|
||||
- **f64 read:** ADR 009's 0.6–1.1 µs.
|
||||
- **Memory is still O(distinct denominators)**, because the map must survive
|
||||
retraction to know when the count falls back under K. For a 90k-record margin sum
|
||||
that is about 90k × (16-byte key + 40-byte numerator + map overhead): an estimate
|
||||
of 7–9 MB for that one summed group, the same order as ADR 009's per-cell multisets.
|
||||
Not measured.
|
||||
|
||||
This keeps (d)'s wins, because `SUM(v / 3)`, averages and percentages have one or a
|
||||
handful of denominators, and it bounds the rest. The sum of margins reads the f64
|
||||
accumulator and is inexact, as under (a). Its exact combination would overflow by the
|
||||
6th term anyway (below). The 32 is a judgement: large enough for a `/ N` over a few
|
||||
different Ns, and small enough to bound the read. It is not tuned.
|
||||
|
||||
### The file and the wire
|
||||
|
||||
@@ -953,7 +1016,7 @@ their own arm.** Under it, this SUM costs what it costs under (a).
|
||||
| formula | overflows |
|
||||
|---|---|
|
||||
| `(Rev − Cost) / Rev` per record | **never** (864,000 records: 8 seeds × (18k + 90k), both bounds) |
|
||||
| running `SUM` of those margins | **at the 4th–5th term** in every seed (`i64`: 2nd–3rd) |
|
||||
| running `SUM` of those margins | **at the 5th–6th term** in every seed, counting 1-based (`i64`: 3rd–4th) |
|
||||
| `v / SUM(v) × 100` per cell (a percentage of the total) | **never** (0 of 144,000 and 0 of 720,000, both bounds) |
|
||||
| `SUM(v) / N` (the average) | never |
|
||||
| `SUM(v / 3)` against `SUM(v) / 3` | never; **equal exactly** |
|
||||
@@ -970,7 +1033,7 @@ their own arm.** Under it, this SUM costs what it costs under (a).
|
||||
- compound growth exact to k = 28 rather than 14.
|
||||
|
||||
**(d) is no better:**
|
||||
- the sum of ratios, which overflows by the fifth term and ends inexact as under (a);
|
||||
- the sum of ratios, which overflows by the 6th term and ends inexact as under (a);
|
||||
- anything already exact under (a), which is nearly all typed data.
|
||||
|
||||
**(d) costs:**
|
||||
@@ -1030,8 +1093,12 @@ In order. Each step lands on its own, with the suite green.
|
||||
- an `Exact` result is never a rounded one (inject a silently-rounding add and watch
|
||||
it fail);
|
||||
- contagion is total;
|
||||
- the conversion agrees with `str::parse::<f64>` of the decimal text (inject
|
||||
`to_f64` and watch it fail on the review's `63294.60…` case);
|
||||
- the conversion agrees with `str::parse::<f64>` of the decimal text. Inject `to_f64`
|
||||
and watch it fail on the review's `63294.60…` case. The random generator spans
|
||||
**96-bit mantissas and scales 0–28**: with 15 or fewer digits the broken `to_f64`
|
||||
agreed 200,000 times out of 200,000, so a narrower range is vacuous;
|
||||
- a fraction's conversion lies inside the round-to-nearest-even interval of the
|
||||
exact value (the review's independent form);
|
||||
- exact mixed comparison is transitive;
|
||||
- the accumulator is independent of order (clause 8's seed case).
|
||||
|
||||
@@ -1051,7 +1118,9 @@ In order. Each step lands on its own, with the suite green.
|
||||
`[0.30000000000000004, 1e12, −1e12]` through the evaluator. `Decimal`'s own `+` must
|
||||
fail it.
|
||||
5. **Entry points:** `typed()`, the import pipeline's measure read, formula literals
|
||||
(clauses 3 and 12).
|
||||
(clauses 3 and 12). The import tests assert both sides of the split: a CSV `12.50`
|
||||
keeps its scale through import (it parses the text), and a JSON `12.50` reads as
|
||||
`12.5` (shortest spelling). The tests must not assert the reverse.
|
||||
6. **Display and edit text** (clause 9). The `1.005` case is the regression test, and
|
||||
it fails at HEAD today. If improvise-felo.9 lands first, this step reuses its test.
|
||||
7. **`.improv`:** read exact, write with scale, `#i` for inexact finite, the version
|
||||
@@ -1080,7 +1149,7 @@ the user decided", as ADRs 004 and 007 did.
|
||||
measurements show:
|
||||
- (d) keeps `10/3 × 3 = 10`, `SUM(v / 3) = SUM(v) / 3`, `AVG` over any count, and
|
||||
every percentage-of-total exact, with **no** overflow in 864,000 cells.
|
||||
- It gains nothing on the sum of ratios. That still overflows `i128` by the fifth
|
||||
- It gains nothing on the sum of ratios. That still overflows `i128` by the 6th
|
||||
term and ends inexact, as under (a).
|
||||
- Its operations cost 120–650 ns against 1–55 ns for a decimal. That cost falls only
|
||||
on values (a) would have made inexact.
|
||||
@@ -1135,7 +1204,13 @@ the user decided", as ADRs 004 and 007 did.
|
||||
number read as inexact), or add a protocol version to the handshake first?
|
||||
*Recommendation:* accept it, and file the handshake version as its own ticket. The
|
||||
skew needs a deployed page and a `ws-server` of different versions, and inexact is
|
||||
the honest reading of a value an old peer computed in f64.
|
||||
the honest reading of a value an old peer computed in f64. **The cost has grown
|
||||
since question 7 flipped** (revision 4 states it). An old peer's `0.1` is
|
||||
`Inexact(0.1)`, which compares unequal to every typed `0.1` while looking identical.
|
||||
If mixed versions turn out to be common, the fix is to spell an inexact finite value
|
||||
on the wire as a `#i` string, like the file, and read a bare JSON number as exact
|
||||
through its shortest spelling. That is a wire change, so it belongs with the handshake
|
||||
version rather than here.
|
||||
|
||||
10. **The exact-sum accumulator** (added in revision 2). How are exact values summed?
|
||||
(a) a 320-bit fixed-point integer at scale 28, which holds any `i64`-weighted term
|
||||
@@ -1226,7 +1301,15 @@ the user decided", as ADRs 004 and 007 did.
|
||||
few ulps from zero, so `IF(… = 0, …)` flips from true to false, and dividing by such a
|
||||
residual yields a huge value where it yields `div/0` today. Exact data is unaffected,
|
||||
because its residuals are exactly zero. Question 3 decides the policy, and this is its
|
||||
cost.
|
||||
cost. Plain examples of formulas that change:
|
||||
- `IF(POW(x, 0.5) = 1.1, …)` with `x = 1.21`. `POW` with a fractional exponent is
|
||||
inexact, and the f64 result is not the decimal `1.1`. So it was true under the
|
||||
epsilon and is now false.
|
||||
- `IF(A / 3 * 3 = A, …)` on typed data: true today within the epsilon. Under option
|
||||
(a) it is false wherever the f64 lands off `A`. Under option (d) it is exactly true.
|
||||
- Under question 9's version skew, an old peer's `0.1` arrives as a JSON number and
|
||||
reads as `Inexact(0.1)`. That is **unequal** to every typed `0.1`, though the two
|
||||
look identical on screen.
|
||||
- A scale-only edit (`12.5` to `12.50`) bumps the record's version (clause 9).
|
||||
- `Exact(0.1) = Inexact(0.1)` is false, because comparison between the two levels is
|
||||
exact (clause 6, question 7).
|
||||
@@ -1237,7 +1320,9 @@ the user decided", as ADRs 004 and 007 did.
|
||||
spell.
|
||||
- The wire spells exact values as strings. A thin client needs no new rule, because
|
||||
`typed()` is shared.
|
||||
- **Costs:** a 16-byte number where there was an 8-byte one, and `rust_decimal` in the
|
||||
- **Costs:** `Num` is 24 bytes where an `f64` is 8, but **`CellValue` stays 32 bytes**
|
||||
under both (a) and (d), because its `String` arm already sets the size (the review
|
||||
measured it). Also `rust_decimal` in the
|
||||
bundle (+15 KB gzipped, probed). Arithmetic is about 8× slower per add and about 100×
|
||||
per division than f64 (measured, microbenchmark). A 90,000-record formula that
|
||||
divides for every record pays about 5–10 ms in arithmetic alone. Whether the
|
||||
@@ -1310,5 +1395,7 @@ the accumulator table above does not depend on the conversion B2 found wrong.
|
||||
18,000 pairs of typed values: seeds 21 and 22 for two-place operands, and those pairs'
|
||||
margins for unrelated denominators. The overflow cases use seeds 1–8, drawing Revenue
|
||||
and Cost from seeds `2s` and `2s + 1`. Sizes are `size_of` of the three `Num` shapes.
|
||||
The `to_f64` check compares `Ratio<i128>::to_f64` with `BigRational::to_f64` on 200,000
|
||||
fractions (seed 5). Every figure is the range over two runs on the machine above.
|
||||
The `to_f64` check compared `Ratio<i128>::to_f64` with `BigRational::to_f64` on 200,000
|
||||
fractions (seed 5). That comparison is **circular**, because the two share one routine,
|
||||
so the ADR now relies on the review's independent interval check instead (option (d),
|
||||
"Operations"). Every figure is the range over two runs on the machine above.
|
||||
|
||||
Reference in New Issue
Block a user