Control flow

Control flow reads like Python: if/elif/else, for x in ..., while, break, continue and pass, with and, or and not. The differences: conditions must be bool (no “truthy” values), and a for loop over an array walks a snapshot of it.

if, elif and else

fn classify(x: int) -> str:
    if x < 0:
        return "negative"
    elif x == 0:
        return "zero"
    else:
        return "positive"

fn main():
    for x in [-3, 0, 8]:
        let parity = "even" if x % 2 == 0 else "odd"
        print(x, classify(x), parity)

Output

-3 negative odd
0 zero even
8 positive even

a if cond else b is the conditional expression. Both branches must have the same type.

A condition must be a bool. An integer, a string or an array isn’t true or false on its own; compare explicitly.

fn main():
    let items = [1, 2]
    if len(items):
        print("not empty")

error[E0307]: condition must be a `bool`, found `int`
 --> main.br:3:8
  |
3 |     if len(items):
  |        ^^^^^^^^^^ not a bool
  |
  = help: compare explicitly, e.g. `x != 0`
  = run `brine explain E0307` for more about this error
error: could not compile due to 1 error

Habits from other languages get a direct fix. else if is E0114 (write elif), and &&, || and ! are E0105 (write and, or, not):

fn main():
    let x = 3
    if x > 0 && x < 5:
        print("in range")

error[E0105]: `&&` is not an operator in brine
 --> main.br:3:14
  |
3 |     if x > 0 && x < 5:
  |              ^^ use `and`
  = run `brine explain E0105` for more about this error
error: could not compile due to 1 error

Comparisons and logic

Comparisons chain, as in Python: 0 <= i < n means 0 <= i and i < n. and and or short-circuit: the right side runs only when it’s needed.

fn main():
    let xs = [4, 8, 15]
    let i = 2
    print(0 <= i < len(xs))
    print(1 < 2 < 3 > 0)
    print(len(xs) > 0 and xs[0] == 4)
    let empty: [int] = []
    print(len(empty) > 0 and empty[0] == 4)   # stops before the index
    print(not (i == 2) or i > 1)

Output

true
true
true
false
true

== and != compare values by content on every type (two arrays are equal when their elements are; the same goes for maps, tuples, structs and enums). <, <=, > and >= work on numbers and strings.

for over ranges

a..b counts from a up to b - 1; a..=b includes b. range(...) works like Python’s and is the way to count with a step, including downward.

fn main():
    for i in 0..4:
        print(i, end=" ")
    print()
    for i in 1..=4:
        print(i, end=" ")
    print()
    for i in range(5):
        print(i, end=" ")
    print()
    for i in range(2, 5):
        print(i, end=" ")
    print()
    for i in range(0, 10, 3):
        print(i, end=" ")
    print()
    for i in range(10, 0, -3):
        print(i, end=" ")
    print()

Output

0 1 2 3
1 2 3 4
0 1 2 3 4
2 3 4
0 3 6 9
10 7 4 1

A range whose end is below its start runs zero times. A range step of zero panics. The loop variable has the type of the bounds: for j in 0..n with n: u8 gives a u8.

Ranges exist only in for loops and comprehensions; they aren’t values:

fn main():
    let r = 0..5
    print(r)

error[E0312]: ranges can only be used in `for` loops and comprehensions
 --> main.br:2:13
  |
2 |     let r = 0..5
  |             ^^^^ range used as a value
  |
  = help: to make an array, write `[i for i in 0..n]`
  = run `brine explain E0312` for more about this error
error: could not compile due to 1 error

for over arrays, strings and maps

fn main():
    var xs = [1, 2, 3]
    for x in xs:                 # loops over xs as it was here
        xs.push(x * 10)
    print(xs)
    for i, name in enumerate(["ann", "bob"]):
        print(i, name)
    for c in "héllo":
        print(c, end="|")
    print()

Output

[1, 2, 3, 10, 20, 30]
0 ann
1 bob
h|é|l|l|o|

• for x in xs walks a snapshot of xs taken when the loop starts. The body may change xs (push, pop, assign) without affecting the iteration, and it never runs past the end.
• enumerate(xs) gives (index, element) tuples.
• for c in s walks the UTF-8 characters of a string, each as a one-character str. (Indexing a string counts bytes; see strings.)
• for k in m walks a map’s keys in insertion order, also over a snapshot; see maps.

Tuple unpacking in for

When the elements are tuples, name their parts in the loop header. Patterns nest, and they work the same in comprehensions.

fn main():
    let pairs = [("x", 1), ("y", 2)]
    for name, value in pairs:
        print(name, value)
    for i, (name, value) in enumerate(pairs):
        print(i, name, value)
    let flat = [f"{k}={v}" for k, v in pairs]
    print(flat)

Output

x 1
y 2
0 x 1
1 y 2
["x=1", "y=2"]

Loop variables take annotations too: for i: int in 0..n:, or for name: str, age: int in ages.items():.

while, break, continue and pass

fn main():
    var k = 0
    while k < 10:
        k += 1
        if k % 2 == 0:
            continue             # skip even numbers
        if k > 7:
            break                # leave the loop
        print(k, end=" ")
    print()
    for i in 0..3:
        if i == 1:
            pass                 # nothing to do here (yet)
        else:
            print(i)

Output

1 3 5 7
0
2

break and continue apply to the innermost loop. pass is a statement that does nothing, for a block that must not be empty.

Loops that the prover should reason about can carry an invariant; parallel loops are written par for (see parallelism).

Summary

• if / elif / else; conditions must be bool.
• a if cond else b is an expression.
• Comparisons chain (0 <= i < n); and / or short-circuit; not negates.
• for i in a..b (exclusive), a..=b (inclusive), range(stop), range(start, stop), range(start, stop, step).
• for x in xs iterates over a snapshot; enumerate adds indexes; for c in s walks characters; tuple elements unpack in the loop header.
• while, break, continue, pass work as in Python.