understand3

搜索

SearchSearch

第十九章 Move 证明器

2024年11月19日11分钟阅读

1. 概述

Move 证明器支持对 Move 代码进行正式的规范与验证。Move 证明器可以自动验证 Move 智能合约的逻辑属性，同时提供类似于类型检查器或代码检查工具的用户体验。

Move 证明器的存在旨在使合约更具可信度；它：

  • 保护由 Aptos 区块链管理的大量资产免受智能合约漏洞的影响
  • 防范资源丰富的对手
  • 预期合理的监管审查和合规要求
  • 允许具有数学背景但不一定具有软件工程背景的领域专家理解智能合约的作用

更多信息，请参考以下文档：

2. 用户指南

这是 Move 证明器的用户指南。此文档与 Move 规范语言配套。详情请参阅以下各节。

2.1 运行 Move 证明器

Move 证明器通过 Aptos CLI 调用。为了调用 CLI，您必须有一个 Move 包就位。在最简单的情况下，Move 包由一个目录定义，其中包含一组 .move 文件和一个名为 Move.toml 的清单。您可以通过运行以下命令在给定位置创建一个新的 Move 包：aptos move init --name <名称>

一旦包存在，从要测试的目录调用 Move 证明器或通过将其路径提供给 —package-dir 参数：

证明当前目录中包的源文件：

aptos move prove

证明特定目录中包的源文件：

aptos move prove --package-dir <路径>

在“使用 Aptos CLI 进行 Move 证明”部分查看示例输出和其他可用选项。

2.2 目标筛选

默认情况下，aptos move prove 命令会验证包的所有文件。在较大包的迭代开发过程中，使用 -f (--filter) 选项将验证集中在特定文件上通常更有效，如下所示：

aptos move prove -f coin

通常，如果提供给 -f 选项的字符串包含在源文件的文件名中的某个位置，则该源文件将包含在验证中。

注意

Move 证明器确保逐个验证模块或一次验证所有模块之间没有语义差异。但是，如果您的目标是验证所有模块，在单个 aptos move prove 运行中验证它们将比顺序验证快得多。

2.3 证明器选项

Move 证明器有许多选项（如上述筛选选项），您可以通过调用：aptos move prove <选项> 来传递。最常用的选项是 -t（--trace）选项，当 Move 证明器遇到错误时，它会生成更丰富的诊断：

aptos move prove -f coin -t

要查看所有命令行选项的列表，请运行：

aptos move prove --help

2.4 证明器配置文件

您还可以创建一个名为 Prover.toml 的 Move 证明器配置文件，该文件与 Move.toml 清单文件一起位于包目录的根目录中。例如，要为包默认启用跟踪，添加一个具有以下配置的 Prover.toml 文件：

[prover]
auto_trace_level = "VerifiedFunction"

在下面的示例 .toml 中找到最常用的选项，您可以根据需要剪切、粘贴和采用（根据显示的值调整默认值）：

# 详细程度级别
# 可能的值："ERROR"、"WARN"、"INFO"、"DEBUG"。每个级别包含前一个级别的输出。
verbosity_level = "INFO"
 
[prover]
# 设置自动跟踪级别，增强 Move 证明器在验证错误时产生的诊断。
# 可能的值："Off"、"VerifiedFunction"、"AllFunctions"
auto_trace_level = "Off"
 
# 要报告的诊断的最小严重程度级别。
# 可能的值："Error"、"Warning"、"Note"
report_severity = "Warning"
 
[backend]
# 求解器后端的超时（秒）。请注意，这是一个软超时，可能并不总是被遵守。
vc_timeout = 40
 
# 求解器后端的随机种子。不同的种子可能导致不同的验证运行时间，因为求解器使用启发式方法。
random_seed = 1
 
# 假设用于并发检查验证条件的处理器核心数量。
proc_cores = 4

提示：对于本地验证，您可能希望将 proc_cores 设置为一个激进的数字（您的实际核心数）以加快周转周期。

2.5 证明器诊断

