[验证器]: prover-guide.md

Move 规范语言

版本 1.4

本文档描述了 Move 规范语言，它是 Move 语言的一个子集，支持 Move 程序行为的规范。在本文档中，我们将此 Move 子集简称为 MSL。

MSL 与 [Move Prover][PROVER] 协同工作，Move Prover 是一种可以静态验证 MSL 规范相对于 Move 程序正确性的工具。与传统的测试相比，MSL 的验证是详尽的，并且适用于 Move 模块或事务脚本的所有可能的输入和全局状态。同时，它足够快速和自动化，可以像在开发人员工作流程中使用测试一样使用（例如，用于持续集成中拉取请求的评估）。

虽然 Move 编程语言在这一点上是稳定的，但 MSL 所代表的子集应被认为是不断发展的。这对平台稳定性没有影响，因为 MSL 不在生产环境中运行，而是用于离线质量保证，并在不断改进以适应不断变化的目标。

本文档仅描述该语言；有关如何使用 Move prover 工具的信息，请参见 [此处][PROVER_USAGE]。读者应具备 Move 语言的基本知识，以及前置/后置条件规范的基本原则（例如，请参见 [本文][PRE_POST_REFERENCE]）。有关规范的示例，我们参考了嵌入规范的 [Diem 框架文档][FRAMEWORK]。

---

• 表达式
  • 类型系统
  • 命名
  • 运算符
  • 函数调用
  • 语句
  • 打包和解包
  • 量词
  • 选择运算符
  • 内置函数
  • 部分语义
• 规范
  • 分离规范
  • 编译指示和属性
    • 编译指示继承
    • 常规编译指示和属性
  • 前置和后置状态
  • 辅助函数
    • 未解释函数
    • 公理
  • Let 绑定
    • Aborts-If 条件
      • 带代码的 Aborts-If 条件
    • Aborts-With 条件
    • Requires 条件
    • Ensures 条件
    • Modifies 条件
    • Invariant 条件
      • 函数不变量
      • 结构体不变量
      • 全局不变量
        • 禁用不变量
        • 更新不变量
        • 隔离的全局不变量
        • 模块化验证和全局不变量
    • 代码中的 Assume 和 Assert 条件
      • 循环不变量
      • 引用前置状态
    • 规范变量
    • 模式
      • 基本模式用法
      • 模式表达式
      • 模式应用操作
    • 不透明规范
    • 抽象规范
    • 文档生成
• 表现力

---

表达式

MSL 中的表达式是 Move 程序表达式的子集，加上一组附加构造，如以下各节所述。

类型系统

MSL 的类型系统与 Move 的类型系统相似，但有以下区别：

• 整数类型有两种编码方式：num 和 bv（位向量）。 如果一个整数（无论是常量还是变量）没有直接或间接地参与任何按位运算，那么无论它在 Move 中的类型（u8、u16、u32、u64、u128 和 u256）如何，它都被视为相同的类型。在规范中，这种类型被称为 num，它是一种任意精度的 有符号 整数类型。 当 MSL 引用表示 u8 或类似类型的 Move 名称时，它会自动扩展为 num。这允许编写 MSL 表达式，例如 x + 1 <= MAX_U128 或 x - y >= 0，而无需担心溢出或下溢。 与 num 不同，bv 不能也不需要显式地在规范中使用：如果一个整数参与按位运算，例如 &、| 或 ^，它将在后端自动编码为 bv。 此外，bv 整数具有固定的精度，这与其在 Move 中的精度一致（bv8、bv16、bv32、bv64、bv128 和 bv256）。 请注意，通常在 SMT 求解器中使用 bv 不如 num 效率高。因此，prover 在使用按位运算时有一些限制，这将在下面详细说明。
• Move 类型 &T、&mut T 和 T 对于 MSL 被认为是等价的。相等性被解释为值相等。无需担心从 Move 程序中解引用：这些会根据需要自动解引用。这种简化是可能的，因为 MSL 无法修改 Move 程序中的值，并且该程序无法直接推断引用相等性（这消除了在 MSL 中执行此操作的需要）。（请注意，这也有一个表现力方面的限制，即对于 返回 &mut T 的函数，但是，这种情况在实践中很少遇到，并且有解决方法。）
• 还有一个附加类型 type，它是所有类型的类型。它只能在量词中使用。
• 还有一个附加类型 range，它表示整数范围（以及表示值的符号 n..m）。

命名

名称解析的工作方式与 Move 语言类似。use 声明可以为导入的名称引入别名。MSL 函数和变量名必须以小写字母开头。模式名称被视为类型，并且必须以大写字母开头（模式是一种新的命名构造，稍后会 讨论）。

Move 函数、MSL 函数、Move 类型和模式都共享相同的命名空间，因此如果通过 Move use 子句使用别名，则它们是明确的。由于公共命名空间，MSL 函数不能与 Move 函数具有相同的名称。这通常通过约定来处理，即在相关的 Move 函数被称为 has_access 时，MSL 函数以 spec_has_access 为前缀。

运算符

MSL 支持所有 Move 运算符，除了 &、&mut 和 *（解引用）。

除了现有运算符之外，还支持向量下标 v[i]、切片 v[i..j] 和范围构造 i..j（整数范围的类型是一种名为 range 的新内置类型）。此外，还支持布尔蕴含 p ==> q，它比 !p || q 更直观。

函数调用

在 MSL 表达式中，可以像在 Move 中一样调用函数。但是，被调用者必须是 MSL 函数 或 纯 Move 函数。

如果 Move 函数不修改全局状态，并且不使用 MSL 表达式中不支持的 Move 表达式功能（如此处定义），则认为它是纯函数。

有一个例外。如果 Move 函数定义包含直接的 assert，那么当从 MSL 表达式调用它时，这将将被忽略，并且该函数将被认为是纯函数。例如：

fun get(addr: address): &T { assert(exists<T>(addr), ERROR_CODE); borrow_global<T>(addr) }

这个函数是纯函数，可以从 MSL 表达式中调用。断言将被忽略，并且该函数将被解释为：

