Proofs: contracts, the prover and runtime checks # Contracts > The syntax and meaning of requires, ensures (with result), loop invariants, prove and assert; where each may appear, what it obliges callers and bodies to do, how it works in par, and the errors it reports. 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 [Section titled “At a glance”](#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 [Section titled “requires”](#requires) A precondition. Every caller must prove it, and inside the function it’s a known fact: clamp.br ```brine 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 ```text 10 0 4 ``` A call the prover can’t show satisfies it is [E0601](/reference/errors/#e0601). Adding `print(clamp(1, 10, 0))` to `main` gives: ```text 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 ```brine 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()) ``` ```text 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](/proofs/overview/#a-worked-example). ## ensures [Section titled “ensures”](#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 ```brine fn half(n: int) -> int: return n / 2 fn main(): let xs = [1, 2, 3, 4] print(xs[half(len(xs))]) ``` ```sh brine check half.br --report ``` ```text 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 ```brine 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))]) ``` ```text 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](/reference/errors/#e0602). Often it has found a bug: dist.br ```brine 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)) ``` ```text 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 ```brine 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 ```text 0 ``` ## invariant [Section titled “invariant”](#invariant) A loop invariant is a claim that holds before every iteration. The prover checks it twice: once when the loop starts ([E0603](/reference/errors/#e0603) if it can’t), and once at the end of an iteration, assuming it held at the start ([E0604](/reference/errors/#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 ```brine 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)) ``` ```text 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 ```brine 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)) ``` ```text 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 [Section titled “Invariants in for loops”](#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 ```brine 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)) ``` ```text 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 ```brine 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 ```text 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](/reference/errors/#e0507)); write a stepped loop as a `while` loop when it needs one. ## prove [Section titled “prove”](#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 ```brine 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](/reference/errors/#e0605). `k * k >= 0` is true for every integer, but it multiplies two variables, which the prover doesn’t handle: square.br ```brine fn main(): let k = len(args()) prove k * k >= 0 ``` ```text 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 [Section titled “assert”](#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 ```brine 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: ```text Checked args in 0.00s — 2 runtime checks proven unnecessary, 0 remain ``` Run without arguments, it stops with exit code 101: Output ```text 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 [Section titled “What a specification may contain”](#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](/reference/errors/#e0606)), even ones without side effects: spec.br ```brine 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)) ``` ```text 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 ```brine fn root(x: float) -> float: requires x >= 0.0 return sqrt(x) fn main(): print(root(2.0)) ``` ```text 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 [Section titled “Placement”](#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](/reference/errors/#e0112): place.br ```brine fn f(x: int) -> int: let y = x + 1 requires x > 0 return y fn main(): print(f(1)) ``` ```text 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 [Section titled “Contracts and par”](#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 ```brine 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 ```text 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 ```text 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](/parallelism/gpu/)). `par for` can’t have an `invariant`: invariants describe the state between iterations, and parallel iterations have no order. parinv.br ```brine fn main(): var out = [0] * 8 par for i in 0..8: invariant 0 <= i <= 8 out[i] = i * i print(out) ``` ```text 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 [Section titled “Rules”](#rules) * `requires` and `ensures` go first in a function body, `invariant` first in a loop body ([E0112](/reference/errors/#e0112)). * `requires` is proven at every call ([E0601](/reference/errors/#e0601)), `ensures` at every `return` ([E0602](/reference/errors/#e0602)), an invariant on loop entry ([E0603](/reference/errors/#e0603)) and after each iteration ([E0604](/reference/errors/#e0604)), `prove` where it stands ([E0605](/reference/errors/#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](/reference/errors/#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](/proofs/overview/), [fixing proof failures](/proofs/fixing-proof-failures/), [runtime checks](/proofs/runtime-checks/), [error codes](/reference/errors/). # Fixing proof failures > How to read the facts and goal in an E0601-E0606 error, and the usual fixes (a guard, a requires, an ensures, an assert, an invariant, or a code fix) with real before-and-after examples. 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 [Section titled “Reading a proof failure”](#reading-a-proof-failure) pick.br ```brine 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)) ``` ```text 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: 1. **The code and the place.** `E0601` at `pick.br:7:16`: the call to `get`. 2. **The claim.** The `-` underline points at the contract that had to hold, here `requires 0 <= i < len(xs)` on line 2. 3. **`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). 4. **`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)`. 5. **`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 [Section titled “Choosing a fix”](#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 [Section titled “Guard the code”](#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: pick.br ```brine 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 [Section titled “Pass it to the callers”](#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): pick.br ```brine 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 [Section titled “Check it at run time”](#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: pick.br ```brine 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 [Section titled “The goal is the missing requires”](#the-goal-is-the-missing-requires) When `to prove:` names only parameters, the function needs a `requires`. This `clamp` has its precondition missing: clamp.br ```brine 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)) ``` ```text 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](/proofs/contracts/#ensures). ## A value from a call [Section titled “A value from a call”](#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: wrap.br ```brine 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]) ``` ```text 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: wrap.br ```brine 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]) ``` ```text 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: wrap.br ```brine 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]) ``` ```text Checked wrap in 0.00s — 2 runtime checks proven unnecessary, 0 remain ``` ## A value changed by a loop [Section titled “A value changed by a loop”](#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: first.br ```brine 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)) ``` ```text 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: first.br ```brine 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](/proofs/overview/#a-worked-example). ## E0603: invariant false on entry [Section titled “E0603: invariant false on entry”](#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`: count.br ```brine 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)) ``` ```text 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 [Section titled “E0604: invariant not preserved”](#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: reverse.br ```brine 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) ``` ```text 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: reverse.br ```brine 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) ``` ```text 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 [Section titled “E0605: a claim it can’t prove”](#e0605-a-claim-it-cant-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: area.br ```brine 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)) ``` ```text 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 ``` area.br ```brine 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 [Section titled “E0606: a call in a specification”](#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: ```brine fn get(xs: [int], i: int) -> int: requires in_bounds(i, len(xs)) # E0606 return xs[i] ``` ```brine 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 [Section titled “Floats”](#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`: root.br ```brine fn root(x: float) -> float: assert x >= 0.0, "root of a negative number" return sqrt(x) fn main(): print(root(2.0)) ``` Output ```text 1.4142135623730951 ``` ## Removing a runtime check [Section titled “Removing a runtime check”](#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`: pairs.br ```brine 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])) ``` ```text 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: ```brine while i + 1 < len(xs): invariant i >= 0 ``` ```text 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: pairs.br ```brine 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])) ``` ```text 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](/proofs/runtime-checks/#what-the-report-leaves-out)). * Assigning an element (`xs[j] = v`) makes the prover forget the array’s contents, though not its length. ## A checklist for agents [Section titled “A checklist for agents”](#a-checklist-for-agents) 1. Run `brine check` (or `brine check --json`) and take the first error. 2. Read `to prove:` against `known facts here:`. The missing piece is the difference. 3. If the note says `always false`, or the facts contradict the goal, the code is wrong. Fix the code, not the contract. 4. If the goal names only the current function’s parameters, add a `requires`, then fix the callers it breaks. 5. If the goal names a call’s result, add an `ensures` to that function. 6. If the goal names a variable a loop changes, add or strengthen an `invariant` with its bounds; check E0603 (entry) and E0604 (preserved) separately. 7. If the goal needs a product, a variable divisor, a float or array contents, use an `assert` where the fact is cheapest to check. 8. 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. 9. Re-run `brine check --report` and confirm the checks you meant to remove are gone. See also: [contracts](/proofs/contracts/), [runtime checks](/proofs/runtime-checks/), [error codes](/reference/errors/#e0601), [JSON output](/agents/json-output/). # 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. 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 ") 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. # 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. 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/).