# Runtime checks > Every runtime check Brine inserts (bounds, slices, overflow, division, conversions, pop), what a failing check prints, which checks proofs remove, how to list the rest with brine check --report, and why release builds keep them. Source: https://docs.brinelang.org/proofs/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 [Section titled “The checks”](#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](/language/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 [Section titled “What a failing check prints”](#what-a-failing-check-prints) oob.br ```brine fn main(): let xs = [1, 2, 3] let i = len(args()) + 5 print(xs[i]) ``` ```sh brine build oob.br -o oob ./oob echo $? ``` Output ```text 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 ```text 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 [Section titled “How proofs remove checks”](#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](/proofs/overview/#how-proofs-remove-checks) 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 ```brine 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)) ``` ```sh brine check pick.br --report ``` ```text 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 ```brine 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)) ``` ```text 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](/proofs/fixing-proof-failures/#removing-a-runtime-check) 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 [Section titled “brine check –report”](#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`: ```sh brine check pick.br ``` ```text 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: ```sh brine check pick.br --report --json ``` ```text {"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](/tooling/cli/) and [JSON output](/agents/json-output/). ## What the report leaves out [Section titled “What the report leaves out”](#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 ```brine fn main(): let xs = [9223372036854775807, 1] var s = 0 for i in 0..len(xs): s += xs[i] print(s) ``` ```text Checked total in 0.00s — 1 runtime check proven unnecessary, 0 remain ``` but the `+=` is checked, and it overflows: Output ```text panic: integer overflow in addition --> total.br:5:9 ``` With `s = s + xs[i]` the same check is listed: ```text total.br:5:13: overflow check `s + xs[i]` Checked total in 0.00s — 1 runtime check proven unnecessary, 1 remain ``` ## Negative indexes [Section titled “Negative indexes”](#negative-indexes) Brine has no negative indexes. `xs[-1]` compiles, is listed as a remaining check, and panics when it runs: neg.br ```brine fn main(): let xs = [10, 20, 30] print(xs[-1]) ``` ```text neg.br:3:11: index bounds check `xs[-1]` Checked neg in 0.00s — 0 runtime checks proven unnecessary, 1 remain ``` Output ```text 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 [Section titled “Release builds keep their checks”](#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](/proofs/overview/#a-worked-example): ```sh brine run empty.br --release ``` Output ```text panic: division by zero --> empty.br:5:12 ``` There is no option to remove them: ```sh brine build empty.br --unchecked ``` ```text error: unknown option `--unchecked` ``` The way to a faster program is to prove checks away, not to switch them off. See [builds and backends](/tooling/builds-and-backends/). ## Summary [Section titled “Summary”](#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](/proofs/contracts/), [fixing proof failures](/proofs/fixing-proof-failures/).