spec fun get(addr: address): T { global<T>(addr) }

这是合理的，因为 MSL 具有 部分语义。

语句

支持有限形式的序列 { let x = foo(); x + x }，以及 if-then-else。不支持 Move 语言的其他语句形式。

打包和解包

支持打包表达式。目前 不 支持解包表达式。

量词

支持全称量化和存在量化。一般形式是

forall <binding>, ..., <binding> [ where <exp> ] : <exp>
exists <binding>, ..., <binding> [ where <exp> ] : <exp>

• 绑定可以是 name: <type> 或 name in <exp> 的形式。对于第二种形式，表达式目前必须是 range 或向量。
• 可选约束 where <exp> 允许限制量化范围。forall x: T where p: q 等价于 forall x: T : p ==> q，exists x: T where p: q 等价于 exists x: T : p && q。

请注意，可以量化类型。例如：

forall t: type, addr: address where exists<R<t>>(addr): exists<T<t>>(addr)

选择运算符

选择运算符允许选择满足谓词的值：

choose a: address where exists<R>(a) && global<R>(a).value > 0

如果谓词不可满足，则选择的结果将是不确定的（请参见 部分语义 的讨论）。

选择运算符还有一种形式，用于从一组整数中选择 最小 值，例如：

choose min i: num where in_range(v, i) && v[i] == 2

类型转换运算符

在规范语言中，我们可以使用相同的语法 (e as T) 将表达式 e 与一个整数类型转换为另一种大小的整数类型 T。

移位运算符

移位运算符 << 和 >> 在规范语言中受支持，并且它们都具有与 Move 语言相同的语义。 至于中止，如果一个值 v 的宽度为 n，那么如果 m >= n，v << m 或 v >> m 将中止。

按位运算符

使用按位运算符 &、| 和 ^ 的 Move 程序可以在 prover 中进行验证，并且规范语言中也支持这些运算符。 由于编码和效率问题，使用按位运算符有更多的注意事项：

• 参与按位运算的整数在后端编码为 bv 类型，并且两种整数编码不兼容。例如，如果变量 v 参与按位运算，例如 v & 2 或 v = a ^ b，那么当它在算术运算 v * w 或移位运算 v << w 中使用时，w 将在 Move 程序中隐式转换为 bv 类型。 但是，规范语言不支持隐式类型转换，因此用户必须在规范中显式使用内置函数 int2bv：v << int2bv(w)。 请注意，由于每个 bv 类型都有一个固定的长度（从 8 到 256），因此类型为 num 的值无法转换为 bv。

• 验证 bv 类型效率不高，可能会导致超时。因此，用户可能更喜欢将按位运算与其他运算隔离，并在可能的情况下不使用 int2bv。此外，用户需要使用编译指示来显式指定哪些整数类型的函数参数或结构体字段将用于按位计算：

    struct C has drop {
        a: u64,
        b: u64
    }
    spec C {
        // C 的第二个字段 b 将是 bv 类型
        pragma bv=b"1";
    }
    public fun foo_generic<T>(i: T): T {
      i
    }

    spec foo_generic {
     // 如果 T 实例化为数字类型，则第一个参数将是 bv 类型
      pragma bv=b"0";
     // 如果 T 实例化为数字类型，则第一个返回值将是 bv 类型
      pragma bv_ret=b"0";
    }

    public fun test(i: C): u64 {
      let x1 = foo_generic(C.b);
      x1 ^ x1
    }

    spec test {
      // 显式类型转换对于生成正确的 boogie 程序是强制性的
      ensures result == (0 as u64);
    }

请注意，如果泛型函数或结构体的参数或字段使用指定为 bv 类型，那么当实例化的类型是整数类型时，它们将在函数的所有的实例或结构体中是 bv 类型。

• 向量和表中的整数类型的值可以编码为 bv 类型；目前，表中的索引和键不能是 bv 类型。使用其他类型将导致内部错误。

内置函数

MSL 支持许多内置常量和函数。其中大多数在 Move 语言中不可用：

• MAX_U8: num、MAX_U64: num、MAX_U128: num 返回相应类型的最大值。
• exists<T>(address): bool 如果资源 T 存在于地址，则返回 true。
• global<T>(address): T 返回地址处的资源值。
• len<T>(vector<T>): num 返回向量的长度。
• update<T>(vector<T>, num, T>): vector<T> 返回一个新向量，其中的元素在给定索引处被替换。
• vec<T>(): vector<T> 返回一个空向量。
• vec<T>(x): vector<T> 返回一个单例向量。
• concat<T>(vector<T>, vector<T>): vector<T> 返回参数的串联。
• contains<T>(vector<T>, T): bool 如果元素在向量中，则返回 true。
• index_of<T>(vector<T>, T): num 返回元素在向量中的索引，如果向量不包含该元素，则返回向量的长度。
• range<T>(vector<T>): range 返回向量的索引范围。
• in_range<T>(vector<T>, num): bool 如果数字在向量的索引范围内，则返回 true。
• in_range<T>(range, num): bool 如果数字在该范围内，则返回 true。
• update_field(S, F, T): S 更新结构体中的字段，保留其他字段的值，其中 S 是某个结构体，F 是 S 中字段的名称，T 是该字段的值。
• old(T): T 传递 Move 函数入口点参数的值。这在 ensures 后置条件、内联 spec 块（带有附加限制）和某些形式的不变量中是允许的，如稍后讨论的那样。
• TRACE(T): T 在语义上是恒等函数，并且会导致 prover 创建的错误消息中显示参数的值。
• int2bv(v) 显式地将整数 v 转换为其 bv 表示形式。
• bv2int(b) 显式地将 'bv' 整数 'b' 转换为 num 表示形式。但是，由于效率问题，不鼓励使用它。

内置函数存在于模块的未命名外部作用域中。如果模块定义了一个函数 len，那么此定义将隐藏相应的内置函数。为了在这种情况下访问内置函数，可以使用符号 ::len(v)。

部分语义

