白皮书的描述语言move语法详细解析

move语法

白皮书使用了一种半形式化（semi-formal）的描述语言进行了描叙。至于这套描述语言，主要符号解释如下：

=： 定义

：：= ： 赋值

⇀： 映射

×： product type，也就是表示结构体

∈： 表示属于某个类型或者集合中的一个元素

通过这些符号，Move定义了如下的语法类型：

Global state： 地址到账户的map，账户由Resource和Module构成。形式化定义如下：

Modules：由名字，结构体声明以及过程声明组成， 可以简单理解为c++的class。module通过ModuleId被外部索引（访问），结构体通过structId被外部索引，结构体声明是一个《kind， FieldName-》非引用类型》的product类型。

Module定义了资源的作用域，类似于c++的namespace的功能。其中Module内置了几个重要的函数用来进行类型操作：

· Pack and Unpack 用于从非受限类型创建和销毁模块的资源；

· MoveToSender/MoveFrom 在当前账户地址下面发布或者删除对应的资源；

· BorrowField ：获得结构体的一个字段的引用

Types： 包含基本类型（bytes是fixed-size字符串，AccountAddress是256bits），结构体类型，非引用类型，以及

在Module里面除去被声明为资源的类型（标记了resource kind），其余的类型统称为unrestricted types（不受限类型）。资源类型的变量或者字段只能被move，并且资源类型变量的引用不能被解引用，也不能被重复赋值。另外an unrestricted struct不能包含restricted field，原因很简单， unrestricted 结构体被赋值或者复制的时候，如果有restricted字段，那这个字段不会实际被操作到。

Values：

Move支持引用，引用是短暂的，因此不能被用来定义结构体的字段，也不能引用引用，应用的声明周期就是交易脚本的执行过程。通过Borrow{Loc， Field， Global}可以分别可以获得局部变量，结构体变量或者全局变量的引用（敲黑板，请学习rust）。

另外因为struct里不能存储reference，所以可以保证struct一定是一个tree而不会有backedge。这也是move比rust简化的最重要的一点，正因此move不需要复杂的lifeTIme。 因此Resource同样也不可能出现图结构。这样确实大大简化了语言的处理。

Procedures and transacTIon scripts：

过程的签名包含函数的访问控制修饰符，参数类型和返回值类型。过程声明包括一个过程签名，局部变量和一系列的指令，（作者认为，这个声明理解为定义（definiTIon）更合适一些）。一个交易脚本是一个不关联具体module的过程，因此他不会被复用，交易脚本操作的全局状态转换，这些状态的修改要么全部成功，要么全部失败。

ProcedureID标识一个过程，被moduleId和过程签名唯一确定，并且Call指定将其作为第一个参数，进行调用。这也就意味着函数调用是静态可确定（staTIcly determined）的，不存在什么函数指针或者函数表。同时模块内的过程依赖是无环的，加上模块本身的没有动态指派，这样就加强了执行期间的函数调用的不可变性：也就是一个procedure在执行过程的call frame必然是相邻的。因此也防止了类似于以太坊里面的re-entrancy攻击（这个就是有名导致分叉出ETC的攻击）。

move解释器

Move的字节码指令在一个栈式的解释器进行执行，栈式虚拟机的好处是易于实现和控制，对硬件环境的要求较少，非常适合区块链场景。同时文中也提到，相对寄存器式的解释器， 栈式解释器在不同的变量之间进行copy和move更容易控制和检测。

解释器的定义如下：

解释器由一个Value Stack，Call Stack以及全局变量引用计数器和一个GasUnits（类似以太坊的Gas Limits）组成。CallStackFrame包含了一个过程执行的所有上下文信息以及指令编号（指令会被唯一编码，减少代码体积，常规处理方法）。Locals是一个变量名到运行时候的Value的map。

字节码解释器支持过程调用（废话啊）。当在一个过程中执行Call指令调用其他的过程的时候，会创建一个新的CallStackFrame对象，然后将对应的调用参数存储到Locals上面，最后解释器开始以此执行新的合约的指令。执行过程遇到分支指令的时候，会在本过程内部（也就是Basic Block之前的跳转）发生一个静态跳转，所谓静态跳转实际上是指跳转的offset是事先已经确定好的，不会像evm一样动态跳转。这也就是之前提到的no dynamic dispath。最后调用return结束调用，同时返回值放在栈顶。

Gas衡量的思路跟EVM是一样的，每个指令有对应的Gas Units，执行一次，减去对应指令的Gas消耗，直到减到0或者所有指令执行完成。

Move的指令包括6大类：

· 变量操作： CopyLoc/MoveLoc实现数据从本地变量到栈的拷贝和移动，StoreLoc是讲数据存回来到本地

· 常量/数值/逻辑操作

· Pack/Unpack/MoveToSender/MoveFrom/BorrowField 等资源操作，具体的解释可以看前一篇文章

