Contracts

A contract is a claim the compiler must prove. requires is proven at every call, ensures at every return, invariant around every loop iteration and prove where it stands; if one can’t be proven, the program doesn’t compile. assert is the exception: it is checked at run time, and the prover treats it as true afterwards.

At a glance

Contract	Where it goes	Proven	At run time
requires e	first lines of a function body	at every call	nothing
ensures e	first lines of a function body, with requires	at every return	nothing
invariant e	first lines of a while or for body	before the first iteration and after each one	nothing
prove e	any statement in a body	where it stands	nothing
assert e	any statement in a body	not required	checked, unless proven

Only assert produces code, and only when the prover can’t show it’s always true. The others cost nothing at run time.

requires

A precondition. Every caller must prove it, and inside the function it’s a known fact:

clamp.br

fn clamp(x: int, lo: int, hi: int) -> int:
    requires lo <= hi
    ensures lo <= result <= hi
    if x < lo:
        return lo
    if x > hi:
        return hi
    return x

fn main():
    print(clamp(15, 0, 10), clamp(-3, 0, 10), clamp(4, 0, 10))

Output

10 0 4

A call the prover can’t show satisfies it is E0601. Adding print(clamp(1, 10, 0)) to main gives:

error[E0601]: cannot prove the precondition of `clamp`
  --> clamp.br:12:11
   |
12 |     print(clamp(1, 10, 0))
   |           ^^^^^^^^^^^^^^^ this call might violate `requires lo <= hi`
 2 |     requires lo <= hi
   |              -------- precondition declared here
   |
   = note: with the values used here, this is always false
   = 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

Write several requires lines, or join claims with and; they mean the same. Methods take contracts too, and can talk about fields:

range.br

struct Span:
    lo: int
    hi: int

    fn width(self) -> int:
        requires self.lo <= self.hi
        ensures result >= 0
        return self.hi - self.lo

fn main():
    let s = Span(lo=2, hi=9)
    print(s.width())
    let bad = Span(lo=5, hi=1)
    print(bad.width())

error[E0601]: cannot prove the precondition of `width`
  --> range.br:14:11
   |
14 |     print(bad.width())
   |           ^^^^^^^^^^^ this call might violate `requires self.lo <= self.hi`
 6 |         requires self.lo <= self.hi
   |                  ------------------ precondition declared here
   |
   = note: with the values used here, this is always false
   = 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

A requires moves a check from inside the function to its callers, where more is known. A caller that knows the fact (a literal, a guard, its own requires) proves it for free; one that doesn’t has to establish it. That is how a requires removes runtime checks: see the worked example.

ensures

A postcondition. result names the returned value. It’s proven at every return, and every caller gets it as a fact. Without an ensures, a caller knows nothing about what a function returns, not even something as simple as this:

half.br

fn half(n: int) -> int:
    return n / 2

fn main():
    let xs = [1, 2, 3, 4]
    print(xs[half(len(xs))])

brine check half.br --report

half.br:6:11: index bounds check `xs[half(len(xs))]`
   Checked half in 0.00s — 1 runtime check proven unnecessary, 1 remain

The prover never looks inside a called function, only at its contract. Say what the result is, and the index is proven:

half.br

fn half(n: int) -> int:
    requires n >= 0
    ensures 0 <= result <= n
    ensures n == 0 or result < n
    return n / 2

fn main():
    let xs = [1, 2, 3, 4]
    print(xs[half(len(xs))])

   Checked half in 0.00s — 2 runtime checks proven unnecessary, 0 remain

Because each function is proven against its callees’ contracts and not their bodies, changing a function’s body can never break a proof in another function, as long as its contract still holds.

An ensures that doesn’t hold on some path is E0602. Often it has found a bug:

dist.br

fn distance(a: int, b: int) -> int:
    ensures result >= 0
    if a > b:
        return a - b
    return a - b

fn main():
    print(distance(3, 5))

error[E0602]: cannot prove the postcondition of `distance`
 --> dist.br:5:5
  |
5 |     return a - b
  |     ^^^^^^^^^^^^ this might return without `result >= 0` being true
2 |     ensures result >= 0
  |             ----------- postcondition declared here
  |
  = note: known facts here: b >= a
  = note: to prove: a >= b
  = help: strengthen the function's `requires`, add a loop `invariant`, or check the claim with `assert` before returning
  = run `brine explain E0602` for more about this error
error: could not compile due to 1 error

On the second path b >= a, so the function should return b - a.

ensures works on functions that return nothing, too. With a ref parameter, it describes the variable after the call:

fill.br

fn append_zero(ref xs: [int]):
    ensures len(xs) >= 1
    xs.push(0)

fn main():
    var xs: [int] = []
    append_zero(ref xs)
    print(xs[0])

Output

0

invariant

A loop invariant is a claim that holds before every iteration. The prover checks it twice: once when the loop starts (E0603 if it can’t), and once at the end of an iteration, assuming it held at the start (E0604 if it can’t).

You need one because the prover can’t run a loop. At the top of a loop it forgets every variable the loop assigns, and the invariant is all it keeps. This binary search has no invariant:

