Proofs

Fixing proof failures

A proof failure means the prover couldn’t show a claim from the facts it had at that point. The error lists those facts and the exact goal; the fix is to supply the missing fact where it’s true (a guard, a requires, an ensures, an invariant, or an assert), or to fix the bug the error found. Never weaken or delete the contract just to make the error go away.

Reading a proof failure

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

fn pick(xs: [int], k: int) -> int:
    if k < 5:
        return get(xs, k)
    return 0

fn main():
    print(pick([10, 20, 30], 1))

error[E0601]: cannot prove the precondition of `get`
 --> pick.br:7:16
  |
7 |         return get(xs, k)
  |                ^^^^^^^^^^ this call might violate `requires 0 <= i < len(xs)`
2 |     requires 0 <= i < len(xs)
  |              ---------------- precondition declared here
  |
  = note: known facts here: 0 >= k - 4
  = note: to prove: k >= 0 and len(xs) > k
  = 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

Read it from the top:

The code and the place. E0601 at pick.br:7:16: the call to get.
The claim. The - underline points at the contract that had to hold, here requires 0 <= i < len(xs) on line 2.
known facts here: the facts the prover had about the values in the goal. 0 >= k - 4 is k < 5 from the if, rewritten (see below).
to prove: the goal, with the call’s arguments put in for the parameters: i became k. The difference between the facts and the goal is what’s missing. Here it’s k >= 0 and k < len(xs).
help: the general ways out.

Facts and goals are printed in a normal form, with every term moved to one side and integer bounds tightened, so they may not look like your source:

Printed	Means
`0 >= k - 4`	`k <= 4`, that is `k < 5`
`len(xs) > k`	`k < len(xs)`
`hi >= lo + 2`	`lo + 2 <= hi`
`a, b`	two separate facts
`len(args())`, `[...][0]`	a value without a name: the length of a call’s result, an element of an array
`?`	a value the prover can’t express, such as a float comparison

Two other notes replace the list of facts:

nothing is known here about the values involved: the prover had no facts about these variables. Common causes: a parameter with no requires, a call result with no ensures, or a variable a loop changed.
with the values used here, this is always false: the claim can never hold at this point, for example clamp(1, 10, 0) with requires lo <= hi. This is a bug in the calling code.

Choosing a fix

Situation	Fix
the claim is false on some path	fix the code
the caller should never be in this state	`requires` on the caller
the state is possible and has a sensible answer	an `if` guard
the fact depends on input, or the prover can’t show it	`assert`
a value comes from a call	`ensures` on the callee
a value was changed by a loop	`invariant` on the loop
the fact needs a product, a variable divisor or a float	`assert`, or restructure

All three fixes for pick above compile. Which is right depends on what pick should do when k is out of range.

Guard the code

If an out-of-range k is a normal case, say what to do with it. Inside the if, the condition is a fact:

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

fn pick(xs: [int], k: int) -> int:
    if 0 <= k < len(xs):
        return get(xs, k)
    return 0

fn main():
    print(pick([10, 20, 30], 1))

Pass it to the callers

If calling pick with a bad k is a mistake, make that the caller’s obligation. The fact is then known inside pick, and every caller must prove it (here main does, with constants):

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

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

fn main():
    print(pick([10, 20, 30], 1))

This is usually the best fix: the rule is checked at compile time, and it documents what pick needs.

Check it at run time

If the value comes from outside and there’s no sensible fallback, assert it. The program stops with a clear message if it’s false, and the prover knows it’s true after the line:

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

fn pick(xs: [int], k: int) -> int:
    assert 0 <= k < len(xs)
    return get(xs, k)

fn main():
    print(pick([10, 20, 30], 1))

An assert is a runtime check you wrote on purpose, in one place, instead of one the compiler would otherwise need to insert.

The goal is the missing requires

When to prove: names only parameters, the function needs a requires. This clamp has its precondition missing:

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

fn main():
    print(clamp(5, 0, 10))

error[E0602]: cannot prove the postcondition of `clamp`
 --> clamp.br:4:9
  |
