Nikaia
Menu
v0.0.1343pre-alpha GitHub

ADR-306: An Index or Overflow Check a Proof Shows Unneeded Is Not Emitted, at the Level the Build Asks For — --optimization=remove-bounds-checks and remove-overflow-checks

Status: Accepted Date: October 3, 2026 (D12-D16: October 4, 2026, #383, #390; D17: October 19, 2026, #384; D18: October 20, 2026; D20: October 22, 2026, #781) History: the records this one replaces are archived in docs/history/adr; read them only for how the decision was reached Answers: ADR-269 §6’s open question for two of the checks nobody writes - whether a proved check is not emitted - for an index out of bounds and for an arithmetic overflow; and the owner’s question whether the compiler should know bounds on the values a list holds, who finds them, and what they cost Related: ADR-269 D4 (a claim the compiler proves has no check emitted, and means the same either way), D9-D10 (what the prover reads), ADR-270 D1 (Fourier-Motzkin in the logic layer) and D5 (a check is dropped only on a certificate its checker accepts), ADR-285 D1 (an index is an i64) and D5 (an overflow stops the program at every build), ADR-293 D2 (an assignment’s value is computed before the place it writes), ADR-218 D1 (every unsafe topic is a small crate of its own), ADR-258 (the four weights), Part III A.2 (an index out of bounds, an overflow and a conversion that does not fit stop the program at every build) and 13.3 ([build])

1. Question

xs[i] stops the program where i is outside xs, and a + b stops it where the sum leaves its type (Part III A.2). Each check is a compare and a branch, nothing alone; in a loop it is what keeps the code generator from unrolling and vectorising. In the big-integer kernel of benches/solver-kernels.nika the index checks in out[i + j] are 34 % of the instructions.

The checks are not optional: reading past a list’s end or overflowing is a defect, and the stop is how it is seen. But a check that cannot fail is a cost, not a check. ADR-269 D4 drops a written assert the prover proves; the same question stands for the checks nobody wrote.

Many of the costly checks are on a value read out of a list:

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

The walk knows nothing of start, yet the program says what is in those lists: watched only ever receives c * size with c < clauses, arena only … % (2 * variables). Without a bound on the values a list holds, an overflow option buys nothing - the overflow checks a walk can prove from ordinary facts (2 * v + 1 with v < 2000) are the ones LLVM already drops.

May the compiler drop an index or an overflow check, when, who decides that it tries, and may it know what a list holds?

2. How others do it

Language / tool Its answer Who writes the bound Source
Rust always checked; LLVM removes what it proves from the code it sees; get_unchecked in unsafe for the rest - the language, from memory
Swift checked; -Ounchecked removes the checks without proof, so a wrong index is undefined behaviour - from memory, not checked
HotSpot C1, .NET RyuJIT range-check elimination from induction variables, conditions, lengths and a type’s own range; never from what an array holds - c1_RangeCheckElimination.cpp, RyuJIT rangecheck.cpp
Ada / SPARK range subtypes, also as component types; checked at each store, or GNATprove proves the absence of run-time errors the programmer GNATprove output
Wuffs refinement types, also as element types (array[4096] base.u16[..= 4095]); every index and overflow proved at compile time, by interval arithmetic and earlier ifs; what is not proved is refused the programmer, in the type bounds-checking note
Pascal subrange types; with {$R+} stores are checked at run time the programmer range and overflow checks
Liquid Haskell, Dafny refinements in type arguments ([{v:Int \| v < n}]), quantified invariants or subset types; an index is a proof obligation the programmer, partly inferred ICFP’14 paper, Dafny types
Astrée array smashing: an array is one abstract cell, an interval every write joins inferred snippet only, the paper was not reachable
Clousot (FunArray) an array split into segments with symbolic bounds, one interval each inferred Cousot, Cousot, Logozzo, POPL 2011
LLVM !range metadata on a load; rustc sets it for bool, char, enum tags, NonZero the frontend, as an assumption rustc’s builder.rs
Rust pattern types, Zig ranged integers exist only inside the compiler (Rust) or as an open proposal (Zig) would be the programmer rust#123646, zig#3806

What transfers. SPARK’s and Dafny’s order - prove, then drop - and the JIT’s range-check elimination for the loop shape that is most of the cost. For what a list holds, two families: the programmer writes a bound in the element type (Wuffs, Ada, Liquid Haskell, Dafny), or the tool infers one interval per array from every write (Astrée, Clousot). Both put the work at the write, which runs less often than the read.

What does not. Swift’s -Ounchecked and LLVM’s !range used as a guess: a build option that turns a stop into undefined behaviour changes what a program means, and Part I 1.2 lets no build option do that. Wuffs refuses what it cannot prove; Nikaia checks it, so a proof not found costs speed, never a refusal. Astrée’s and Clousot’s precision comes from a fixpoint over loops; the walk here is a single forward pass that forgets at a loop’s head.

3. Options, weighed

  What it is D1 the special case pays D2 the compiler works D3 no cost for the common case D4 consistent If it is wrong
A leave it to LLVM every check emitted yes no: the author rewrites the loop until LLVM sees it yes yes slow, never wrong
B an unchecked mode -Ounchecked, or !range assumed yes yes yes no: a flag changes meaning memory read past the end, silently
C drop what is proved, always ADR-269 D4’s rule as it stands for an assert no: every build proves yes no yes a wrong proof, everywhere, unasked
D drop what is proved, at a level the build asks for --optimization=…:basic\|aggressive; values’ bounds inferred from every write yes: only a build that asks proves yes: nothing is written yes: off by default yes: meaning never changes a wrong proof, caught by the certificate’s checker before a check is dropped; a bound not found costs speed only
E the bound written in the element type Vec[Vec[u32 in 0..<32000]] (illustration only), checked or proved at each write yes no: the author writes and keeps ranges yes no: a range type for list elements alone, which the language has nowhere else a new place for the program to stop

D is chosen. B and C lose on the promise to the program: B changes what it means, C makes every build pay and lets a growing prover change every program’s emitted code unasked. A leaves the work to the developer. E reaches what D cannot - a bound across a call, a list behind a parameter - but is a new kind of type, and ADR-258 D2 says the compiler works first.

The number that decided it: on the solver’s watch kernel the index proof alone gives 10.44 M instructions against 10.69 M for Rust by hand, and 9.41 M with the bound on a list’s values.

4. Decision

D1 — One option, --optimization=NAME:LEVEL, and its first name, remove-bounds-checks.

--optimization=remove-bounds-checks:LEVEL on the command line, for every command that lowers (lower, build, run, test), or optimization = "remove-bounds-checks:LEVEL" in [build]. The levels are off (the default), basic and aggressive. Words are comma-separated, and the command line may give the flag more than once; a later word for a name wins. A name or a level the compiler does not know stops the build before anything is read, naming the words there are.

Unlike Part I 1.2’s options it changes nothing a program means (D2), so a single build may override it, as it may --target. It is part of the build’s cache key, and reaches the wrapper Cargo runs as the other options do. std is lowered at off: the toolchain’s own lowering does not follow an option of the program it serves (Part III 13.2).

D2 — No level drops a check that is not proved.

An index check is dropped only where 0 <= i < xs.len() holds every time the index is reached. The program means the same at every level: where the proof holds, the check could not have stopped it; where it does not, the check stays. A level says how hard the compiler tries, not what the program may do, and a program that stops at an index at off stops at it at aggressive. The same holds for every name of D1’s option.

D3 — basic: the loop over a list’s own length.

xs[k] where k is the binding of an enclosing for k in lo..<xs.len(), lo is a literal that is not negative or the binding of such a loop, and nothing in the loop’s body can change xs’s length or k: xs is not assigned or bound again, not handed to a call, not captured by a lambda, and every method called on it is one a fixed list knows to keep the length (len, contains, iter, sort, swap, …). An index inside a lambda in the loop is not proved: the lambda may run after the loop. No solver is asked; the pass is linear in the body.

D4 — aggressive: the solver, from the facts a forward walk keeps.

Each function body is walked forward, keeping the linear facts that hold at each point, over whole numbers and the lengths of std’s lists, text and maps:

Polarity decides what a condition says. A condition is read as a formula it implies: of a && b, what is known of either half; of a || b, something only where both halves are known. Its denial is read the other way round: a || b false says what is known of either half false, and a && b false says something only where both halves can be denied. Reading a && b as a under a negation would prove what does not hold.

A conversion keeps its value or stops the program (Part III A.2), and so does arithmetic: a fact about x as i64, or about 2 * v + 1, is a fact about the number, wherever the program goes on.

The walk follows the order the lowering runs things in. An assignment’s value is walked before the index it writes at, because the value is computed first (ADR-293 D2): in xs[2] = xs.pop() ?? 0 the list is shorter by the time the write happens. A call’s receiver comes before its arguments, and its effect after both.

A match arm starts with nothing known. Its pattern may bind a name that hides an outer one.

At a loop’s head, every fact about a name the body changes is forgotten, and what holds of it everywhere - never negative - is said again. A name a lambda, a task, an overlap branch or a select arm changes has no facts at all. A point keeps its 48 newest facts, so a long body costs the solver what a short one does.

The goal 0 <= i && i < xs.len() is asked of Fourier-Motzkin (ADR-270 D1); a check is dropped only where the answer is proved and its certificate passes the checker (ADR-270 D5). x.len() is a number of the proof only where the checker typed x as a std list, text, map or set: a len() a program writes for its own type may say anything.

D5 — A dropped index check lowers to proven::read and proven::write.

The checker records which indexes are a position into a Vec or an Array (not a range, not a map’s key); the emitter writes a proved one of those as

*unsafe { nikaia_std::proven::read(&xs, (i) as usize) }
unsafe { nikaia_std::proven::write(&mut xs, (i) as usize, value) }

proven is crates/unsafe/proven-index (ADR-218 D1): three functions over get_unchecked, each with a debug assertion, its README listing every unsafe and its argument, checked by scripts/check-unsafe-crates.sh like the others. nikaia-std re-exports it and stays #![forbid(unsafe_code)]. The unsafe the emitted code writes stands on the proof, which is the argument; the crate holds the one operation the proof licenses.

D6 — remove-overflow-checks:aggressive, the second name of 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 name is independent of remove-bounds-checks and part of the cache key like it. D2 holds: an overflow check that is not proved stays.

D7 — A list whose every write is seen has a bound on its values.

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 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, and 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 - Astrée’s smashing, with no fixpoint. The constants a write’s value lies between come from interval propagation over the linear facts that hold there; 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.

D8 — 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.

D9 — 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.

D5a — A compound assignment is the read, the operation and the write it means.

xs[i] += d on a list of numbers (or of bools) at a position D4 or D7 proves is lowered as the value, then the position, then one proven::read, the operation and one proven::write - the element read once, as += reads it. A slot that is not a copy, such as text, keeps its checked index, because reading it out would move it. x += d on a name of one whole-number type is recorded by the statement’s first byte and proved as x + d with what is known of x before the statement; a proved one is x = <T>::wrapping_add(x, d) (D10) (#387).

D10 — A dropped overflow check lowers to <T>::wrapping_*.

Its lowering is replaced by D19.

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.

D11 — Every level is held to the same output and the same stop.

Every program the tests run prints the same at every level of every name, and a program that stops at an index or an overflow at off stops at the same one at aggressive, with the language’s message - never with proven-index’s debug assertion. The tests that hold a level to this are compiled without -O, so that a wrong proof stops there instead of reading past the end. A level is kept only where, on the solver’s kernels, it is at or below off with LTO.

D12 — A length whose elements take space is below 2^60.

Added October 4, 2026 (#383).

let mut row = Vec[i64]()
for i in 0..<line.len() + 1 { row.push(i) }   // line.len() + 1 is proved

len() of a list, text, Bytes, map or set whose elements take at least one byte is a fact of the walk: below 2^60, the same on every target. It is read where the walk reads len(), as a callee’s promise is read (ADR-314 D3), and a tighter bound the program gives replaces it.

Why memory and not the language below. Rust promises an allocation of at most isize::MAX bytes, 2^63 - 1, the edge of an i64: that proves nothing about len() + 1. The machine promises more: no target this compiler builds for addresses more than 2^57 bytes (x86-64 with five-level paging; aarch64 2^52; wasm32 2^32). 2^60 leaves a factor of eight, and holds x.len() + 1, a.len() + b.len() and c.len() - w.len() - 1 inside an i64.

Why one number for every target. What a program means does not depend on the target (ADR-037 D1), and which checks it carries should not either: a bound per target would make wasm32 prove products that x86_64 checks. A target that addresses more than 2^60 bytes reopens this.

What it buys. With the bound, a product of two lengths still reaches 2^120 and stays checked; without it, nothing past a literal offset is proved, and those are about a quarter of the overflow checks the corpus keeps (docs/solver-workload.md §8.4).

D13 — A list whose elements take no space is bounded only by how it was built.

enum One { Only } takes no space, and neither does a tuple or a struct of such parts or an Array[T, 0]. A Vec[One] holds as many as resize(n, …) asks for in one step, without a byte of memory, so D12 is not true of it and is not read. Whether a type takes space is a structural walk, as whether it compares is (ADR-204 D1). Its length is what the walk already reads off how it was built (D4, D9): [] is 0, resize(n, …) is n, a push per counted turn adds the count, extend adds the other’s length; anything else leaves it unknown, and the check stays. A run-time limit on such a list was the other way: it would cost a check at every resize and extend of every list, to cover a list that takes no memory.

As built (#383, #444): the walk reads D12 as 0 <= len(x) <= 2^60 for every len() whose container’s elements take space, and D13’s structural walk answers *no for a type variable, a function, or a type nothing here declares. A proof states its goal inside ±2^62 where the type is wider: the solver counts in i64 and refuses on overflow, so term <= i64::MAX (negated, 2^63) was never decided, and no i64 or u64 operation had been proved. Over the repository’s .nika files, the checks left standing at aggressive went from 551 to 442 (docs/solver-workload.md §8.5).*

D14 — How hard the compiler proves and what it does with a proof are two settings.

Added October 4, 2026 (#390). It replaces D1’s levels, D3’s and D6’s names for them, and §6’s question of the default.

proving says how hard the compiler proves: a level that maps to a step budget for the solver (ADR-270), counting only its expensive steps - a case, an elimination - which costs less than reading a clock and answers the same everywhere. It reaches both clients: the claims a program writes (ADR-269) and the checks it does not write, index and overflow. remove-bounds-checks and remove-overflow-checks say only what happens to a check that was proved: on writes it without its check, off (the default) keeps it.

Why two. One switch meant both search harder and drop what was found. A program that wanted more of its defects found at build time had to take the dropped checks with it, and a program that wanted neither had no budget to set. The two buy different things: more proving buys safety, because more defects are found before the program runs (D15); dropping checks buys speed, at a risk proving alone does not carry.

Why dropping stays off by default. A proof is checked by its certificate (ADR-270 D5), but the certificate covers the solver’s arithmetic, not whether the query the walk built says what the program does. A wrong walk is a defect of the compiler, as a wrong lowering is - and where it drops a check, it turns a defect of the program that would have stopped cleanly into a read past a list’s end (get_unchecked, D5, with its debug assertion off in the profile a program is built with) or a wrong number (wrapping_*, D10). A wrong refutation is a visible error with a bypass; a wrong drop is invisible.

Why changing one does not redo the other. The proofs depend on proving and the sources; remove-*-checks only chooses what is written. A build that switches dropping on or off proves nothing again and caches nothing twice.

As built: remove-bounds-checks and remove-overflow-checks take on and off, and the walk runs at every build, D3’s shape and D4’s solver together, whatever they say. basic is no longer a word of the option: its one shape is proved at every build, and whether a level without the solver is worth offering is proving’s question (§6). The old words are refused with the word they now are.

D15 — A check nobody writes that the compiler shows fails is an error.

let third = xs[5] over a list the walk knows holds three is refused, with the value that fails, as a claim a program writes is (ADR-269 D8, NK1207); refuted-claims = "warn" builds it with the check. Why an error. The check would stop the program where the line runs; it would not rescue it. A program the compiler has shown wrong does not build, whichever kind of check showed it. Only on a refutation, never on unknown, and on ADR-269 D8’s terms: a model checked by evaluation, for values the program reaches. The walk runs at every build for this, whatever remove-*-checks says.

D16 — The walk’s answers are recorded in nikaia.proofs.

Every answer a build uses is recorded there with its evidence (ADR-270 D19-D23), the walk’s as much as a claim’s: a build is a function of the sources and the committed file, whatever the solver’s search does.

D17 — A field is a name of the walk while nothing can change it.

A path of fields from a name, t.slots, p.end, self.at, is read as a name of its own: a number at the path is one, and t.slots.len() is a length (D12) as a list binding’s is. A fact about a path holds from where it is learned until something may change the path:

A precondition (ADR-269 D5) may read a path from a parameter, and a caller proves it as it proves any other.

Scanners keep a cursor and a buffer in one value (self.at + 1 < self.c.len()), tables keep their slots in a field, and work is cut into pieces that carry their bounds: the field is where such a program keeps the numbers a check is about, and a walk that forgets them at the dot proves none of it. Copying each field into a let first is the same proof with a line per field, asked of every program.

D18 — A shift’s count is a goal of the walk, as an index is.

if dot > 28 { throw BadRow {} }
let digits = (w & keep) << (28 - dot)      // 0 <= 28 - dot < 64: no check

A shift whose count is not a literal, x << k and x >> k, asks 0 <= k < w, w the width of x’s type, as an index asks 0 <= i < len. Where the walk proves it, remove-overflow-checks:on writes the shift without its check; where it does not, the shift is checked as Part I says, and a count it shows outside is an error as D15 says.

Why. A shift by more places than its type is wide stops the program (Part I), so the count is checked at every such shift, and the checks a program writes before it - a guard on a value it read - prove it as they prove an index. Without the goal, the only way to lose the check is a wrapping_shl, which turns a wrong count into a wrong value without a word, against what the check is for; an assert does not help, because nothing reads it as the shift’s goal. Rejected: masking the count as Rust’s release build and Java do, which gives a value where the program means a stop; a switch of its own, for a goal of the same kind as +, - and *’s.

D19 — A dropped overflow check lowers to proven::add, sub and mul.

Replaces D10’s lowering, October 22, 2026.

A proved +, - or * lowers to unsafe { nikaia_std::proven::add::<T>(a, b) } (sub, mul), from proven-index, as a proved index lowers to proven::read: <T>::unchecked_add behind a debug_assert of checked_add. T stays named, so D10’s tie between the proof’s type and the emitted one holds. The operation tells the optimiser that it does not overflow, which wrapping_add does not: in 1BRC’s fast.nika that saves one instruction a row at x86-64-v3, where wrapping_add lost what the check it replaced had told the optimiser. A wrong proof stops at the assertion in every build that keeps debug assertions, D11’s tests among them, and is undefined behaviour in one that does not, as a wrong proved index already is and a proved shift already is (D18).

Rejected: keeping wrapping_* (D10). It turns a wrong proof into a wrong number rather than undefined behaviour, but the index and the shift beside it do not, so the operation was the one place that paid for a guarantee the program as a whole does not have. <T>::unchecked_add written into the program directly: the same code, but an unsafe outside the listed crates (ADR-218) and no assertion in a debug build.

D20 — A path through one element is a name of the walk too.

October 22, 2026, #781.

t.slots[at].sum, a path of fields through one element of a list that is itself a path (D17), indexed by a name, is a name of the walk as t.used is: unsafe { assume(t.slots[at].sum <= B) } bounds it, and t.slots[at].sum += v is proved from that. What is known of it holds until

A write to another field of the same element keeps it: t.slots[at].min = v cannot change t.slots[at].sum. An index that is not a name makes no path; a write through it drops what is known of every element.

An aggregation loop keeps its sums in the elements of a table, and the bound that keeps them from overflowing is about the element the row lands in: a walk that knows fields only from a name proves none of the four writes a row makes.

5. Consequences

6. What this does not decide

This site is open source. Improve this page.