在 MSL 中，表达式具有部分语义。这与 Move 程序表达式形成对比，Move 程序表达式具有完全语义，因为它们要么传递一个值，要么中止。

依赖于某些变量 X 的表达式 e[X] 可能对 X 中变量的某些赋值具有已知的解释，而对其他赋值则未知。如果整体表达式结果不需要子表达式的值，则子表达式的未知解释不会引起问题。因此，我们说 y != 0 && x / y > 0 或 x / y > 0 && y != 0 无关紧要：布尔运算符是可交换的。

这个基本原则继承到更高级别的语言构造。例如，在规范中，以什么顺序提供条件并不重要：aborts_if y != 0; ensures result == x / y; 与 ensures result == x / y; aborts_if y != 0; 相同。同样，aborts_if P; aborts_if Q; 与 aborts_if Q || P 相同。

此外，部分语义原理继承到 规范辅助函数，它们的行为是透明的。具体来说，内联这些函数等同于调用它们（按表达式调用参数传递语义）。

规范

规范包含在所谓的 规范块（缩写为 spec 块）中，规范块可以作为模块成员和 Move 函数内部出现。各种类型的 spec 块如下所示，将在后续章节中讨论。

module M {
    resource struct Counter {
        value: u8,
    }

    public fun increment(a: address) acquires Counter {
        let r = borrow_global_mut<Counter>(a);
        spec {
            // 以此代码位置为目标的 spec 块
            ...
        };
        r.value = r.value + 1;
    }

    spec increment {
        // 以函数 increment 为目标的 spec 块
        ...
    }

    spec Counter {
        // 以结构体 Counter 为目标的 spec 块
        ...
    }

    spec schema Schema {
        // 声明模式的 spec 块
        ...
    }

    spec fun f(x: num): num {
        // 声明辅助函数的 spec 块
        ...
    }

    spec module {
        // 以整个模块为目标的 spec 块
        ...
    }
}

除了 Move 函数内部的 spec 块之外，spec 块的文本位置无关紧要。此外，可以多次重复结构体、函数或模块的 spec 块，从而累积内容。

分离规范

除了将规范放入与常规 Move 定义相同的模块中之外，还可以将它们放入单独的“规范”模块中，该模块可以位于相同或不同的文件中：

module M {
    ...
}
spec M {
    spec increment { .. }
}

规范模块的语法与常规模块的语法相同，但是，不允许使用 Move 函数和结构。

规范模块必须与它所针对的 Move 模块一起编译，并且不能单独编译和验证。

如果 Move 定义相距很远（例如，在不同的文件中），则可以使用此函数的签名来扩充 Move 函数的规范，以便为理解该规范提供足够的上下文。此语法在常规模块和规范模块中是可选启用的：

public fun increment(a: address) acquires Counter { .. }
...
spec increment(a: address) { .. }

编译指示和属性

编译指示和属性是一种通用机制，用于影响规范的解释。它们也是在新的概念成为主流语法的一部分之前尝试新概念的扩展点。在这里，我们将简要介绍它们的一般语法；各个实例将在稍后讨论。

编译指示的一般形式是：

spec .. {
    pragma <name> = <literal>;
}

属性的一般形式是：

spec .. {
    <directive> [<name> = <literal>] <content>; // ensures, aborts_if, include, etc..
}

<literal> 可以是 MSL（或 Move 语言）支持的任何值。值分配也可以省略，在这种情况下，将使用默认值。例如，通常使用 pragma option; 作为 pragma option = true; 的简写。

可以提供一个 pragma 或属性列表，而不是单个 pragma 或属性，例如 invariant [global, isolated] P。

编译指示继承

模块规约中的 pragma 设置一个值，该值适用于模块中的所有其他规约块。函数或结构体规约中的 pragma 可以覆盖函数或结构体的该值。此外，某些 pragma 的默认值可以通过 prover 配置来定义。

作为一个例子，我们来看一下 verify pragma。此 pragma 用于打开或关闭验证。

spec module {
    pragma verify = false; // 默认情况下，不验证此模块中的规约 ...
}

spec increment {
    pragma verify = true; // ... 但确实验证了此函数。
    ...
}

常规编译指示和属性

许多编译指示控制验证的一般行为。这些列在下表中。

名字	描述
verify	开启或关闭验证。
intrinsic	标记一个函数以跳过 Move 实现并使用 prover 原生实现。这使得一个函数的行为类似于原生函数，即使它在 Move 中不是这样。
timeout	设置函数或模块的超时时间（以秒为单位）。覆盖命令行标志提供的超时时间。
verify_duration_estimate	设置函数验证所需时间的估计值（以秒为单位）。如果配置的 timeout 小于此值，则将跳过验证。
seed	设置函数或模块的随机种子。覆盖命令行标志提供的种子。

以下属性控制着验证的一般行为：

名字	描述
[deactivated]	从验证中排除相关的条件。

前置和后置状态

规范块中的多个条件使用 前置 和 后置 状态，将它们相互关联。函数规范是其中的一个例子：在 ensures P 条件中，前置状态（在函数入口处）和后置状态（在函数出口处）通过谓词 P 相关联。但是，这个概念更通用，也适用于不变量，其中前置状态在全局更新之前，后置状态在全局更新之后。

在 前/后 状态处于活动状态的上下文中，表达式在前置状态中隐式计算。为了在前置状态中计算表达式，可以使用内置函数 old(exp)，它在前置状态中计算其参数并返回其值。重要的是要理解 exp 中的每个子表达式也在前置状态下计算，包括对辅助函数的调用。

这里所说的“状态”包括对全局资源内存的赋值，以及对类型为 &mut T 的函数的任何参数的赋值。例子：

fun increment(counter: &mut u64) { *counter = *counter + 1 }
spec increment {
   ensures counter == old(counter) + 1;
}

fun increment_R(addr: address) {
    let r =  borrow_global_mut<R>(addr);
    r.value = r.value + 1;
}
spec increment_R {
    ensures global<R>(addr).value == old(global<R>(addr).value) + 1;
}

辅助函数