4 |         return lo
  |         ^^^^^^^^^ this might return without `lo <= result <= hi` being true
2 |     ensures lo <= result <= hi
  |             ------------------ postcondition declared here
  |
  = note: known facts here: lo > x
  = note: to prove: hi >= lo
  = 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[E0602]: cannot prove the postcondition of `clamp`
 --> clamp.br:6:9
  |
6 |         return hi
  |         ^^^^^^^^^ this might return without `lo <= result <= hi` being true
2 |     ensures lo <= result <= hi
  |             ------------------ postcondition declared here
  |
  = note: known facts here: x >= lo, x > hi
  = note: to prove: hi >= lo
  = 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 2 errors

E0602 is reported once for each return it can’t prove. Both goals are hi >= lo, which no code in clamp can make true; add requires lo <= hi.

When the facts contradict the goal instead (the facts say b >= a and the goal is a >= b), the code is wrong on that path. See the distance example in contracts.

A value from a call

The prover doesn’t look inside called functions. A result is unknown except for the callee’s ensures. Here xs[k] keeps its bounds check, because nothing says what wrap returns:

fn wrap(i: int, n: int) -> int:
    requires n > 0
    return i % n

fn main():
    let xs = [10, 20, 30]
    let k = wrap(7, len(xs))
    print(xs[k])

wrap.br:8:11: index bounds check `xs[k]`
   Checked wrap in 0.00s — 1 runtime check proven unnecessary, 1 remain

Add the ensures. Now the prover has to show it inside wrap, and it can’t, because % by a variable is outside its arithmetic:

fn wrap(i: int, n: int) -> int:
    requires n > 0
    ensures 0 <= result < n
    return i % n

fn main():
    let xs = [10, 20, 30]
    let k = wrap(7, len(xs))
    print(xs[k])

error[E0602]: cannot prove the postcondition of `wrap`
 --> wrap.br:4:5
  |
4 |     return i % n
  |     ^^^^^^^^^^^^ this might return without `0 <= result < n` being true
3 |     ensures 0 <= result < n
  |             --------------- postcondition declared here
  |
  = note: known facts here: n > 0, n != 0
  = note: to prove: i % n >= 0 and n > i % n
  = 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

The claim is true (Brine’s % takes the sign of the right side), so assert it. The assert runs once per call, and in exchange every caller knows the result is a valid index:

fn wrap(i: int, n: int) -> int:
    requires n > 0
    ensures 0 <= result < n
    let r = i % n
    assert 0 <= r < n
    return r

fn main():
    let xs = [10, 20, 30]
    let k = wrap(7, len(xs))
    print(xs[k])

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

A value changed by a loop

At the top of a loop, the prover forgets everything about the variables the loop assigns, and it keeps only the loop’s invariants. After the loop, the same is true. xs starts with one element and the loop only adds more, but after the loop that’s forgotten:

fn first(xs: [int]) -> int:
    requires len(xs) > 0
    return xs[0]

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

error[E0601]: cannot prove the precondition of `first`
 --> first.br:9:11
  |
