The Sui Prover is a tool for verifying the correctness of Move smart contracts on the Sui blockchain. It is based on the Boogie verification engine and the Z3 SMT solver.

Installation

Install from brew

brew install asymptotic-code/sui-prover/sui-prover

Update Move.toml to use implicit dependencies

The Sui Prover relies on the recent convention for Move.toml to rely on implicit dependencies. So you need to remove any direct dependencies to Sui and MoveStdlib . See this message for more context.

// delete this line:
Sui = { git = "<https://github.com/MystenLabs/sui.git>", subdir = "crates/sui-framework/packages/sui-framework", rev = "framework/testnet", override = true }

If you do need to reference Sui directly, put the specs in a separate package.

Basic usage

<aside> 💡

You can find the complete example used in this guide here: https://github.com/asymptotic-code/sui-kit/tree/main/examples/guide

</aside>

To use the Sui Prover you need to write specifications for your smart contract. The Sui Prover will then attempt to prove that your smart contract satisfies these specifications.

Example

Let's consider a simple example, the withdraw function of a simplified LP (Liquidity Pool) smart contract:

module amm::simple_lp;

use sui::balance::{Balance, Supply, zero};

public struct LP<phantom T> has drop {}

public struct Pool<phantom T> has store {
    balance: Balance<T>,
    shares: Supply<LP<T>>,
}

public fun withdraw<T>(pool: &mut Pool<T>, shares_in: Balance<LP<T>>): Balance<T> {
    if (shares_in.value() == 0) {
        shares_in.destroy_zero();
        return zero()
    };

    let balance = pool.balance.value();
    let shares = pool.shares.supply_value();

    let balance_to_withdraw = (((shares_in.value() as u128) * (balance as u128)) / (shares as u128)) as u64;

    pool.shares.decrease_supply(shares_in);
    pool.balance.split(balance_to_withdraw)
}

To verify that the withdraw function is correct, we need to write a specification for it. The specification should describe the expected behavior of the function.

The structure of a specification

Specs usually have the following structure:

#[spec(prove)]
fun withdraw_spec<T>(pool: &mut Pool<T>, shares_in: Balance<LP<T>>): Balance<T> {

    // Conditions which are assumed to hold on the arguments of the function

    let result = withdraw(pool, shares_in);

    // Conditions which must hold as an effect of the function call

    result
}