MSL 允许定义辅助函数。然后可以在表达式中使用这些函数。

辅助函数使用以下语法定义：

spec fun exists_balance<Currency>(a: address): bool { exists<Balance<Currency>>(a) }

如示例所示，辅助函数可以是泛型的。此外，他们可以访问全局状态。

辅助函数的定义对于它们是否适用于 前置或后置状态 是中立的。它们在当前活动状态下进行评估。例如，为了查看前置状态中是否存在余额，可以使用 old(exists_balance<Currency>(a))。因此，不允许在辅助函数的定义中使用 old(..)表达式。

辅助函数是部分函数；请参阅 部分语义 的讨论。

未解释函数

可以通过简单地省略其主体将辅助函数定义为 未解释的 ：

spec fun something(x: num): num;

未解释的函数是指 prover 可以在给定的验证上下文中为其分配一些任意含义，只要它在该上下文中是一致的。未解释的函数是规范中抽象的有用工具（另请参见 此处）。

公理

可以使用 公理 进一步约束辅助函数的含义。目前，公理必须包含在模块 spec 块中：

spec module {
    axiom forall x: num: something(x) == x + 1;
}

应谨慎使用公理，因为它们可能会通过矛盾的假设在规范逻辑中引入不合理性。Move prover 支持通过 --check-inconsistency 标志来检测不合理性的冒烟测试。

Let 绑定

spec 块可以包含 let 绑定，这些绑定为表达式引入名称：

fun get_R(account: signer): R { ... }
spec get_R {
    let addr = signer::spec_address_of(account);
    aborts_if addr != ROOT;
    ensures result == global<R>(addr);
}

在具有前置和后置状态的 spec 块（例如函数规范）中，let name = e 形式将在前置状态中求值 e。为了在后置状态中计算表达式，可以使用 let post name = e。在这种形式的 rhs 表达式中，可以使用 old(..) 来引用前置状态。

Aborts-If 条件

aborts_if 条件是一个 spec 块成员，它只能出现在函数上下文中。它指定函数中止的条件。

在以下示例中，我们指定如果 Counter 资源在地址 a 处不存在，函数 increment 将中止（回想一下 a 是 increment 的参数的名称）。

spec increment {
    aborts_if !exists<Counter>(a);
}

如果一个函数有多个 aborts_if 条件，这些条件将相互或运算。组合中止条件（从每个单独的条件或运算）的评估取决于 pragma aborts_if_is_partial 的值。如果此值为 false（默认值），则函数 当且仅当 组合中止条件为真时才中止。在这种情况下，上面 increment 的中止规范将导致验证错误，因为在其他情况下 increment 可能会中止，即如果递增 Counter.value 会导致溢出。要解决此问题，可以像这样完成规范：

spec increment {
    pragma aborts_if_is_partial = false; // 这是默认值，但在此处添加以进行说明。
    aborts_if !exists<Counter>(a);
    aborts_if global<Counter>(a).value == 255;
}

如果 aborts_if_is_partial 的值为 true，则组合中止条件（或运算的单独条件）仅 暗示 函数中止。形式上，如果 A 是组合中止条件，那么对于 aborts_if_is_partial = true，我们有 A ==> function_aborts，否则我们有 A <==> function_aborts。因此，以下确实验证：

spec increment {
    pragma aborts_if_is_partial = true;
    aborts_if !exists<Counter>(a);
}

<a name="risk-aborts-if-is-partial"></a>

请注意，将 aborts_if_is_partial 设置为 true 存在一定的风险，最好的做法是在公共函数和事务脚本的规范一旦被认为是最终的，就避免使用它。这是因为在规约最终确定后更改代码可能会添加新的（非平凡的、不需要的）中止情况，这些中止情况是原始规约没有预料到的，但无论如何都将以静默方式通过验证。

如果未为函数指定任何中止条件，则中止行为未指定。该函数可能会或可能不会中止，并且验证不会引发任何错误，无论是否设置了 aborts_if_is_partial。为了说明函数永远不会中止，请使用 aborts_if false。可以使用 pragma aborts_if_is_strict 来更改此行为；这等效于好像已将 aborts_if false 添加到每个没有显式 aborts_if 子句的函数中。

带代码的 Aborts-If 条件

可以使用代码扩充 aborts_if 条件：

fun get_value(addr: address): u64 {
    aborts(exists<Counter>(addr), 3);
    borrow_global<Counter>(addr).value
}
spec get_value {
    aborts_if !exists<Counter>(addr) with 3;
}

如果上述函数在给定条件下没有以代码 3 中止，则这是一个验证错误。

为了指定直接 VM 中止，可以使用特殊常量 EXECUTION_FAILURE：

fun get(addr: address): &Counter acquires Counter {
    borrow_global<Counter>(addr)
}
spec get {
    aborts_if !exists<Counter>(addr) with EXECUTION_FAILURE;
}

此相同常量可用于所有其他 VM 失败（除以零、溢出等）。

Aborts-With 条件

aborts_with 条件允许指定函数可以在哪些代码下中止，与其条件无关。它类似于 Java 等语言中的“throws”子句。

fun get_one_off(addr: address): u64 {
    aborts(exists<Counter>(addr), 3);
    borrow_global<Counter>(addr).value - 1
}
spec get_one_off {
    aborts_with 3, EXECUTION_FAILURE;
}

如果该函数使用任何其他代码或不使用指定的代码中止，将产生验证错误。

aborts_with 条件可以与 aborts_if 条件结合使用。在这种情况下，aborts_with 指定除了 aborts_if 中给出的代码之外，该函数可能中止的任何其他代码：

spec get_one_off {
    aborts_if !exists<Counter>(addr) with 3;
    aborts_with EXECUTION_FAILURE;
}

如果不希望这样，并且 aborts_with 应该独立于 aborts_if，则可以使用属性 [check]：

spec get_one_off {
    aborts_if !exists<Counter>(addr) with 3;
    aborts_if global<Counter>(addr) == 0 with EXECUTION_FAILURE;

    aborts_with [check] 3, EXECUTION_FAILURE;
}

