介绍 [V] 规范语言

引入 [V] 规范语言

在之前的博客中，我们探讨了如何使用形式化验证来证明程序不存在逻辑错误。然而，为了使用形式化验证工具，开发者需要提供一个 规范 以数学精确的方式描述程序的预期行为。在本博客中，我们将通过说明 Veridise 的规范语言 [V] 如何用于指定以下简单钱包合约的各种属性进行探讨：

contract Wallet {
    mapping(address => uint) balances;
    function balanceOf(address addr) public view returns (uint) {
        return balances[addr];
    }
    function deposit() payable external {
        balances[msg.sender] += msg.value;
   }
   function withdraw(uint amt) external {
       require(amt <= balanceOf(msg.sender));
       payable(msg.sender).transfer(amt);
   }
}

[V] 语句

[V] 规范语言的核心是 [V] 语句，它们是构成所有 [V] 规范的基本构件。简单来说，[V] 语句允许用户指定在某些交易发生时应该满足的属性。例如，考虑钱包合约的 deposit 方法，假设我们想要表示调用 deposit 总是成功完成，并且状态下用户的钱包余额会按存入的金额更新。这可以使用以下 [V] 语句表示：

finished(Wallet.deposit(), this.balanceOf(sender) =
         old(this.balanceOf(sender)) + value)

该语句的形式为 finished(transaction, property)，表示交易应该始终成功完成（不应回滚），处于满足该属性的状态。因此，上述 [V] 语句指定了两个重要的信息：

1. 调用 Wallet.deposit() 应该永远不会导致异常
2. 当 Wallet.deposit() 执行完毕时，用户的余额（即，sender）应该增加发送的金额（即，value）。

这里请注意，构造 old(t) 指的是交易开始之前，t 的值，而在规范中使用的任何整数都假设为数学整数（即，没有溢出）。

作为另一个例子，假设我们想表示钱包不允许用户提取超过其拥有金额的资金。这一属性可以使用以下 [V] 语句表示：

reverted(Wallet.withdraw(amt), amt > this.balanceOf(sender))

该规范使用了另一种谓词，称为 reverted，形式为 reverted(transaction, property)，表示当在满足该属性的状态下调用时，交易应该回滚。因此，它表达了，当消息发送者的余额小于指定金额时，提取 amt 会导致交易失败。

更一般地，所有 [V] 语句具有以下形式：

predicate ( transaction, property )

其中：

• predicate 约束交易执行结果在区块链上的表现。 [V] 中最常用的三个谓词是 started、finished 和 reverted。
• transaction 是形如 contract.methodName(arguments) 的表达式，描述某个合约方法的调用。
• property 是一个布尔表达式，可以引用方法参数、合约变量、合约函数、隐含的区块链变量和 [V] 内置函数。其中一些最常见的内置函数是 old(t) 和 sum(t)，其中 old(t) 返回在交易开始时评估的 t 的值，sum(t) 返回集合 t 中所有值的总和。

合约不变式

在许多情况下，我们希望表达在每个交易之前和之后某个属性应该保持成立。我们称这些属性为 合约不变式。直观地说，合约不变式表示某个属性应该在每个合约方法执行之前和之后保持成立。

例如，上述钱包合约的一个关键属性是合约的余额应该等于不同账户之间的所有余额的总和。这个属性可以使用以下 [V] 不变式表示：

inv: started(Wallet.*, balance(this) = sum(this.balances))

其中 * 匹配合约的任何方法。这样的注释告诉验证器检查合约在其执行过程中是否遵循合约不变式。

方法合约

除了指定合约不变式外，我们还通常希望表达每个方法的个别属性。这些属性使用方法合约形式 Pre |=> Post 来捕捉，其中 Pre 是在调用该方法时应成立的属性，Post 是在该方法完成执行后应成立的属性。例如，回到我们的钱包示例，我们自然希望在 withdraw 方法成功执行后，用户的余额会因提取的金额而减少。这个属性可以使用以下 [V] 方法合约表示：

spec: finished(Wallet.withdraw(amt), this.balanceOf(sender) >= amt
               |=> balance(this) = old(balance(this)) - amt)

