为什么 Move 是一个更安全的智能合约语言？
受 MoveBit 和 电子科技大学邀请，Aptos world、SUI world、智谷星图、Mynft、 MoveFuns 等机构协办，2022 年 9 月 23 日本周五上午 10:30， 滑铁卢大学计算机学院助理教授徐萌在线上主讲「用 Move Prover 对智能合约进行快速、可靠的形式化验证」主题学术报告。 徐萌教授本次讲座的内容围绕从用户视角解读 Move 语言及 Move Prover，内容深入浅出，本文为徐萌教授讲座内容的文字整理稿。1 为什么 Move 是一个更安全的智能合约语言？
大量的资产存放在区块链上，所以区块链的智能合约的编程语言一定要尽可能的提供安全保障，而 Move 是一个面向区块链设计的编程语言，它提供了更好的安全性。简单来说 Move 语言的安全性能是由两部分组成的，一部分是 Move 自带的类型系统，另一部分是 Move Prover 这种 Move 自带的形式化验证的工具。这两个东西分别提供了不同程度的安全保护，后面的内容会解释他们提供了哪些保护，以及为什么会把 Move 设计成这个样子。 Move 的类型系统提供了很多保护，我们着重强调三点：一是类型的安全，二是资源的安全，最后是引用的安全。形式化验证工具 Move Prover，它主要提供了更多更高级的表述方法，就是更高级的去表达你想做什么的规范。-struct invariants 就是一个类型，一个结构体应该有什么样的状态。-unit specification (per single function ) 每一个程序每一个函数要遵循什么样的规范-state-machine specification: 全局的状态，特别是在区块链上整个全局的状态要遵循怎么样的一个状态规范。这三个东西都可以由 Move prover 形式化验证的工具来规范。 区块链是一个很重要的系统，大量资产存放在了区块链上，而且区块链上的这些交易，一旦执行了它是不可以撤销的。所以智能合约就需要有一些规范来规定它是否真的能提供了它所宣传提供的功能，而不是一些意料之外的功能，这就需要我们有一个语言和一套工具来保证这一点。 在这种背景下， Move 语言以及 Move Prover 这个工具就应运而生。 
Move 最早是为 Libra 项目所设计，后来 Libra 改名为 Deim，Diem 后来卖给了 Silvergate。而 Move 现在变成一个很多开发者参与，由社区来维护的开源的语言。Move 的核心设计思想其实包括两点，第一点是它遵循了所谓的 borrow semantic，一个借用的思想，这个就很像 Rust 的 borrow semantic，如果大家用过 Rust 语言的话，你会发现很多思想其实是借鉴于 Rust 来的。（编者注：Rust 使用了借用机制。对象可以通过引用（&T）来传递，从而取代通过值（T）来传递。编译器（通过借用检查）静态地保证了引用总是指向有效的对象。也就是说，当存在引用指向一个对象时，该对象不能被销毁。） 另外一点就是 Move 遵循了所谓的 Linear Types，就像如果大家习惯于用这种所谓 smart pointer 的话，那么在 c++ 里面有一个东西叫 unique pointer，它其实就是规范了一个对象的所有权，然后这个东西也被 Move 所吸收进来，所以 Move 语言的核心有这两点。（编者注：Linear types 的思想来源于 Linear Logic, 它确保对象在程序运行期间有且仅有一个它的引用，这种类型用来描述不能被修改的值，比如文件描述符。linear 类型系统允许引用，但不允许别名 ( 被多个变量引用 ), 类似于 C++ 的 _unique_ptr_ 指针, 只能被移动，不能被复制）还有关键的一点就是 Move 里面不允许动态调用别的函数，也就是说在编译一个 Move 智能合约的时候，我们就知道所有可能的执行路径，不会像 solidity 这样会有一个所谓的 call back( 动态调用的回调 )，然后你不知道回调哪里，这种事情在 Move 里面是不存在的。在 Move 里，如果是有一个函数调用另一个函数，我们永远知道它调用的函数在哪里以及该函数是什么，这极大的保证了智能合约的安全性，同时也保证了形式化证明可以顺利的进行。同时 Move 它并不像通用的编程语言，像 c 或者是 Java 那样有系统调用，去读写文件，或者是连接网络等操作。Move 里的智能合约跟外界通讯的主要方式，其实就是通过跟全局变量或者说全局状态来交互。它有一个很小的 API，然后只能通过这几个 API 去跟外界交互，你不能去调用任意的 system call，这个也是帮助我们可以去形式化验证这种智能合约的一个前提，同时 Move 有一个完整的并且很强大的一个规范语言 MSL。除了 Move 语言本身，开发者还可以对 Move 的程序做出一些规范（spec），这个规范包括常见的 pre/post condition，然后还有全局的全局状态不变量（global state invariant），这些我们都可以通过规范语言来实现。MSL 规范语言其实是比 Move 语言本身要更强大的，因为它支持所谓的 universal 和 existential quantifier，其实就是数学里面那种 for all （对于所有的变量都符合），或者 exist （存在某个变量符合某一种原则），这些在 Move 语言是很难做到的，但是在规范语言里面可以这样写。 简单来说它长得像一个 Rust 程序，你可以定义你的 module 是什么，有一个自己的 address，可以定义 module 的名字是什么，可以定义自己的结构体，就像定义自己的类型一样，可以定义函数，可以给定函数的参数，然后对函数做一些处理，然后给你一个返回值，然后可以定义智能合约里面那种入口函数。我们可以对所写的 Move 程序做出一些规范，比如对转账函数做出一些规范，比如转账的金额不能太大，不能太小，然后转出的金额必须等于转入的金额等等。我们还可以对全局的状态做出一些规范，比如说所有开户的人必须保持一个最小的数额，或者是每次转账不能超过多少等，这些都可以通过 Move 的规范语言来描述。 如果用 Move 规范语言写好了规范，就可以用 Move Prover 来去验证。也就是写完这个规范之后，可以去验证我们写的 Move 程序是不是真的符合我们写的这套规范。如果符合则 prover 不会报错，如果不符合 prover 就会告诉你哪里不对，然后我们可以去修改。 目前 Move Prover 是百分百开源，所有人都可以在 github 上下载。它在 Move 里面是默认是 turn on 的，也就是说 by default，如果你改动任何 Move 的程序， Move Prover 就会 running 程序，并且确保你的改动并不会违反之前写的规范。目前 Move Prover 运行速度还是很快的，比如 8000 多行的 Move 代码以及 6000 多行的规范，整个验证的过程其实只需要几分钟，这个速度还是很快。因为它速度很快，所以可以支持持续集成 continuous integration，每次改动任何的 Move 代码，其实都会引发 Move prover 重新去验证一下，然后并且确认改动是没有问题的。 Move 类型系统其实是 Move 的第一个安全特性。如果说我们讲的稍微哲学一点的话，Move 类型系统和 Move Prover 都是为了去帮助 Move 的开发者去挖掘他们自己真正想要什么，他们真的对自己的程序想要什么，并且以一种形式化的方式来把自己的这种意图给固化下来。Move 类型系统和 Move 形式化验证系统其实做的都是做这件事情。
基于这样一个思想，如果说你写了一个 Move 程序，并且 Move 的类型系统或者 Move prover 发现你哪里有问题，不要试图去绕过这个东西，因为它其实是在帮助你去理解你真正想干什么，以及用一种很严谨的方式去记录你想干什么。如果 Move prover 或者是 Move 编译器给你报错，最好去研究一下自己是不是哪里没有想清楚，然后去修复一下，一开始会很难，但是如果习惯了，其实你会发现他会很帮助你去挖掘你自己对于程序的理解。然后 Move 的类型系统其实主要保证了三个问题，一个是类型安全，一个是资源安全，一个是引用安全。我们来讲一下为什么要保证这三个安全。首先类型安全，简单来说 Move 它是一个强类型系统，并且它严格保证了在任何情况下都不可以做类型转换，你永远不可能把一个类型转化为另一个类型，这是 Move 这个类型系统所提供的一个保证。如果分开来说的话，就是你写 Move 程序，你的每一个变量或者每一个所谓的表达式，它都有且只有一个类型，而且这个类型是在静态的时候就知道，并且这个类型在动态或者在静态，它永远不可能被改变，这个是 Move 的这个类型系统所要保证的。 熟悉 Move 会觉得这个说法的不太对，比如有一个 Freeze 这样的 operation，它可以把一个 mutable reference 改成一个 immutable，或者是有那种 cast 操作可以把一个 uint 变成另一个 uint，但实际你却发现这个操作它并没有对变量做改变，它做的其实是重新新建了一个变量，并且把新的变量给它一个固定的类型，所以这些操作并没有违反 Move 的类型安全保证。然后至于为什么 Move 做类型安全，其实比较容易思考。就举个例子，如果你写了一个智能合约，然后你有一个账户，然后你的智能合约里面有一个就是 coin 硬币这样一个结构体，这个硬币当然是很重要的，它存着你自己有多少钱，如果我们允许类型转化，那么我们在这里我就可以把 1000 这样一个 integer 转换成一个 coin，其实就是我自己凭空制造出来的一个 coin。我们并没有真的去造 coin 这样一个结构体，我们只是把 1000 这样的数字转化成一个 coin 的类型，这样显然是不对的，因为你就凭空造出来了一个 coin，这样是所以 Move 的类型系统其实就会就是会阻止你去做这件事情。同样的你还可以通过直接复制一个 value 或者怎么样的方式来做一个转换，但是你会发现不管你怎么去尝试， Move 的类型安全一定会阻止你去把一个类型去转化成另一个类型。如果编译上图的代码的话，你会发现如果你写了一个类型不安全的程序， Move compiler 根本就不会让你通过，会直接给你报错，说你在这里试图把一个 integer 转换成一个 coin，当然这样是不合理的，所以这就是 Move 类型安全所要保证的。下一个就是资源安全，在常见的这种编程语言里没有资源安全这个东西。它其实是强制允许你去做一些很细力度的控制，对于比如说一个 object 它可以做什么，它不可以做什么，这个是对整个 type 的一个控制。第一它保证了资源的稀缺性，通过 copy 和 drop 这两个 ability，它保证说一个资源它是不是能被复制，或者是不是能被扔到一边不管，它是由这两个 ability 决定。还有两个 ability (key 和 store ) 决定这个资源它可以出现在哪里，它是否可以出现在你的 function 里面，并且随着你的智能合约结束就消失了，还是它可以写到区块链上，这个也是这两个 ability 决定的。Move 还对一个资源做了封装，所有关于资源的代码都应该封装在一个模块，你不能把它打包成多个模块来做对资源的处理，所以 Move 资源安全其实保证的是这一点。 这一点的设计其实比较好理解，比如说你有一个区块链上那种 coin，当然你不可以随意把它复制，或者是不会把它扔掉。你如果复制一个 coin，相当于你从一个 coin 变成两个 coin，那显然你钱就变多了，这个是不能接受的，同时 coin 也不可能凭空消失，你必须把它花出去，不可能说 coin 说没了就没了。 Move 的资源安全简单来说就是一个东西它不能凭空出现，也不能凭空消失，Move 把这个概念然后放到语言里。其中一个例子就是这样，如果说你有一个 coin，不允许去复制 coin 或者是扔掉这个 coin 。如果你试图去复制这个 coin 把从一个硬币变成两个硬币，这个是会报错的。同时你通过一些别的方式去复制 coin，也不会让你通过的。你想默默把这个 coin 给它扔掉，这个也是不可以的。这些是在静态编译 Move 程序的时候就会直接报错。我最喜欢的例子英文叫 hot potato，中文可以叫“烫手的山芋”， 你可以定义一个“烫手的山芋”，然后这个山芋它什么 ability 都没有，也就是说你既不能扔掉它，也不能破坏它，也不能复制它，也不能把它存到区块链上。你拿到烫手山芋之后，你唯一能做的事情其实就是看一下它，然后把它就返回出去，所以这个就是一个烫手的山芋。 我们在实际操作中很常见的方法，是把 hot potato 当做一个 capability 来处理，把它当做一种认证的机制来用，然后可以通过这种是 resource-safety 可以保证一些很花里胡哨的一些 pattern。 如果我们试图去验证一下 hot potato 的话，你会发现如果你有一个 hot potato 的时候，你并没有办法把它写到一个东西里，然后再把它放到 blockchain 上去，在静态编译时就不允许你去看 potato 里面 value 是什么，你也不能去试图复制 potato，比如把一个 potato 变成两个 potato。然后你也不能去把 potato 给破坏掉，你唯一能做的事情，就是你怎么拿进来的，再怎么把它拿出去。 这种 hot potato 的模式是从来没有在别的语言里面见过的，是一种非常奇特的机制。（编者注：可以去对比下 solidity 中闪电贷的实现）最后一点就是引用安全。如果习惯于 c 语言或者 c++，你肯定会遇到这种所谓的 dangling pinter 的问题，就是你的对象已经被 free/deallocate 掉了，然后你发现还有一个指针在指向它，这个可以搞出很多很奇怪的东西来，就因为一个被 free 掉对象是永远不能有一个指针指向它。 这个在 Move 里面其实是用通过“引用安全”的方式来保证的，它简单来说就是遵循了 Rust 的所谓的 ownership 的规则，就是任何一个函数里面的本地变量，在任何一个时间有且最多只有一个进程可以去改它。同时对于一个全局变量，在整个 blockchain 里面，对于任何一个类型有且只有一个所有者可以去改变它，这个是通过 Move 的引用安全来保证。如果大家熟悉 Rust 的话，应该会比较好理解。最后我们讲一下 Move Prover 这个形式化验证的系统。 思考下在有了类型系统之后，为什么我们还需要 Move Prover 这样一个形式化验证的东西？已有的这些类型系统为什么不能满足我们这些需要？很关键的原因是：Move 类型系统它并不能满足于我们表述更复杂的逻辑需求或者更复杂的意图，这种东西是没有办法被 Move 类型系统所记录的。举一个例子，我们有这种结构体的不变的状态，还有函数前后的关系的约束，以及 global state 这种状态，这些目前没有办法全部被类型系统记录。 3.1 结构体不变量 Struct Invariant第一个具体的例子就是说结构体的不变量，结构体的不变量就允许在一个复杂的结构体，它的这些一个结构体里面有很多个 field，然后在这个结构里面不同的 field 之间会存在一个关系，然后 结构体的不变量就允许你对它不同的 field 之间的关系作出一个规定，然后这个是目前类型系统所达不到的。 举一个很简单的实例，比如你如何去用类型系统实现一个非 0 的 64 位的整数？这个东西在目前的 Move 里面是没有办法做到，因为没有一个类型叫非 0 的 64 位整数。这个东西在类型系统里面是没有办法保证的，你能得到的最近的一个东西就是一个 64 位整数，但它有可能是 0，所以你没有办法创造一个非 0 的 64 位整数的类型。但我们可以创造一个结构体，然后结构体的名字叫非零 64 位整数，然后里面有一个 field，它叫结构体的值，然后它是 64 位整数。整个所有的这些类型这个系统并不能阻止你写一个 0 进去，所以这个时候就需要形式化验证的工具来给你提供能力。这个时候你就可以写一个形式化验证的一个规范，规定说在非零的结构体里面，它叫 value 的 field 一定是要大于 0。然后在你有了这个规范之后，你就可以开始写你的程序，然后你如果不小心写出来一个上图的程序 fun create_zero()，允许把一个 0 放到了结构体里面，那么 prover 其实是会在这里报错，说你写了一个 0 在这里面，而你的规范里面要求说这里面一定不能是 0，所以这个是不允许的。 而上图的第二个函数 fun create_x_checked() 是允许的，你会发现如果这个函数是把一个 x 这样的值放到 value 域里面，它有一个检查说要保证 x 一定不能为 0，只要 x 不能是 0，就可以把 x 放到这个值里面。所以当我们生成这样一个叫非 0 的 64 位整数的这样一个结构体的时候，其实就可以保证结构体的值一定不是 0。这就是一个典型的 Move prove 可以应用的一个例子。这一套结构体加结构体的规范，它其实起到的是一个“增强类型”的作用，它可以保证说结构体里面域之间的关系是符合某种关系。刚举的是一个非常简单的例子，其实 Move Spec 可以支持写很复杂的关系，比如说我有一个结构体，然后里面有两个数字，然后要保证第一个数字一定比别的要数字大，同时这两个数字加起来是 100，又比如说要保证这两个结构体里面的这种值应该是保持一个什么样状态，开发者可以写很多很有用的规范，然后 Move prover 就会去验证说你写的代码是不是真的符合这样的一个逻辑。比如下图我们实现了 fun create_valid() 函数，我们代码逻辑是如果保证 a 比 50 大，b =100 - a，那么我们生成的结构体会符合我们写的规范。我们如果对下列代码进行验证， Move prover 应该不会报错。 也就是说 Move Prover 会运行检查，并且告诉你没有问题，还没有报错，就说明没有问题，你写的程序其实是符合结构体的规范。 如果开发者在这里弄错了，比如代码中第 12 行改成 assert!( x>=40 )，这个情况下就会出一个问题，Move Prover 就会报错。Move Prover 提示给了一个反例，说当 输入 x 等于 47 的时候，因为 a 是 47，b 是 53，违反了 a>=b 这条，所以它就不符合，所以如果开发者写了这样的规范之后，它会有效的减少代码的写出错误的可能。 当然如果代码写的不是 assert!( x>=50 )，而是 assert!( x>=60 )，其实也是能通过的，因为 60 的话照样也是符合这个规定，就看开发者怎么去写这个代码的事情。这个是结构体的的规范，然后如果你是第一次接触形式化验证的话，或者是第一次接触 Move Prover 这个工具的话，其实建议从结构体的规范开始写，因为它基本上最简单，它基本上什么都不考虑，它不考虑后续的这个函数是怎么实现的，它只考虑当前这个结构体本身，而当前一个结构体的复杂度是往往来说是比较小的，所以只考虑一个结构体本身写出来的规范是比较简单的，同时也是比较容易上手。3.2 函数规范 Function Specification
刚刚讲的是对结构体写 specification，然后其实 Move 一个重点是要做 function 的 specification，就是对一个函数做一个规范，其中就包括函数应该表现成什么样子，他在什么样情况下会异常报错，什么样的情况下会结束执行，而在结束执行的情况下，他又应该保持一个什么样的状态？这个就是函数规范所要达到的一个目的。 如果大家对形式化验证不熟，其实可以把函数规范想象成一个非常全面的单元测试。你写一段代码，然后你想知道这个代码对还是不对？那么你就对他做单元测试，然后你去试图穷尽你写的代码里面所有的可能的路径，然后你发现穷尽所有路径都没问题，这个是单元测试想要做的。你可以想象成对于函数的规范形式化验证工具 Move prove 它也是在做这样一件事情。虽然它并不是实际上去把所有的可能情况都遍历一下。举一个简单的例子，比如说一段 Move 程序有一个定义的结构体，其实就是一个模拟的银行账户，然后有一个就是取钱的 function，把一个把钱从一个账户里面取出来。写完这个 function 之后，你想知道这个 function 到底对不对，它到底能不能实现你的意图？你可以开始做单元测试，大家可能都听过一个单元测试的笑话，说 QA 工程师走进一家酒吧，要了一杯啤酒；要了 -1 杯啤酒，要了 9999999 杯啤酒，要了一杯洗脚水.... 大家可能都听过这笑话，然后这其实就是单元测试做的一个事情。如果想去测试这个就取钱的函数，你会怎么做？你去走到一个 ATM 机前，然后你开始取钱，取 10 块钱，取 1000 块钱，取 9999999999999999999999999099 块钱，甚至从一个不应该取钱的一个地址，比如说零这个地址去取，取 0 块钱等，就是有目的的去测试一些边界值的可能性。您去从一个叫 deadbeef 的账户里面取一个 -123 的钱，或者是取 666*2 这么多钱，这是一个单元测试工程师去做的事情。那就在你去做这个单元测试的时候，你实际上在想做什么？你实际上是想去发现整个函数它实际在干什么，它这边怎么进行各种极端情况的处理。3.2.1 异常退出 Abort Conditions
Move prover 给你提供了允许你去更专业去表达这个函数应该怎么样做事务处理的机会，就是通过所谓的函数的规范你可以写一个取钱函数的规范。 如果我要去取钱的话，那么如果这个地址就没有根本没有开户，那你一定会报错，对吧？这个就是第一条 abort if （第 9 行）的意思。如果你去从一个没有开户的地方取钱一定会报错。第二个（第 10 行）意思如果你取的钱太多，他账户里没有那么多钱，那也一定会报错。这里（从第 8 到 11 行）提供了一个取钱的专业的规范，它会报错并且它只会在这两个地方报错。不仅是它会报错，同时是这两个报错是涵盖了所有可能的报错，这个就是函数的规范。我们可以对上图的代码做一个简单的测试，跑一下形式化验证的工具，然后我们发现这个规范是对的，确实这个函数会在这两个情况下报错。如果假设说我足够粗心，或者我们认为不存在开户的情况下程序不会报错，我们把第 9 行注释掉（相当于我们的规范不完整），在这个情况下，形式化验证的工具其实会报错的（如下图），它会提醒你有一个异常发生了，但是我们并没有在规范里面去提到它。 当你去从一个不存在的就是没有开过户的一个账户上去取钱的时候，他肯定是不可以的，然后他会给你这样一个报错的提醒。如果说我们的 code 的里面有错误，比如说你本来是取钱的，但是你把它你不小心写成了存钱，其实就是一个正负号的事情，你这件事情上你再去跑 Prover 的话，很可能也会报错。 然后这里面还有一个技巧，如果你觉得你的程序有地方会报错，但是你又不想去思考这个程序在哪里会报错，其实可以让 Prove 这个工具来提示你或者引导你去发现程序哪些地方可能有问题。 这个技巧其实也很简单，就是你直接声明，abort_if false( 如下图 )，你直接说这个工具这个代码不可能报错，然后让 prover 去推导你这个声明到底对不对，如果不对的话哪里可能有问题。 这个是不是这两个报错的条件，是不是真的是你期望看到的这种条件，我们都可以利用形式化验证工具来帮我们去理解这个程序的代码有什么问题。 我们在实际的开发中经常会遇到说没想到它会报错，但是它实际上报错了的情况，这种时候这个 Prover 工具其实是非常有效的，这个是关于 abort_if false 的介绍。3.2.2 后置条件 Post-conditions
对于一个函数，我们其实除了关注它在什么情况下会出错，我们还想知道它在没有出错的情况下，它这个函数执行完要达到什么样的状态，这是比报错情况更重要的一个事情。 这个在学术上叫 Post Condition, 就是这个函数运行之后的状态，那么显然对于取钱这个函数的话，你得到的状态应该是当你的取钱函数结束了，你的钱肯定会减少，同时你减少的钱一定是等于你要取出来的钱。比如说你说要取 100 万，它一定是只减少 100 万，它不能减少 200 万，他也不能减少 50 万，他只能减少 100 万，这个东西就叫 post condition。 Post condition 是通过一个叫 ensures 的方法来规范，简单来说在区块链上开的户的钱，在这个函数结束之后，是比原来函数开始之前的钱少了多少，少了 amount 这么多，其实就是规范了你取钱的功能。 如果说函数本身写错了，它其实是会报错的，但是这个情况下可能会报两个错，一个是 abort 的，一个是 post condition。他会说你的 post condition 这里其实是不对的，因为你的代码执行完了并不能保证规范的条件，他还会给你一个反例，所以你可以通过这种方法来检测说你的这个函数在运行结束之后，是不是还是符合你的标准。同样的你的 specification 也有可能写错，如果你这里写错了，Prover 会说你这个东西不对。 所以说当你看你看到一个报错的时候，其实就可以想一下，到底是你的规范写错了，还是你的代码写错了，当然也有可能两个都错了，反正但是无论如何它这个东西它给你提供了一个检查的机会。 3.2.3 前置条件 Pre-conditions
函数规范最后一点是“前置条件”，也就是说除了可以写什么情况下会异常、没有异常的话状态会发生什么变化，我们还可以规范在什么情况下，我们可以真正的进入这个函数。比如要求“无论什么时候调用这个函数，必须要求这个人已经开过户了”。在调用内部取钱这个函数的时候，一定要求有一个账户存在，你就可以把这个东西列为所谓的前置条件，你在调用这个函数的时候前置条件一定要存在，有了这个前置条件，就可以简化你的所谓的异常条件。所以简单来说就是你有前置条件，你有异常条件和你有后置条件，你这个东西就可以完整的规范说你这个函数应该做什么，以及不能做什么，这就是函数的规范的内容。3.3 全局不变量 Global Invariants
最后说下全局不变量的规范。之前有人问到，说能不能写一个就是超越函数本身的规则，这个全局变量的全局不变性其实提供的就是这样一个功能。大家都知道程序其实就是一个状态机，如果把整个全局的区块链系统看作一个状态机的话，那么 Global 应该就是全局不变量的功能，它给你提供了一个你去描述什么状态是对的，什么状态是不对的这样一个功能。 同时它还给你描述了在哪些情况下你可以做这个状态的转换，这个是全局不变量能给你提供的。 我们可以给一个具体的例子来看，你写一个银行账户系统，每个账户里面存了每个人多少钱，你其实都不用去定义任何函数，只要定义了账户系统，就可以开始去定义一些全局的东西。 比如说你想建一个非常安全的账户系统，那么你可以定义这个账户系统要保证任何现有的账户不能少于 100 块钱，也就是每个账户都有至少 100 块钱存款。 任何单次的提取，不管你是怎么提取，不管你是去 withdraw 去银行提取或者直接转账，任何提取不能单次提取不能超过 10% 的现有的钱，这些都是可以通过形式化的规范来写的。 其实写出来就是上图这样，只要有一个账户，那么这个账户里面的余额就一定要超过 100 块钱，每任何一次余额的变化，就是比如说余额减少了，那么它必须要小于你原有余额的 10%。 假设说你想描述这样一个金融系统，然后你会发现你在描述这个时候，你根本就不去关心它函数到底怎么实现，你根本不去关心取钱是怎么实现的，只要写这个就可以，然后写完这个之后，就可以去真正去写金融的实现，比如说你有一个取钱的函数，如下图的实现。 当写完上述代码，我们写完的这两个函数自动的就会被这两个全局的规范所限制。 刚刚那个代码去 Prover 验证的时候，我们会发现验证不过，因为写的函数里面并没有去支持的全局规范。 全局的规范在生成支票 make_cheque() 这个函数里面不满足，因为函数逻辑是可以允许违反余额小于 100 这个约束，然后也允许单次取钱超过 10% 这个约束。 同时取钱函数 withdraw() 也不对，它也允许余额小于 100，并且允许余额单次取钱超过 10%。就是这种全局的规范其实是可以作用于所有的函数的，就不管你这个函数写在哪里，这个全局的规范都会去规范到这个函数。 所以说全局规范简单点说，它是一个比函数的本身的规范更高层次的一个规范，它可以允许你去直接描述区块链的状态机，而不去关心具体实现。 如果一个区块链的构架师不关心每个函数怎么执行，但是关心整个全局状态，他要整个区块链系统要保持一个什么样状态，就是这种全局的不变性或者不变量，那么全局规范可以满足这种要求。 其实 Move Prover 里还有很多其他高级的功能，如果大家感兴趣的话，可以持续关注 Move Prover 的进展。推荐阅读
关注 Aptos world
发现 Web3 时代新机遇
公众号后台回复“1” 加入 Aptos 官方社群
【免责声明】市场有风险，投资需谨慎。本文不构成投资建议，用户应考虑本文中的任何意见、观点或结论是否符合其特定状况。据此投资，责任自负。
来源链接
