Runtime checks

Every operation that could go wrong at run time (an index out of range, an integer overflow, a division by zero) is checked, and a failing check stops the program with a message and exit code 101. When the prover can show a check always passes, the check is removed. brine check --report lists the ones that remain. No flag or build profile removes a check the prover couldn’t.

The checks

Check	Example	Panic message	Removed when proven	In --report as
index bounds	xs[i], s[i]	index 6 is out of bounds for an array of length 3	yes	index bounds check
slice bounds	xs[a:b], s[a:b]	slice [1:6] is out of bounds for an array of length 3	yes	slice bounds check
division by zero	a / b	division by zero	yes	division check
remainder by zero	a % b	remainder by zero	yes	remainder check
division overflow	a / b with a the minimum and b == -1	integer overflow in division	yes	division check
overflow	a + b, a - b, a * b	integer overflow in addition (subtraction, multiplication)	yes	overflow check
overflow in compound assignment	s += x, s -= x, s *= x	integer overflow in addition (…)	no	not listed
negation and abs	-x, abs(x) with x the minimum	integer overflow in negation, integer overflow in abs	no	not listed
narrowing conversion	i32(n), u8(n)	integer conversion out of range for i32	no	not listed
pop() on an empty array	xs.pop()	pop() from an empty array	no	not listed

A few more operations can panic, but they depend on data the prover doesn’t track, so they’re always checked and never listed:

Operation	Panic message
a missing map key, m[k]	key "b" is not in the map
unwrap() on None or Err	unwrap() called on None
int(s) on text that isn’t a number	invalid integer: "abc"
min or max of an empty sequence	max() of an empty sequence
assert e	assertion failed: e

Error handling covers the alternatives that return an Option or Result instead (m.get(k), unwrap_or, checking with is_digit).

Floats have no checks: division by zero gives inf or nan, as IEEE says.

What a failing check prints

oob.br

fn main():
    let xs = [1, 2, 3]
    let i = len(args()) + 5
    print(xs[i])

brine build oob.br -o oob
./oob
echo $?

Output

panic: index 5 is out of bounds for an array of length 3
  --> oob.br:4:11
101

A panic goes to stderr: a blank line, panic: with what went wrong, and the place in your source. The program stops at once and exits with code 101 (brine run returns the same code). For an assert with a message, the message is on its own line:

Output

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

The message and place are the same in every build profile, on every backend, and inside par bodies. A check that fails in a construct running on a GPU reruns the construct on the CPU, which then panics with the usual message.

How proofs remove checks

For each check, the prover asks whether the facts it has at that point imply that the check passes. If they do, the check is removed from the generated code. Facts come from conditions, loop ranges, lengths, contracts and earlier checks; the overview lists them.

The usual way to remove a check is to state the fact it needs as a requires, so callers prove it where more is known. Here nothing is known about the parameters:

pick.br

fn pick(xs: [int], k: int) -> int:
    return xs[k]

fn window(xs: [int], lo: int, n: int) -> [int]:
    return xs[lo:lo + n]

fn ratio(a: int, b: int) -> int:
    return a / b

fn main():
    let xs = [1, 2, 3, 4]
    print(pick(xs, 2), window(xs, 1, 2), ratio(7, 2))

brine check pick.br --report

pick.br:2:12: index bounds check `xs[k]`
pick.br:5:12: slice bounds check `xs[lo:lo + n]`
pick.br:5:18: overflow check `lo + n`
pick.br:8:12: division check `a / b`
   Checked pick in 0.00s — 0 runtime checks proven unnecessary, 4 remain

With the ranges stated, all four checks go, and main proves the contracts with its constants:

pick.br

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

fn window(xs: [int], lo: int, n: int) -> [int]:
    requires 0 <= lo and 0 <= n and lo + n <= len(xs)
    return xs[lo:lo + n]

fn ratio(a: int, b: int) -> int:
    requires b > 0
    return a / b

fn main():
    let xs = [1, 2, 3, 4]
    print(pick(xs, 2), window(xs, 1, 2), ratio(7, 2))

   Checked pick in 0.00s — 4 runtime checks proven unnecessary, 0 remain