TODO: 目前不再实现 [check] 属性

Requires 条件

requires 条件是一个 spec 块成员，它假定了一个函数的前提条件。 对于调用时违反前提条件的函数，验证器将产生验证错误。

requires 不同于 aborts_if：在后一种情况下，可以调用该函数，并且它产生的任何 aborts 都将传播到调用者上下文中。 在 requires 情况下，验证器将不允许首先调用该函数。 然而，如果跳过验证，该函数仍然可以在运行时被调用。 因此，requires 在 Move 规范中很少见，而 aborts_if 更常见。 具体来说，对于公共 API，应避免使用 requires。

requires 的一个例子如下：

spec increment {
    requires global<Counter>(a).value < 255;
}

Ensures 条件

ensures 条件假定了一个函数的后置条件，该条件必须在该函数成功终止时（即不中止）得到满足。 验证器将为此验证每个 ensures。

ensures 条件的一个例子如下：

spec increment {
    ensures global<Counter>(a) == old(global<Counter>(a)) + 1;
}

在 ensures 条件的表达式中，可以使用 old 函数，如此处讨论。

Modifies 条件

modifies 条件用于为函数提供修改全局存储的权限。 该注解本身包含全局访问表达式的列表。 它专门与不透明函数规范一起使用。

resource struct S {
    x: u64
}

fun mutate_at(addr: address) acquires S {
    let s = borrow_global_mut<S>(addr);
    s.x = 2;
}
spec mutate_at {
    pragma opaque;
    modifies global<S>(addr);
}

通常，全局访问表达式的形式为 global<type_expr>(address_expr)。 地址值表达式在带注释函数的前置状态中进行评估。

fun read_at(addr: address): u64 acquires S {
    let s = borrow_global<S>(addr);
    s.x
}

fun mutate_S_test(addr1: address, addr2: address): bool acquires T {
    assert(addr1 != addr2, 43);
    let x = read_at(addr2);
    mutate_at(addr1); // 注意，我们正在修改与之前和之后读取的地址不同的地址
    x == read_at(addr2)
}
spec mutate_S_test {
    aborts_if addr1 == addr2;
    ensures result == true;
}

在函数 mutate_S_test 中，期望 spec 块中的断言成立。 mutate_at 上的 modifies 规范的一个好处是，无论是否内联 mutate_at，都可以证明该断言。

如果在函数上省略了 modifies 注解，则该函数被认为具有其在执行期间可能修改的资源的 所有 可能权限。 函数可能修改的所有资源的集合是通过代码的跨过程分析获得的。 在上面的例子中，mutate_S_test 没有 modifies 规范，并通过调用 mutate_at 修改资源 S。 因此，它被认为已经修改了任何可能地址的 S。 相反，如果程序员将 modifies global<S>(addr1) 添加到 mutate_S_test 的规范中，则会检查对 mutate_at 的调用，以确保授予 mutate_S_test 的修改权限涵盖了它授予 mutate_at 的权限。

Invariant 条件

invariant 条件可以应用于结构体和全局级别。

函数 Invariant

函数上的 invariant 条件只是一个 requires 和 ensures 的快捷方式，具有相同的谓词。

因此，以下 spec 块：

spec increment {
    invariant global<Counter>(a).value < 128;
}

...相当于：

spec increment {
    requires global<Counter>(a).value < 128;
    ensures global<Counter>(a).value < 128;
}

结构体 Invariant

当 invariant 条件应用于结构体时，它表达了结构体数据的良好形式属性。 当前未被修改的此结构体的任何实例都将满足此属性（以下概述的例外情况除外）。

例如，我们可以假定计数器的 invariant，使其永远不能超过 127 的值：

spec Counter {
    invariant value < 128;
}

每当构造（打包）结构体值时，验证器都会检查结构体 invariant。 当结构体被修改时（例如，通过 &mut Counter），invariant 不成立（但请参见下面的例外情况）。 通常，我们将修改视为隐式解包，将修改结束视为打包。

Move 语言语义明确地标识修改何时结束和开始的时间点。 这遵循 Move 的借用语义，并且包括通过封闭结构体的修改。 （内部结构体的修改在开始修改的根结构体的修改结束时结束。）

此规则有一个例外。 当对模块 M 中声明的结构体的可变引用传递到 M 的 公共 函数中时，该函数本身 不 返回任何其他可变引用（可以从输入参数借用），我们将此参数视为“已打包”。 这意味着，在函数入口处，我们将解包它，并在函数出口处再次打包，从而强制执行 invariant。 这反映在 Move 中，结构体数据只能在声明结构体的模块中修改，因此对于公共函数的外部调用者，除非再次调用模块 M 的公共函数，否则实际上无法修改可变引用。 这是对语义中利用的验证问题的一个重大简化。

全局 Invariant

全局不变式显示为模块的成员。 它可以表达 Move 程序的全局状态的条件，如内存中存储的资源所表示。 例如，下面的 invariant 声明存储在任何给定地址的 Counter 资源永远不能为零：

module M {
    invariant forall a: addr where exists<Counter>(a): global<Counter>(a).value > 0;
}

当从全局状态读取数据时，假定全局 invariant 成立，并在更新状态时断言（并且可能无法验证）（并可能无法验证）。 例如，下面的函数永远不会因算术下溢而中止，因为计数器值始终大于零；但是，它会创建一个验证错误，因为计数器可以降至零：

fun decrement_ad(addr: address) acquires Counter {
    let counter = borrow_global_mut<Counter>(addr);
    let new_value = counter.value - 1;   // 不会中止，因为 counter.value > 0
    *counter.value = new_value;          // 验证失败，因为 value 可以降至零
}

禁用 Invariant

有时，全局 invariant 几乎在所有地方都成立，除了函数内部的短暂间隔。 在当前的 move 代码中，这通常发生在设置某些东西（例如，帐户）并且将几个结构体一起发布时。 几乎在所有地方，都有一个 invariant 成立，即所有结构体都已发布，或者都没有发布。 但是，发布结构体的代码必须按顺序执行。 在发布它们时，将存在一些已发布而另一些未发布的情况。

