Status: Accepted
Date: October 19, 2026
Answers: whether a counter or a sum that a fold or par_fold keeps can
be proved not to overflow, and from which facts
Related: ADR-285 D1 (every whole-number operation is
checked), ADR-306 D2 (a check is dropped only on a certificate),
ADR-314 (what a grammar matched is a fact of the walk),
ADR-361 D4 (every invariant used is checked), D6 (a proposal is
only checked), ADR-366 D1 (an entry takes text or Bytes);
Part II 10.7 (fold, par_fold), Part III’s optimization (the facts a proof
reads)
grammar Measurements {
@frame(boundary: "\n")
rule MEASUREMENT -> Reading =
name:NAME ";" => temp:TENTHS frame_end { Reading { name, temp } }
entry rule file -> Summary =
par_fold(MEASUREMENT, Summary, fn(acc, m) { acc.record(m) }, Summary::merge)
}
impl Stats {
fn add(ref mut self, temp: i32) {
self.sum += temp as i64 // checked
self.count += 1 // checked
}
fn merge(ref mut self, other: ref Stats) {
self.sum += other.sum // checked
self.count += other.count // checked
}
}The temperature’s checks are proved (ADR-314): |temp| ≤ 999. The
accumulator’s are not, because a sum over a file looks unbounded to the walk:
it does not know how many rows there are. But a fold over a grammar’s input
cannot take more steps than the input has bytes, each step consumes at least
what its element rule matches at the least, and the input’s length has a
bound. Can the compiler prove the counters from that, and where does the
argument stop holding?
Count <= I with I the loop index, and the index’s range.None of them takes the bound from the platform’s address space; a length is a fact of the value.
i64 holds. A compiler for x86-64 does not know which the
machine runs. Rejected: a wrong bound removes a check that is needed, and an
overflow then runs on silently into a wrong result.@bounded, an annotation, an
ensures). Rejected: the facts are in the program already, and a wrong
annotation is the failure mode of A in the author’s hands.i128 for a sum).
Rejected: it changes the type the author wrote and what it costs.B for every field that fits, C for the rest, both only where the input’s length is known when the fold starts.
The least width of a rule is the fewest bytes any match of it takes,
read from the grammar: a literal its length, a class one byte (a character of
text takes one to four), a sequence the sum of its elements, an alternative
the least of its branches, p{m,n} m times p’s, p* and p? nothing,
dec[T](p) and bytes(p) what p takes, a call the callee’s, frame_end
its boundary’s length. A rule that reaches itself is taken at nothing for the
recursive call, which can only make the width smaller. A step that consumed
nothing would repeat forever and is a parse error, so a step takes at least
max(w, 1) bytes, with w the element rule’s least width.
A fold over an input of len bytes therefore takes at most len / max(w, 1)
steps, and a par_fold the same in all its pieces together: the pieces cut
the input, and every frame belongs to exactly one.
Every input a grammar reads today is held whole before the parse starts: text
(a String or a mapping, ADR-016 D1) or a Bytes (ADR-366 D1). Its length is
a value the fold starts with, below 2^60 as every text’s and every Bytes’.
A fold over a stream has no such fact. Should a grammar one day read input
that arrives while it parses (winnow’s Partial), its length is not known at
the start and has no bound, and D1’s step count does not exist there; no proof
of this record applies to it. The compiler carries the distinction now, not
when streams come: the length a fold’s proof starts from is taken from the
input’s extent, which is known for every input above and unbounded for
anything else, and the code that reads it says so. A new kind of input starts
as unbounded until a record decides otherwise.
For each whole-number field of the accumulator’s types the walk computes k,
the most one step can add to it or take from it, through everything the step
calls: the step’s lambda, the methods it calls, the value a map entry hands
it. Every write of the field along one run of the step counts; a write inside
a loop, or one whose amount has no bound, gives no k. The initial value
counts as a step’s. The merge must leave each such field the sum of the two
partial results’ fields, or one of them; any other merge gives no k.
From k the walk proposes the invariant |f| ≤ k · steps, with steps the
count of D1 kept beside the accumulator as a ghost: it exists in the proof,
not in the program. Like every invariant it is used only once checked
(ADR-361 D4): the initial value satisfies it, a step keeps it with steps + 1,
the merge keeps it with steps_a + steps_b. With steps ≤ len / max(w, 1) and
len < 2^60, the field’s check is proved where k · 2^60 / max(w, 1) fits its
type. A counter (k = 1) fits an i64 always.
The proof holds for a method only where it runs inside the fold. A method the step reaches that is also called elsewhere keeps its checks there; D4’s copy is how the fold gets one without them.
Where k · 2^60 / max(w, 1) does not fit, but k · len / max(w, 1) does for
the lengths below some L, the fold is versioned: the entry compares the
input’s length with L once, and runs a copy of the step and the merge without
the field’s checks below it and the checked fold as written above it. 1BRC’s
sum (k = 999, w = 5) fits below about 4.6·10^16 bytes. The copy is the
lowering’s; the grammar and the program do not change.
The facts are the walk’s at proving = aggressive (ADR-314 D4); a check is
written without its overflow test only under remove-overflow-checks:on
(Part III), and what is proved does not depend on it.
Bytes, on every platform, where the address space
is not (option A).count by D3 and sum by D4,
about 2 instructions a row (callgrind, 0.0.1045).k, not a general summary.for over a list
has its length already; one over a stream keeps its checks).k that depends on the step’s
input beyond what ADR-314 proves of a binding.