requires b > 0 also rules out the one overflowing division (the minimum divided by -1), so it removes the whole division check.

Other ways to supply a fact: an if around the code, a loop invariant, an ensures on the function that computes the value, or an assert (which is a runtime check itself, but one you place, and it can stand in for several). Fixing proof failures works through an example.

You don’t have to remove every check. A check on data the program reads (an index from a file, a sum of input values) is often exactly right, and it costs a compare and a branch that is almost never taken. Remove checks in hot loops and where a contract also documents what the function expects.

brine check –report

brine check proves without building. It prints how many checks were proven unnecessary and how many remain. For the first pick.br above, without the requires:

brine check pick.br

   Checked pick in 0.00s — 0 runtime checks proven unnecessary, 4 remain (see --report)

--report lists each remaining check before the summary, sorted by position: file:line:column: kind source``. The kinds are index bounds check, slice bounds check, overflow check, division check and remainder check. Remaining checks aren’t errors; brine check exits with 0.

With --json, each check is one JSON object, followed by the summary:

brine check pick.br --report --json

{"runtime_check":"index bounds check","location":"pick.br:2:12","code":"xs[k]"}
{"runtime_check":"slice bounds check","location":"pick.br:5:12","code":"xs[lo:lo + n]"}
{"runtime_check":"overflow check","location":"pick.br:5:18","code":"lo + n"}
{"runtime_check":"division check","location":"pick.br:8:12","code":"a / b"}
{"ok":true,"checks_proven":0,"checks_remaining":4}

Without a file, brine check checks the current project. See the brine command and JSON output.

What the report leaves out

--report lists the checks the prover tries to remove and couldn’t. Some checks are always kept, and the report doesn’t mention them:

• Overflow in compound assignments. s += x, s -= x and s *= x are always checked at run time, even when the prover could show they can’t overflow, and they’re not counted. Write s = s + x to have the check proven or listed.
• Negation and abs of an integer.
• Narrowing conversions such as i32(n) and u8(n).
• pop() on an array.
• assert, map lookups, unwrap(), int(s), and min/max of an empty sequence.

So “0 remain” means no bounds, slice, division or + - * check remains; it doesn’t mean the program can’t panic. This loop reports nothing:

total.br

fn main():
    let xs = [9223372036854775807, 1]
    var s = 0
    for i in 0..len(xs):
        s += xs[i]
    print(s)

   Checked total in 0.00s — 1 runtime check proven unnecessary, 0 remain

but the += is checked, and it overflows:

Output

panic: integer overflow in addition
  --> total.br:5:9

With s = s + xs[i] the same check is listed:

total.br:5:13: overflow check `s + xs[i]`
   Checked total in 0.00s — 1 runtime check proven unnecessary, 1 remain

Negative indexes

Brine has no negative indexes. xs[-1] compiles, is listed as a remaining check, and panics when it runs:

neg.br

fn main():
    let xs = [10, 20, 30]
    print(xs[-1])

neg.br:3:11: index bounds check `xs[-1]`
   Checked neg in 0.00s — 0 runtime checks proven unnecessary, 1 remain

Output

panic: index -1 is out of bounds for an array of length 3
  --> neg.br:3:11

Write xs[len(xs) - 1] for the last element.

Release builds keep their checks

--release changes how the code is optimized, not what it checks. The checks that remain in a dev build remain in a release build, and fail with the same message at the same place. empty.br passes an empty array to the average function from the overview:

brine run empty.br --release

Output

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

There is no option to remove them:

brine build empty.br --unchecked

error: unknown option `--unchecked`

The way to a faster program is to prove checks away, not to switch them off. See builds and backends.

Summary

• Bounds, slices, + - * overflow, division and remainder checks are removed when proven; the rest run every time.
• Compound-assignment overflow, negation, abs, conversions and pop() are always checked and not listed by --report.
• A failed check prints panic: ... and the source location to stderr and exits with 101, in every build.
• brine check --report lists what remains; --json gives one object per check.
• To remove a check, give the prover the fact it needs: contracts, fixing proof failures.