IR-0: the one place a check may be dropped

A language that removes bounds checks is making a safety claim on your behalf. This page is about where that claim is made in kola. The compiler has one verified intermediate representation, called IR-0 in the design and KIR in the source (crates/kola/src/ir.rs), and it is the only place where the compiler may decide that a safety check can be dropped. Each such decision is made once per site and written down with its reason.

An intermediate representation (IR) is the form a compiler translates your program into between reading the source and producing machine code. Most compilers have several, and each backend may make its own decisions on the way. kola keeps this one decision in one place on purpose.

The problem it solves

kola began with two hand-written implementations of the same semantics: an interpreter that walks the program directly, and a code generator that translates it to C. Both were careful and both were tested, but the difference between them was attack surface. In the first round of adversarial testing, all five memory-safety breaks were native-only: the interpreter trapped correctly, while the compiled program corrupted memory. Every one of them lived in the gap between the two implementations.

Running the same tests on both and comparing the results (a differential test) catches a lot, and kola relies on it. It has one blind spot that matters here: a program that traps never reaches the point where values are compared. If one side traps and the other silently writes past the end of a buffer, a value comparison sees nothing useful. Trap versus corruption is exactly the class of bug a systems language exists to get right.

So the fix was not more tests. It was to stop letting two pieces of code each decide which checks are safe to remove, and to make that decision once, in a checked IR that every compiled backend reads. A disagreement about a removed check then cannot be expressed, instead of being something to test for.

What KIR is

KIR is a checked syntax tree, not the lower-level graph form (SSA) that optimizers usually work on. It stays a tree so that a person can read it. What makes it checked is that every fact a backend would otherwise work out for itself is settled once, when the program is lowered into KIR, and stored in the node:

• Types: every expression carries its resolved type, so no consumer infers anything.

• Names: each variable is resolved to a numbered slot in its function's stack frame, and each call to a numbered function, so no consumer looks anything up by name.

• Arithmetic: whether an operation traps on overflow or wraps is decided per node (Add or AddW), with its width.

• Obligations: every index carries a fact that is either Checked (a run-time check stays) or Discharged with a reason, and the reason is printed.

The decisions come from crates/kola/src/prove.rs, a small difference-bound prover. It reasons about facts of the form "x minus y is at most c", which covers what bounds checks need: i < xs.len, n + 4 <= buf.len, and so on. It is not a general theorem prover, and it is fast and predictable because of that. Four kinds of obligation go through it: index and slice bounds, req preconditions at call sites, arithmetic overflow, and ens postconditions.

The backends contain no prover, no type inference and no name resolution of their own. A backend cannot disagree about whether a check was removed, because by the time it sees the site the decision is data.

What it looks like

Three functions with the same index expression and different amounts of information in scope:

pub fn sum[r](xs: &r [u64]) -> u64 !{} {
    let mut acc: u64 = 0;
    for i in 0..xs.len {
        acc = acc +% xs[i];
    }
    acc
}

pub fn at[r](src: &r [u64], n: usize) -> u64 !{}
    req n < src.len
{
    src[n]
}

pub fn any[r](s: &r [u64], k: usize) -> u64 !{} {
    s[k]
}

kola ir prints the IR with each decision. This is the place to review which checks were dropped and why:

$ kola ir slices.kl
fn sum(xs: &[u64]) -> u64
  let acc[1]: u64 = 0u64
  for i[2] in 0usize..xs.len {
    acc[1] = (acc +% xs[i] [discharged: loop guard i < xs.len])
  }
  acc

fn at(src: &[u64], n: usize) -> u64
  req (n < src.len)
  src[n] [discharged: proved n < src.len from req+guards]

fn any(s: &[u64], k: usize) -> u64
  s[k] [checked]

The generated C carries the same three decisions, and a marker comment survives into it, so you can search a build for every removed check:

$ kola build slices.kl && grep 'IR:discharged\|k_idx_at' build/slices.c
    ... xs__rp[/*IR:discharged*/i] ...
    return src__rp[/*IR:discharged*/n];
    return s__rp[k_idx_at(k, (s).len, K_SITE("\n  --> slices.kl:16"))];

k_idx_at is the runtime's checked index: it traps with the source location if k is out of range. kola report checks shows the same ledger as a report:

$ kola report checks slices.kl
fn sum
  proven   xs[i]  [loop guard i < xs.len]
fn at
  proven   src[n]  [proved n < src.len from req+guards]