search.br

fn index_of(xs: [int], target: int) -> int:
    ensures -1 <= result < len(xs)
    var lo = 0
    var hi = len(xs)
    while lo < hi:
        let mid = lo + (hi - lo) / 2
        if xs[mid] == target:
            return mid
        if xs[mid] < target:
            lo = mid + 1
        else:
            hi = mid
    return -1

fn main():
    print(index_of([1, 3, 5, 7, 9], 7))

search.br:6:24: overflow check `(hi - lo)`
search.br:7:12: index bounds check `xs[mid]`
   Checked search in 0.00s — 4 runtime checks proven unnecessary, 2 remain

Inside the loop, lo and hi could be anything, so mid could be out of bounds. (The ensures is still proven: return mid comes after the checked xs[mid], so mid is known to be in range there.) Say what stays true:

search.br

fn index_of(xs: [int], target: int) -> int:
    ensures -1 <= result < len(xs)
    var lo = 0
    var hi = len(xs)
    while lo < hi:
        invariant 0 <= lo <= hi <= len(xs)
        let mid = lo + (hi - lo) / 2
        if xs[mid] == target:
            return mid
        if xs[mid] < target:
            lo = mid + 1
        else:
            hi = mid
    return -1

fn main():
    print(index_of([1, 3, 5, 7, 9], 7))

   Checked search in 0.00s — 6 runtime checks proven unnecessary, 0 remain

After a while loop, the prover knows the invariant and that the condition is false.

Invariants in for loops

In for i in a..b, an invariant may mention the loop variable. It must hold with i = a when the loop starts, with i + 1 at the end of each iteration, and after the loop it holds with i = b. That’s how a count is tied to the array length:

count.br

fn count_below(xs: [int], limit: int) -> int:
    ensures 0 <= result <= len(xs)
    var count = 0
    for i in 0..len(xs):
        if xs[i] < limit:
            count += 1
    return count

fn main():
    print(count_below([5, 1, 9, 2], 4))

error[E0602]: cannot prove the postcondition of `count_below`
 --> count.br:7:5
  |
7 |     return count
  |     ^^^^^^^^^^^^ this might return without `0 <= result <= len(xs)` being true
2 |     ensures 0 <= result <= len(xs)
  |             ---------------------- postcondition declared here
  |
  = note: nothing is known here about the values involved
  = note: to prove: count >= 0 and len(xs) >= count
  = help: strengthen the function's `requires`, add a loop `invariant`, or check the claim with `assert` before returning
  = run `brine explain E0602` for more about this error
error: could not compile due to 1 error

count.br

fn count_below(xs: [int], limit: int) -> int:
    ensures 0 <= result <= len(xs)
    var count = 0
    for i in 0..len(xs):
        invariant 0 <= count <= i
        if xs[i] < limit:
            count += 1
    return count

fn main():
    print(count_below([5, 1, 9, 2], 4))

Output

2

At the end of the loop i = len(xs), so count <= len(xs).

for x in xs loops take invariants too, but have no index to mention; use for i in 0..len(xs) when the claim needs one. Stepped ranges (range(a, b, step)) and par for can’t have invariants (E0507); write a stepped loop as a while loop when it needs one.

prove

prove e asks the compiler to show e is true at that point. It generates no code. Use it to check your understanding of what the prover knows, or to document a fact for readers:

steps.br

fn main():
    let xs = [3, 1, 4, 1, 5]
    let n = len(xs)
    prove n == 5
    var i = 0
    while i < n:
        invariant 0 <= i <= n
        i += 1
    prove i == n

A claim it can’t show is E0605. k * k >= 0 is true for every integer, but it multiplies two variables, which the prover doesn’t handle:

square.br

fn main():
    let k = len(args())
    prove k * k >= 0

error[E0605]: cannot prove this claim
 --> square.br:3:11
  |
3 |     prove k * k >= 0
  |           ^^^^^^^^^^ the prover could not show this is always true
  |
  = note: nothing is known here about the values involved
  = note: to prove: len(args()) * len(args()) >= 0
  = help: add facts it can use (`requires`, `invariant`, or an `assert` before this line), or use `assert` to check it at runtime instead
  = run `brine explain E0605` for more about this error
error: could not compile due to 1 error

assert

assert e checks e when the program runs, in every build, and the prover treats e as a fact after it. It’s how you hand the prover something it can’t work out, such as a fact about input. An optional message follows a comma:

args.br

fn main():
    let a = args()
    assert len(a) >= 2, f"need 2 arguments, got {len(a)}"
    print(a[0], a[1])

The assert makes both indexes safe, so their checks are removed:

   Checked args in 0.00s — 2 runtime checks proven unnecessary, 0 remain

Run without arguments, it stops with exit code 101:

Output

panic: assertion failed: len(a) >= 2
  message: need 2 arguments, got 0
  --> args.br:3:5

An assert the prover can show is always true is removed from the program like any other proven check. One it can’t is never skipped: there is no build that leaves asserts out.

Prefer the other contracts when they can do the job. A requires makes the caller prove the fact at compile time; an assert finds out at run time. Use assert for facts that depend on input, or that the prover can’t reason about (products, floats, array contents).