这个方法合约表示，如果用户请求提取 amt ETH 并且 balanceOf(msg.sender) 至少为要提取的 ETH 金额，则交易不应回滚，并且合约的 ETH 余额应该减少提取的金额。请注意，finished 的第二个参数使用 Pre |=> Post 构造，其中 Pre 指定了 withdraw 成功完成的前置条件，Post 指定了 withdraw 成功终止时应成立的条件。根据这样的合约，验证器需要检查两个条件：

1. 如果满足指定的前置条件，withdraw 方法永远不会回滚；
2. 在满足前置条件的假设下，withdraw 终止时处于满足后置条件的状态。

行为规范

除了指定单个方法的属性外，我们可能还希望指定同一合约的不同方法之间如何相互作用。我们也可以在 [V] 语言中表达这些更复杂的规范。

为了说明这些规范，假设我们希望表达一个钱包的 withdraw 函数是 deposit 的逆向操作。也就是说，如果用户能够成功存入一些 ETH，那么他们应该能够成功地提取相同的金额，以撤销存入函数所做的更改。这可以使用以下 [V] 规范表示：

vars: Wallet wallet, uint ethBal, address u, uint uBal, uint a
spec: finished(wallet.deposit(), value = a && u = sender &&
          ethBal = old(balance(this)) &&
          uBal = old(this.balanceOf(u)));
      finished(wallet.withdraw(amt), amt = a && u = sender
          |=> ethBal = balance(this) && uBal = this.balanceOf(u))

这里的 ; 表示顺序操作符。特别地，表达式

predicate1( transaction1, property1 ) ;
predicate2 ( transaction2, property2 )

具有以下语义：“在一个交易2在交易1之前执行的执行中，两个属性都应该成立”。因此，上述钱包规范表明存入一些金额 amt，然后提取相同的金额应该结束在一个余额没有总体变化的状态。请注意，在该规范中使用的变量 ethBal、u、uBal 和 a 使我们能够在不同交易之间关联值。

现在我们知道如何将交易彼此关联，让我们看看如何表达一组帐户的属性。作为示例，请考虑以下 [V] 规范，表示用户只能提取自己的资金：

vars: Wallet wallet, address u1, address u2, uint a
init: finished(wallet.constructor()) ;
      finished(wallet.deposit(), sender = u1 && value = a) ;
      finished(wallet.deposit(), sender = u2 && u2 != u1)
spec: reverted(wallet.withdraw(amt), sender = u1 && amt > a)

这样的规范最好被视为“符号单元测试”，其中规范的 “init” 部分设置了一些期望的区块链状态，而 “spec” 部分则断言在该状态下应该具备的属性。具体而言，该规范声明了一个钱包 wallet 和两个用户 u1 和 u2。初始化阶段考虑了一个钱包的用例，其中 u1 存入金额 a，然后是另一个用户 u2 的（未知）存款。该规范断言，在该合约的此类用例下，u1 不应能够提取超过 a 的金额。这样的规范类似于测试用例，只不过用户和存款/提取的金额是符号的。因此，检查这样的规范就像是测试所有满足给定约束的存款/提取金额的所有可能实例。

展望未来

到目前为止，我们所看的所有规范都是安全属性的实例，它们表示某种不良事件永远不会发生（即，不会到达不希望的状态）。在某些情况下，我们可能也希望表达某些良好事件最终会发生。例如，作为竞拍的参与者，我们可能希望表达如果我不是拍卖的赢家，我最终会拿回我的出价。这样的属性是活跃性属性的示例，可以使用时间操作符在 [V] 中表达。我们将把这种时间规范的讨论留到我们系列中的下一篇博客中。

总结

[V] 是一种强大的规范语言，提供了很多工具让用户表达他们关心的属性。它通过允许用户表达多种类型的规范，包括方法合约、行为规范和时间规范，来实现这一点。所有这些规范都使用一个共同的组件，即 [V] 语句，使用户能够轻松地表达新类型的规范，而无需额外的知识。 [V] 语句是声明式的，允许用户简洁地表达交易的属性及其之间的关系。有关 [V] 的更多信息，请参见 我们的文档。

• 原文链接： medium.com/veridise/intr...
• 登链社区 AI 助手，为大家转译优秀英文文章，如有翻译不通的地方，还请包涵～