sui prover 101

Sui Prover 是什么

Sui Prover 是一种专为 Sui 区块链设计的智能合约语言，它在 Move 语言的基础上进行了扩展，强调安全性、可组合性和形式化验证。形式化证明在 Sui Move 中的应用主要是通过数学方法严格验证合约逻辑，确保其符合预期行为，避免漏洞。

为什么 Sui Move 适合形式化证明？

Sui Move 在设计时就考虑了形式化验证，具有以下特点：

基于线性类型（Linear Types）：资源（如代币）不能被复制或丢弃，确保资产安全。
显式所有权（Explicit Ownership）：所有权的转移必须显式声明，减少权限漏洞。
模块化设计：代码结构清晰，便于形式化建模。
静态验证支持：Move Prover（形式化验证工具）可直接集成到开发流程中。

安装

macos brew 安装

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

cargo 安装 >> 如果你的电脑没有cargo命令需要你安装rust开发套件参看rustup安装

cargo install --git https://github.com/asymptotic-code/sui-prover sui-prover

本地编译

git clone  https://github.com/asymptotic-code/sui-prover

切换到 sui-prover目录

argo build --release --bin sui-prover

更新 Move.toml 文件以使用隐式依赖项 Sui 验证器遵循了 Move.toml 文件中近期的惯例，即依赖隐式依赖项。因此，您需要移除对 Sui 和 MoveStdlib 的任何直接依赖关系。有关更多背景信息，请参阅此消息。 // 如果move.toml有这一行请删除:

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

如果您确实需要直接引用 Sui，请将相关规范放在单独的文件中。基本用法您可以在此处找到本指南中使用的完整示例：https://github.com/asymptotic-code/sui-kit/tree/main/examples/guide 要使用 Sui 验证器，您需要为您的智能合约编写规范。然后，Sui 验证器将尝试证明您的智能合约满足这些规范。示例让我们以一个简单的示例来说明一下，即一个简化版的 LP（流动性池）智能合约中的取款功能：

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)
}

为了验证取款功能是否正确，我们需要为其编写一份规范说明。该规范应描述该功能的预期行为。规范的结构规范通常具有以下结构：

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

    // 函数的参数所假定满足的条件
    let result = withdraw(pool, shares_in);

    // 作为函数调用的结果所必须满足的条件
    result
}

让我们来详细分析上述内容：该规范将定义一个新的函数withdraw_spec，它与withdraw函数具有相同的参数，并返回相同的类型。该函数通过 #[spec(prove)] 进行注解，以表明它是规范，并且将使用 Sui 验证器进行验证。规范函数的主体通常包括：首先，指定在函数参数上所假定成立的条件然后调用要验证的函数接着指定函数调用所产生的条件必须成立最后返回函数调用的结果示例规范让我们编写一个规范，说明在提取资金时股票的价格不应下降：

#[spec(prove)]
fun withdraw_spec<T>(pool: &mut Pool<T>, shares_in: Balance<LP<T>>): Balance<T> {
    
    requires(shares_in.value() <= pool.shares.supply_value());

    let old_pool = old!(pool);

    let result = withdraw(pool, shares_in);

    let old_balance = old_pool.balance.value().to_int();
    let new_balance = pool.balance.value().to_int();

    let old_shares = old_pool.shares.supply_value().to_int();
    let new_shares = pool.shares.supply_value().to_int();

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

    result
}

让我们来详细解读一下这个规范：我们明确了函数参数所必须满足的条件。要提取的股份数量必须小于或等于池中的总股份数量：

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

requires 是一个only-spec的关键字，用于指定函数参数所应满足的条件。我们将池的旧状态保存在old_pool中：

let old_pool = old!(pool);

我们称要验证的函数为：

let result = withdraw(pool, shares_in);

我们计算出旧余额和新余额以及各自的份额，并将它们转换为无界整数：

let old_balance = old_pool.balance.value().to_int();
let new_balance = pool.balance.value().to_int();

let old_shares = old_pool.shares.supply_value().to_int();
let new_shares = pool.shares.supply_value().to_int();

无界整数是一种仅在规范中定义的类型，它允许我们编写条件而无需担心溢出问题。这种类型仅在规范环境中可用。我们规定了作为函数调用效果所必须满足的条件。当提取资金时，股票的价格不应下降：

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

ensures 是一个仅用于规范的关键字，它指定了函数调用所产生的必须满足的条件。 mul 和 lte 是上述未受限制整数类型上的仅用于规范的运算符。最后，我们返回结果。运行 Sui 验证器要运行 Sui 验证器，您需要先安装并配置 Sui 验证器。从 move.toml 目录中运行以下命令即可运行 Sui 验证器：

