An example-based guide to getting started with the Move prover.
- Introduction
- Step 0: Installation
- Step 1: First specification
- Step 2: Aborts
- Step 3: Preconditions
- Step 4: Helper functions
- Step 5: State
- Step 6: Operators and Quantifiers
- Step 7: Invariants
- Step 8: Invariants, part two
- Conclusion
The Move Prover is a tool for formally verifying the correctness of smart contracts written in Move. It is designed to be fast and practical—something that can really be used in the code development process. This is something it achieves: the prover nearly always runs in minutes or less, and has been used to verify all the Move in the Diem framework.
The Move smart contract language was designed with formal verification in mind. For instance, its use of Rust-like borrow semantics, lack of dynamic dispatch, and limited state interaction APIs all make program analysis more straightforward. Further, the Move language is developed alongside the Move specification language (MSL), which is more expressive than the language itself.
Despite the power of the Move Prover and its huge influence on the language design, many existing Move contracts we have seen do not utilize it to the fullest. Among other reasons may be difficulty in getting started with the specification language: though it is reasonably documented, there aren't many examples provided.
This resource aims to provide a gentle introduction to writing specifications and using the prover to make Move contracts more secure.
The prover comes with the Move cli. Install it using cargo.
cargo install --git https://github.com/move-language/move move-cliThe prover also depends on the Boogie verifier and a backend SMT solver. Either install Boogie and z3 with your preferred package manager or use the dev setup script provided by Move.
Finally, the prover looks for the Boogie and z3 environment variables in the
Z3_EXE and BOOGIE_EXE environment variables. Make sure these are set.
Let's begin by considering a very simple example function:
fun sum(first: u64, second: u64): u64 {
first + second
}How do we prove that this function works properly? Well, we need to tell the
Move prover what it is supposed to do. In this case, we want to check that
at the end of the function, the result of sum is indeed the sum of the two
arguments.
spec sum {
ensures result == first + second;
}These specification blocks (or spec blocks) can sit in lots of places. For now, let's keep it side by side with our function:
module address::step_1 {
fun sum(first: u64, second: u64): u64 {
first + second
}
spec sum {
ensures result == first + second;
}
}Cool. With our new postcondition, we can run move prove --path step-1...
[INFO] preparing module 0x2::step_1
[INFO] transforming bytecode
[INFO] generating verification conditions
[INFO] 1 verification conditions
[INFO] running solver
[INFO] 0.029s build, 0.001s trafo, 0.008s gen, 2.350s verify, total 2.387s
Awesome, no issues.
Suppose that we want to know when a function can abort. This might be important because aborts will revert the entire transaction.
Working off the previous code, why don't we add a module spec and make the prover always check aborts:
spec module {
pragma aborts_if_is_strict;
}Alternatively, we could add aborts_if false to the sum spec. This common
pattern would tell the prover to check that sum never aborts.
Either way, when we run the prover with move prove --path step-2, we get an
error!
error: abort not covered by any of the `aborts_if` clauses
┌─ ./sources/step-2.move:10:5
│
7 │ first + second
│ - abort happened here with execution failure
·
10 │ ╭ spec sum {
11 │ │ ensures result == first + second;
12 │ │ }
│ ╰─────^
│
= at ./sources/step-2.move:6: sum
= first = 1
= second = 18446744073709551615
= at ./sources/step-2.move:7: sum
= ABORTED
Error: exiting with verification errors
The prover finds a case where our function can abort: when second is
18446744073709551615. This makes sense, because on Move, all "bad arithmetic"
like overflow and division by zero will cause a revert. Let's fix this by
asserting when it will abort:
spec module {
pragma aborts_if_is_strict;
}
spec sum {
aborts_if first + second > MAX_U64;
ensures result == first + second;
}Now when we run the verifier, we see no errors. When writing aborts_if
clauses, it is good to know that once you have at least one written—or the
aborts_if_is_strict pragma is set—then the abort conditions must exactly
cover when the function will abort. To disable this behavior, set the
aborts_if_is_partial pragma to true.
In the specification language, preconditions are used to constrain how a function can be called. If a function is called in a way that violates its preconditions, the prover will give a verification error.
Why don't we modify our spec for sum to see how preconditions work:
module address::step_3 {
spec module {
pragma aborts_if_is_strict;
}
public fun sum(first: u64, second: u64): u64 {
first + second
}
spec sum {
// redundant, because of the `aborts_if_is_strict` pragma
aborts_if false;
requires first + second <= MAX_U64;
ensures result == first + second;
}
}Running the prover, we see that this verifies. Because we provide the
precondition that first + second will not overflow, our assertion that
sum will not abort (aborts_if false) gets verified.
Now, what if we call sum in a way that violates its preconditions?
module address::step_3 {
fun double(number: u64): u64 {
sum(number, number)
}
fun sum(first: u64, second: u64): u64 {
first + second
}
spec sum {
requires first + second <= MAX_U64;
aborts_if false;
ensures result == first + second;
}
}It aborts with the following error:
error: precondition does not hold at this call
┌─ ./sources/step-3.move:12:9
│
12 │ requires first + second <= MAX_U64;
│ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
│
= at ./sources/step-3.move:3: double
= number = 9223372036854775808
= at ./sources/step-3.move:12: sum (spec)
Nice, so it properly checks that functions which call sum can't violate its
preconditions. Let's add guards in double to make this work:
const MAX_U32: u64 = 1 << 32 - 1;
fun double(number: u64): u64 {
assert!(number <= MAX_U32, 0);
sum(number, number)
}
spec double {
aborts_if number > MAX_U32;
}Now, everything verifies properly! However, what happens if sum is called
from some other contract? Let's make it public...
module address::step_3 {
public fun sum(first: u64, second: u64): u64 {
first + second
}
spec sum {
requires first + second <= MAX_U64;
aborts_if false;
ensures result == first + second;
}
}Again running the prover, we see that this verifies. However, because sum is
public, it can still be called in a way that aborts, despite the prover's
verification!
Recall that Move prover specifications have no runtime effects. For example,
adding an aborts_if condition can give meaningful insight about a contract
but won't itself provide runtime guards. Thus, in most contexts, preconditions
do not make much sense in public APIs.
Let's write a contract with a bit more functionality:
module address::account {
use std::signer;
spec module {
pragma aborts_if_is_strict;
}
struct Account has key {
balance: u64;
}
public fun create_account(s: signer) {
let address = signer::address_of(&s);
assert!(!exists<Account>(address), 0);
move_to<Account>(&s, Account {
balance: 1
})
}
}Now, let's write a spec for create_account.
spec create_account {
aborts_if exists<Account>(signer::address_of(s));
ensures exists<Account>(signer::address_of(s));
ensures global<Account>(signer::address_of(s)).balance == 1;
}Notice that we use a number of builtin functions from the specification
language, like exists and borrow_global. The specification language also
includes many builtin helper functions for working with vectors, like
len, contains, and index_of.
To clean up our code, let's write a few helper functions of our own:
spec fun address_of(s: signer): address { signer::address_of(s) }
spec fun balance(a: address): u64 { global<Account>(a).balance }
spec create_account {
let address = address_of(s);
aborts_if exists<Account>(address);
ensures exists<Account>(address);
ensures balance(address) == 1;
}Much better. Here is our final result:
module address::coin {
use std::signer;
spec module {
pragma aborts_if_is_strict;
}
struct Account has key {
balance: u64
}
spec fun address_of(s: signer): address { signer::address_of(s) }
spec fun balance(a: address): u64 { global<Account>(a).balance }
public fun create_account(s: signer) {
let address = signer::address_of(&s);
assert!(!exists<Account>(address), 0);
move_to<Account>(&s, Account {
balance: 1
})
}
spec create_account {
let address = address_of(s);
aborts_if exists<Account>(address);
ensures exists<Account>(address);
ensures balance(address) == 1;
}
}While writing these specifications, we have been implicitly dealing with pre-
and post-state. In the aborts_if and requires conditions, our expressions
were evaluated against state at function entry. In the ensures
conditions, the expressions were evaluated against state at function
exit.
In contexts like ensures, we can also evaluate expressions against the state
at function entry. To do this, we use the old builtin. This is extremely
useful: we can verify the action of functions on state.
Suppose we allow users to transfer funds across accounts. Let's implement that:
fun withdraw(target: address, amount: u64) acquires Account {
let account = borrow_global_mut<Account>(target);
account.balance = account.balance - amount;
}
spec withdraw {
aborts_if !exists<Account>(target);
aborts_if balance(target) < amount;
}
fun deposit(target: address, amount: u64) acquires Account {
let account = borrow_global_mut<Account>(target);
account.balance = account.balance + amount;
}
spec deposit {
aborts_if !exists<Account>(target);
aborts_if balance(target) + amount > MAX_U64;
}
public fun transfer(
s: signer,
to: address,
amount: u64
) acquires Account {
let from = signer::address_of(&s);
assert!(from != to, 0);
withdraw(from, amount);
deposit(to, amount);
}
spec transfer {
let from = address_of(s);
aborts_if from == to;
aborts_if !exists<Account>(from);
aborts_if !exists<Account>(to);
aborts_if balance(from) < amount;
aborts_if balance(to) + amount > MAX_U64;
}Now, let's prove that transfer works properly. Specifically, the balance of
from should decrease by amount and the balance of to should increase by
amount.
ensures balance(from) == old(balance(from)) - amount;
ensures balance(to) == old(balance(to)) + amount;After the prover with move prove --path step-5, we see it verifies!
As an aside, it's good to know that function specifications can only access arguments (as opposed to intermediate variables) and do not respect reassignment. For instance, consider the following two functions.
fun inc_one(num: &mut u64) {
*num = *num + 1;
}
fun inc_two(num: u64): u64 {
num = num + 1;
num
}If inc_one were called on 10, then in its spec, num would be 11 while
old(num) would be 10. However, if inc_two were called on 10, both
num and old(num) would have value 10.
In the Move specification language, all relevant Move operators are supported. However, the MSL provides a few additional ones as well. For instance, consider the following function:
fun first_or_second(condition: bool, a: u64, b: u64): u64 {
if (condition) { a } else { b }
}Now, to write a spec for this, we could just use our standard logical operators.
spec first_or_second {
ensures condition && result == a || !condition && result == b;
}However, this is a bit unnatural. We can use the MSL's implication operator instead!
spec first_or_second {
ensures condition ==> result == a;
ensures !condition ==> result == b;
}Another very powerful aspect of the Move prover is that it supports
quantifiers. We can write assertions about the existence of things using
exists and about all members of a domain using forall. For instance, we
can claim that a vector is sorted.
fun ordered_vector(): vector<u8> {
vector[1, 2, 3, 4, 5]
}
spec ordered_vector {
ensures forall i in 0..len(result), j in 0..len(result) where i < j:
result[i] <= result[j];
}Note that this also uses some more operators specific to the specification
language! For instance, we use the range constructor 0..len(result) to
declare bounds on the indices i and j. Also, we can index the result
vector using square brackets.
Let's return to the coin module from earlier. Suppose we want to add a
maximum balance for each Account. We can do this by adding a check in
deposit.
const MAX_BALANCE: u64 = 1000;
fun deposit(target: address, amount: u64) acquires Account {
let account = borrow_global_mut<Account>(target);
account.balance = account.balance + amount;
assert!(account.balance <= MAX_BALANCE, 0);
}Of course, we update our deposit and transfer specifications to reflect
this possible abort. Now, we can write a global invariant to guarantee that the
balance can never increase above the maximum anywhere in the program. Note that
this invariant is not inside a specification block; it sits directly in the
module.
invariant forall a: address where exists<Account>(a):
balance(a) <= MAX_BALANCE;Unfortunately, this causes a verification error!
error: global memory invariant does not hold
┌─ ./sources/coin.move:76:5
│
76 │ ╭ invariant forall a: address where exists<Account>(a):
77 │ │ balance(a) <= MAX_BALANCE;
│ ╰──────────────────────────────────^
│
= at ./sources/coin.move:42: deposit
= target = 0x0
= amount = 2
= at ./sources/coin.move:43: deposit
= account = &coin.Account{balance = 999}
= at ./sources/coin.move:44: deposit
= at ./sources/coin.move:45: deposit
= at ./sources/coin.move:76
Error: exiting with verification errors
This happens because the invariant is temporarily violated in the process of
executing deposit. However, the balance increase will always be aborted if it
does bring it over MAX_BALANCE. Let's just rewrite our deposit function to
maintain this invariant:
fun deposit(target: address, amount: u64) acquires Account {
let account = borrow_global_mut<Account>(target);
let new_balance = account.balance + amount;
assert!(new_balance <= MAX_BALANCE, 0);
account.balance = new_balance;
}Testing with move prove --path step-7, everything verifies properly.
One of the trickest parts of using the prover is dealing with loops. In the prover internals, an early step of the proving processes involves performing a topological sort on the control flow graph. However, this is impossible if the graph has cycles, so loops are handled in a special way.
Specifically, Move tries to prove loops by using induction. After you provide loop invariants, the prover checks that
- The loop invariants hold at the beginning of the loop
- Loop invariants before an iteration implies them at the end
For instance, consider this simple case:
module address::step_8 {
fun looper(input: u64): u64 {
input = if (input < 50) input else 50;
while (input < 50) {
input = input + 1;
};
input
}
spec looper {
ensures result == 50;
}
}Although this is clearly true, the prover cannot verify it.
error: post-condition does not hold
┌─ ./sources/step-8.move:13:9
│
13 │ ensures result == 50;
│ ^^^^^^^^^^^^^^^^^^^^^
│
= at ./sources/step-8.move:4: looper
= input = 91
= at ./sources/step-8.move:5: looper
= input = 50
= at ./sources/step-8.move:6: looper
= enter loop, variable(s) input havocked and reassigned
= input = 51
= at ./sources/step-8.move:9: looper
= result = 51
= at ./sources/step-8.move:13: looper (spec)
This is because we need to write a loop invariant. Here is one that works.
module address::step_8 {
fun looper(input: u64): u64 {
input = if (input < 50) input else 50;
while ({
spec {
invariant input <= 50;
};
(input < 50)
}) {
input = input + 1;
};
input
}
spec looper {
ensures result == 50;
}
}Now, this verifies properly. Let's take a look at why.
- Because
inputis constrained to 50 or less, the invariant is clearly true at the beginning of the loop. - If our invariant and loop condition are both true, then
input < 50. Sinceinputcan increase by only one every time,input <= 50at the end of the iteration. Thus, the invariant remains true during an iteration. - If we exit the loop, then the invariant is true and the loop condition is
false. If
input <= 50is true butinput < 50is false, theninput = 50. This proves our assertion.
Loop invariants are hard to write because loops are very powerful. To illustrate why this is true, let's consider the following function:
fun collatz(input: u64): u64 {
let steps = 10000;
let min = input;
while (steps > 0) {
if (input % 2 == 0) {
input = input / 2
} else {
input = 3 * input + 1
};
min = if (input < min) input else min;
steps = steps - 1;
};
min
}By exhaustive search in existing research, we know that collatz on any 64-bit
integer will reach a minimum of 1 within a few thousand steps. However, putting
ensures result == 1; into the spec is not sufficient. To make the prover
work, we would have to write an inductive proof that the stopping time of every
64-bit input is less than 10,000, and add it as a loop invariant. No general
proof bounding stopping times exists at this time, though it may be possible to
find one for the restricted input size.
Though writing loop invariants can be hard, we can still use them to do some
pretty cool stuff. Let's say we write a utility function max that finds the
maximum value of a vector<u64>.
fun max(values: &vector<u64>): u64 {
let max = *vector::borrow(values, 0);
let index = 0;
while (index < vector::length(values)) {
let current = *vector::borrow(values, index);
max = if (current > max) current else max;
index = index + 1;
};
max
}Now, let's add the specification we want. Colloquially, given
values: vector<u64>, we want max to return a result such that every other
result >= value[i]. We can write this with a forall quantifier:
ensures forall i in 0..len(values): result >= values[i];We also need to make sure that our result is actually in the vector.
spec max {
ensures forall i in 0..len(values): result >= values[i];
ensures contains(values, result);
}Of course, this doesn't verify quite yet. We have to write a loop invariant! I would encourage readers to work through this one on their own, but here is one solution:
fun max(values: &vector<u64>): u64 {
let max = *vector::borrow(values, 0);
let index = 0;
while ({
spec {
invariant forall i in 0..index: max >= values[i];
invariant contains(values, max);
};
(index < vector::length(values))
}) {
let current = *vector::borrow(values, index);
max = if (current > max) current else max;
index = index + 1;
};
max
}Essentially, we hold the invariant that max holds the maximum of the sublist
seen so far. As in the specification, we also assert that max is actually in
the vector. Now with this invariant, our function gets verified properly.
There are a number of features in the Move specification language that this introduction does not yet cover. As time goes on, we expect to continue updating this resource with more examples—especially as the language itself continues to evolve. In the meantime, be sure to check out the official documentation for more details.
If you find any mistakes, see places for improvement, or want to add another section, issues and pull requests are more than welcome. We hope that this very practical tool for program verification becomes more accessible as Move becomes more prevalant.