--optimization=remove-bounds-checks:basic|aggressiveStatus: Superseded by ADR-306 — its D1-D5 are D1-D5 there, D6 is D11
Date: October 3, 2026
Target Version: Nikaia 0.0.373
Answers: the owner’s decision, measuring the solver’s kernels against Rust
written by hand (ADR-270 D8 step 1), that every piece of the
overhead is closed to nearly nothing, and beyond that an
--optimization=remove-bounds-checks:basic and an
--optimization=remove-bounds-checks:aggressive
Decides: ADR-269 §6’s open question for one of the
implicit checks - whether D4 applies to an index out of bounds - as an
option: yes, a proved index check is not emitted, at the level the build asks
for
Related: ADR-269 D4 (a claim the compiler proves has no
check emitted, and one meaning either way), D9-D10 (what the prover reads);
ADR-270 D5 (a check is dropped on a certificate its checker
accepts); ADR-218 (every unsafe topic a small crate of its
own); ADR-285 D1 (an index is an i64, and outside is a stop);
Part III A.2 (an index out of bounds, an overflow and a conversion that does
not fit stop the program at every build), 13.3 (build options, [build]).
Measurements: docs/solver-workload.md §8.1
xs[i] stops the program where i is outside xs (Part III A.2). The check
is a compare and a branch, which is nothing alone, but 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 checks in out[i + j] cost
34 % of the instructions - with them the Nikaia half is the Rust half’s
count, without them a third below it.
The checks the language asks for are not optional: a program that reads past
a list’s end is a defect, and the stop is how it is seen. But a check that
cannot fail is not a check, it is a cost. ADR-269 D4 already drops a
written assert the prover proves; ADR-269 §6 left open whether the checks
nobody wrote - an index, an overflow, a division - are treated the same way.
May the compiler drop an index check, when, and who decides that it tries?
| Language / tool | Its answer | Source |
|---|---|---|
| Rust | always checked; LLVM removes what it can prove 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 |
| Java HotSpot, .NET RyuJIT | range-check elimination in the JIT, for loops whose bounds it can see | from memory, not checked |
| Ada / SPARK | checked; GNATprove proves the absence of run-time errors, and pragma Suppress drops what was proved - by the programmer’s hand |
from memory, not checked |
| Dafny | an index is a proof obligation; nothing is checked at run time because everything is proved | from memory, not checked |
What transfers: SPARK’s and Dafny’s order - prove, then drop - and the
JIT’s range-check elimination for the shape that is most of the cost. What
does not: Swift’s -Ounchecked. A flag that changes a stop into undefined
behaviour changes what a program means, and Part I 1.2 lets no build option
do that.
Every check is emitted; LLVM removes what it sees. It sees the loop over a
list’s own length. It does not see out[i + j] with out resized to
x.len() + y.len(), nor a merge of two lists whose while and if say
which counter is inside.
-Ounchecked: every index without a check. Fastest; a wrong index reads
memory it does not own. Refused by Part I 1.2.
ADR-269 D4’s rule as it stands for an assert: proved means not emitted,
with no option. Every build pays the proof, and a prover that grows changes
the emitted code of every program under it, unasked.
--optimization=remove-bounds-checks:basic for one shape that needs no
solver, :aggressive for every fact the solver can use. No level drops a
check that is not proved.
| 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: the author rewrites the loop until LLVM sees it | yes | yes | slow, never wrong |
| B | yes | yes | yes | no: a flag changes meaning | memory is read past the end |
| C | no: every build proves | yes | no | yes | a wrong proof, everywhere |
| D | yes: only a build that asks proves | yes | yes: off by default | yes: meaning never changes | a wrong proof, where asked - caught by the certificate’s checker before a check is dropped |
D is chosen.
--optimization=NAME:LEVEL, and its first name.--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).
A 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. So a level is a statement about how hard the compiler tries, not about
what the program may do - and a program that stops at an index at off
stops at it at aggressive.
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.
aggressive: the solver, from the facts the 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:
let and an assignment (n = e; n += d and n = n + d rewrite every
fact about n to the new value), a range’s bounds for its binding, a
parameter’s unsigned type, a counter that starts at a literal and only
grows (never negative);if in its branches, its denial after a branch that
leaves; a while’s condition in its body and its denial after it, where
the body has no break; the left side of && and || where the right
side runs;resize(n, …),
push, insert, remove, clear. A method that is not known to keep the
length forgets it; a name handed to a call that may change it - a mut
parameter, or a callee this program does not declare - forgets it.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 same way 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; the test
a_conjunction_denied_says_nothing_of_one_half is that case.
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 name handed to a method this program
declares with a mut parameter, or to a function that is not this program’s,
loses what was known of it.
A match arm starts with nothing known. Its pattern may bind a name that
hides an outer one, and a fact about the outer i says nothing of the i an
arm binds.
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: it may change whenever they run. 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 (D5 there). 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.
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. A compound assignment (xs[i] += 1) keeps its
check for now.
Against the solver’s kernels, both halves linking the same optimised std
(solver-workload.md §8.1):
| kernel | Rust by hand, fat LTO | Nikaia off |
Nikaia aggressive |
|---|---|---|---|
| combining sparse rows | 966.2 M | 959.0 M (−0.7 %) | 955.1 M (−1.2 %) |
| scanning watch lists | 10.40 M | 10.33 M (−0.7 %) | 10.22 M (−1.8 %) |
| multiplying big integers | 1 088.1 M | 1 087.6 M (−0.0 %) | 720.4 M (−33.8 %) |
aggressive proves 22 of the 40 index sites of the three kernels; the rest
read a position out of memory (value[blocks[k]]), or index one list by a
counter bounded by another list’s length (rv[i] beside rc[i]), which no
fact relates. basic proves 3, each one LLVM proves itself, and buys nothing
measurable here.
The criterion: every program the tests run prints the same at all three
levels, and a program that stops at an index at off stops at it at
aggressive - with the language’s message, never with proven-index’s
debug assertion (tests/bounds_checks.rs, compiled without -O, so a wrong
proof would stop there instead of reading past the end). And
the_solver_kernels_lowered_against_rust_by_hand shows aggressive at or
below off on every kernel with LTO.
unsafe at a second place besides a call into
foreign code, and only where a proof stands behind it.assert (ADR-269), with
queries of its own shape: more facts, mutable counters, lengths that move.
They are queries for ADR-270 D9’s measurement too.ifs and loops in a way the
author can see in the lowered Rust; a listing like --asserts does not exist
for them yet.2 * v + 1
with v < 2000 cannot overflow a u32. Measured, they are what is left
between the watch kernel and the Rust half built without them (+0.7 % with
overflow-checks on, §8.1). The next name for D1’s option, decided with its
first measurement.--bounds, as --asserts lists claims -
with the reason each unproved index is not.x % n, a 0 <= x % n < n the walk could add where x is not negative
and n is positive, which would prove the rows kernel’s cols[r].off until the compile-time cost of aggressive is
measured over the corpus; then possibly basic.nikaia.proofs (ADR-270
D19-D23). Today the walk is deterministic and re-proves on every build;
when the solver’s search is free, its answers go into the file like every
other query’s.