Nikaia
Menu
v0.0.1343pre-alpha GitHub

ADR-272: What Every Write Into a List Keeps In Bounds Is Known of Every Read From It

Status: Superseded by ADR-306 — its D1-D5 are D6-D10 there, D6 is D11 Date: October 3, 2026 Answers: the owner’s question, on ADR-271 §6’s next step (overflow checks, by the same proof), after the measurement showed that step buys nothing on its own: whether the compiler should know bounds on the values a list holds - what it brings, what it costs, who pays, and how others do it Related: ADR-271 D2 (no check is dropped that is not proved), D4 (the walk and its facts), D5 (a proved index lowers to proven::read), §6 (overflow checks, x % n, facts across calls); ADR-269 D4 (a claim the compiler proves has no check emitted); ADR-270 D5 (a check is dropped on a certificate its checker accepts); ADR-285 D5 (an overflow stops the program at every build); ADR-258 (the four weights). Measurements: docs/solver-workload.md §8.2

1. Question

After ADR-271 the solver’s watch kernel is at the hand-written Rust’s count with overflow checks off, and +0.7 % with them on, which is how a Nikaia crate is built (ADR-285 D5). The plan was to drop overflow checks by ADR-271 D4’s proof. Measured, that buys nothing: the checks the walk can prove (2 * v + 1 with v < 2000) are the ones LLVM already drops. The one that costs is

let start = list[k]               // list is one of watched
... value[arena[start + at]] ...  // start + at: u32, checked

and start is a value read out of a list, of which the walk knows nothing. The same holds of the two index checks around it, value[blocks[k]] and value[arena[…]]: ADR-271 D6 lists them as unprovable because the position is read out of memory.

Yet the program says what is in those lists. watched only ever receives c * size with c < clauses; arena only … % (2 * variables); blockers only values of arena. A bound on every value a list holds, known at each read, proves all three.

Should the compiler know a bound on the values of a list, and if so, does it find it or does the program write it?

Without an answer, remove-overflow-checks stays a name with no measured gain, and every index or sum over a value read from a table - a solver’s watch lists, a parser’s tables, a graph’s adjacency lists - keeps its check in the innermost loop.

2. How others do it

Language / tool Its answer Who writes the bound What it costs there Source
Wuffs refinement types, also as element types: prefixes : array[4096] base.u16[..= 4095]; every index and overflow is proved at compile time from refinements, earlier ifs and interval arithmetic the programmer, in the type no run-time check at all; a write must be proved to fit, so the author sometimes writes an extra if or a min bounds-checking note, std/lzw/decode_lzw.wuffs, std/deflate/decode_deflate.wuffs
Ada range subtypes as component types: array (…) of Lit with subtype Lit is Natural range 0 .. 3999; a value is checked when it is stored, reads are free the programmer a check at each store from memory, not checked
SPARK (GNATprove) the same types; the absence of run-time errors is proved, part of it by “a simple static analysis of bounds” the programmer prover time; contracts and loop invariants where the proof needs them GNATprove output
Pascal subrange types; with {$R+} stores and indices are checked at run time, usually off in release the programmer a check at each store, or none and no guarantee range and overflow checks
Liquid Haskell refinements inside type arguments, [{v:Int \| v < n}]; liquid inference fills in what signatures leave out signatures by the programmer, the rest inferred SMT time; the author writes the signatures ICFP’14 paper
Dafny quantified invariants, forall i \| 0 <= i < \|a\| :: a[i] < n, and subset types as element types the programmer an invariant on every loop that writes the array Dafny reference, types
Astrée array smashing: a large array is one abstract cell, an interval that every write joins inferred analysis time; precision lost for arrays whose cells differ snippet only, the paper was not reachable
Clousot (FunArray, POPL 2011) an array split into segments with symbolic bounds, one interval per segment inferred, “fully automatic” about 1 % analysis overhead, reported Cousot, Cousot, Logozzo
LLVM !range metadata on a load: the value is in this range; rustc sets it for bool, char, enum tags, NonZero the frontend, as an assumption nothing; a value outside is poison or undefined behaviour rustc’s builder.rs; the LangRef from a snippet only
HotSpot C1, .NET RyuJIT range-check elimination from induction variables, conditions, lengths and a type’s own range (byte is 0..255); never from what an array holds - - c1_RangeCheckElimination.cpp, RyuJIT rangecheck.cpp
Rust pattern types, Zig ranged integers u32 is 0..4000 exists only inside the compiler, perma-unstable; Zig’s proposal is open, not accepted would be the programmer - rust#123646, zig#3806

