# 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. Source: https://docs.brinelang.org/proofs/fixing-proof-failures/ A proof failure means the prover couldn’t show a claim from the facts it had at that point. The error lists those facts and the exact goal; the fix is to supply the missing fact where it’s true (a guard, a `requires`, an `ensures`, an `invariant`, or an `assert`), or to fix the bug the error found. Never weaken or delete the contract just to make the error go away. ## Reading a proof failure [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/).