Control flow

Vx has five ways to branch or repeat: if, loop, while, for, and match.

if and else

fn classify(x : i32) -> i32 {
    if x < 0 {
        return 0;
    } else if x == 0 {
        return 1;
    } else {
        return 2;
    }
}

fn main() -> i32 {
    return classify(5) - 2;
}

Braces are always required. There is no single-statement form.

An if whose branches all return is a statement, not a value. An if used in value position has to produce a value on every path:

fn main() -> i32 {
    let x : i32 = 3;
    let label = if x > 2 { 1 } else { 0 };
    return label - 1;
}

loop

loop repeats until something breaks out of it.

fn main() -> i32 {
    let mut i : i32 = 0;
    loop {
        if i >= 3 {
            break;
        }
        i = i + 1;
    }
    return i - 3;
}

continue skips to the next turn of the loop:

fn main() -> i32 {
    let mut seen : i32 = 0;
    let mut i : i32 = 0;
    loop {
        i = i + 1;
        if i < 3 {
            continue;
        }
        seen = seen + 1;
        if i >= 5 {
            break;
        }
    }
    return seen - 3;
}

Loop invariants

A loop can carry an invariant: a condition that must hold on every turn. The prover checks it.

fn main() -> i32 {
    let limit : i32 = 3;
    let mut i : i32 = 0;
    loop invariant(limit > 0) {
        if i >= limit {
            break;
        }
        i = i + 1;
    }
    return 0;
}

The parentheses around the condition are required here, unlike requires and ensures on a function, which take theirs optionally. That inconsistency is not deliberate — it is Vx#501.

while

while checks its condition before every turn, including the first, and stops as soon as the condition is false. If the condition is false to begin with, the body never runs.

fn main() -> i32 {
    let mut i : i32 = 0;
    while i < 4 {
        i = i + 1;
    }
    return i - 4;
}

break and continue work as they do in loop. continue goes back to the condition check, so the condition is never skipped:

fn main() -> i32 {
    let mut i : i32 = 0;
    let mut odd : i32 = 0;
    while i < 6 {
        i = i + 1;
        if i % 2 == 0 {
            continue;
        }
        odd = odd + 1;
    }
    return odd - 3;
}

A while is shorthand for loop { if cond { body } else { break } }, and the compiler treats it as exactly that. So a condition that is not a bool is reported as an error in an if.

A while can carry invariant clauses after its condition, as loop and for can:

fn count_to(n : i32) -> i32
    requires n > 0
{
    let mut i : i32 = 0;
    while i < n invariant(n > 0) {
        i = i + 1;
    }
    return i;
}

fn main() -> i32 {
    return count_to(3) - 3;
}

There is no while let yet, because there is no if let. Write while let Some(x) = next() as a loop with a match that breaks on None.

for

for walks a range or anything that implements Iterator.

fn main() -> i32 {
    let mut total : i32 = 0;
    for i in 0..4 {
        total = total + i;
    }
    return total - 6;
}

0..4 counts from 0 up to but not including 4, so that loop adds 0 + 1 + 2 + 3.

A for loop can carry an invariant in the same way a loop can.

match

match compares a value against patterns, in order, and runs the first arm that fits.

fn main() -> i32 {
    let x : i32 = 1;
    match x {
        0 => { return 1; }
        _ => { return 0; }
    }
}

_ matches anything. It is usually the last arm.

match is most useful with an enum, where each arm handles one variant:

enum Colour {
    Red,
    Green,
}

fn main() -> i32 {
    let c = Colour::Red;
    match c {
        Colour::Red => { return 0; }
        Colour::Green => { return 1; }
    }
}

Where to next

• Ownership and borrowing — who owns a value, and who may look at it
• Contracts and verification — requires, ensures, assert
• Generics and traits — writing code once for many types