· 引用相关的指令，包括ReadRef/WriteRef/ReleaseRef/FreezeRef， 其中FreezeRef转换一个可变引用到一个不可变引用

· 控制流结构，包括call和return，branch，BranchIfTrue，BranchIfFalse等

· 区块链特定的操作，包括获得交易脚本的sender或者创建一个账号等指令。

详细的指令列表在白皮书的Appendix A已经列出。

Bytecode验证器

验证器我们在很多编译器里面都能看到，例如普遍使用的SMT证明器Z3. 验证器的核心功能就是在编译阶段保证语言（合约）的安全特性能够得到满足和增强。验证器静态验证是合约脚本发布的必经步骤。

验证器的状态如下：

对于一段可能包含多个module的交易脚本，进行验证，验证结果返回ok，或者各种不满足条件的报错。

Move的模块的二进制格式里面编码了一系列实体的集合，这些实体都放在一个table里面， 包括常量，类型签，结构体定义以及过程定义。检测过程主要有三类：

· 结构体合法检查： 保证字节码的table的完整性（well-formed）， 检测的错误非法的table index， 重复的资源实体以及非法的类型签名，例如引用了一个引用等

· 过程定义的语义检测：包括参数类型错误，悬垂索引以及资源重复定义。

· 链接时错误，非法调用内部过程，或者链接一个声明和定义不匹配的流程。

下面重点解释下语义检测和链接时错误检测。

Control-flow graph construction

验证器会首先创建一个bytescode的BasicBlock的控制流图，一个BasicBlock可以理解为中途没有分支指令的指令块。

Stack balance checking

检测栈里面被调用者的访问范围，保证合约的被调用者不能访问到调用者的栈空间。例如一个过程被执行的时候，调用者首先在CallStackFrame里面初始化局部变量，然后将局部变量放入到栈里面，假设当前栈的高度是n，那么有效的bytecode必须满足不变性： 当到达basic block的结束的时候，栈的高度依然还是n。验证器主要是通过分析每个基本块的指令对栈的可能影响，保证不操作高度低于n的栈空间。这里有一个例外就是，一个以return结尾的block，他退出的时候高度必须是n+m，其中m是过程返回值的个数。（这个特殊的操作有点匪夷所思，难道是把栈的高度默认放在了过程的第一个参数，退出的时候这样可以进一步的进行检测？后面确认了，确实是因为目前不支持多返回值，所以才加在一起）。

Type checking

在二进制格式里面，局部变量的类型是定义好的，但是栈的value确实需要推导的。在每个基本快这种推导和类型检测独立执行的，因为前面保证了调用过程访问的栈的高度是合法的，因此，这个时候就能安全的推导栈里面变量的类型了。具体检测就是给Value Stack维护了一个对应的Type Stack，执行的时候TypeStack也跟这指令执行进行pop和push。

Kind checking

kind和type的区别是type可能包含别名。 kind的检查主要检资源是满足

· 不可双花

· 不可销毁

· 必有归属（返回值必须被接受）

对于非资源类型的话，就没有这些限制了。

reference checking

引用的语法包括可变引用，不可变引用。所以引用检测结合了动态和静态分析。 静态分析利用类似rust类型系统的borrow checking机制，保证：1. 所以引用必须指向的是一个已经被分配的存储上，防止悬空； 2. 所有的引用都有安全的读写权限，引用访问既可以共享，也可以排斥（也就是有限的读写权限）。

为了保证2点， BorrowGlobal调用的时候会动态的对全局变量的引用进行了计数， 解释器会对每个发布了的资源进行判断，如果被borrow或者move了，再次引用就会报错。

Linking with global state

链接的时候还需要对链接的对象和声明是否匹配，过程的访问控制等做再次的检查。

以上就是目前Move的大部分的静态验证了。可以看到每个流程都有非常严格的分析和限制，最大程度的保证Resouce的安全转移和访问。

最后将虚拟机所有的状态和转移总结如下：

Move虚拟机通过执行区块交易里面的脚本实现全局状态Σ的转移。E表示交易脚本产生的针对某个账户的状态修改集（可以理解为XuperChain的读写集）：

虚拟机会顺序执行区块的每个交易，产生一系列的E，并且前一个E在后面交易执行的时候是生效的。

当前vm是串行执行交易，然后产生一系列的读写集。 但是Move在设计的时候，已经考虑到了预测执行产生读写集，然后合并的时候根据资源的access path（可以对比与XuperChain的读写集版本）进行冲突检测来解决冲突。。

最后将讲到了未来的规划，重点还是完善类型系统，提供更多类库支持。

这个白皮书分享系列到此为止，可以整体可以看到，Move通过借助logic type，module。 system在资源的转移控制上面做了大量的静态检测来保证资产转移的安全，相对EVM来说，避免了很多问题，Libra主网上线之后，在DeFi领域可能应该会对以太坊的DeFi Dapp造成不小的冲击。