# Error codes > Every Brine compiler error code with its explanation, generated from `brine explain`. Source: https://docs.brinelang.org/reference/errors/ Every diagnostic Brine prints has a stable code, a primary source span, the reason, and how to fix it. This page lists every code with the same explanation that `brine explain ` prints. Search for a code with `Ctrl` `K`, or jump to it with `#e0601`-style anchors. ```sh brine explain E0601 # the explanation in your terminal brine explain --json E0601 # {"code": ..., "title": ..., "explanation": ...} brine explain # list every code ``` Codes are grouped by the part of the compiler that reports them. 76 codes, from brine 0.4.0. ## Syntax (E01xx) [Section titled “Syntax (E01xx)”](#syntax-e01xx) Literals, indentation, and operators or punctuation from other languages. | Code | Meaning | | --------------- | ------------------------------ | | [E0101](#e0101) | invalid literal | | [E0102](#e0102) | unterminated string | | [E0103](#e0103) | bad indentation | | [E0104](#e0104) | tab in indentation | | [E0105](#e0105) | operator from another language | | [E0106](#e0106) | braces or semicolons | | [E0110](#e0110) | syntax error | | [E0111](#e0111) | expected an expression | | [E0112](#e0112) | contract in the wrong place | | [E0113](#e0113) | misused `par` | | [E0114](#e0114) | `else if` | ### E0101 [Section titled “E0101”](#e0101) **Invalid literal** A number or string literal couldn’t be read: the integer is too large to represent, or a string contains an unknown escape such as `\q`. The largest integer literal is 340282366920938463463374607431768211455, the maximum of `u128` (literals above the `i128` range need a `u128` type). Supported escapes: \n \t \r \0 \\\ \” \’ \\{ \\} and \u{XXXX}. Integers may use `_` separators and the 0x, 0o and 0b prefixes: 1_000_000, 0xff. ### E0102 [Section titled “E0102”](#e0102) **Unterminated string** A string or f-string literal isn’t closed on the same line, or an f-string has an unbalanced brace. In f-strings, `{expr}` interpolates and `{{` / `}}` write literal braces: ```brine print(f"{name} has {{braces}}") ``` ### E0103 [Section titled “E0103”](#e0103) **Bad indentation** brine uses indentation (like Python) to group statements. A block must be indented after a line ending in `:`, and nothing else may be indented. ```brine fn main(): print("indented by 4 spaces") ``` ### E0104 [Section titled “E0104”](#e0104) **Tab in indentation** Indentation must use spaces. Tabs look different in every editor, so they are not allowed. `brine fmt` uses 4 spaces per level. ### E0105 [Section titled “E0105”](#e0105) **Operator from another language** brine spells logical operators as words and has no `++`/`--`: ```brine a and b (not a && b) a or b (not a || b) not a (not !a) x += 1 (not x++) ``` ### E0106 [Section titled “E0106”](#e0106) **Braces or semicolons** Blocks are written with `:` and indentation, and statements end at the end of the line. Remove `{ }` and `;`. ### E0110 [Section titled “E0110”](#e0110) **Syntax error** The parser expected something else here. The message says what it expected. Common causes: a missing `:` at the end of `if`/`for`/`fn` lines, a missing type on a function parameter (`fn f(x: int)`), or a construct that brine doesn’t support yet (slicing, nested comprehensions). Run `brine guide` for the full syntax. ### E0111 [Section titled “E0111”](#e0111) **Expected an expression** A value was expected here (a number, a variable, a call, …), but the parser found something else, such as a keyword or a closing bracket. ### E0112 [Section titled “E0112”](#e0112) **Contract in the wrong place** `requires` and `ensures` must be the first lines of a function body, and `invariant` must be the first lines of a `while` or `for` body: ```brine fn f(x: int) -> int: requires x > 0 ensures result > x return x + 1 ``` ### E0113 [Section titled “E0113”](#e0113) **Misused `par`** `par` comes in exactly four forms: ```brine par for i in 0..n: # parallel loop par [f(x) for x in xs] # parallel map par sum(x * x for x in xs) # parallel reduction (sum/product/min/max/any/all) par(f(a), g(b)) # run two or more expressions in parallel ``` ### E0114 [Section titled “E0114”](#e0114) **`else if`** brine writes `elif` (like Python): ```brine if x < 0: ... elif x == 0: ... else: ... ``` ## Names (E02xx) [Section titled “Names (E02xx)”](#names-e02xx) Names that are not found, defined twice, or shadowed; unknown types, fields and methods. | Code | Meaning | | --------------- | -------------- | | [E0201](#e0201) | name not found | | [E0202](#e0202) | defined twice | | [E0203](#e0203) | unknown type | | [E0205](#e0205) | no such field | | [E0206](#e0206) | no such method | | [E0207](#e0207) | shadowing | ### E0201 [Section titled “E0201”](#e0201) **Name not found** A variable, function, type, or module name isn’t defined where it’s used. The message often suggests the closest existing name. Variables are only visible after their `let`/`var` line and inside the block that declares them. ### E0202 [Section titled “E0202”](#e0202) **Defined twice** Two items, fields, methods, or parameters share a name in the same scope. Rename one of them. ### E0203 [Section titled “E0203”](#e0203) **Unknown type** The type name isn’t a built-in type, struct or enum in scope. Built-in types: int (i64), i8, i16, i32, u8, u16, u32, u64, float (f64), f32, bool, str, arrays \[T], tuples (A, B). Types from another module are written `module.Name`. ### E0205 [Section titled “E0205”](#e0205) **No such field** The struct, tuple or enum variant doesn’t have this field. Tuple fields are numbered: `pair.0`, `pair.1`. Enum values have no fields of their own; read the data of a variant with `match`: ```brine match shape: case Shape.Circle(r): print(r) case _: pass ``` ### E0206 [Section titled “E0206”](#e0206) **No such method** The type doesn’t have this method. Arrays have `push(x)` and `pop()`; other operations are functions, e.g. `len(xs)`. Methods are defined inside a struct body; methods with `self` are called on a value (`p.norm()`), methods without `self` are called on the type (`Point.origin()`). ### E0207 [Section titled “E0207”](#e0207) **Shadowing** brine doesn’t allow a second variable with the same name in one function, even in an inner block. This avoids a classic source of bugs. Pick a new name, or use `var` and assign to the existing variable. ## Types (E03xx) [Section titled “Types (E03xx)”](#types-e03xx) Type mismatches, missing or extra arguments, `match` coverage, generics and conversions. | Code | Meaning | | --------------- | ------------------------------------------------- | | [E0301](#e0301) | type mismatch | | [E0302](#e0302) | wrong arguments | | [E0303](#e0303) | not callable | | [E0304](#e0304) | bad indexing | | [E0305](#e0305) | bad operands | | [E0306](#e0306) | missing return | | [E0307](#e0307) | condition isn’t bool | | [E0308](#e0308) | can’t infer type | | [E0309](#e0309) | recursive struct | | [E0310](#e0310) | not a value | | [E0311](#e0311) | unsupported extern signature | | [E0312](#e0312) | range outside a loop | | [E0313](#e0313) | break/continue outside a loop | | [E0314](#e0314) | not iterable | | [E0315](#e0315) | literal out of range | | [E0316](#e0316) | generator outside a reduction | | [E0317](#e0317) | constant not computable | | [E0318](#e0318) | bad format spec | | [E0319](#e0319) | unsupported type for this operation | | [E0320](#e0320) | `match` doesn’t handle every value | | [E0321](#e0321) | names bound inside \` | | [E0322](#e0322) | constant used as a pattern | | [E0331](#e0331) | a method’s type parameter repeats its type’s | | [E0332](#e0332) | can’t infer a type argument | | [E0333](#e0333) | too many generic instances | | [E0334](#e0334) | wrong type arguments | | [E0335](#e0335) | invalid map key type | | [E0336](#e0336) | duplicate key in a map literal | | [E0337](#e0337) | a variable without a written type | | [E0340](#e0340) | `?` on a value that isn’t an `Option` or `Result` | | [E0341](#e0341) | `?` in a function that can’t return its failure | | [E0342](#e0342) | `?` inside a comprehension or `par` body | ### E0301 [Section titled “E0301”](#e0301) **Type mismatch** A value has a different type than the one required here. brine never converts implicitly; convert explicitly instead: ```brine float(i) int(x) str(n) i32(n) int("42") ``` Numeric literals adapt to context, so `let x: f32 = 1` and `let y: u8 = 200` work without conversions. ### E0302 [Section titled “E0302”](#e0302) **Wrong arguments** A call has the wrong number of arguments or bad keyword arguments. Struct constructors take every field, positionally or by name: ```brine Point(1, 2) Point(x=1, y=2) ``` ### E0303 [Section titled “E0303”](#e0303) **Not callable** Only functions, methods, struct names, and built-ins can be called. ### E0304 [Section titled “E0304”](#e0304) **Bad indexing** Only arrays can be indexed, and only with an integer: `xs[i]`. ### E0305 [Section titled “E0305”](#e0305) **Bad operands** The operator doesn’t work on these types. Arithmetic needs two numbers of the same type; `and`/`or`/`not` need `bool`; `+` also joins two strings. Arrays, tuples and structs support `==` and `!=`; strings and numbers can also be ordered with `<`. ### E0306 [Section titled “E0306”](#e0306) **Missing return** Some path through a function with a return type reaches the end without a `return`. Add a `return` at the end (or make every branch of a final `if/elif/else` return). ### E0307 [Section titled “E0307”](#e0307) **Condition isn’t bool** `if`, `elif` and `while` need a `bool`. brine has no “truthiness”: write `if len(xs) > 0:` instead of `if xs:`. ### E0308 [Section titled “E0308”](#e0308) **Can’t infer type** The compiler can’t tell the type from the expression alone. Add an annotation: ```brine var xs: [int] = [] let n: int = world.recv(0) ``` ### E0309 [Section titled “E0309”](#e0309) **Recursive struct** A struct can’t contain itself directly (it would be infinitely large). Use an enum for recursive data: enum values are stored behind a pointer, so a variant may contain the enum itself. ```brine enum Tree: Leaf(value: int) Node(left: Tree, right: Tree) ``` An array of the struct also works: `children: [Node]`. ### E0310 [Section titled “E0310”](#e0310) **Not a value** Types, modules and functions can’t be stored in variables or passed around (first-class functions are planned). ### E0311 [Section titled “E0311”](#e0311) **Unsupported extern signature** `extern fn` declares a C function. For now extern functions may only take and return integers, floats and bools. ### E0312 [Section titled “E0312”](#e0312) **Range outside a loop** Ranges (`a..b`, `a..=b`, `range(...)`) are only allowed as the iterable of a `for` loop or comprehension. To make an array of a range use `[i for i in 0..n]`. ### E0313 [Section titled “E0313”](#e0313) **Break/continue outside a loop** `break` and `continue` only work inside `for` and `while` loops. ### E0314 [Section titled “E0314”](#e0314) **Not iterable** `for` can iterate over ranges and arrays. ### E0315 [Section titled “E0315”](#e0315) **Literal out of range** The literal doesn’t fit the type it’s used as, e.g. `let x: u8 = 300`. ### E0316 [Section titled “E0316”](#e0316) **Generator outside a reduction** `x for x in xs` (without brackets) is a generator. It can only be passed to sum, product, min, max, any or all. Use `[x for x in xs]` to build an array. ### E0317 [Section titled “E0317”](#e0317) **Constant not computable** `const` values must be computable at compile time from literals and other constants, using arithmetic, comparisons and logic. ### E0318 [Section titled “E0318”](#e0318) **Bad format spec** Format specs in f-strings follow `{value:[<|>][0][width][.precision][kind]}`: ```brine f"{x:.3f}" 3 decimals f"{n:>8}" right-align in 8 columns f"{n:05}" zero-pad to 5 f"{n:x}" hexadecimal (also `b` for binary) f"{x:e}" scientific ``` ### E0319 [Section titled “E0319”](#e0319) **Unsupported type for this operation** This operation only works on certain types. `world` messages can be int, float, bool, str, \[int] or \[float]; world reductions work on int and float. ### E0320 [Section titled “E0320”](#e0320) **`match` doesn’t handle every value** Every `match` must handle every possible value, so a new enum variant can never slip through unnoticed. The error shows an example value that no case handles. Add a case for it, or end with a catch-all: ```brine match shape: case Shape.Circle(r): return 3.14 * r * r case _: return 0.0 ``` Cases with an `if` guard don’t count toward this, because the guard may be false. Integers and strings have too many values to list, so matching on them always needs `case _:` (or a plain name, which also matches everything). ### E0321 [Section titled “E0321”](#e0321) **Names bound inside `|`** In `case A | B:` either alternative may match, so a name bound in only one of them might not have a value. Use `_` inside `|` patterns, or write a separate `case` for each alternative. ### E0322 [Section titled “E0322”](#e0322) **Constant used as a pattern** A plain name in a pattern always captures the matched value under that name; it doesn’t compare against a constant of the same name. Compare explicitly: ```brine match n: case x if x == LIMIT: ... ``` ### E0331 [Section titled “E0331”](#e0331) **A method’s type parameter repeats its type’s** A method can have type parameters of its own, and a method of a generic type can also use the type’s parameters. The two can’t share a name, since `T` would then mean two things inside the method: ```brine struct Box[T]: v: T fn pair[T](self, x: T) -> (T, T): # error: `T` is already Box's ... fn pair[U](self, x: U) -> (T, U): # ok return (self.v, x) ``` Type arguments of a method are inferred from its arguments, or written after the method name: `b.pair[str]("x")`. ### E0332 [Section titled “E0332”](#e0332) **Can’t infer a type argument** The compiler works out type arguments from the arguments and from the type the result must have. When neither says what a type parameter is, write it: ```brine let xs = make[int]() # explicit type argument let o: Option[str] = None # or annotate the variable let p = Pair[int, str](a=1, b="x") ``` ### E0333 [Section titled “E0333”](#e0333) **Too many generic instances** Each combination of type arguments makes a separate copy of a generic function or type. A function that calls itself with an ever larger type, like `f[[T]]` inside `f[T]`, would need infinitely many. Restructure the recursion so the type arguments stay the same. ### E0334 [Section titled “E0334”](#e0334) **Wrong type arguments** Generic types need one type argument per parameter: `Option[int]`, `Result[int, str]`, `Pair[A, B]`. Types that aren’t generic take none. ### E0335 [Section titled “E0335”](#e0335) **Invalid map key type** Map keys must be compared with `==` reliably, so they can be integers, `bool`, `str`, enums, or arrays, tuples and structs made of those. Floats are not allowed because `nan != nan`; maps can’t be keys either. ```brine var by_id: {int: str} = {} # ok var cells: {(int, int): bool} = {} # ok var bad: {float: str} = {} # error ``` ### E0336 [Section titled “E0336”](#e0336) **Duplicate key in a map literal** The same constant key appears twice in one `{...}` literal, so the first value would be silently replaced. Remove one of them. ### E0337 [Section titled “E0337”](#e0337) **A variable without a written type** This project asks for a written type on every variable: its brine.toml has ```brine [check] typed = true ``` (or the command was given `--typed`). Types are written after the name: ```brine let count: int = 0 var names: [str] = [] let (q, r): (int, int) = (17 / 5, 17 % 5) for i: int in 0..n: for name: str, age: int in ages.items(): ``` Comprehension variables (`[x * x for x in xs]`), `match` bindings and `_` don’t need one: their types come from the code right next to them. Without `typed = true`, writing types is optional everywhere. ### E0340 [Section titled “E0340”](#e0340) **`?` on a value that isn’t an `Option` or `Result`** `x?` unwraps an `Option` or a `Result`: it gives the value inside `Some`/`Ok`, or returns `None`/`Err` from the current function right away. ```brine let n = parse(s)? # parse returns Result[int, str] ``` Other values have nothing to unwrap, so `?` doesn’t apply to them. ### E0341 [Section titled “E0341”](#e0341) **`?` in a function that can’t return its failure** `?` returns early with the `None` or `Err` it found, so the function has to be able to return that: * `opt?` needs the function to return `Option[...]`; * `res?` needs it to return `Result[..., E]` with the same error type `E`. ```brine fn total(parts: [str]) -> Result[int, str]: var sum = 0 for p in parts: sum += parse_int(p)? # an Err(str) is returned as is return Ok(sum) ``` There are no automatic conversions between error types; use `match` to turn one error into another. In `main`, return `Result[(), str]` to use `?`. ### E0342 [Section titled “E0342”](#e0342) **`?` inside a comprehension or `par` body** A comprehension or `par` body isn’t a function you can return from early, so `?` can’t be used inside it. Write a `for` loop instead: ```brine var out: [int] = [] for s in parts: out.push(parse_int(s)?) ``` ## Mutability and references (E04xx) [Section titled “Mutability and references (E04xx)”](#mutability-and-references-e04xx) `let` and `var`, `ref` parameters and arguments, and aliasing. | Code | Meaning | | --------------- | ------------------------------------------------------ | | [E0401](#e0401) | assigning to an immutable binding | | [E0402](#e0402) | `ref` mismatch at a call | | [E0403](#e0403) | modifying a parameter | | [E0404](#e0404) | not assignable | | [E0405](#e0405) | a variable is changed and used again in one expression | ### E0401 [Section titled “E0401”](#e0401) **Assigning to an immutable binding** Variables declared with `let` (and loop variables) can’t change. Declare the variable with `var` if it needs to change: ```brine var total = 0 total += 1 ``` ### E0402 [Section titled “E0402”](#e0402) **`ref` mismatch at a call** Arguments are passed by value. When a function takes `ref x: T`, it can change the caller’s variable, and the caller must say so explicitly: `f(ref xs)`. Without `ref` in the parameter list, the argument may not be marked `ref`. This makes every change to a caller’s variable visible at the call site. Methods that change their receiver are declared with `ref self` and called normally: `p.move_by(1.0)`. ### E0403 [Section titled “E0403”](#e0403) **Modifying a parameter** Parameters are read-only. To change a local copy, declare the parameter `mut`; to change the caller’s variable, declare it `ref`: ```brine fn countdown(mut n: int): # local copy while n > 0: n -= 1 fn fill(ref xs: [int], v: int): # caller's variable: call as fill(ref data, 0) for i in 0..len(xs): xs[i] = v ``` ### E0404 [Section titled “E0404”](#e0404) **Not assignable** Only variables, their fields and their elements can be assigned: `x = 1`, `p.x = 1`, `xs[i] = 1`. References are made with `let r = ref x`, where `x` is a variable. `r` is then another name for `x` for the rest of the block. A reference is always declared with `let` (it can’t be re-pointed) and names a whole variable. ### E0405 [Section titled “E0405”](#e0405) **A variable is changed and used again in one expression** An expression that changes a variable in place (`xs.pop()`, `m.remove(k)`, a `ref self` method, a `ref` argument) can’t also read that variable somewhere else, or change it a second time, because the result would depend on the order of evaluation: ```brine print(xs, xs.pop()) # error: read and changed print(xs.pop(), xs.pop()) # error: changed twice xs.push(xs.pop()) # error: changed twice let last = xs.pop() # ok: change first, print(xs, last) # then read ``` Reading the variable in the changing call’s own receiver and arguments is fine: they are evaluated before the call (as in Rust and Swift), and a by-value argument keeps that value even while the call changes the variable: ```brine append_twice(ref v, v) # ok: the second argument is v before the call xs.push(len(xs)) # ok ``` The two sides of `and`/`or`, and the parts of `a if cond else b`, run one after the other, so they may change and read the same variable: ```brine if not self.eat(Tok.Comma) or self.at(Tok.RBracket): # ok ``` The same variable can’t be passed as `ref` twice in one call (two names for one variable inside the function). Copy it first: `let snapshot = xs`. ## Parallel safety and communication (E05xx) [Section titled “Parallel safety and communication (E05xx)”](#parallel-safety-and-communication-e05xx) `par` rules, and the `world` checks that rule out deadlocks. | Code | Meaning | | --------------- | --------------------------------------- | | [E0501](#e0501) | writing shared state in `par` | | [E0502](#e0502) | par write array accessed elsewhere | | [E0503](#e0503) | side effect not allowed in `par` | | [E0505](#e0505) | control flow out of `par` | | [E0507](#e0507) | unsupported invariant | | [E0508](#e0508) | filter in `par [...]` | | [E0510](#e0510) | communication not reached by every rank | | [E0511](#e0511) | value must be the same on every rank | | [E0512](#e0512) | no `send`/`recv` | ### E0501 [Section titled “E0501”](#e0501) **Writing shared state in `par`** Iterations of `par` code run at the same time. To rule out data races, a `par` body may not assign variables from outside it, call functions that mutate them, or push/pop them. The one exception: in `par for i in ...`, arrays from outside may be written at index `i`: ```brine var out = [0.0] * n par for i in 0..n: out[i] = f(i) # OK: each iteration writes its own slot ``` To combine results, use a reduction instead: `par sum(f(i) for i in 0..n)`. ### E0502 [Section titled “E0502”](#e0502) **Par write array accessed elsewhere** An array written as `out[i]` inside a `par for` may only be accessed as `out[i]` in that loop (with exactly the loop variable as the index), since any other index might belong to an iteration running at the same time. ### E0503 [Section titled “E0503”](#e0503) **Side effect not allowed in `par`** `exit` and `world` communication would be non-deterministic inside parallel code, and so would `write_file`, `run` and the `os` functions that change things outside the program (`os.spawn`, `os.wait`, `os.poll`, `os.kill`, `os.make_dir`, `os.remove_file`, `os.rename`, `os.sleep`, `os.enable_ansi`). Do them before or after the `par` construct. ### E0505 [Section titled “E0505”](#e0505) **Control flow out of `par`** `return` and `break` can’t leave a `par` body: other iterations are running at the same time. `continue` is fine (it ends the current iteration). ### E0507 [Section titled “E0507”](#e0507) **Unsupported invariant** Invariants describe the state between iterations, which doesn’t exist for a `par for`. Stepped ranges don’t support invariants yet; rewrite the loop as a `while` loop with an invariant. ### E0508 [Section titled “E0508”](#e0508) **Filter in `par [...]`** Parallel comprehensions need a known output size. Filter afterwards, or use a sequential comprehension: `[x for x in xs if x > 0]`. ### E0510 [Section titled “E0510”](#e0510) **Communication not reached by every rank** `world` communication is collective: every rank takes part in every call, and all ranks must make the same calls in the same order. If some ranks skip a call that others make, the others would wait forever. brine rules this out at compile time. A call is rejected when the condition that leads to it may differ between ranks: anything computed from `world.rank()`, `clock()`, values received with `world.shift`/`world.exchange`, files, processes, `os` functions (except `os.name()` and `os.arch()`), or C functions. Early `return`, `break` and `continue` under such a condition count too, as do `and`/`or`. ```brine if world.rank() == 0: world.barrier() # error: only rank 0 gets here ``` Compute the rank-specific part first, then communicate on every rank: ```brine let mine = 1 if world.rank() == 0 else 0 let total = world.sum(mine) # every rank calls this ``` Results of `world.sum`, `min`, `max`, `broadcast` and `gather_all` are the same on every rank, so they can be used in conditions freely: ```brine while world.max(err) > 1e-6: ... ``` ### E0511 [Section titled “E0511”](#e0511) **Value must be the same on every rank** Some arguments must have the same value on every rank: the root of `world.broadcast`, the distance of `world.shift`, and parameters that decide whether a function communicates (for example a loop count around a `world.sum`). Compute them from values that are the same everywhere: constants, `world.size()`, `args()`, or results of `world.broadcast`/`sum`. ### E0512 [Section titled “E0512”](#e0512) **No `send`/`recv`** brine has no unmatched `send`/`recv`, because a receive without a matching send hangs forever. Every communication is collective instead: ```brine world.shift(v, 1) # send v to rank + 1, receive from rank - 1 (wraps around) world.exchange(xs) # send xs[j] to rank j; returns what each rank sent you world.broadcast(root, v) # everyone gets root's value world.gather_all(v) # everyone gets [v from rank 0, v from rank 1, ...] ``` For example, “rank 0 sends a message to rank 1”: ```brine var outbox = [""] * world.size() if world.rank() == 0 and world.size() > 1: outbox[1] = "hello" let inbox = world.exchange(outbox) # on rank 1, inbox[0] == "hello" ``` ## Proofs (E06xx) [Section titled “Proofs (E06xx)”](#proofs-e06xx) Contracts (`requires`, `ensures`, `invariant`, `prove`) the compiler could not prove. | Code | Meaning | | --------------- | ------------------------------ | | [E0601](#e0601) | precondition not proven | | [E0602](#e0602) | postcondition not proven | | [E0603](#e0603) | invariant false on entry | | [E0604](#e0604) | invariant not preserved | | [E0605](#e0605) | claim not proven | | [E0606](#e0606) | not allowed in a specification | ### E0601 [Section titled “E0601”](#e0601) **Precondition not proven** The function’s `requires` clause must hold at every call, and the compiler must be able to prove it from what it knows at the call site. Rules can’t be broken, so an unproven claim is an error, not a runtime check. Fix it by giving the prover the facts it needs, for example: ```brine if 0 <= i and i < len(xs): # the call is only made when it's safe print(get(xs, i)) assert 0 <= i < len(xs) # checked at runtime, then known to the prover print(get(xs, i)) ``` or by adding a `requires` to the calling function, which moves the obligation to its callers. The error lists the facts the prover knew and the claim it needed. ### E0602 [Section titled “E0602”](#e0602) **Postcondition not proven** An `ensures` clause must hold on every `return`. The prover reasons about each path through the function. If it can’t show the claim on some path, add a `requires` the claim depends on, an `invariant` to loops before the return, or an `assert` (runtime check) before the return. ### E0603 [Section titled “E0603”](#e0603) **Invariant false on entry** A loop `invariant` must hold before the first iteration. For `for i in a..b` loops, invariants may mention `i`; on entry they’re checked with `i = a`. Initialize variables so the invariant holds, or weaken the invariant. ### E0604 [Section titled “E0604”](#e0604) **Invariant not preserved** Assuming the invariant (and the loop condition) at the start of an iteration, the prover couldn’t show it holds again at the end. For `for i in a..b`, the invariant is checked at the end of the iteration with `i + 1`. The prover only knows what the invariant says about variables the loop changes, so invariants often need to carry bounds such as `0 <= i <= n`. ### E0605 [Section titled “E0605”](#e0605) **Claim not proven** `prove e` asks the compiler to show `e` is always true at that point. Unlike `assert`, it generates no runtime code, so it must be provable. Use `assert` if a runtime check is acceptable. ### E0606 [Section titled “E0606”](#e0606) **Not allowed in a specification** Contracts (`requires`, `ensures`, `invariant`, `prove`) are pure logical statements. They may use arithmetic, comparisons, `and`/`or`/`not`, `len`, `abs`, `min`, `max`, fields, indexing, constants, and `result` (in `ensures`). Function calls and other side effects aren’t allowed. ## Driver (E07xx) [Section titled “Driver (E07xx)”](#driver-e07xx) Missing modules, no `main`, and C compiler or linker problems. | Code | Meaning | | --------------- | ---------------------------------- | | [E0701](#e0701) | module not found | | [E0702](#e0702) | no C compiler | | [E0703](#e0703) | no main function | | [E0704](#e0704) | cannot write build files | | [E0705](#e0705) | building the generated code failed | | [E0706](#e0706) | invalid `main` signature | | [E0707](#e0707) | cannot embed a file | ### E0701 [Section titled “E0701”](#e0701) **Module not found** `import a.b` loads `a/b.br` relative to the directory of the main file. Check the file name and location. ### E0702 [Section titled “E0702”](#e0702) **No C compiler** brine uses the system C compiler (clang or gcc) to build its runtime and link executables, and for optimized builds it compiles the program through C. Install one, or point BRINE_CC at it. `brine doctor` checks your setup. WebAssembly (`--target wasm` or `web`) takes the clang and C library of wasi-sdk instead: download it from and set WASI_SDK_PATH to its folder (or unpack it to /opt/wasi-sdk). ### E0703 [Section titled “E0703”](#e0703) **No main function** A program starts at `fn main():` in its main file. `main` may also return an `int`, which becomes the process exit code. (Libraries and test-only files can be checked with `brine check` and tested with `brine test`.) ### E0704 [Section titled “E0704”](#e0704) **Cannot write build files** The compiler couldn’t create its output or cache files. Check permissions and free disk space for the `target/` directory. ### E0705 [Section titled “E0705”](#e0705) **Building the generated code failed** The generated code didn’t compile or link. That’s a bug in brine, not in your program. Please report it with the source file and the output of `brine doctor`. Building with `BRINE_BACKEND=c` (or `=native`) tries the other backend. ### E0706 [Section titled “E0706”](#e0706) **Invalid `main` signature** `main` takes no parameters (command-line arguments come from `args()`) and returns one of: ```brine fn main(): # exit code 0 fn main() -> int: # the exit code fn main() -> Result[(), str]: # Err(e) prints "error: e" and exits with 1 ``` The `Result` form lets `main` use `?`: ```brine fn main() -> Result[(), str]: let text = read_file("config.txt")? print(len(text)) return Ok(()) ``` ### E0707 [Section titled “E0707”](#e0707) **Cannot embed a file** `embed(path)` puts a file’s text into the program when it is compiled, so the file must exist then, be UTF-8 text, and its path must be a string literal (not a variable or an f-string). The path is relative to the directory of the `.br` file that contains the call; “\r\n” line endings become “\n”. ```brine const HELP = embed("help.txt") # help.txt next to this file fn main(): print(HELP) ``` To read a file while the program runs instead, use `read_file(path)`.