为了验证除了在小区域内成立的 invariant，有一种功能允许用户临时禁用 invariant。 考虑以下代码片段：

fn setup() {
    publish1();
    publish2();
    }
}

其中 publish1 和 publish2 在地址 a 处发布两个不同的结构体 T1 和 T2。

module M {
    invariant [global] exists<T1>(a) == exists<T2>(a)
}

按照编写方式，验证器将报告在调用 publish1 之后和调用 publish2 之前违规了 invariant。 如果 publish1 或 publish2 中任何一个没有另一个，则验证器还将报告违反了该 invariant。

默认情况下，在触摸全局 invariant 中提到的资源的指令 I 之后立即检查全局 invariant。 [suspendable] 属性（在 invariant 侧）与两个编译指示（在函数 spec 块中指定）一起提供了对我们希望检查此 invariant 的位置的细粒度控制：

• disable_invariants_in_body：将在 I 所在的函数的末尾检查 invariant。
• delegate_invariants_to_caller：将由 I 所在的函数的所有调用者检查 invariant。

对于上面的示例，我们可以添加编译指示 disable_invariants_in_body：

spec setup {
    pragma disable_invariants_in_body;
}

这意味着在 setup 正在执行时不需要保持 invariant，但假定 invariant 在进入和退出 setup 时成立。

此编译指示更改了验证器的行为。 假定 invariant 在进入 setup 时成立，但在 publish1 和 publish2 期间或之后未得到证明。 相反，在 setup 的主体中可能无效的所有 invariant 都在从 setup 返回时断言和证明。 此处理的一个结果是，用户可能需要在 publish1 和 publish2 上提供更强的后置条件，以便能够证明从 setup 退出时的 invariant。

此处理的另一个结果是，不能安全地假定 invariant 在 publish1 和 publish2 的执行期间成立（除非 setup 的主体中没有任何内容更改 invariant 中提到的状态）。 因此，如果证明后置条件需要假定 invariant 成立，则后置条件将失败。

在示例中，invariant 在 setup 的调用站点成立，但在主体中不成立。 对于 publish1，invariant 不一定在调用站点 或 函数的主体中成立。 在示例中，隐含了此行为，因为 publish1 在 invariant 被禁用的上下文中调用。

当在上面的示例中禁用 setup 中的 invariant 时，验证器无法假定它们在进入 publish1 和 publish2 时成立，并且不应尝试在从这些函数退出时证明它们。 验证器对于由 publish1 或 publish2 调用的任何函数都将具有相同的行为。 当在调用函数中禁用 invariant 时，验证器 自动 采用此行为，但是用户可以声明将函数视为 publish1。

例如，如果 publish2 仅 从上面的设置函数调用，并且我们 没有 在 setup 中禁用 invariant，我们可以通过使用编译指示 delegate_invariants_to_caller 来实现类似的效果。

spec setup {
    pragma delegate_invariants_to_caller;
}

只有当 setup 是私有或 public (friend) 函数时，这才是合法的。 这与禁用 setup 中的 invariant 的区别在于，invariant 不会在 setup 的开头假定，而是在 setup 返回后在调用它的每个站点上进行证明。

虽然两个编译指示都禁用函数主体中的 invariant，但区别在于 disable_invariants_in_body 在条目中断言 invariant 并在存在时证明它们，而 delegate_invariants_to_caller 则不执行任何操作。

对于这些编译指示的使用方式存在一些限制。 不能为 invariant 委托给调用者的函数声明 disable_invariants_in_body，无论是通过编译指示显式委托还是因为在禁用 invariant 的上下文中调用了该函数。 （此限制是为了确保一致的处理，因为在调用上下文中假定 invariant 成立的一个编译指示，而另一个则不成立）。 其次，公共或脚本函数将其 invariant 检查委托给其调用者是非法的（因为验证器不知道所有调用站点），除非 该函数不可能使 invariant 无效，因为它不会更改出现在 invariant 中的 exists 和 global 表达式中提到的任何状态。

更新 Invariant

全局 invariant 的 update 形式允许表达全局状态更新的前置状态和后置状态之间的关系。 例如，以下 invariant 声明计数器每当更新时都必须单调递减：

module M {
    invariant update [global] forall a: addr where old(exists<Counter>(a)) && exists<Counter>(addr):
        global<Counter>(a).value <= old(global<Counter>(a));
}

隔离的全局 Invariant

全局 invariant 可以标记为 [isolated]，以指示它与证明程序的其他属性无关。 读取相关全局状态时，不会假定隔离的全局 invariant。 仅会在更新状态之前假定它，以帮助证明更新后 invariant 仍然成立。 此功能用于提高在存在许多全局invariant 但对验证没有直接影响的情况下提高性能。

模块化验证和全局 Invariant

全局 invariant 的某些用法会导致无法以模块化方式检查的验证问题。 “模块化”在此处意味着可以独立验证模块，并证明在所有使用上下文中普遍正确（如果满足前提条件）。

如果全局 invariant 引用多个模块的状态，则可能出现非模块化验证问题。 考虑模块 M1 使用模块 M2 的情况，并且 M1 包含以下 invariant，辅助函数 condition 引用每个相应模块的全局状态：

module M1 {
    invariant M1::condition() ==> M2::condition();
}

当我们独立验证 M1 时，Move 验证器将确定它还需要验证 M2 中的函数，即那些更新 M2 内存以使 M1 中的 invariant 可能失败的函数。

TODO：记录用于延迟代码段的 invariant 验证的机制和编译指示

代码中的 Assume 和 Assert 条件

spec 块也可能出现在任何可以出现普通 Move 语句块的地方。 这是一个例子：

fun simple1(x: u64, y: u64) {
    let z;
    y = x;
    z = x + y;
    spec {
        assert x == y;
        assert z == 2*x;
    }
}

在此类内联 spec 块中，仅允许一部分条件：

• assume 和 assert 语句允许在任何代码位置
• loop invariant 语句仅允许在表示loop 标头的代码位置。

