# Proofs overview

> What Brine's built-in prover does, the promise that rules can't be broken, how proofs remove runtime checks, and what the prover can and can't show.

Source: https://docs.brinelang.org/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

[Section titled “The promise”](#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](/reference/errors/#e0601)-[E0605](/reference/errors/#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

[Section titled “A worked example”](#a-worked-example)

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

stats.br

```brine
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:

```sh
brine check stats.br --report
```

```text
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:

Output

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

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

stats.br

```brine
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))
```

```text
   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](/proofs/runtime-checks/#what-the-report-leaves-out).)

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:

avg.br

```brine
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))
```

```text
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:

avg.br

```brine
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))
```

```sh
brine run avg.br -- 3 4 8
```

Output

```text
5
```

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

[Section titled “How proofs remove checks”](#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 `invariant`s, `assert`s and `prove`s;
* 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

[Section titled “What it can prove”](#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

[Section titled “What it can’t prove”](#what-it-cant-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](/proofs/fixing-proof-failures/) shows how.

## Next

[Section titled “Next”](#next)

* [Contracts](/proofs/contracts/): `requires`, `ensures`, `invariant`, `prove` and `assert` in detail.
* [Runtime checks](/proofs/runtime-checks/): every check, what it prints, and `brine check --report`.
* [Fixing proof failures](/proofs/fixing-proof-failures/): reading E0601-E0606 and the usual fixes.
* [Design](/reference/design/): why the rules are what they are.