The Sui Move 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.

The prover module

The prover module is a spec-only module that provides the building blocks for writing specifications.

Function requires

The requires function is used to specify the conditions which are assumed to hold on the arguments of the function.

requires(shares_in.value() <= pool.shares.supply_value());

Function ensures

The ensures function is used to specify the conditions which must hold as an effect of the function call.

ensures(new_shares.mul(old_balance).lte(old_shares.mul(new_balance)));

Function asserts

The asserts function is used to specify conditions that must always hold.

asserts(shares_in.value() <= pool.shares.supply_value());

Macro old

The old macro is used to refer to the state of an object before the function call.

let old_pool = old!(pool);

Method to_int

The to_int method is used to convert a fixed-precision unsigned integer to an unbounded integer. Unbounded integers are only available while executing a specification.

let x = 10u64.to_int();

Method to_real