fn any
  RUNTIME  s[k]

3 index site(s): 2 proven at compile time, 1 runtime

The real report also prints a header naming the root file and a footer listing what is always checked at run time. There is no heuristic here that ran three times. There is one decision per site, recorded once and read by every backend.

A wrong proof cannot hide

The reference consumer of KIR is an evaluator, ir::eval_fn, which runs the IR directly. A Checked index traps just as the native build does. A Discharged index is still verified at run time, and if the fact turns out to be false, the evaluator reports IrTrap::Ice: an internal compiler error, distinct from every trap a user program can raise.

This is the property the design rests on. The native backend removes exactly the checks that the reference evaluator verifies on every execution. A bug in the prover therefore shows up as a loud internal error when tests run through the evaluator, not as silent memory corruption in a shipped binary. A unit test, ir::tests::discharged_fact_false_is_ice, builds a function with a deliberately false Discharged fact and requires Ice, not a value and not a user trap.

One decision site

The C backend once kept its own machinery for removing checks and merely cross-checked it against the IR. That is a safety net, but two opinions still existed. The second one was deleted rather than reconciled: the C code generator contains no prover and no loop-bound bookkeeping, and the rules for when a fact stops being valid (a variable reassigned or shadowed, for example) live only in the IR lowering.

A test, codegen::tests::ir_fact_is_the_only_elision_authority, locks both directions. A Discharged fact removes the check and is marked in the C. Without one (the fact flipped to Checked, or the map emptied as for a function outside the IR) every index keeps its check. A function KIR cannot lower keeps all of its checks, which is always safe.

Everything downstream inherits it

Every compiled path reads its decisions from KIR: the C backend, the own backend (which lowers KIR further into its optimizing layer, LIR, and never emits a discharged check), the older per-architecture generators, and Cranelift. A new IR node reaches all of them, and none of them owns a proof.

The JIT inside the interpreter is the clearest case. To compile a function it needs the function to be lowerable into KIR, not proven, and KIR was already there.

The IR also records the target's pointer width (IrModule.ptr_bits), so 32-bit targets, where usize is 32 bits, are a property of the IR rather than a fiction maintained by one backend.

What it does not cover, and how you know

KIR does not lower the whole language. What matters is that every function outside it is listed, never silently absent. A function either reaches the lowered set or appears in a skipped list with a reason, and that one list feeds kola check's note, the "not analyzed" counts in kola report leaks and the [leaks] budget, and kola check --require-analyzed, which makes any skip an error:

$ kola check --require-analyzed first.kl
error[not analyzed]: `first` does not reach the verified IR: generic over data `T` is outside
  IR-v0; a monomorphization template with no instantiating call site in this file, so no
  instance body was lowered
  = note: nothing is wrong with the fn. A generic fn is lowered per INSTANCE, and this file
    instantiates none — so it is proven at its CALLERS' call sites, not here, ...

Here first was a generic function, fn first[T: data](xs: &[T]) -> Option[T]. Generics are compiled by monomorphization: a separate copy of the function is generated for each type it is used with. A file that defines a generic but never uses it has no copy to lower, so its checks are proven where it is called instead. The full diagnostic goes on to suggest the repairs.

Skipping loudly matters because a function that reached neither list would make every one of those numbers understate how much the analysis could not see, and a reviewer could not tell. That happened once: generic functions used to go to a third place that no list counted, so a per-iteration region leak in a generic function was reported by nothing. The rule that came out of it applies beyond this compiler: in a split that is meant to fail closed into two cases, a third case is an escape.

Coverage is broad today. Whole standard-library modules, including the SHA-256, X25519 and Ed25519 implementations, pass kola check --require-analyzed.

Limits

• Progress is not an obligation. Every check is about a trap. A loop that never advances is fully green in report checks and hangs at run time.

• Two executors agreeing is not proof. Once, a &mut subslice of a local array went through a node that copied it in the KIR evaluator, so a callee wrote to the copy. kola run and kola run --native agreed with each other, and only the evaluator disagreed. That is why the evaluator is tested as a separate leg rather than trusted by association.

• The prover is difference-bound, not an SMT solver (a general-purpose automated theorem prover). When a site stays RUNTIME, give it a fact: strengthen a req, add a guard, or use a fixed-size array. A [T; N] value contributes len == N for free, which is what discharges fixed-width arithmetic loops with no annotations.

The commands