Move 语言 中文白皮书 (三)----- Move的设计目标

3. Move 的设计目标

Libra 的使命是打造一个简单的全球货币和金融基础设施,为数十亿人提供支持 [1]。Move 语言旨在提供一个安全、可编程的基础,可以在此基础上构建这一愿景。Move 必须能够以精确、可理解和可验证的方式表达 Libra 货币和治理规则。 从长远来看,Move 必须能够对构成金融基础设施的各种资产和相应的业务逻辑进行编码。

为了满足这些要求,我们在设计 Move 时考虑了四个关键目标:first-class 资产、灵活性、安全性和可验证性。

3.1. First-Class Resources

区块链系统允许用户编写直接与数字资产交互的程序。 正如我们在 2.2 节中所讨论的,数字资产具有将它们与传统编程中使用的值(如布尔值、整数和字符串)区分开来的特殊特征。 使用资产进行编程的强大而优雅的方法需要保留这些特征的表示。

Move 的关键特性是能够使用受线性逻辑启发的语义定义自定义Resources类型 [3]:Resources永远不能被复制或隐式丢弃,只能在程序存储位置之间移动。 这些安全保证由 Move 的类型系统静态强制执行。 尽管有这些特殊保护,Resouces也可以作为普通的程序值——它们可以存储在数据结构中,作为参数传递给 过程(函数),等等。 First-Class Resources是一个非常笼统的概念,程序员不仅可以使用它来实现安全的数字资产,还可以编写正确的业务逻辑来包装资产和执行访问控制策略。

Libra 币本身是作为普通的 Move Resouces实现的,在语言中没有特殊状态。由于 Libra 代币代表由 Libra 储备管理的现实世界资产 [19],Move 必须允许创建Resources(例如,当新的现实世界资产进入 Libra 储备时)、修改(例如,当数字资产更改所有权时) ) 和销毁(例如,当支持数字资产的实物资产被出售时)。Move程序员可以使用模块保护对这些关键操作的访问。 Move 模块类似于其他区块链语言中的智能合约。模块声明资源类型和过程,这些过程对创建、销毁和更新其声明的资源的规则进行编码。模块可以调用其他模块声明的过程并使用其他模块声明的类型。然而,模块强制执行强大的数据抽象——一个类型在其声明模块内部是透明的,而在其外部是不透明的。此外,对资源类型 T 的关键操作只能在定义 T 的模块内执行。

3.2. 灵活性

Move 通过交易脚本为 Libra 增加了灵活性。 每个 Libra 交易都包含一个交易脚本,该脚本实际上是交易的主要程序。 交易脚本是包含任意Move代码的单个过程,允许自定义交易。 一个脚本可以调用区块链中发布的模块的多个过程,并对结果进行本地计算。 这意味着脚本可以执行表达性的一次性行为(例如支付一组特定的收件人)或可重用行为(通过调用封装可重用逻辑的单个过程)。

Move模块通过安全但灵活的代码组合实现了不同类型的灵活性。 在高层次上,Move 中的模块/Resources/过程之间的关系类似于面向对象编程中的类/对象/方法之间的关系。 但是,有一些重要的区别——Move 模块可以声明多种Resource类型(或零Resource类型),而 Move 过程没有 self 或 this 值的概念。 Move模块最类似于 ML样式[20]模块的受限版本。

3.3. 安全

Move 必须拒绝不满足关键属性的程序,例如Resource安全、类型安全和内存安全。 我们如何选择一个可执行的表示,以确保在区块链上执行的每个程序都满足这些属性? 两种可能的方法是:
(a) 使用带有检查这些属性的编译器的高级编程语言
(b) 使用低级无类型汇编并在运行时执行这些安全检查。

Move 采取了介于这两个极端之间的方法。 Move 的可执行格式是一种类型化的字节码,它比汇编高级,但比源语言低。 字节码由字节码验证器在链上检查Resource、类型和内存安全性,然后由字节码解释器直接执行。 这种选择允许 Move 提供通常与源语言相关的安全保证,但无需将源编译器添加到受信任的计算库或将编译成本添加到交易执行的关键路径中。

3.4. 可验证性

理想情况下,我们将通过链上字节码分析或运行时检查来检查 Move 程序的每个安全属性。不幸的是,这是不可行的。 我们必须仔细权衡安全保证的重要性和普遍性与计算成本和通过链上验证执行保证的增加的协议复杂性。

我们的方法是尽可能多地对关键安全属性执行轻量级的链上验证,但设计 Move 语言以支持先进的链下静态验证工具。 我们做出了一些设计决策,使 Move 比大多数通用语言更适合静态验证:

  1. 没有动态调用。 每个过程的调用点都可以静态确定。 这使得验证工具可以轻松准确地推断过程调用的效果,而无需执行复杂的调用图构造分析。
  2. 有限的可变性。 Move每个值的变化都是通过引用发生的。 引用是必须在单个交易脚本范围内创建和销毁的临时值。 Move 的字节码验证器使用类似于 Rust 的“借用检查”方案来确保在任何时间点最多存在一个对值的可变引用。 此外,该语言确保全局存储始终是树而不是任意图。 这允许验证工具模块化推理写操作的影响。
  3. 模块化。 Move模块强制执行数据抽象并本地化对resouces的关键操作。 模块启用的封装与 Move 类型系统强制执行的保护相结合,确保为模块类型建立的属性不会被模块外部的代码违反。我们希望这种设计能够通过孤立地查看模块而不考虑外部调用者来对重要的模块不变量进行详尽的功能验证。

静态验证工具可以利用 Move 的这些属性来准确有效地检查是否存在运行时故障(例如,整数溢出)和重要的程序特定功能正确性属性(例如,最终可以由参与者来声明锁定在支付渠道中的resources)。 我们将在第 7 节中分享有关我们功能验证计划的更多细节。