Bounds-check elimination

Every array and container index in Axle is memory-safe: reading a[i] past the end of a traps instead of corrupting memory. That safety has a cost — a comparison against the length on every access — and for a hot loop that comparison can dominate the work.

The compiler removes that check whenever it can prove the index is already in range, and keeps it otherwise. The proof is conservative by construction: the analysis only ever upgrades an access from “checked” to “unchecked”, and it only does so when a chain of facts it has established forces 0 ≤ index < length. If it cannot prove that, the check stays. A wrong elision would be an out-of-bounds read, so doubt always resolves to keeping the check.

What it proves, from simplest to hardest

A constant or counted loop

The classic case needs no cleverness: a for … of loop whose counter ranges below the length.

fn main() : i32 {
    let a : i32[5] = [10, 20, 30, 40, 50];
    let total : i32 = 0;
    for (i of 0..a.length) {
        total = total + a[i];   // i < a.length by construction — no check
    }
    return total;
}

The loop bound is the length, so i is in range on every iteration and the per-access check disappears.

A chain of comparisons — reasoning between variables

The interesting case is when the bound is not a constant but another variable, related to the length by a guard:

fn first_n(a : i32[5], n : i64) : i32 {
    let total : i32 = 0;
    for (i of 0..n) {                 // i is not tied to a.length here
        if (i < a.length) {           // fact: i < a.length
            total = total + a[i];     // guarded — the access needs no check
        }
    }
    return total;
}

The loop counter itself carries no relation to a.length, so the trip count alone proves nothing. What discharges the check is the guard that dominates the access: on the path where a[i] is evaluated, i < a.length is a fact the compiler already holds, and a second test of the same predicate is dead. The emitted IR for this function contains no call to axle_panic_oob.

The condition to keep in mind is where the fact is established. A bound that reaches the function as a parameter — if (n <= a.length) around the loop, with n supplied by the caller — is not the same situation: the relation has to survive the call boundary, which is the subject of the next section.

Across a function call

The chain can cross a call boundary. When every call site of a function establishes the bound its body needs, the body may assume it at entry:

use std::collections::arraylist::ArrayList;

fn sum_first(h : ArrayList<i64>, n : i32) : i64 {
    let total : i64 = 0;
    let i : i32 = 0;
    while (i < n) {
        total = total + (h.get(i) ?? 0);  // bound comes from the caller
        i = i + 1;
    }
    return total;
}

fn main() : i32 {
    let v : ArrayList<i64> = new ArrayList<i64>();
    v.add(10); v.add(20); v.add(30);
    let n : i32 = 2;
    if (n <= v.size()) {                  // the caller guarantees n ≤ v.size()
        return sum_first(v, n) as i32;    // so the body's h.get(i) needs no box
    }
    return 0;
}

The ?? 0 fallback and its nullable result — the checked-access machinery — fold away inside sum_first, because the compiler proved at the call site that n is within v’s size and carried that fact into the callee. If a single call site cannot establish it (passes an unrelated value, or an unguarded one), the bound is dropped for the whole function — again, fail-closed.

From how a container was built

The bound can also come from the container’s own history. A freshly constructed container starts empty, and each append grows its size by one — facts the compiler tracks. So an index it can relate to that concrete size is provably in range even without a guard:

use std::collections::ArrayList;

fn build() : ArrayList<i64> {
    let v : ArrayList<i64> = new ArrayList<i64>();
    v.add(10); v.add(20); v.add(30);   // the compiler knows v.size() ≥ 3
    return v;
}

This rests on one always-true fact the compiler injects for every container — a size is never negative — which lets size == 0 of a fresh container and size ≥ 3 after three appends compose into the bounds a later access needs.

A container built up inside a loop

The hardest shape of the previous case is a container grown inside the same loop that indexes it, where the index tracks the growing size:

use std::collections::arraylist::ArrayList;

fn build_sum(n : i32) : i64 ! IndexOutOfBoundsException {
    let buf : ArrayList<i64> = new ArrayList<i64>();
    let size : i32 = 0;
    let acc : i64 = 0;
    while (size < n) {
        if (size < buf.size()) {
            buf.set(size, 7);                 // in range: size < buf.size()
        } else {
            buf.add(7);                       // grows buf.size() by one
        }
        acc = acc + (buf.get(size) ?? 0);     // size ≤ buf.size() every iteration
        size = size + 1;
    }
    return acc;
}

