Proofs

Proofs overview

Brine’s compiler proves things about your program before it runs. Claims you write (requires, ensures, invariant, prove) must be proven, or the program doesn’t compile. The language’s own safety rules (array bounds, overflow, division by zero) are proven where possible and checked at run time everywhere else, and nothing turns those checks off.

The promise

Every rule in Brine is enforced one of two ways: by a proof at compile time, or by a check at run time that stops the program with a clear message. There is no third way. There is no unsafe, no flag that skips checks, and no build profile without them.

Rule	Who writes it	When the prover can’t show it
`requires`, `ensures`, `invariant`, `prove`	you	compile error (E0601-E0605)
array and string bounds, slices, overflow, division by zero, narrowing conversions, `pop()` on an empty array	the language	the check stays and runs every time
`assert`	you	checked at run time, and a known fact afterwards

A rule that could be switched off could be broken, and then nobody reading the code could trust it. So the compiler’s job is to prove checks away; you can’t switch them off. If you want a check gone, give the prover the fact it needs.

The same reasoning is why an unproven contract is an error and never falls back to a runtime check: a requires that sometimes runs and sometimes doesn’t would be a rule that can be broken. When a runtime check is what you want, write assert.

A worked example

This program has two functions that fail on an empty array:

fn average(xs: [int]) -> int:
    var total = 0
    for x in xs:
        total += x
    return total / len(xs)

fn middle(xs: [int]) -> int:
    return xs[len(xs) / 2]

fn main():
    let xs = [4, 8, 15, 16, 23, 42]
    print(average(xs), middle(xs))

It compiles. brine check proves what it can and says how many checks are left:

brine check stats.br --report

stats.br:5:12: division check `total / len(xs)`
stats.br:8:12: index bounds check `xs[len(xs) / 2]`
   Checked stats in 0.00s — 1 runtime check proven unnecessary, 2 remain

Nothing says xs isn’t empty, so the division and the index stay checked. The one it removed is len(xs) / 2, a division by a constant. If an empty array does reach average (here from a program called empty.br), the check stops the program:

panic: division by zero
  --> empty.br:5:12

To remove both checks, state the rule the functions depend on:

fn average(xs: [int]) -> int:
    requires len(xs) > 0
    var total = 0
    for x in xs:
        total += x
    return total / len(xs)

fn middle(xs: [int]) -> int:
    requires len(xs) > 0
    return xs[len(xs) / 2]

fn main():
    let xs = [4, 8, 15, 16, 23, 42]
    print(average(xs), middle(xs))

   Checked stats in 0.00s — 3 runtime checks proven unnecessary, 0 remain

Inside the functions, len(xs) > 0 is now a known fact, so the division can’t be by zero and len(xs) / 2 is a valid index. (The total += x overflow check stays: it depends on the values in the array. --report doesn’t list checks in compound assignments; see runtime checks.)

The obligation moved to the callers. main passes a six-element literal, so the call is proven. A caller that can’t show the array is non-empty doesn’t compile:

fn average(xs: [int]) -> int:
    requires len(xs) > 0
    var total = 0
    for x in xs:
        total += x
    return total / len(xs)

fn main():
    var xs: [int] = []
    for a in args():
        xs.push(int(a))
    print(average(xs))

error[E0601]: cannot prove the precondition of `average`
  --> avg.br:12:11
   |
12 |     print(average(xs))
   |           ^^^^^^^^^^^ this call might violate `requires len(xs) > 0`
 2 |     requires len(xs) > 0
   |              ----------- precondition declared here
   |
   = note: nothing is known here about the values involved
   = note: to prove: len(xs) > 0
   = help: add an `assert` before the call to check it at runtime, or a `requires` to this function so its callers must prove it
   = run `brine explain E0601` for more about this error
error: could not compile due to 1 error

The error is right: with no arguments, xs is empty. Handle that case, and the call is proven:

fn average(xs: [int]) -> int:
    requires len(xs) > 0
    var total = 0
    for x in xs:
        total += x
    return total / len(xs)

fn main():
    var xs: [int] = []
    for a in args():
        xs.push(int(a))
    if len(xs) == 0:
        eprint("usage: avg <numbers>")
        return
    print(average(xs))

brine run avg.br -- 3 4 8

The bug that used to be a crash on empty input is now a compile error until the empty case is handled.

How proofs remove checks

The prover goes through each function on its own, path by path, and keeps a list of facts that are true at each point. Facts come from:

requires clauses of the function (true on entry);
if, elif, while and match guard conditions (true inside the branch, false after it);
for i in a..b (inside the loop, a <= i < b);
let and assignments of integer expressions (let mid = lo + (hi - lo) / 2);
array and string lengths: literals ([1, 2, 3] has length 3), [x] * n, push and pop, slices;
the ensures of every function called;
loop invariants, asserts and proves;
every check that ran before (after xs[i], 0 <= i < len(xs) is known).

At each check, the prover asks whether the facts imply that the check passes. If they do, the check is deleted from the generated code; if not, it stays. Either way, the condition is a fact afterwards, because the program can only continue if it held.

The removal happens in every build profile (dev, --release, --debug) and on every backend, so a proof is also a speed-up: a loop like for i in 0..len(xs): total = total + xs[i] runs with no bounds check at all.

What it can prove

The prover is a decision procedure for linear integer arithmetic with booleans. It handles:

+ and -, multiplication by a constant, and / and % by a constant (2 * (n / 2) <= n and 0 <= n % 8 < 8 are proven for n >= 0);
comparisons, including chains (0 <= i < len(xs)), and and, or, not;
len, abs, min and max;
struct fields (requires self.lo <= self.hi);
elements of arrays whose contents it knows (a literal, before it’s changed).

It reasons about integers as exact mathematical numbers. That’s sound because overflow is itself checked: a program that keeps running has exact values.

What it can’t prove

Some true claims are out of its reach. When the prover can’t show something it says so; it never guesses. It can’t prove:

Products of variables. i * j, w * h >= 0, k * k >= 0.
Division or remainder by a variable. n / m <= n and n % m < m.
Anything about floats. A contract that compares floats can’t be proven, even requires x >= 0.0 called with 2.0. Write those as assert.
Array contents it hasn’t seen. The elements of a parameter, or of any array after one of its elements is assigned, are unknown values.
What a call returns, beyond the callee’s ensures. Without an ensures, a function’s result is an unknown value.
What a loop changes, beyond its invariant. After a loop, every variable it assigns is unknown except for what the invariant says.

It is sound: it never accepts a false claim. It is incomplete: when it can’t prove a true claim, you add the missing fact with a requires, an ensures, an invariant or an assert, or restructure the code so the fact is visible. Fixing proof failures shows how.

Contracts: requires, ensures, invariant, prove and assert in detail.
Runtime checks: every check, what it prints, and brine check --report.
Fixing proof failures: reading E0601-E0606 and the usual fixes.
Design: why the rules are what they are.