当 Move 证明器发现验证错误时，它会以类似于编译器或调试器的样式将诊断打印到标准输出。我们根据以下不断演变的示例解释不同类型的诊断：

module 0x42::m {
  struct Counter has key {
    value: u8,
  }
 
  public fun increment(a: address) acquires Counter {
    let r = borrow_global_mut<Counter>(a);
    r.value = r.value + 1;
  }
 
  spec increment {
    aborts_if!exists<Counter>(a);
    ensures global<Counter>(a).value == old(global<Counter>(a)).value + 1;
  }
}

我们将在演示不同类型的诊断时修改此示例。

2.6 意外中止

如果我们立即对上述示例运行 Move 证明器，我们会得到以下错误：

error: abort not covered by any of the `aborts_if` clauses
   ┌─ m.move:11:5
   │
 8 │           r.value = r.value + 1;
   │                             - abort happened here with execution failure
   ·
11 │ ╭     spec increment {
12 │ │         aborts_if!exists<Counter>(a);
13 │ │         ensures global<Counter>(a).value == old(global<Counter>(a)).value + 1;
14 │ │     }
   │ ╰─────^
   │
   =     at m.move:6: increment
   =         a = 0x29
   =     at m.move:7: increment
   =         r = &mmm.Counter{value = 255u8}
   =     at m.move:8: increment
   =         ABORTED
 
{
  "Error": "Move Prover failed: exiting with verification errors"
}

Move 证明器生成了一个示例计数器，当对 u8 的值 255 加 1 时会导致溢出。如果函数规范要求中止行为，但函数中止的条件未被规范涵盖，则会发生这种溢出。实际上，使用 aborts_if!exists<Counter>(a)，我们仅涵盖了由于资源不存在导致的中止，而不是由于算术溢出导致的中止。

让我们修复上述问题并添加以下条件：

module 0x42::m {
  spec increment {
    aborts_if global<Counter>(a).value == 255;
    //...
  }
}

这样，Move 证明器将成功运行，没有任何错误。

2.7 后置条件失败

让我们在上述示例的 ensures 条件中注入一个错误：

module 0x42::m {
  spec increment {
    ensures global<Counter>(a).value == /*old*/(global<Counter>(a).value) + 1;
  }
}

这样，Move 证明器将产生以下诊断：

error: post-condition does not hold
   ┌─ m.move:14:9
   │
14 │         ensures global<Counter>(a).value == /*old*/(global<Counter>(a).value) + 1;
   │         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
   │
   =     at m.move:6: increment
   =         a = 0x29
   =     at m.move:7: increment
   =         r = &mmm.Counter{value = 0u8}
   =     at m.move:8: increment
   =     at m.move:9: increment
   =     at m.move:12: increment (spec)
   =     at m.move:15: increment (spec)
   =     at m.move:13: increment (spec)
   =     at m.move:14: increment (spec)
 
{
  "Error": "Move Prover failed: exiting with verification errors"
}

虽然我们知道错误是什么（因为我们刚刚注入了它），但在输出中这并不是特别明显。这是因为我们没有直接看到 ensures 条件实际上是在哪些值上进行评估的。要查看此内容，请使用 -t (--trace) 选项；此选项默认未启用，因为它会使求解器的验证问题稍微困难一些。

除了 --trace 选项之外，您还可以在条件中使用内置函数 TRACE(exp) 来明确标记在验证失败时应打印其值的表达式。

注意

依赖于量化符号的表达式无法跟踪。此外，当前规范函数中出现的表达式无法跟踪。

2.8 调试 Move 证明器

Move 证明器是一个不断发展的工具，存在错误和不足。有时可能需要根据 Move 证明器传递给底层后端的输出来调试问题。如果您传递 --dump 选项，Move 证明器将输出原始的 Move 字节码以及 Move 证明器字节码，因为前者在编译过程中会进行转换。

2. Move 证明器支持资源

2.1 标准库和框架规范

2.2 示例

2.3 教程

2.4 演示文稿

2.5 会议论文

关系图谱

反向链接