ADR-314: What a Grammar Matched and What a Callee Promises Are Facts of the Walk

Status: Accepted - Option B, with a short loop’s turns left open (§7) Date: October 3, 2026; decided October 4, 2026 examples/1brc.nika reads the whole part with dec[i32](digit{1,2}) since 0.0.419, so its action has no loop left: whole * 10 + digit_value(frac). The action quoted in §1 is the one §3 measured, and the question stands for every action that folds digits by hand. Answers: the owner’s question, after 1BRC’s profile, whether the checks that stay in a grammar’s actions - value * 10 + digit_value(d) over a digit{1,2} - say something is missing, given that the question reaches other parsers and other code than 1BRC Related: ADR-306 D4 (the walk and what it reads), §6 (facts across a call); ADR-306 D7 (a bound on a list’s values), D10 (an unchecked operation names its type); ADR-269 D9 (what the prover reads), D14 (a promise crosses a package, an observation does not), D16 (a call or a loop stops the calculus), D17-D18 (postconditions and the ledger’s ensures); ADR-296 (frames and par_fold); ADR-258 (the four weights). Measurements: docs/solver-workload.md §8.4

1. Question

1BRC’s temperature is parsed in an action of its grammar:

rule TENTHS -> i32 =
    neg:"-"? whole:digit{1,2} "." frac:digit
    {
        let mut value = 0
        for d in whole.chars() { value = value * 10 + text::digit_value(d) }
        value = value * 10 + text::digit_value(frac)
        if neg != null { -value } else { value }
    }

Every *, + and the negation keep their overflow check at remove-overflow-checks:aggressive, though value cannot pass 999. Three things the program says are not facts the walk of ADR-306 can use:

What the grammar matched. digit{1,2} matched one or two characters, each of them '0' to '9'; frac:digit is one of them. The walk does not enter a grammar’s actions at all.
What a callee returns. text::digit_value(c) is c as i32 - 48, so for a digit it is 0 to 9. The walk reads nothing across a call (ADR-306), and std publishes no postcondition: std.contracts has not one ensures.
How often a loop turns. The loop runs at most twice, and value * 10 is not linear in the turns. The walk forgets value at the loop’s head, and no linear fact says value <= 99 after it.

Should the walk learn these three kinds of fact, and who states them?

The question is not 1BRC’s. Every parser of a number - JSON, CSV, a date, an HTTP Content-Length - has the same action, and every call into std hides a result the caller’s proof needs.

2. How others do it

Facts across a call - how a prover learns that a callee returns 0 to 9:

tool	how	what the programmer writes	source
SPARK (GNATprove)	callers see the callee’s `Post`; an expression function’s body is an implicit postcondition; a local helper without a contract is analysed “as if inlined” at each call (contextual analysis)	nothing for a local helper or an expression function; a `Post` otherwise	contracts, expression functions
Frama-C EVA	re-analyses the callee’s body in each calling context; `-eva-use-spec` uses the written spec instead	nothing	value_parameters.ml
Dafny	modular: a method is seen only through its `ensures`; a `function`’s body is visible unless `opaque`	`ensures` on methods	user guide
Wuffs	a refinement on the return type, `base.u32[..= 0x3FF]`, checked in the callee and assumed by the caller	the refinement	decode_json.wuffs
Liquid Haskell	refined signatures, partly inferred from qualifiers	usually a signature	overflow post
Rust / LLVM	inlining first, then range analysis - `ConstraintElimination` is Fourier-Motzkin over the inlined code; an optimisation, never a report	nothing	ConstraintSystem.cpp

A loop with a small trip count whose value grows nonlinearly:

tool	how	what the programmer writes	source
SPARK	unrolls a `for` over a range of at most 20 turns with no written invariant	nothing; a written invariant turns it off	loop invariants
Frama-C EVA	`-eva-auto-loop-unroll n` unrolls a loop it can bound by `n`, syntactically; `-eva-slevel` keeps separate states	an option or a `loop unroll` annotation	auto_loop_unroll.ml
Astrée	unrolling with widening	configuration; not checked, the site was unreachable	-
Dafny, Wuffs	a loop needs a written invariant; nothing is unrolled for a proof	`invariant`, `pre`/`inv`/`post`	Wuffs facts

Plain interval widening sends value to infinity; only unrolling, or an invariant someone writes, keeps it at 999.

Facts from a grammar - does any tool hand an action what its rule matched?