spec 块中的 assert 语句指示控制到达该块时必须成立的条件。 如果条件不成立，Move Prover 将报告错误。 另一方面，assume 语句会阻止违反该语句中条件的执行。 下面显示的函数 simple2 由 Move Prover 验证。 但是，如果删除包含 assume 语句的第一个 spec 块，则 Move Prover 将显示违反第二个 spec 块中的 assert 语句。

fun simple2(x: u64, y: u64) {
    let z: u64;
    spec {
        assume x > y;
    };
    z = x + y;
    spec {
        assert z > 2*y;
    }
}

Loop Invariant

invariant 语句编码一个循环不变式，并且必须放置在循环头中，如以下示例所示。

fun simple3(n: u64) {
    let x = 0
    loop {
        spec {
            invariant x <= n;
        };
        if (x < n) {
            x = x + 1
        } else {
            break
        }
    };
    spec {
        assert x == n;
    }
}

循环不变式被转换为两个 assert 语句和一个 assume 语句，以方便对循环的属性进行归纳推理。 分解后，循环不变式转换为：

• assert 语句，用于检查在执行过程中第一次遇到循环时 invariant 是否成立 - 建立基本情况。
• assume 语句，用于编码 invariant 在循环迭代 I 时成立的属性。
• assert 语句，用于检查 invariant 是否在循环迭代 I+1 时继续成立。

引用前置状态

有时，我们希望在内联 spec 块中引用一个可变函数参数的前置状态。 在 MSL 中，可以使用 old(T) 表达式来完成。 与后置条件中 old(..) 的语义类似，assume 或 assert 语句中的 old(T) 表达式总是产出函数入口点处 T 的值。 以下是一个说明在内联 spec 块中使用 old(..) 的示例。

fun swap(x: &mut u64, y: &mut u64) {
    let t = *x;
    *x = *y;
    *y = t;
    spec {
        assert x == old(y);
        assert y == old(x);
    };
}

上面的示例很简单，因为可以使用后置条件(即，ensures)来表达相同的属性。 但是，在某些情况下，我们必须使用 old(..) 来引用前置状态，尤其是在loop invariant 的规范中。 考虑以下示例，我们验证 vector_reverse 函数是否正确地反转了向量中所有元素的顺序：

fun verify_reverse<Element>(v: &mut vector<Element>) {
    let vlen = vector::length(v);
    if (vlen == 0) return ();

    let front_index = 0;
    let back_index = vlen -1;
    while ({
        spec {
            assert front_index + back_index == vlen - 1;
            assert forall i in 0..front_index: v[i] == old(v)[vlen-1-i];
            assert forall i in 0..front_index: v[vlen-1-i] == old(v)[i];
            assert forall j in front_index..back_index+1: v[j] == old(v)[j];
            assert len(v) == vlen;
        };
        (front_index < back_index)
    }) {
        vector::swap(v, front_index, back_index);
        front_index = front_index + 1;
        back_index = back_index - 1;
    };
}
spec verify_reverse {
    aborts_if false;
    ensures forall i in 0..len(v): v[i] == old(v)[len(v)-1-i];
}

注意 loop invariant 中 old(v) 的用法。 如果没有它们，很难表达向量在循环迭代时部分反转而其余部分保持不变的 invariant。

但是，与 ensures 条件中的 old(T) 表达式(其中 T 可以是任何有效的表达式，例如，允许 old(v[i]))不同，assert 和 assumes 语句中的 old(T) 表达式仅接受单个变量作为 T，并且该变量必须是可变引用类型的函数参数。 在上面的示例中，不允许使用 old(v[i])，我们应该使用 old(v)[i]。

规范变量

MSL 支持 规范变量，在验证社区中也称为幽灵变量。 这些变量仅在规范中使用，并表示从资源全局状态派生的信息。 一个用例是计算系统中所有可用 coin 的总和，并指定该总和只能在某些情况下更改。

我们通过引入一个规范变量来说明此功能，该变量从我们正在运行的示例中维护所有 Counter 资源的总和。 首先，通过 spec 模块块引入一个规范变量，如下所示：

spec module {
    global sum_of_counters: num;
}

每当打包或解包 Counter 时，都会更新此值。 （回想一下，修改被解释为隐式解包和打包）：

spec Counter {
    invariant pack sum_of_counters = sum_of_counters + value;
    invariant unpack sum_of_counters = sum_of_counters - value;
}

TODO: 目前未实现 invariant pack 和 invariant unpack

现在，例如，我们可能想要指定全局状态中所有 Counter 实例的总和永远不应超过特定值。 我们可以这样做：

spec module {
    invariant [global] sum_of_counters < 4711;
}

请注意，规范变量也可以从辅助函数引用。 此外，规范变量可以是泛型的：

spec module {
    global some_generic_var<T>: num;
}

使用此类规范变量时，需要提供类型参数，如 some_generic_var<u64> 中所示。 实际上，泛型规范变量就像由类型索引的变量族。

Schema

Schema 是一种通过将属性组合在一起来构造规范的方法。 从语义上讲，它们只是语法糖，可以扩展到functions、struct 或模块上的条件。

基本 Schema 用法

Schema 的用法如下：

spec schema IncrementAborts {
    a: address;
    aborts_if !exists<Counter>(a);
    aborts_if global<Counter>(a).value == 255;
}

spec increment {
    include IncrementAborts;
}

每个 Schema 都可以声明多个类型化的变量名和这些变量上的条件列表。 所有支持的条件类型都可以在 Schema 中使用。 然后 schema 可以包含在另一个 spec 块中：

• 如果该 spec 块用于 function 或 struct，则 schema 声明的所有变量名都必须与上下文中兼容类型的现有名称匹配。
• 如果 schema 包含在另一个 schema 中，则现有名称将匹配，并且必须具有相同的类型，但不存在的名称将作为新声明添加到包含上下文中。

当 schema 包含在另一个 spec 块中时，将检查它包含的条件是否允许在此块中。 例如，将 schema IncrementAborts 包含到 struct spec 块中将导致编译时错误。