At the if, one branch writes an existing slot and the other appends — and after they rejoin, size ≤ buf.size() holds on both paths. The compiler carries that relationship around the loop, so the following buf.set(size, …) and buf.get(size) are provably in range: the bounds check, the nullable ?? 0 box, and the internal out-of-range branch all fold away, leaving a bare store and load — even though there is no single dominating size < buf.size() guard written above them. Keeping a loop-carried relationship like this alive across the merge point is what lets a container you fill and read in one pass cost nothing for its safety.

Inside the standard library’s containers

HashMap, HashSet and friends index their internal storage with expressions like slot = hash & (capacity − 1). That an internal slot is in range rests on an invariant spanning the constructor, the grow path and every accessor (mask == capacity − 1, storage.length == capacity, capacity ≥ 1). The compiler infers and verifies such a class invariant — it keeps only the relations every method re-establishes at every exit — and uses it to remove the internal probe-loop checks. This is why the built-in containers pay for their safety only where the compiler could not discharge it.

The same machinery works on a container you write. A class with a backing array data and a length field len, whose methods maintain len ≤ data.length, gets its self.data[i] access under a guard i < self.len elided by exactly the inferred invariant — no annotation, and nothing special about it being in the standard library. A hand-rolled RingBuffer or Matrix with the same shape drops the same checks.

One proof, three costs

The check itself is often the smallest thing an elision removes. Look again at what a container accessor costs:

use std::collections::ArrayList;

fn read(h : ArrayList<i64>, i : i32, total : i64) : i64 {
    return total + (h.get(i) ?? 0);
}

get returns null when the index is out of range, so the callee builds a nullable box to carry “no value” and the caller unwraps it with ?? 0. A set that throws instead pays an exception poll after the call. And the accessor still runs its own bounds check inside.

All of that machinery hangs off one branch — the fault guard if (index < 0 || index >= self.len). Prove that guard false at the call site and the whole branch is dead, so the box, the unwrapping, the throwing status, the poll and the internal trap disappear together. “Elide null”, “elide exception” and “elide bounds” are not three optimisations; they are one proof consumed once.

Nothing about this is specific to the standard library’s containers. The rule is that a fault lives on a branch guarded by a relation — so a Matrix.at(r, c) that returns null when r >= self.rows, or a RingBuffer.peek() that returns null when self.count == 0, is treated identically. The compiler never asks what the type is called.

What it looks like on a real program

Take a Dijkstra shortest-path implementation — a binary heap, a CSR adjacency structure, an ArrayList of distances, the usual shape. Compiled unoptimised, the relational proofs remove 40 nullable boxes and 13 exception polls from that one file: every one of them a ?? 0 unwrap or a post-call exception check that the program was paying for an out-of-range case the caller had already ruled out.

The bounds traps that remain in it are instructive, because they are the honest ones. dist[node] where node was read out of the frontier array cannot be proven — nothing states the range of a value that came out of an i32[]. The CSR walk needs a fact about the contents of the offsets array. Those checks stay, and should.

What it costs to compile. The expensive whole-program stage only runs where a function offers it something to prove. On that same program it takes the analysis from 3.7 ms to 38.5 ms, and the whole compile from 0.11 s to 0.14 s. A program that proposes nothing to prove pays nothing measurable.

The point is not a headline ratio. It is that the elisions are the ones you could have argued for yourself, and the checks that remain are the ones you could not.

Where it stops — honestly

Some bounds a local, per-function-and-summary analysis cannot recover, and there the check stays:

Data-dependent indices. dist[adj[k]] — an index read from another array — has no static relationship to the target’s length. The value could be anything the data holds.
Non-local structural invariants. A prefix-sum array where offsets[i] ≤ total for the whole structure, or a bit-mask wider than the array it indexes, needs a whole-program data invariant the compiler does not track.
A bound that outruns the proof chain. The analysis composes a bounded number of steps; a relationship that needs a longer chain is left unproven rather than guessed.

In every one of these cases the runtime check remains and your program stays safe. The point of this page is not that Axle removes all bounds checks — it is that it removes the ones it can prove redundant, and tells you plainly which ones it cannot.