5. Move 语言 详解
在本节中，我们给出了 Move 语言、字节码验证器和虚拟机的半正式描述。 附录 A 详细列出了所有这些组成部分，但没有任何附带的散文。 我们在这里的讨论将使用附录中的摘录，并且偶尔会引用其中定义的符号。
Global state.
Σ ∈ GlobalState = AccountAddress ⇀ Account
Account = (StructID ⇀ Resource) × (ModuleName ⇀ Module)
Move 的目标是使程序员能够定义全局区块链状态并安全地实现更新全局状态的操作。 正如我们在 4.2 节中解释的那样，全局状态被组织为从地址到帐户的部分映射。 帐户包含resource数据值和模块
代码值。 帐户中的不同resource必须具有不同的标识符。 帐户中的不同模块必须具有不同的名称。
Modules.
Module = ModuleName × (StructName ⇀ StructDecl) × (ProcedureName ⇀ ProcedureDecl)
ModuleID = AccountAddress × ModuleName
StructID = ModuleID × StructName
StructDecl = Kind × (FieldName ⇀ NonReferenceType)
模块由名称、结构声明（包括resource，我们稍后将解释）和程序声明组成。 代码可以使用由模块的帐户地址和模块名称组成的唯一标识符来引用已发布的模块。 模块标识符用作命名空间，用于限定其结构类型的标识符和模块外部代码的程序。
Move模块支持强大的数据抽象。 模块的程序对创建、写入和销毁模块声明的类型的规则进行编码。 类型在其声明模块内部是透明的，在外部是不透明的。但Move 可以通过以下几个特定程序获得不同权限
- 通过 MoveToSender 指令强制发布帐户下的resource
- 通过 BorrowGlobal 指令获取对帐户下resource的引用
- 通过 MoveFrom 指令从帐户中删除resource的先决条件。
模块使 Move 程序员可以灵活地为resource定义丰富的访问控制策略。 例如，一个模块可以定义一个只有在其f字段为零时才能被销毁的resource类型，或者一个只能在某些帐户地址下才能被发布的resource。
类型
PrimitiveType = AccountAddress ∪ Bool ∪ UnsignedInt64 ∪ Bytes
StructType = StructID × Kind
𝒯 ⊆ NonReferenceType = StructType ∪ PrimitiveType
Type ::= 𝒯 |&mut𝒯 |&𝒯
Move 支持基本类型，包括布尔值、64 位无符号整数、256 位帐户地址和固定大小的字节数组。 结构是由模块声明的用户定义类型。 通过使用resource种类标记结构类型，将其指定为resource。 所有其他类型，包括非resource结构类型和原始类型，都称为无限制类型。
resource类型的变量是resource变量； 不受限制类型的变量是不受限制的变量。 字节码验证器对resource变量和resource类型的结构字段实施限制。 resource变量无法复制，必须始终Move。 resource变量和resource类型的结构字段都不能重新分配 - 这样做会破坏先前保存在存储位置中的resource值。 此外，不能取消对resource类型的引用，因为这会产生底层resource的副本。 相比之下，不受限制的类型可以被复制、重新分配和取消引用。
最后，不受限制的结构类型可能不包含具有resource类型的字段。此限制确保 (a) 复制不受限制的结构不会导致嵌套resource的复制，并且 (b) 重新分配不受限制的结构不会导致嵌套resource的破坏。
引用类型可以是可变的或不可变的； 不允许通过不可变引用进行写入。 字节码验证器执行引用安全检查，以强制执行这些规则以及对resource类型的限制（参见第 5.2 节）。
值：
Resource = FieldName ⇀ Value
Struct = FieldName ⇀ UnrestrictedValue
UnrestrictedValue = Struct ∪ PrimitiveValue
𝑣 ∈ Value = Resource ∪ UnrestrictedValue
g ∈ GlobalResourceKey = AccountAddress × StructID
𝑎𝑝 ∈ AccessPath ::= 𝑥|𝑔|𝑎𝑝.𝑓
𝑟 ∈ RuntimeValue ::= 𝑣 |ref𝑎𝑝
除了结构和原始值之外，Move 还支持引用值。参考不同于其他Move值，因为应用值是瞬态的。字节码验证器不允许引用类型的字段。该要求会约束引用只能在交易脚本执行期间被创建，并在该交易脚本结束之前释放引用。
对结构值形状的限制确保全局状态始终是树而不是任意图。状态树中的每个存储位置都可以使用其访问路径 [24] 进行规范表示 - 从存储树中的根（局部变量𝑥或全局resource键𝑔）到由字段序列标记的后代节点的路径标识符𝑓。
该语言允许引用原始值和结构，但不允许引用其他引用。 Move程序员可以使用 BorrowLoc 指令获取对局部变量的引用，使用 BorrowField 指令获取结构的字段，使用 BorrowGlobal 指令获取在帐户下发布的全局resource。 后两个构造只能用于当前模块内声明的结构类型。
程序和交易脚本：
程序签名由可见性、类型化的形式参数和返回类型组成。 程序声明包含签名、类型化的局部变量和字节码指令数组。 程序可见性可以是公开的或内部的。 内部程序只能由同一模块中的其他程序调用。 公共程序可以由任何模块或交易脚本调用。
区块链状态由交易脚本更新，该脚本可以调用当前在帐户下发布的任何模块的公共程序。 交易脚本只是一个没有关联模块的程序声明。
一个程序可以由它的模块标识符和它的签名来唯一标识。 调用字节码指令需要一个唯一的程序 ID 作为输入。 这确保了 Move 中的所有程序调用都是静态确定的——没有函数指针或虚拟调用。 此外，模块之间的依赖关系在构造上是非循环的。 一个模块只能依赖于线性交易历史中较早发布的模块。 非循环模块依赖图和不能动态分派两者的组合决定了确定性执行逻辑：属于模块中的程序的所有堆栈帧必须是连续的。 因此，Move 模块中没有以太坊智能合约的重入 [16] 问题。
在本节的其余部分，我们将介绍字节码操作及其语义（第 5.1 节），并描述字节码验证器在允许执行或存储模块代码之前执行的静态分析（第 5.2 节）
字节码解释器
𝜎 ∈ InterpreterState = ValueStack × CallStack × GlobalRefCount × GasUnits
𝑣𝑠𝑡𝑘 ∈ ValueStack ::= []|𝑟::𝑣𝑠𝑡𝑘
𝑐𝑠𝑡𝑘 ∈ CallStack ::= []|𝑐::𝑐𝑠𝑡𝑘
𝑐 ∈ CallStackFrame = Locals × ProcedureID × InstrIndex
Locals = VarName ⇀ RuntimeValue
移动字节码指令由类似于通用语言运行时 [22] 和 Java 虚拟机 [21] 的基于堆栈的解释器执行。 一条指令使用堆栈中的操作数并将结果压入堆栈。 指令还可以从当前过程的局部变量（包括形式参数）移动和复制值。
字节码解释器支持程序调用。 传递给被调用者的输入值和返回给调用者的输出值也通过堆栈进行通信。 首先，调用者将过程的参数压入堆栈。 接下来，调用者调用 Call 指令，该指令为被调用者创建一个新的调用堆栈帧，并将推送的值加载到被调用者的局部变量中。 最后，字节码解释器开始执行被调用程序的字节码指令。
字节码的执行按顺序执行操作，除非有一个分支操作导致跳转到当前过程中静态确定的偏移量。 当被调用者希望返回时，它将返回值压入堆栈并调用 Return 指令。 然后将控制权返回给调用者，调用者在堆栈上查找输出值。
Move程序的执行以类似于 EVM [9] 的方式计量。 每个字节码指令都有一个相关的gas单位成本，任何要执行的交易都必须包括一个gas单位预算。 解释器在执行期间跟踪剩余的gas单位，如果剩余量达到零，则停止并报错。
我们参考比较了基于寄存器和基于堆栈的字节码解释器，发现具有类型化局部变量的堆栈机器非常适合 Move 的Resource语义。 在局部变量、堆栈和调用者/被调用者对之间来回移动值的低级（指面向机器的是低级）机制密切反映了 Move 程序的高级（指面向人类可读的语言是高级）意图。 没有局部变量的堆栈机器会更加冗长，而寄存器机器会使跨过程边界移动resource变得更加复杂。
指令集：Move 支持六大类字节码指令
- 用于将数据从局部变量复制/移动到堆栈的 CopyLoc/MoveLoc 等操作，StoreLoc 用于将数据从堆栈移动到局部变量。
- 对类型化堆栈值的操作，例如将常量推入堆栈，以及对堆栈操作数的算术/逻辑操作。
- 模块内置函数，例如 Pack 和 Unpack 用于创建/销毁模块声明的类型，MoveToSender/MoveFrom 用于取得/取消 账户下的发布模块类型权利，以及 BorrowField 用于获取对模块类型之一的字段的引用。
- 与引用相关的指令，例如 ReadRef 用于读取引用，WriteRef 用于写入引用，ReleaseRef 用于销毁引用，以及 FreezeRef 用于将可变引用转换为不可变引用。
- 控制流操作，例如条件分支和从程序调用/返回。
- 特定于区块链的内置操作，例如获取交易脚本发送者的地址和创建新帐户。
附录 A 给出了Move字节码指令的完整列表。 Move 还提供加密原语，例如 sha3，但这些原语是作为标准库中的模块而不是字节码指令实现的。 在这些标准库模块中，过程被声明为本机，过程体由 Move VM 提供。 只有 VM 可以定义新的本机过程，这意味着这些加密原语可以改为作为普通字节码指令来实现。 但是，本机过程很方便，因为 VM 可以依赖现有机制来调用过程，而不是为每个加密原语重新实现调用约定。
5.2. 字节码验证器
𝐶 ∈ Code = TransactionScript ∪ Module
𝑧 ∈ VerificationResult ::= ok | stack_err | type_err | reference_err | ...
𝐶 ⇝ 𝑧 = bytecode verification
字节码验证器的目标是验证提交发布的任何模块和*提交执行的任何交易脚本静态强制执行的安全。 不通过字节码验证器，任何 Move 程序都不能发布或执行。
字节码验证器强制执行任何格式良好的 Move 程序必须具备的一般安全属性。 我们的目标是在未来的工作中为特定于程序的属性开发一个单独的离线验证器（见第 7 节）。
Move 模块或交易脚本的二进制格式对实体表的集合进行编码，例如常量、类型签名、结构定义和程序定义。 验证者执行的检查分为三类：
- 结构检查以确保字节码表格式正确。 这些检查发现诸如非法表索引、重复表条目和非法类型签名（如对引用的引用）之类的错误。
- 程序主体的语义检查。 这些检查检测错误，例如不正确的过程参数、悬空引用和复制资源。
- 将结构类型和程序签名的使用与其声明模块联系起来。 这些检查检测错误，例如非法调用内部程序和使用与其声明不匹配的程序标识符。
在本节的其余部分，我们将描述语义验证和链接方面的内容。
控制流图构造。 验证者通过将指令序列分解为基本块的集合来构建控制流图（请注意，这些与区块链中的交易“块”无关）。 每个基本块都包含一个连续的指令序列； 所有指令的集合在块之间进行划分。 每个基本块都以分支或返回指令结束。 分解保证分支目标仅在某些基本块的开始处着陆。 分解还试图确保生成的块是最大的。 然而，字节码验证器的健全性并不依赖于最大值。
堆栈余额检查。堆栈平衡检查确保被调用者无法访问属于调用者的堆栈位置。基本块的执行发生在局部变量数组和堆栈的上下文中。程序的参数是局部变量数组的前缀。跨程序调用传递参数和返回值是通过堆栈完成的。当一个程序开始执行时，它的参数已经加载到它的参数中。假设程序开始执行时堆栈高度为 n。有效字节码必须满足以下不变量：当执行到达基本块的末尾时，堆栈高度为 n。验证者通过分别分析每个基本块并计算每条指令对堆栈高度的影响来确保这一点。它检查高度不低于 n，并且在基本块出口处为 n。一个例外是以 Return 指令结束的块，其中高度必须为 n+m（其中 m 是过程返回的值的数量）。
类型检查。验证器的第二阶段检查每个指令和程序（包括内置程序和用户自定义程序）是否使用适当类型的参数调用。指令的操作数是位于局部变量或堆栈中的值。字节码中已经提供了程序的局部变量的类型。但是，堆栈值的类型是推断出来的。这种推断和每个操作的类型检查是针对每个基本块单独完成的。由于每个基本块开头的堆栈高度为 n 并且在块执行期间不会低于 n，因此我们只需对从 n 开始的堆栈后缀进行建模，以便对块指令进行类型检查。我们使用类型堆栈对这个后缀进行建模，在处理基本块中的指令序列时，这些类型会被压入和弹出。类型堆栈和静态已知类型的局部变量足以对每个字节码指令进行类型检查。
仔细的检查。 验证者在类型检查阶段通过以下附加检查来执行resource安全：
- resource不能被复制：CopyLoc 不用于类型resource的局部变量，并且 ReadRef 不用于类型是对类型resource值的引用的堆栈值。
- resource不能被销毁：PopUnrestricted 不用于类型resource的堆栈位置，StoreLoc 不用于已保存resource的局部变量，并且 WriteRef 不用于对类型resource值的引用。
- 必须使用resource：当程序返回时，任何局部变量都不能保存resource值，并且评估堆栈的被调用者段必须只保存程序的返回值。
非resource结构类型不能具有resource类型的字段，因此这些检查不能通过（例如）复制具有resource字段的非resource结构来破坏。
非resource结构类型不能具有resource类型的字段，因此这些检查不能通过（例如）复制具有resource字段的非resource结构来破坏。resource不能被因错误而停止的程序执行破坏。 正如我们在 4.2 节中解释的那样，交易脚本的部分执行所产生的状态变化不会被提交到全局状态。 这意味着在运行时失败时位于堆栈或局部变量中的resource将（有效地）返回到它们在交易开始执行之前的任何位置。
原则上，非终止程序执行可以使resource无法访问。 但是，第 5.1 节中描述的gas计量方案可确保 Move 程序的执行始终终止。 耗尽gas的执行会因错误而停止，这不会导致resource丢失（如上所述）。
参考检查。 使用静态和动态分析的组合检查参考的安全性。 静态分析以类似于 Rust 类型系统的方式使用借用检查，但在字节码级别而不是在源代码级别执行。 这些参考检查确保了两个强大的属性：
- 所有引用都指向分配的存储（即，没有悬空引用）。
- 所有引用都具有安全的读写访问权限。 引用要么是共享的（没有写访问权和有限的读访问权），要么是独占的（有有限的读写访问权）。
为了确保这些属性对通过 BorrowGlobal 创建的全局存储的引用保持有效，字节码解释器执行轻量级动态引用计数。 解释器跟踪每个已发布资源的未完成引用的数量。 如果在对该资源的引用仍然存在的情况下借用或移动了全局资源，它会使用此信息停止并出现错误。
这种参考检查方案具有许多新颖的功能，将成为另一篇论文的主题。
全局状态链接器。
𝐷 ∈ Dependencies = StructType∗ × ProcedureID∗
deps ∈ Code → Dependencies computing dependencies
𝑙 ∈ LinkingResult := success | fail
⟨𝐷, Σ⟩ ↪ 𝑙. linking dependencies with global state
在字节码验证过程中，验证者假定当前代码单元使用的外部结构类型和过程 ID 存在并且如实表示。 链接步骤通过从全局状态 Σ 读取结构和程序声明并确保声明与它们的用法相匹配来检查此假设。 具体来说，链接器检查全局状态中的以下声明是否与它们在当前代码单元中的用法相匹配：
- 结构声明（名称和种类）。
- 程序签名（名称、可见性、形式参数类型和返回类型）。