What a specification may contain

requires, ensures, invariant and prove are logical claims. They may use:

• integer arithmetic, comparisons (chained too: 0 <= i < len(xs)), and and, or, not;
• len, abs, min and max;
• variables, parameters, constants, struct fields and indexing (xs[0] > 0);
• result, in ensures.

Calls to your own functions aren’t allowed (E0606), even ones without side effects:

spec.br

fn in_bounds(i: int, n: int) -> bool:
    return 0 <= i and i < n

fn get(xs: [int], i: int) -> int:
    requires in_bounds(i, len(xs))
    return xs[i]

fn main():
    print(get([1, 2, 3], 1))

error[E0606]: this is not allowed in a specification
 --> spec.br:5:14
  |
5 |     requires in_bounds(i, len(xs))
  |              ^^^^^^^^^^^^^^^^^^^^^ not allowed here
  |
  = note: `requires`, `ensures`, `invariant` and `prove` may use arithmetic, comparisons, `and`/`or`/`not`, `len`, `abs`, `min`, `max`, fields, indexing, and `result`
  = run `brine explain E0606` for more about this error
error: could not compile due to 1 error

Write the condition out: requires 0 <= i < len(xs).

Float comparisons are allowed in a specification but can’t be proven, not even with constants, because the prover reasons only about integers and booleans:

root.br

fn root(x: float) -> float:
    requires x >= 0.0
    return sqrt(x)

fn main():
    print(root(2.0))

error[E0601]: cannot prove the precondition of `root`
 --> root.br:6:11
  |
6 |     print(root(2.0))
  |           ^^^^^^^^^ this call might violate `requires x >= 0.0`
2 |     requires x >= 0.0
  |              -------- precondition declared here
  |
  = note: nothing is known here about the values involved
  = note: to prove: ?
  = 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 ? in to prove means the prover has no way to express the claim. Check float conditions with assert inside the function instead.

Placement

requires and ensures must be the first lines of a function body, and invariant the first lines of a loop body. Anywhere else is E0112:

place.br

fn f(x: int) -> int:
    let y = x + 1
    requires x > 0
    return y

fn main():
    print(f(1))

error[E0112]: `requires` is only allowed at the start of a function body
 --> place.br:3:5
  |
3 |     requires x > 0
  |     ^^^^^^^^^^^^^^ misplaced contract
  |
  = help: move it to the top of the body, before any other statement
  = run `brine explain E0112` for more about this error
error: could not compile due to 1 error

prove and assert are ordinary statements and can go anywhere a statement can, including test blocks.

Contracts and par

Contracts work the same inside par bodies. A function called from a par for, par [...] or a par reduction must have its requires proven at that call, and the loop variable’s range is a known fact there. Facts from before the par carry in. assert and prove can be used in a par body:

dot.br

fn dot(xs: [float], ys: [float]) -> float:
    requires len(xs) == len(ys)
    return par sum(xs[i] * ys[i] for i in 0..len(xs))

fn get(xs: [int], i: int) -> int:
    requires 0 <= i < len(xs)
    return xs[i]

fn main():
    print(dot([1.0, 2.0, 3.0], [4.0, 5.0, 6.0]))
    let xs = [10, 20, 30, 40]
    let shift = len(args())
    var out = [0] * 4
    par for i in 0..4:
        assert i + shift < len(xs)
        out[i] = get(xs, i + shift)
    print(out)

Output

32.0
[10, 20, 30, 40]

The requires of dot makes ys[i] safe in every iteration, and the assert proves the requires of get. A failing assert in a par body stops the program like anywhere else. With one argument, shift is 1 and the last iteration fails:

Output

32.0

panic: assertion failed: i + shift < len(xs)
  --> dot.br:15:9

A check that fails in a construct running on a GPU reruns it on the CPU, which panics with the same message (see GPUs).

par for can’t have an invariant: invariants describe the state between iterations, and parallel iterations have no order.

parinv.br

fn main():
    var out = [0] * 8
    par for i in 0..8:
        invariant 0 <= i <= 8
        out[i] = i * i
    print(out)

error[E0507]: `par for` loops can't have invariants
 --> parinv.br:4:19
  |
4 |         invariant 0 <= i <= 8
  |                   ^^^^^^^^^^^ remove this
  = run `brine explain E0507` for more about this error
error: could not compile due to 1 error

Rules

• requires and ensures go first in a function body, invariant first in a loop body (E0112).
• requires is proven at every call (E0601), ensures at every return (E0602), an invariant on loop entry (E0603) and after each iteration (E0604), prove where it stands (E0605).
• A caller knows a function’s ensures, never its body. A loop keeps only its invariant about the variables it assigns.
• Specifications use integer arithmetic, comparisons, and/or/not, len, abs, min, max, fields, indexing, constants and result; no calls (E0606). Float claims can’t be proven.
• assert is checked at run time in every build and is a fact afterwards.
• An unproven contract is always an error. There’s no mode that turns it into a runtime check.

See also: proofs overview, fixing proof failures, runtime checks, error codes.