tool	parsed values carry facts?	source
EverParse / 3D	constraints the author writes (`age >= 21`) are checked while parsing, and a later constraint may assume an earlier one; the generated C carries none of it	3d-lang
Vest (Verus)	refinements such as `u16 \\| 1..1024`, checked while parsing, known to Verus specs only	refinements
Kaitai Struct	`valid:` is a run-time check, not a fact	user guide
nom, pest, ANTLR	no; not checked	-

None derives facts from a text grammar’s repetition counts or character classes. The closest are binary-format tools where the author writes the predicate. What transfers: SPARK’s two automatic rules - an expression body is a postcondition, a short counted loop is unrolled - and LLVM’s evidence that Fourier-Motzkin over inlined code is how a production compiler drops these checks. What does not: EVA’s whole-program re-analysis, which costs every call site a walk of the callee and reads across a package boundary a body that ADR-269 D14 says is the callee’s to change.

3. What it brings, and what blocks proofs today

1BRC. Removing the checks of TENTHS by hand from the lowered Rust (the method of §8.2): 481.3 M instructions to 476.5 M over a million rows, 4.8 a row, 1.0 %. The checks are cheap - predicted, off the hot path’s critical chain - and the action is a small part of a row.

The corpus. The 46 files of the repository that lower alone have 129 +, - and * sites of one whole-number type outside grammar actions (ADR-306 D10). aggressive proves 23. What blocks the other 106, read off each site:

what the proof lacks	sites	example
a bound on values in a list of lists	~28	`d[i - 1][j] + 1` (an edit distance), `common[i + 1][j + 1] + 1`
an upper bound on a length	~25	`x.len() + 1`, `a.len() + b.len()`, `c.len() - w.len() - 1`
a field of `self`	~12	`self.at + 1 < self.c.len()`
a product or quotient of two unknowns	~12	`i * i > n`, `(n + 4) / 5`
recursion, an unbounded parameter	~6	`show(item, indent + 1)`
a callee’s result, a `char`’s range	few	`c as i32 - 48` in `std`’s own `parse_i64`
(grammar actions, not walked)	3 + 3	1BRC’s `TENTHS`, its test fixture

So the three facts this record is about unblock few sites today: the corpus has two grammars that compute in their actions, and calc’s computes on numbers that come from its input, where an overflow is real. Their value is that they are general, and that each is the first case of a mechanism

a fact from a declaration, a promise across a call, a loop with a known trip count - that the larger rows above need as well.

4. Options, weighed

Option A - nothing

The checks stay. 1BRC keeps its 1.0 %; every parser of a number keeps them.

Option B - the compiler derives all three

The walk enters a grammar’s actions with what each binding matched; a callee’s published ensures is a fact at the call, and a sync function whose body is one return of an expression the prover reads publishes that expression; a loop the walk can count to a few turns is walked turn by turn. The program writes nothing:

rule TENTHS -> i32 =
    neg:"-"? whole:digit{1,2} "." frac:digit
    { ... }                       // whole.len() in 1..2, each char '0'..'9'

pub fn digit_value(c: char) -> i32 sync {
    return c as i32 - 48          // ensures result == c as i32 - 48
}

Option C - the program writes the facts

Contracts on every helper, invariants on loops, refinements on bindings - as Dafny and Wuffs require.

pub fn digit_value(c: char) -> i32 sync {
    assert c >= '0' && c <= '9'           // syntax for illustration only
    return c as i32 - 48
}
for d in whole.chars() invariant value < 100 { ... }

Option D - read the callee’s body at each call

EVA’s and GNATprove’s contextual analysis for every callee, across packages.

Weighed

	D1 the special case pays	D2 the compiler works	D3 no cost for the common case	D4 consistent	If it is wrong
A	yes	no	yes	yes	slow, never wrong
B	yes: only `aggressive` pays	yes	yes: `off` by default	yes: each rule is ADR-269’s (D9, D17, D18) widened by one kind of fact	a wrong fact, caught by the certificate’s checker before a check is dropped
C	yes	no: the author proves what the grammar already says	yes	no: Nikaia has no loop invariants or refinements	a wrong invariant stops the program, a new place to stop
D	no: every call pays a walk of its callee	yes	no	no: a body is read across a package where ADR-269 D14 lets only promises cross	a callee’s change silently changes a caller’s proof