sui-prover

使用幽灵变量 幽灵变量是一种用于声明仅在规范中使用的全局变量的方法。它们特别适用于在不同规范之间传递信息。以上述示例为例，接下来：添加一个功能，使其在进行大额取款时触发事件，然后添加一个幽灵变量来检查该事件是否正确触发。更新后的示例首先，让我们将事件触发功能添加到原始示例中：

module amm::simple_lp;

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

#[spec_only]
use prover::prover::{requires, ensures, asserts, old};
#[spec_only]
use prover::ghost::{declare_global, global};

public struct LP<phantom T> has drop {}

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

const LARGE_WITHDRAW_AMOUNT: u64 = 10000;

public struct LargeWithdrawEvent has copy, drop {}

fun emit_large_withdraw_event() {
    event::emit(LargeWithdrawEvent { });
}

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 shares_in_value = shares_in.value();

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

    pool.shares.decrease_supply(shares_in);

    if (shares_in_value >= LARGE_WITHDRAW_AMOUNT) {
        emit_large_withdraw_event();
    };

    pool.balance.split(balance_to_withdraw)
}

我们进行了以下更改：添加了事件模块，声明了LARGE_WITHDRAW_AMOUNT限制条件，添加了一个LargeWithdrawEvent结构体，添加了用于发出事件的event::emit函数。更新了规范现在，为了检查该事件是否正确发出，我们需要声明一个虚拟变量，并检查在事件发出后该变量是否被设置为真：首先，我们在规范的开头添加以下行来声明这个虚拟变量：

declare_global<LargeWithdrawEvent, bool>();

然后，我们检查在事件发出后该值是否已被设置为真。我们可以使用常规的 if 语句来实现这一点，而在规范中它会成为一个逻辑条件。

if (shares_in_value >= LARGE_WITHDRAW_AMOUNT) {
    ensures(*global<LargeWithdrawEvent, bool>());
};

最后，我们确保原始函数在触发事件时需要先设置幽灵变量：

requires(*global<LargeWithdrawEvent, bool>());

完整的代码如下所示。完整的示例以供参考以下是完整的示例供参考：

module amm::simple_lp;

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

#[spec_only]
use prover::prover::{requires, ensures, asserts, old};
#[spec_only]
use prover::ghost::{declare_global, global};

public struct LP<phantom T> has drop {}

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

const LARGE_WITHDRAW_AMOUNT: u64 = 10000;

public struct LargeWithdrawEvent has copy, drop {}

fun emit_large_withdraw_event() {
event::emit(LargeWithdrawEvent { });
requires(*global<LargeWithdrawEvent, bool>());
}

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 shares_in_value = shares_in.value();

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

    pool.shares.decrease_supply(shares_in);

    if (shares_in_value >= LARGE_WITHDRAW_AMOUNT) {
        emit_large_withdraw_event();
    };

    pool.balance.split(balance_to_withdraw)
}

// Verify that the price of the token is not decreased by withdrawing liquidity
#[spec(prove)]
fun withdraw_spec<T>(pool: &mut Pool<T>, shares_in: Balance<LP<T>>): Balance<T> {
requires(shares_in.value() <= pool.shares.supply_value());

    declare_global<LargeWithdrawEvent, bool>();

    let old_pool = old!(pool);
    let shares_in_value = shares_in.value();

    let result = withdraw(pool, shares_in);

    let old_balance = old_pool.balance.value().to_int();
    let new_balance = pool.balance.value().to_int();

    let old_shares = old_pool.shares.supply_value().to_int();
    let new_shares = pool.shares.supply_value().to_int();

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

    if (shares_in_value >= LARGE_WITHDRAW_AMOUNT) {
        ensures(*global<LargeWithdrawEvent, bool>());
    };

    result
}

`prover` 模块

prover 模块是一个仅包含规范内容的模块，它为编写规范提供了基础构建要素。

`requires`函数

requires 用于指定函数参数必须满足的前提条件。

#![allow(unused)]
fn main() {
requires(shares_in.value() <= pool.shares.supply_value());
}

`ensures` 函数

ensures 用于指定函数调用后必须满足的后置条件。

#![allow(unused)]
fn main() {
ensures(new_shares.mul(old_balance).lte(old_shares.mul(new_balance)));
}

`asserts`函数

asserts 用于指定必须始终成立的条件断言。

