Issue #432: The prover: a counter per consumed item cannot overflow, bounded by the input’s size

Open and answer this issue on GitHub.

compiler, performance, ready · opened 2026-10-04 · updated 2026-10-31 · 4 comments

#420 assumes the overflow checks in 1BRC’s Stats::add cannot be proved, because “a sum over a file is unbounded”. With four facts the compiler could have, they can:

1. The input is bounded. fs::map maps the file into the address space, which on x86-64 is at most 2^47 bytes for a user program. That is a platform fact, like a pointer’s width.
2. Each item consumes bytes. The grammar says how few bytes a MEASUREMENT can have: NAME may be empty, then ;, at least 0.0, and \n, so 5. A par_fold therefore has at most 2^47 / 5 items.

3. Each item adds a bounded amount. count += 1. sum += temp, where

   temp

   ≤ 999 follows from dec[i32](digit{1,2}) and the action under ADR-314 D1.

4. An invariant over the fold and its merge. count and

   sum

   grow by at most 1 and 999 per item, and merge only adds two partial results that each satisfy that bound.

From these: count ≤ 2.8·10^13 and

sum

≤ 2.8·10^16, both far below i64’s 9.2·10^18. Both checks are provably unnecessary.

What it is worth: on 1BRC about 2 instructions a row, the two overflow branches, which are always predicted (callgrind, 0.0.433). It is more interesting in general: counters and sums in an aggregation are among the most common integer code, and today every one of them keeps its check.

What it needs, beyond ADR-314:

• a bound on input size per source;
• the minimum width of a grammar rule’s match;
• a relational invariant across a par_fold’s step and merge, of the form “this field grows by at most k per item”.

That is a decision for an ADR of its own. Until then the checks stay, as the language says (ADR-285 D1).

Comments

keywan-ghadami, 2026-10-19

Decided: ADR-367 (0.0.1049)

A correction first

Fact 1 above, the 2^47-byte address space of x86-64, is wrong in general. With 5-level paging (LA57) a user program maps up to 2^56 bytes. Linux supports this, and so do Intel servers since Ice Lake. Then 2^56 / 5 · 999 ≈ 1.4·10^19, which is more than an i64 holds (9.2·10^18), and a compiler for x86-64 does not know which paging the machine uses. A proof built on fact 1 would remove a check that is needed, and the sum would then overflow silently into a wrong result. ADR-367 §3 rejects that option.

What holds instead

• The bound comes from the value, not from the machine. Every input a grammar reads is held whole before the parse starts: text or a mapping, or Bytes (ADR-366 D1). Part III already bounds the length of a text or Bytes below 2^60.
• Each step consumes something. It takes at least the element rule’s least width w, and at least one byte. So a fold takes at most len / max(w, 1) steps. 1BRC’s MEASUREMENT has w = 5. (D1)
• A field grows by a bounded amount. For a field that each step changes by at most k, and that the merge only adds, the walk proposes |f| ≤ k · steps. Here steps is a ghost: it exists in the proof, not in the program. Like every invariant, it is checked before it is used (ADR-361 D4). (D3)
• count (k = 1) therefore fits an i64 for every length, so its check is proved.
• sum (k = 999) fits only below about 4.6·10^16 bytes. For it, the entry compares the input’s length once before the fold. Below the limit it runs a copy of the step and the merge without the field’s checks; above it, the checked fold as written. (D4)

Never over a stream (D2)

A fold over input that arrives while it parses, such as a future grammar over winnow’s Partial, has no known length. None of this applies there. The compiler carries the distinction from the first step: the proof starts from the input’s extent, which is known for text and Bytes and unbounded for anything else. The code that reads it names ADR-367 D2, as a warning for whoever adds streaming input.

• Record: ADR-367
• Rule: Part III’s optimization paragraph (30-nikaia-tooling.md)

To build

1. Least width of a rule (D1). A function over the compiler’s grammar AST, following D1’s table:
   • literal = its length, class = 1, sequence = sum, alternative = least, p{m,n} = m·p, p*/p? = 0;
   • dec/bytes = what p takes, call = the callee’s, frame_end = its boundary’s length;
   • recursion counts as 0.

   Unit tests: 1BRC’s MEASUREMENT = 5; a rule that may match empty = 0, so the step count uses 1; a recursive rule.

2. Input extent (D2). A fact the fold’s proof starts from: known for text, a mapping and Bytes, unbounded otherwise.
   • Every grammar input today is known.
   • The type and the place that reads it carry a comment naming ADR-367 D2: a streaming input must be unbounded, and no step count exists for it.
   • A unit test shows that unbounded gives no proof.