B is decided, without the loop of its third fact: the one site it was for is gone (§7). It keeps ADR-269’s line between a promise and an observation: the facts B adds are all stated - by the grammar, which is a declaration; by an ensures in the ledger; by a body that is nothing but an expression, which SPARK too reads as a postcondition. D loses on D4: it would make every callee’s body a contract nobody wrote.

5. Decision

D1 - The walk enters a grammar’s actions, knowing what each binding matched.

A rule’s action is walked like a function’s body (ADR-306 D4), starting from these facts for its bindings:

x:p{m,n}, x:p+, x:p* over a character class p - digit, alpha, a range, a set of ASCII characters - is text: x.len() is between m and n (1 and none, 0 and none), and every character of x is in p. For a class of ASCII characters a character is one byte, so the length counts both.
c:p over a class is a char in p.
x:"lit"? is a literal or null; nothing numeric.
x:dec[T](p{m,n}) over a class of digits is a T between 0 and 10^n - 1 (and between 10^(m-1) and that where the class excludes 0, which digit does not). dec reads the text the run matched, and a run of at most n digits writes no larger number; a T too small for it is dec’s own error at the parse, never a value. 1BRC’s whole is 0..=99.
a binding of another rule is that rule’s result type; a numeric result carries no bound, unless the rule’s every alternative is proved within one (§7).

The characters of a bound text are what ADR-306 D7 calls the values of a list: for d in x.chars() binds d within p.

D2 - A character’s code is a number of the proof.

c as i32 (and any wider whole-number type) of a char is in 0..=0x10FFFF always, and within its class where D1 gave one. A conversion keeps its value (Part III A.2), so this is a fact about the number, as ADR-306 D4 reads every conversion.

D3 - At a call, the callee’s published `ensures` is a fact about the result.

Where the callee’s ledger entry has ensures (ADR-269 D17-D18), the walk assumes it of the call’s value, with the arguments for the parameters - in the same package also what is inferred, across one only promises (ADR-269 D14). And a sync function whose body is a single return e, with e a value the prover reads, publishes ensures result == e: the expression is the function, as SPARK reads an expression function. It is a contract like any other: ADR-269 D19 warns its author when it changes in the breaking direction. text::digit_value publishes result == c as i32 - 48 this way, and with D1 and D2 a digit gives 0 to 9.

D4 - All of it at `aggressive`, and only facts the solver confirms.

Since ADR-306 D14 how hard the compiler proves is proving’s and not optimization’s, so these facts serve the defects a build finds as much as the checks it drops. Nothing here changes off or basic. Every bound D1 to D3 adds is a fact the solver uses, and a check is dropped only on a certificate its checker accepts (ADR-306 D2). A grammar’s class and a callee’s ensures are statements of the program; a wrong one would be the program’s, and an ensures is checked where its function returns (ADR-269 D17).

D5 - The criterion it is built against.

the gain: every check in 1BRC’s TENTHS proved - whole * 10, + digit_value(frac) and the negation, by D1, D2 and D3 together - and what they cost a row measured again on today’s action (§3’s 4.8 were taken on the loop);
the cost: lowering the repository’s standalone files at aggressive within +5 % of today’s aggressive;
the meaning: every program the tests run prints and stops the same at every level, including an action whose input does overflow (calc).

6. Consequences

A grammar becomes a source of facts, which no other tool’s grammar is (§2): an action is checked against what its rule matched.
std’s small arithmetic functions get contracts in the ledger without anyone writing them, and their authors are warned when they break one.

7. What this does not decide

An upper bound on a length - the largest row of §3 (~25 sites, x.len() + 1). A list or text cannot hold more elements than memory bytes, so len() + k cannot overflow an i64 for any small k; whether the compiler may rely on the machine’s address space is a question of its own.
Values in a list of lists (~28), which need ADR-306 D7 widened to nested writes that read each other. Fields of self (~12 sites) are decided by ADR-306 D17.
A rule’s result as a bounded number (D1’s last bullet).
How often a short loop turns. Proposed as walking a loop of at most 8 counted turns turn by turn, without forgetting what it changes at its head (SPARK unrolls up to 20). Left open when B was decided: the case it was for, for d in whole.chars() in 1BRC’s action, is dec[i32](…) now, and §3’s table has no other site it would prove. It returns with the first program that needs it, and with a number for the turn count.
Products and quotients of two unknowns - interval arithmetic for *, / and % beside Fourier-Motzkin.

This site is open source. Improve this page.