#![allow(unused)]
fn main() {
asserts(shares_in.value() <= pool.shares.supply_value());
}

`old` 宏函数

old 用于引用函数调用前对象的状态值。

#![allow(unused)]
fn main() {
let old_pool = old!(pool);
}

`to_int` 方法

to_int 将固定精度无符号整数转换为无界整数（仅在规范执行时可用）

#![allow(unused)]
fn main() {
let x = 10u64.to_int();
}

`to_real` 方法

to_real 将固定精度无符号整数转换为任意精度实数（用于检查舍入方向，仅在规范执行时可用）。

#![allow(unused)]
fn main() {
let x = 10u64.to_real();
}

幽灵变量(Ghost variables)

仅用于规范的全局变量，通过以下函数声明：这些变量是通过 ghost::declare_global 和 ghost:：declare_global_mut 函数来声明的：

#![allow(unused)]
fn main() {
ghost::declare_global_mut<Name, Type>();
}

该声明接受两个类型级别的参数：幽灵变量的名称及其实际类型。在大多数情况下，幽灵变量的类型级别名称要么是用户定义的类型，要么只是新声明的仅用于规范的结构体。例如：

#![allow(unused)]
fn main() {
public struct MyGhostVariableName {}
}

然后，这个“幽灵”变量就可以在“要求”、“保证”和“断言”函数中使用了：例如：

#![allow(unused)]
fn main() {
requires(ghost::global<MyGhostVariableName, _>() == true);
}

循环不变量(Loop invariant)

循环不变量是指在循环的所有迭代过程中都必须满足的条件。如果规格说明中包含了在循环内部会被修改的变量的相关条件，那么就必须指定循环不变量。该不变量是通过在循环之前调用invariant宏来指定的。

#![allow(unused)]
fn main() {
invariant!(|| {
    ensures(i <= n);
});
while (i < n) {
    i = i + 1;
}
}

Object `invariant`

对象不变性是指对于某一特定类型的所有对象而言，都必须满足的条件。通过创建一个名为 <type_name>_inv 的新函数，并在该函数上添加 #[spec_only] 标记，即可声明一个对象不变量。

#![allow(unused)]
fn main() {
#[spec_only]
public fun MyType_inv(self: &MyType): bool {
    ...
}
}

该函数必须接受一个参数，该参数是一个指向对象的引用，并返回一个布尔值，该值表示对象的不变性是否成立。

Attributes

`#[spec]` 作用在方法上

spec属性用于表明某个函数属于规范范畴。当spec属性赋值给名为<函数名称>_spec的函数时，移动证明器在验证调用<函数名称>的其他函数时，会使用该规格说明，而非原始函数。在这种情况下，spec 函数必须：

其名称与原始函数相同，但会在末尾添加_spec——若情况并非如此，则该spec仅用于检查特定场景（详情见下文）
与原始函数具有相同的签名
调用原始函数——根据规范返回的值通常就是原始函数所返回的值，但并非必须如此。

`#[spec]` as a spec of a scenario

#[spec] 属性可用于指定一个可由 Move 验证器进行验证的场景。在这种情况下，对 spec 函数的名称和签名没有限制。

`#[spec(prove)]`

#[spec(prove)] 这个属性用于指定一个函数是需要由 Move 验证器进行验证的规范。没有 prove 关键字的规范不会被验证器进行检查，但在作为其他函数证明的一部分被调用时，它会被使用——请参阅我们的常见问题解答中关于规范如何组合的说明。在规格说明/场景中添加focus属性（使用形式为 #[spec(prove, focus)]）会使验证者仅尝试验证此特定的规格说明。而focus属性还可同时用于多个规格说明。

`#[spec_only]`

与 test_only 类似，spec_only 使得任何带有注释的代码（模块、函数等）仅对证明者可见。该代码不会出现在常规编译过程中，也不会在测试模式下出现。

sui prover 提供了标准库

prover

module prover::prover;

#[spec_only]
native public fun requires(p: bool);
#[spec_only]
native public fun ensures(p: bool);
#[spec_only]
native public fun asserts(p: bool);
#[spec_only]
public macro fun invariant($invariants: ||) {
    invariant_begin();
    $invariants();
    invariant_end();
}

public fun implies(p: bool, q: bool): bool {
    !p || q
}

#[spec_only]
native public fun invariant_begin();
#[spec_only]
native public fun invariant_end();

#[spec_only]
native public fun val<T>(x: &T): T;
#[spec]
fun val_spec<T>(x: &T): T {
    let result = val(x);

    ensures(result == x);

    result
}