3. Growth per step and the invariant (D3).
   • Compute k: for each whole-number field of the accumulator’s types, by a walk of the step itself. It goes through the lambda, the methods it calls, and the value a map entry hands it, and does not depend on general result summaries (#641).
   • When there is no k: a write in a loop, or one with an unbounded amount.
   • The merge: it must be additive (a field becomes the sum of both, or one of them).
   • The invariant: proposed as |f| ≤ k·steps with the ghost steps, and checked through ADR-361 D4: it holds for the initial value, a step keeps it, the merge keeps it.
   • Where the proof applies: only where every call of the method is inside the fold.

   1BRC: the checks of self.count += 1 and self.count += other.count are proved, and with remove-overflow-checks:on they are written without the check. sum keeps its checks until step 4.

   Tests:

   • 1BRC-like: count proved, sum still checked;
   • the method also called outside the fold: checks kept;
   • an increment in a loop: kept;
   • a merge that takes max for a counter field: kept;
   • output the same as before.
4. Versioning before the fold (D4). The lowering writes a second, hidden entry rule. It uses the same element rule, with copies of the step and the merge without the field’s checks, and the entry compares the length against L once. Test: an input above L runs the checked fold. Then measure 1BRC again with benches/brc/brc.sh; it should lose about 2 instructions a row.

Steps 1 to 3 are being built now. Step 4 comes after.

---

Generated by Claude Code

keywan-ghadami, 2026-10-19

Steps 1-3 built (0.0.1051)

Built in crates/nikaia/src/fold_bound.rs (6bc5a1d, 18a71d1), with tests in crates/nikaia/tests/fold_counters.rs (10).

What was decided where ADR-367 left room:

• D1, least width:
  • The classes digit, hex_digit, any, char, alpha1 and multispace1 count 1 each.
  • Every other built-in counts 0, including until, text, peek and list. That can only make the width smaller.
  • frame_end counts the length of the element rule’s own @frame boundary, and 0 where the rule has none.
• D2, extent: the extent is Extent { Known, Unbounded }, and input_extent answers Known for every grammar input today. The type, the function and the place that reads the extent each carry a comment naming ADR-367 D2: a streaming input must answer Unbounded, and so does any new kind of input until a record decides otherwise. A test shows that Unbounded gives no proof.
• D3, growth per step:
  • k: only a literal amount gives k.
  • Matching fields: a field is matched by its name across all structs.
  • Where the proof applies: every write of the field, and every struct literal of its type, must stand where nothing outside the fold can reach it. Reachability is by name, closed over calls, and trait methods count as reachable from outside. This is stricter than the ADR: a struct literal of the type in main already blocks the proof.
  • The merge: it may be self.f += other.f, or the map merge entry by entry, drain plus entry(...).and_modify(merge).or_insert(v), recursively.
  • par_fold: proves only fields whose initial value is 0, because its pieces are not counted. The invariant is |f| ≤ k·steps + k0·pieces.
  • Checking the invariant: it is checked through proofs::ask three times: for the initial value, for a step, and for the merge.

  Each of these is a place where a later step could prove more.

Result: in 1BRC, self.count += 1 and self.count += other.count are proved and written as wrapping_add, while sum keeps its check. In the release binary, count is now a single incq, and sum is an add followed by a jo.

Open: step 4 (D4, versioning before the fold) and the re-measurement after it.

---

Generated by Claude Code

keywan-ghadami, 2026-10-20

Another case: a counter over find_all (benches/brc/scan.nika, 0.0.1146):

for p in data.find_all(seps) {
    n += 1
    x = x ^ p
}

Each hit is a different position below data.len(), so n cannot exceed the input’s length, exactly as with a counter per consumed item (ADR-367). Today n += 1 keeps its inc/jo.

Callgrind also shows that n and x are stored to memory at every hit, presumably because the println after the loop takes their address and the panic path of the jo keeps them alive. That is unconfirmed, and it may go away together with the check.

Together these are most of the remaining gap between Nikaia’s scan and Rust’s at x86-64: 37.7 against 31.3 instructions a row. At x86-64-v3 the two are level, 29.5 against 29.4.

To build:

1. A for over a std producer whose items are distinct positions in a buffer (find_all, and, once built, par_pieces’s pieces) bounds a counter incremented once per item by that buffer’s length. The ledger names such producers.
2. Test: scan.nika lowers n += 1 without an overflow check.
3. If the stores are still there afterwards, trace them with callgrind_annotate and file what remains.

---

Generated by Claude Code

keywan-ghadami, 2026-10-31

The loop part of this (a counter in a for bounded by the turns, which a length bounds below 2^60) is decided as ADR-361 D13 (architect, 2026-10-31) and built by the prover lane under #1053 step 4 (brief p6). The input-size, grammar-width and par_fold merge parts stay open here.

---

Generated by Claude Code

Back to Open Issues