9 |     print(first(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

State what the loop keeps true:

fn first(xs: [int]) -> int:
    requires len(xs) > 0
    return xs[0]

fn main():
    var xs = [0]
    for a in args():
        invariant len(xs) >= 1
        xs.push(int(a))
    print(first(xs))

The other option is to check after the loop, which suits values that really can be anything, like the arguments in the overview example.

E0603: invariant false on entry

An invariant must hold before the first iteration. For for i in a..b, it’s checked with i = a:

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

error[E0603]: loop invariant might not hold when the loop starts
 --> count.br:5:19
  |
5 |         invariant 0 <= count < i
  |                   ^^^^^^^^^^^^^^ might be false before the first iteration
  |
  = note: with the values used here, this is always false
  = help: establish it before the loop, e.g. by initializing variables so the claim holds
  = run `brine explain E0603` for more about this error
error: could not compile due to 1 error

With count = 0 and i = 0, count < i is false. Invariants are usually <= where the loop variable is involved: 0 <= count <= i.

E0604: invariant not preserved

The prover assumes the invariant at the start of an iteration and must show it again at the end. This in-place reverse has an invariant that is false after the last swap, and also before the first one when the array is empty:

fn reverse(ref xs: [int]):
    var lo = 0
    var hi = len(xs) - 1
    while lo < hi:
        invariant 0 <= lo <= hi < len(xs)
        let t = xs[lo]
        xs[lo] = xs[hi]
        xs[hi] = t
        lo += 1
        hi -= 1

fn main():
    var xs = [1, 2, 3, 4, 5]
    reverse(ref xs)
    print(xs)

error[E0603]: loop invariant might not hold when the loop starts
 --> reverse.br:5:19
  |
5 |         invariant 0 <= lo <= hi < len(xs)
  |                   ^^^^^^^^^^^^^^^^^^^^^^^ might be false before the first iteration
  |
  = note: nothing is known here about the values involved
  = note: to prove: len(xs) > 0
  = help: establish it before the loop, e.g. by initializing variables so the claim holds
  = run `brine explain E0603` for more about this error
error[E0604]: loop invariant might not be preserved by the loop body
  --> reverse.br:5:19
   |
 5 |         invariant 0 <= lo <= hi < len(xs)
   |                   ^^^^^^^^^^^^^^^^^^^^^^^ might be false after an iteration
10 |         hi -= 1
   |         ------- at the end of this iteration
   |
   = note: known facts here: lo >= 0 and hi >= lo and len(xs) > hi, hi > lo, lo >= 0 and len(xs) > lo, hi >= 0 and len(xs) > hi
   = note: to prove: lo >= -1 and hi >= lo + 2 and len(xs) >= hi
   = help: make sure every path through the loop body re-establishes the invariant
   = run `brine explain E0604` for more about this error
error: could not compile due to 2 errors

In E0604, lo and hi in the facts and the goal are their values at the start of the iteration. The goal is the invariant with the end-of-iteration values put in: lo + 1 <= hi - 1 became hi >= lo + 2. The facts only give hi > lo, so when hi == lo + 1 the pointers cross and lo <= hi breaks. The - label shows the end of the iteration it checked.

The invariant only needs what the body uses: lo is a valid index from below, hi from above. Dropping the middle comparison fixes both errors:

fn reverse(ref xs: [int]):
    var lo = 0
    var hi = len(xs) - 1
    while lo < hi:
        invariant 0 <= lo and hi < len(xs)
        let t = xs[lo]
        xs[lo] = xs[hi]
        xs[hi] = t
        lo += 1
        hi -= 1

fn main():
    var xs = [1, 2, 3, 4, 5]
    reverse(ref xs)
    print(xs)

   Checked reverse in 0.00s — 5 runtime checks proven unnecessary, 0 remain

The loop condition lo < hi supplies the rest. An invariant that’s too weak isn’t an error: with only invariant 0 <= lo, this compiles and the bounds checks on xs[lo] and xs[hi] stay.

When E0604 is about a variable the invariant doesn’t bound, the usual fix is to add the bound (0 <= i <= n): the prover knows nothing else about variables the loop changes.

E0605: a claim it can’t prove

prove has no runtime fallback. If the prover can’t show the claim, either give it the facts (as for the other errors) or use assert if a runtime check is acceptable. The most common cause is arithmetic outside what it handles: products of two variables, and / or % by a variable. The same limit shows up in other codes:

fn area(w: int, h: int) -> int:
    requires w >= 0 and h >= 0
    ensures result >= 0
    return w * h

fn main():
    print(area(3, 4))

error[E0602]: cannot prove the postcondition of `area`
 --> area.br:4:5
  |
4 |     return w * h
  |     ^^^^^^^^^^^^ this might return without `result >= 0` being true
3 |     ensures result >= 0
  |             ----------- postcondition declared here
  |
  = note: nothing is known here about the values involved
  = note: to prove: w * h >= 0
  = 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

fn area(w: int, h: int) -> int:
    requires w >= 0 and h >= 0
    ensures result >= 0
    let a = w * h
    assert a >= 0
    return a

fn main():
    print(area(3, 4))

Products by a constant (2 * i, 3 * n + 1) are fine.

E0606: a call in a specification

Specifications can’t call your functions. Write out what the function computes, using arithmetic, comparisons, len, abs, min, max, fields and indexing:

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

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

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

If the condition can’t be written that way (it loops over an array, say), check it with assert in the function.

Floats

The prover reasons only about integers and booleans. A float claim in a contract can never be proven (to prove: ?), so it’s always an error. Check float conditions with assert:

fn root(x: float) -> float:
    assert x >= 0.0, "root of a negative number"
    return sqrt(x)

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

1.4142135623730951

Removing a runtime check

A remaining runtime check is not an error, but you remove it the same way: find the missing fact and supply it. Start from brine check --report:

fn pair_sums(xs: [int]) -> [int]:
    var out: [int] = []
    var i = 0
    while i + 1 < len(xs):
        out.push(xs[i] + xs[i + 1])
        i += 2
    return out

fn main():
    print(pair_sums([1, 2, 3, 4, 5, 6]))

pairs.br:4:11: overflow check `i + 1`
pairs.br:5:18: index bounds check `xs[i]`
pairs.br:5:18: overflow check `xs[i] + xs[i + 1]`
   Checked pairs in 0.00s — 2 runtime checks proven unnecessary, 3 remain

xs[i + 1] is already proven by the loop condition. xs[i] isn’t, because the loop changes i and nothing says it stays non-negative. Add that as an invariant:

    while i + 1 < len(xs):
        invariant i >= 0

pairs.br:4:11: overflow check `i + 1`
pairs.br:6:18: overflow check `xs[i] + xs[i + 1]`
   Checked pairs in 0.00s — 3 runtime checks proven unnecessary, 2 remain

i + 1 in the condition could overflow if i were the largest integer. The prover doesn’t bound len(xs), so it can’t rule that out. Subtract instead, since len(xs) - 1 can’t overflow:

fn pair_sums(xs: [int]) -> [int]:
    var out: [int] = []
    var i = 0
    while i < len(xs) - 1:
        invariant i >= 0
        out.push(xs[i] + xs[i + 1])
        i += 2
    return out

fn main():
    print(pair_sums([1, 2, 3, 4, 5, 6]))

pairs.br:6:18: overflow check `xs[i] + xs[i + 1]`
   Checked pairs in 0.00s — 4 runtime checks proven unnecessary, 1 remain

The last check adds two elements of the array. Their values are input, so the check is right to stay.

Patterns that help the prover:

Loop over for i in 0..len(xs) when you index xs. The range gives 0 <= i < len(xs) for free. (for i, x in enumerate(xs) doesn’t: xs[i] there keeps its check.)
Compare against len(xs) - k rather than i + k < len(xs).
Write lo + (hi - lo) / 2, and give both pointers bounds in an invariant.
Use s = s + x instead of s += x when you want an overflow check proven or reported; compound assignments are always checked and never listed (see runtime checks).
Assigning an element (xs[j] = v) makes the prover forget the array’s contents, though not its length.

A checklist for agents

Run brine check (or brine check --json) and take the first error.
Read to prove: against known facts here:. The missing piece is the difference.
If the note says always false, or the facts contradict the goal, the code is wrong. Fix the code, not the contract.
If the goal names only the current function’s parameters, add a requires, then fix the callers it breaks.
If the goal names a call’s result, add an ensures to that function.
If the goal names a variable a loop changes, add or strengthen an invariant with its bounds; check E0603 (entry) and E0604 (preserved) separately.
If the goal needs a product, a variable divisor, a float or array contents, use an assert where the fact is cheapest to check.
Never delete or weaken a contract to get past the error, and never replace a requires with an assert unless the value really comes from input.
Re-run brine check --report and confirm the checks you meant to remove are gone.