#[spec_only]
native public fun ref<T>(x: T): &T;
#[spec]
fun ref_spec<T>(x: T): &T {
    let old_x = val(&x);

    let result = ref(x);

    ensures(result == old_x);
    drop(old_x);

    result
}

#[spec_only]
native public fun drop<T>(x: T);
#[spec]
fun drop_spec<T>(x: T) {
    drop(x);
}

#[spec_only]
public macro fun old<$T>($x: &$T): &$T {
    ref(val($x))
}

#[spec_only]
native public fun fresh<T>(): T;
#[spec]
fun fresh_spec<T>(): T {
    fresh()
}

#[spec_only]
#[allow(unused)]
native fun type_inv<T>(x: &T): bool;

ghost

module prover::ghost;

#[spec_only]
use prover::prover;

#[spec_only]
public native fun global<T, U>(): &U;

#[spec_only]
public native fun set<T, U>(x: &U);

#[spec]
public fun set_spec<T, U>(x: &U) {
  declare_global_mut<T, U>();
  set<T, U>(x);
  prover::ensures(global<T, U>() == x);
}

#[spec_only]
public native fun borrow_mut<T, U>(): &mut U;

#[spec_only]
public native fun declare_global<T, U>();
#[spec_only]
public native fun declare_global_mut<T, U>();

#[spec_only]
#[allow(unused)]
native fun havoc_global<T, U>();

log

module prover::log;

#[spec_only]
public native fun text(x: vector<u8>);

#[spec_only]
public native fun var<T>(x: &T);

#[spec_only]
public native fun ghost<T, U>();

1.如何组合使用`spec`

Move Prover 将依据某个函数的spec来验证调用该函数的其他函数。

例如，如果有一个名为foo的函数会调用bar，并且我们还有针对bar函数的bar_spec规范，那么移动证明器将会利用bar_spec来验证foo。

使用 #[spec(prove)] 标记一个规范说明将促使证明者尝试对其进行证明。若省略 prove 属性，则证明者将依据该规范说明来验证其他函数，但不会尝试对其进行证明。

2. 如何让验证器专注于特定的规范呢？

在规格说明/场景中添加focus属性（使用#[spec(prove， focus)语法）会使验证者仅尝试验证此特定的规格说明。您可以同时为多个规格应用focus属性，这样验证者将在一次运行中尝试验证所有这些规格。

3.如何设定一个场景，而非针对某个特定功能来编写说明呢？

通过在不以_spec结尾且没有target属性的函数上使用#[spec]属性来指定场景。与功能规范不同，场景无需调用其所针对的函数，因为根本就没有这样的目标函数。

4.我该如何为位于不同模块中的一个函数编写说明文档呢？

target属性可用于指定所要使用的具体函数，而非依赖于_spec后缀。按照惯例，如果将名为 <function_name>_spec 的函数放在同一模块中，那么它将针对 <function_name> 进行操作。如果我们想要指定一个不在同一模块中的函数，可以使用target属性来指定所要指定的函数。例如，如果我们有一个名为foo的函数，并且想要编写一个具有不同名称的测试脚本，可以使用target属性来指定其目标为foo：

#![allow(unused)]
fn main() {
module 0x42::foo {
    public fun inc(x: u64): u64 {
        x + 1
    }
}

module 0x43::foo_spec {
    // ...

    #[spec(prove, target = foo::inc)]
    public fun this_is_not_inc_spec_yet_it_targets_inc(x: u64): u64 {
        let res = foo::inc(x);
        // ...
        res
    }
}

}

5. 在编写规范文档时，我该如何访问私有成员或函数呢？

这些规格只是普通的 Move 代码，因此无法访问私有成员或函数。但在某些情况下这是必要的，尤其是当为不同模块中的函数编写规格时。为绕过这一限制，您可以使用 #[spec_only] 来添加所需的获取器和其他访问函数。正如其名称所示，这些访问器仅对规格可见，并且不会包含在常规编译中。

6. 我该如何设定交易终止的条件呢？

在某些算术条件（例如溢出）以及 assert! 语句失败的情况下，事务会自动终止——详情请参阅终止与断言。函数的规格说明还必须详细阐述该函数在何种情况下会终止运行。这一内容是通过使用asserts函数来实现的。例如，如果我们有一个名为 foo 的函数，其会在 x 不小于 y 的情况下终止执行：

