常见问答 - sui prover 101

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]属性来指定场景。与功能规范不同，场景无需调用其所针对的函数，因为根本就没有这样的目标函数。

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 属性。