What transfers. Two families answer the question. In one the programmer writes the bound in the element type (Wuffs, Ada, SPARK, Pascal, Liquid Haskell, Dafny), and it is checked at each store, or proved there. In the other the tool infers one interval per array from every write (Astrée, Clousot), with no annotation. Both put the work at the write, which runs less often than the read in every kernel measured here. Neither uses a bound nobody established: LLVM’s !range is the one that does, and it is an assumption a frontend may emit only after the bound is proved.

What does not transfer. Wuffs proves everything and refuses what it cannot prove. Nikaia checks what is not proved (ADR-271 D2), so a bound that is not found costs speed, never a refusal. Astrée’s and Clousot’s precision comes from a fixpoint over loops. ADR-271 D4’s walk is a single forward pass that forgets at a loop’s head, and the proposal below stays within that.

3. Options, weighed

Option A — do nothing

The checks stay. Record the measurement; the watch kernel keeps its +0.7 % with overflow checks on.

Option B — the compiler finds the bound (one interval per list)

Smashing, in ADR-271 D4’s walk. A local list whose every write the walk can see gets a bound: the join of what each write puts in, each one proved at its write from the facts that hold there. The program writes nothing:

let mut watched: Vec[Vec[u32]] = []
watched.resize((2 * variables) as i64, [])
for c in 0..<clauses {
    watched[first].push(c * size)      // c * size <= (clauses - 1) * size
}
...
let start = list[k]                    // list = watched[lit]: start <= 31996
... arena[start + at] ...              // start + at <= 31999: no overflow

Option C — the program writes the bound in the element type

As Wuffs and Ada do. The write is checked, or proved, and a read knows the bound:

let mut watched: Vec[Vec[u32 in 0..<32000]] = []   // syntax for illustration only

Option D — assume it

Emit LLVM’s !range or assume from what the program seems to hold, without a proof. Refused by ADR-271 D2: a wrong guess is undefined behaviour.

Weighed

  D1 the special case pays, not the common one D2 the compiler works, not the developer D3 no cost for the common case D4 consistent with itself If it is wrong
A yes no: the author rewrites the loop, or keeps the cost yes yes slow, never wrong
B yes: only aggressive pays the walk yes: nothing is written yes: off by default, and the walk added nothing measurable over the corpus (§8.2) yes: it is ADR-271 D4’s walk with one more kind of fact, under ADR-271 D2 a wrong proof, caught by the certificate’s checker before a check is dropped; a bound not found costs speed only
C yes no: the author writes and maintains ranges yes no, not yet: Nikaia has no range types, and one for list elements alone would be a type the language has nowhere else a wrong range stops the program at a write, which is a new place to stop
D yes yes yes no: a build option changes what a program means memory read past the end, silently

What B brings, measured by removing from the lowered Rust exactly the checks it would prove (§8.2, fat LTO, overflow checks on, as a Nikaia crate is built):

watch kernel, n = 2 000 instructions against Rust by hand
Rust by hand 10.69 M -
Nikaia today, aggressive 10.44 M −2.3 %
B: values’ bounds 9.68 M −9.4 %
B and a filling loop’s length (D4 below) 9.41 M −12.0 %