#![allow(unused)]
fn main() {
fun foo(x: u64, y: u64): u64 {
    assert!(x < y);
    x
}

}

我们可以为foo编写一个规范说明，其中明确指出foo只有在x小于y时才会停止运行：

#![allow(unused)]
fn main() {
#[spec(prove)]
fun foo_spec(x: u64, y: u64): u64 {
    asserts(x < y); // This is the condition under which foo aborts
    let res = foo(x, y);
    // ...
    res
}

}

请参见下文第 8 条，其中介绍了避免指定终止条件的一种方法。

7. 如何设定溢出中断条件呢？

规格说明必须明确指出一个功能终止运行的所有条件。请参考上述第 6 个问题中的示例，了解如何通过 assert! 语句来指定终止条件。下面，让我们以一个指定溢出中断条件的示例来进行探讨。假设我们有一个名为 add 的函数，它用于将两个 u64 类型的值相加：

#![allow(unused)]
fn main() {
fun add(x: u64, y: u64): u64 {
    x + y
}

}

可以为 add 函数编写一个规格说明，其中明确指出：如果 x 和 y 的和大于 u64 的最大值，则 add 函数将终止执行。

#![allow(unused)]
fn main() {
#[spec(prove)]
fun add_spec(x: u64, y: u64): u64 {
    asserts((x as u128) + (y as u128) <= u64::max_value!() as u128);
    let res = add(x, y);
    // ...
    res
}
}

请参见下文第 8 条，其中介绍了避免指定终止条件的一种方法。

8. 我该如何避免明确设定终止条件呢？?

ignore_abort注解允许我们省略对精确终止条件的明确说明：

#![allow(unused)]
fn main() {
#[spec(prove, ignore_abort)]
fun add_spec(x: u64, y: u64): u64 {
    let res = add(x, y);
    // ...
    res
}
}

9. 为什么我在添加`spec`时会出现编译错误？

这是一个棘手的问题。证明者需要对主 Move 编译流程以及stdlib和sui-framework进行修改，不幸的是，这目前使得规范无法与常规的 Move 代码很好地共存。正在与 Mysten 团队合作，将这些能够让您将规范保留在同一代码库中的更改向上推送到 Sui 的主仓库。与此同时，您需要创建一个新的包来存放这些证明文件，并使用目标机制来引用您的代码。

10. 我们如何避免在验证其他规格的过程中使用到那些规格本身呢？

默认情况下，在证明另一个规范的过程中使用函数的规范时，会采用该函数的规范。

#![allow(unused)]
fn main() {
fun foo(x: &mut u8) {
    *x = 70;
}

fun bar(x: &mut u8) {
    foo(x);
}

#[spec(prove, no_opaque)]
fun foo_spec(x: &mut u8) {
    foo(x);
}

#[spec(prove)]
fun bar_spec(x: &mut u8) {
    bar(x);

    ensures(x == 70); // ok
}
}

在上述示例中，对于 bar_spec 的证明将尝试将 foo_spec 用作 foo 的实现部分，除非存在 no_opaque 属性。

Cetus 简介（Sui 生态 DEX 及流动性协议）

Cetus 是 Sui区块链上的去中心化交易所（DEX）和流动性协议，专注于集中流动性做市商（CLMM）模型，类似于 Uniswap v3。 Sui的流动性基础设施，提供高效、低滑点的交易体验。

核心功能

集中流动性做市（CLMM）

允许流动性提供者（LPs）在特定价格区间内提供流动性，提高资金利用率（类似 Uniswap v3）。
相比传统 AMM（如 PancakeSwap），CLMM 能减少无常损失并提升资本效率。

定点数（Fixed-Point）运算

提供高精度的十进制计算，避免浮点数在区块链环境中的不稳定性。
适用于价格区间、手续费、流动性份额等 DeFi 关键计算。

安全的整数运算

防止溢出（Overflow）和下溢（Underflow），确保智能合约的安全性。
支持加减乘除、指数、开方等常见数学操作。

与 Cetus 协议深度集成

用于集中流动性做市（CLMM）的价格计算、滑点控制等核心逻辑。

使用场景

DEX 价格计算（如 Uniswap v3 风格的 CLMM）。
流动性池份额管理（计算 LP 代币的价值）。
交易手续费计算（精确到小数点后多位）。
任何需要高精度整数运算的 DeFi 或区块链应用。

如何集成？

[dependencies]
integer-mate = { git = "https://github.com/CetusProtocol/integer-mate" }

给 clmm_math

写形式化证明

给 tick_math

写形式化证明