当包含 schema 时，它声明的名称也可以通过表达式绑定。 例如，可以编写 include IncrementAborts{a: some_helper_address()}。 实际上，如果不提供绑定，则等效于编写 IncrementAborts{a: a}，如果 a 是范围内的现有名称。

Schema 可以是泛型的。 泛型 schema 必须在包含它们的地方完全实例化；类型推断不适用于 schema。

Schema 表达式

包含 schema 时，可以使用一组有限的布尔运算符，如下所示：

• P ==> SchemaExp：schema 中的所有条件都将以 P ==> .. 为前缀。 不基于布尔表达式的条件将被拒绝。
• if (P) SchemaExp1 else SchemaExp2：这被视为类似于同时包含 P ==> SchemaExp1 和 !P ==> SchemaExp2。
• SchemaExp1 && SchemaExp2：这被视为两个包含用于两个 schema 表达式。

Schema 应用操作

Schema 的主要用例之一是能够命名一组属性，然后将这些属性应用于一组 functions。 这是通过 apply 运算符实现的。 apply spec 块成员只能出现在 module spec 块中。

apply 运算符的一般形式是 apply Schema to FunctionPattern, .. except FunctionPattern, ..。 此处，Schema 可以是 schema 名称或 schema 名称加上形式类型参数。 FunctionPatterns 由一个可选的可见性修饰符 public 或 internal 组成（如果未提供，则两种可见性都将匹配），一个 shell 文件样式的名称模式（例如 *, foo*, foo*bar 等），最后是一个可选的类型参数列表。 提供给 Schema 的所有类型参数必须绑定在此列表中，反之亦然。

apply 运算符将给定的 schema 包含在所有与模式匹配的 function spec 块中，除了那些通过 except 模式排除的 function spec 块。

apply 运算符的典型用途是为带有某些异常的模块中的所有函数提供通用的前置条件和后置条件。 例子：

spec schema Unchanged {
    let resource = global<R>(ADDR):
    ensures resource == old(resource);
}

spec module {
    // 对所有函数强制执行 Unchanged，但 initialize 函数除外。
    apply Unchanged to * except initialize;
}

请注意，虽然我们可以使用全局 invariant来表达类似的事情，但我们 无法 表达将 invariant 限制为仅特定函数。

不透明规范

使用编译指示 opaque，声明一个函数仅由其在调用者侧的规范定义。 相反，如果未提供此编译指示，则函数的实现将用作验证调用者的基础。

使用 opaque 需要规范对于手头的验证问题来说足够完整。 如果没有 opaque，Move 验证器将使用该实现作为函数定义的真相来源。 但是使用 opaque，如果函数的定义有未指定的方面，将假定任意含义。 例如，使用下面的规范，increment 函数可以在任意条件下中止：

spec increment {
    pragma opaque;
    // aborts_if !exists<Counter>(a);  // 我们需要添加此内容，以使函数不会任意中止
    ensures global<Counter>(a) == old(global<Counter>(a)) + 1;
}

通常，不透明函数可以实现模块化验证，因为它们从函数的实现中抽象出来，从而可以更快地进行验证。

如果一个不透明函数修改了状态，建议在其规范中使用modifies 条件。 如果省略此条件，则状态更改的验证将失败。

抽象规范

[abstract] 属性允许指定一个函数，以便在调用者侧使用与实际实现不同的抽象语义。 如果实现太复杂而无法进行验证，并且抽象语义足以满足验证目标，这将非常有用。 反过来，[concrete] 属性允许仍然指定针对实现进行验证，但未在调用者侧使用的条件。

考虑以下哈希函数的示例。 哈希的实际值与验证调用者无关，我们使用一个未解释的辅助函数，该函数传递一个由验证器选择的任意值。 我们仍然可以指定具体的实现并验证其正确性：

fun hash(v: vector<u8>): u64 {
    <<sum up values>>(v)
}
spec hash {
    pragma opaque;
    aborts_if false;
    ensures [concrete] result == <<sum up values>>(v);
    ensures [abstract] result == spec_hash_abstract(v);
}
spec fun abstract_hash(v: vector<u8>): u64; // 未解释的函数

抽象的可靠性由指定者负责，而不是由验证器验证。

注意：抽象/具体属性应仅与不透明规范一起使用，但如果不是，验证器目前不会生成错误。

注意：modifies 子句当前不支持抽象/具体。 此外，如果没有给出修改，也会从实现中计算出修改后的状态，这可能会与 [abstract] 属性冲突。

文档生成

文件中规范块的组织与文档生成相关——即使它对于语义无关紧要。 参见规范块的组织的讨论。

表达能力

Move 规范语言具有足够的表达能力来表示完整的 Move 语言语义（正式论证未决），但有一个例外：返回 &mut T 类型的函数。

考虑以下代码：

struct S { x: u64, y: u64 }

fun x_or_y(b: bool, s: &mut S): &mut u64 {
    if (b) &mut s.x else &mut s.y
}
spec x_or_y {
    ensures b ==> result == s.x;
    ensures !b ==> result == s.y;
}

我们无法在 MSL 中指定 x_or_y 的 完整 语义，因为我们无法捕获可变引用的语义。 虽然我们可以说出函数退出时引用后面的值，但无法指定后续效果，如 *x_or_y(b, &mut s) = 2。

但是，Move 验证器 确实 理解这种函数的含义——限制仅在于我们可以指定的内容。 实际上，这意味着我们无法使函数 x_or_y 不透明，并且必须让验证依赖于验证器直接使用实现。 具体来说，我们可以验证以下内容 （然后可以将其设置为不透明）：

fun x_or_y_test(s: S): S {
    *x_or_y(true, &mut s) = 2;
    s
}
spec x_or_y_test {
    pragma opaque;
    ensures result.x == 2;
    ensures result.y == s.y;
}

• 原文链接： github.com/move-language...
• 登链社区 AI 助手，为大家转译优秀英文文章，如有翻译不通的地方，还请包涵～