Index sites proved: 22 of 40 today, 28 with values’ bounds, 31 with a filling loop’s length. rows and bignum gain nothing: their remaining checks need x % n, two lists of equal length, or a product of two unknowns, none of which is a bound on values.

What B costs, and who pays.

Why not C now. C reaches what B cannot: a bound across a call, a list behind a parameter, a value the program only knows from outside. But it is a new kind of type, and ADR-258 D2 says the compiler works first. If B’s measurement over real programs shows bounds it cannot find, that is C’s question, asked with that evidence.

4. Decision

B is chosen, together with the overflow option that makes its gain reachable.

D1 — remove-overflow-checks:aggressive, a second name for ADR-271 D1’s option.

--optimization=remove-overflow-checks:aggressive, or the same word in [build] optimization, with the levels off (the default) and aggressive. There is no basic: the one shape a walk without a solver would prove is the one LLVM already proves. The option is independent of remove-bounds-checks and part of the cache key like it. ADR-271 D2 holds unchanged: a check that is not proved stays.

D2 — A bound on a list’s values, when every write is seen.

For a list bound in the body being walked (a let, not a parameter), the walk keeps a lower and an upper bound that hold of every value it holds, linear terms over names the body never changes. The bound is the join of what each write puts in: a literal’s items, push, insert, resize’s fill value, xs[i] = v, and, for a list of lists, the same writes into xs[i]. Each write’s value is proved within the bound at that write, from the facts that hold there.

The list has no bound if it is handed to a call that may change it (a mut parameter, or a callee this program does not declare), captured by a lambda, a task, an overlap branch or a select arm, or written by any method not on a closed list. A value read from a list with a bound is a number of the proof with that bound, wherever ADR-271 D4 reads a number: in an index, a comparison, an arithmetic check. A binding of such a read (let start = list[k]) keeps the bound. So does a binding of an inner list (let list = watched[lit]) for its values.

The bound is found flow-insensitively, before the walk, from the writes of the whole body. That is Astrée’s smashing, and it needs no fixpoint.

The constants a write’s value lies between come from interval propagation over the linear facts that hold there, as Wuffs bounds a value; each end is then confirmed by the solver on a certificate the checker accepts, and an end it does not confirm is open. Two passes find the bounds, each reading the last one’s, and a third keeps only those every write is proved to stay within while assuming all of them - an inductive invariant. A bound that holds only by assuming itself larger is dropped.

D3 — x % n is a bound.

Where x is not negative and n is a positive term, 0 <= x % n < n; for an unsigned x, always. This is what bounds arena’s values (ADR-271 §6 names the same rule for the rows kernel’s cols[r]).

D4 — A loop that pushes once per turn adds its count to the length.

for _ in lo..<hi { … xs.push(v) … }, with exactly one push on every path through the body and no other change to xs, leaves xs.len() larger by hi - lo where lo <= hi. That is what proves arena[start + at].

D5 — What a dropped overflow check lowers to.

The checker records each +, - and * whose two sides are of one whole-number type, by the operator’s span, with that type. A proved one lowers to <T>::wrapping_add(a, b) (_sub, _mul). With no overflow, that is the same number with no check, and no unsafe is needed. Naming T ties the proof’s type to the emitted one: if they ever disagreed, rustc would refuse the program instead of computing something else.

D6 — The criterion, before it is accepted.

Built behind the option, B is accepted only if all three hold:

If the gain holds and the cost does not, the bound is kept for lists whose reads sit in a loop, and the rest are not tracked.

Met (solver-workload.md §8.3): the watch kernel at 9.41 M (10.44 M at off), with every site D2 to D4 name proved; lowering the standalone files within noise of off (about +3 %), the kernels +16 ms (24 to 40 ms); every test program printing the same at both levels, and tests/value_bounds.rs stopping where off stops.

5. Consequences

6. What this does not decide

This site is open source. Improve this page.