# 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. Source: https://docs.brinelang.org/proofs/contracts/ A contract is a claim the compiler must prove. `requires` is proven at every call, `ensures` at every `return`, `invariant` around every loop iteration and `prove` where it stands; if one can’t be proven, the program doesn’t compile. `assert` is the exception: it is checked at run time, and the prover treats it as true afterwards. ## At a glance [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/).