The assign statement is used to assign a value, or generally speaking, the result of an expression evaluation to a variable or the lval expression. The syntax for the assign statement is the variable name followed by the assignment operator (=) and the expression value.
fn example() -> u32 {
let mut a: u32 = 42;
a = 10;
return a;
}
A block is a sequence of statements enclosed in curly braces {}. Blocks are used to group statements together and can be nested. Usually, blocks are used as function bodies, loop bodies, or conditional branches.
fn foo() {
/// This is the function body block
}
fn bar() {
let flag: bool = true;
if flag {
/// This is the 'if' block
} else {
/// This is the 'else' block
}
let mut i: i32 = 0;
loop i < 10 {
/// This is the loop block
i = i + 1;
}
}
The return statement returns an expression from a function. The expression must have the same type as the function's return type.
fn foo() -> i32 {
let res: i32 = 0;
return res;
}
The forall keyword is followed by a block. Semantically, forall is a logical analog of for all
The exists keyword is followed by a block. Semantically, exists is a logical analog of exists
The assume keyword is followed by a block. Semantically, assume converts traps and proven infinite loops into the successful completion of the closest forall block (understood in terms of dynamic, not lexical scope).
Regarding unwinding the call stack, handling traps inside assume is similar to exception handling in other languages (termination propagates up through activation frames until the point of handling) but differs in that assume doesn't retain any information about the cause and spec of failure.
assume is not a representation of any logical quantifier and makes sense only when it is embedded into the forall block as a mechanism of filtering execution paths (that are not satisfied with the pre-conditions).
fn foo(i: i32) -> () forall {
assume {
assert i > 0;
}
// This is equivalent to:
if !(i > 0) {
// Terminate the function or handle the case accordingly
return ();
}
}
The unique keyword is followed by a block. It should be embedded in the exists block to locally strengthen its execution semantics. By wrapping a code block in a unique modifier, we add a restriction on execution paths entering it to continue after its closing bracket.
If and only if every combination of @ values encountered through block execution either leads it to failure or to states of success indistinguishable from each other, unique block succeeds with this exit state.
As unique doesn't erase changes to machine state upon exit, it is not a quantifier and can't be used in deterministic code or inside quantifiers otside of exists.
fn foo(n: u32) exists {
let mut p: u64;
let mut q: u64;
unique {
p = @;
assert(p > 1 && p < n);
q = @;
assert(q > 1 && q < n);
assert(p < q && p * q == n);
}
}
Quantified procedure foo succeeds if and only if its argument is a composite number with exactly two non-trivial divisors. So, foo(6); and foo(8); will succeed, while foo(7); and foo(12); fail.
The loop statement comes in two forms:
-
Conditional loop:
loop CONDITION { ... }— evaluates the boolean condition before each iteration and continues as long as the condition istrue. The condition is an expression that must evaluate to a boolean value. -
Infinite loop:
loop { ... }— repeats the loop body indefinitely. An infinite loop must contain abreakstatement to exit.
The break statement exits the innermost enclosing loop.
fn loop_example() {
let mut i: i32 = 0;
loop i < 10 {
// This block will be executed 10 times
i = i + 1;
}
loop false {
// This block will not be executed
}
let mut n: i32 = 10;
loop n > 0 {
// This block will be executed 10 times
n = n - 1;
}
}
The infinite loop form uses loop without a condition. It must contain a break statement to exit.
fn infinite_loop_example() {
let mut i: i32 = 0;
loop {
if i >= 100 {
break;
}
i = i + 7;
}
}
The if statement is used to execute a block of code if a condition is true. If the condition is false, an optional else block can be executed. The condition is an expression that must explicitly evaluate to a Boolean value.
fn foo() {
let flag: bool = true;
if flag {
// This block will be executed
} else {
// This block will not be executed
}
}
Variable definition is a statement that declares a variable and optionally initializes it with a value. The type of the variable must be explicitly specified.
When a variable is declared with @ on its right-hand side, it carries no concrete initial value — instead, the expression splits the surrounding computation into a sub-path per value of the variable's type. The @ expression may appear only inside a non-deterministic block — forall, exists, assume, or unique — or inside the body of a function whose body is itself such a block (e.g. a function marked with the forall modifier).
let x: i32 = @;
Here, @ for x splits the execution path of the non-deterministic computation into sub-paths. Each sub-path considers one of every possible i32 value.
@ is an expression, not exclusively a let-initializer: it may appear anywhere a value of its inferred type is expected — for example as a function argument or a return operand. See also §8.3 Function Call.
fn sum_is_zero_or_not() forall {
let y: i32 = sum(@, @);
assert(y >= 0 || y < 0);
}
fn foo() {
let x: i32 = 10;
let y: i32 = @;
// 'y' can be any possible i32 value
}
The type definition statement is a way to create a type alias or reference an existing type.
type Address = u32;
The assert statement is used to check a condition and generate properties for the verifier. If the condition is false, the verifier will find a contradiction.
In compile mode assert(cond) evaluates cond at runtime and traps via unreachable if cond is false. In proof mode the assert becomes a proof obligation: the verifier must show that no execution path can reach the assert with cond == false. See §3.2 Compiler Design for the difference between the two modes.
fn foo() {
let flag: i32 = 0;
assert(flag <= 0);
}