Solidity 语言的形式化规约

一篇来自BME的论文介绍了基于事件的形式化规约，并给出了名为 SOLC_VERIFY的 验证程序。但是本文章只关心其提出的形式化规约说明。验证程序基于模块化程序验证，由Mike Barnett在其之前的论文中提出，这与计算科学和程序语义等学科相关，不做讨论。

智能合约事件介绍

本文介绍的方法主要用于依靠事件 (Event) 传递消息的 Solidity 程序。

Solidity 是面向合约的智能合约编程语言的代表。而事件代表了与用户相关的、有限的交易执行。合约可以利用事件传递链上数据的状态改变情况。技术上来说，事件可以看做有参数的触发器，其存储位置位于区块链的日志。这些日志是合约无法访问的，而用户却可以轻易的监听这些事件从而获得值。以往，事件往往是被认为是一种日志记录机制，与程序设计的正确性无关。然而，既然事件是DAPP中最主要的为用户设计的状态改变提示机制，确保用户正确理解且信任发送的事件是十分关键的。

Solidity 不为发送事件设置任何限制，因此错误的（或恶意的）合约可以发送与状态改变不一致的事件，或对于某些改变忽略发送事件，潜在的将会误导用户。

语法举例

请首先看已经加入形式化规约的 Solidity 演示代码：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29

contract Registry {
	struct Entry { bool set; int data; } // User-defined type
	mapping(address=>Entry) entries; // State variable
	
	/// @notice tracks-changes-in entries
	/// @notice precondition !entries[at].set
	/// @notice postcondition entries[at].set && entries[at].data == value 
	event new_entry(address at, int value);
	
	/// @notice tracks-changes-in entries
	/// @notice precondition entries[at].set && entries[at].data < value 		
	/// @notice postcondition entries[at].set && entries[at].data == value 
	event updated_entry(address at, int value);
	
	/// @notice emits new_entry
	function add(int value) public { 
		require(!entries[msg.sender].set); 
		entries[msg.sender].set = true; 
		entries[msg.sender].data = value; 
		emit new_entry(msg.sender, value);
	}
	
	/// @notice emits updated_entry
	function update(int value) public {
		require(entries[msg.sender].set && entries[msg.sender].data < value); 
		entries[msg.sender].data = value;
		emit updated_entry(msg.sender, value);
	} 
}

演示代码非常简单，定义了一个 Entry 结构，和一个地址到 Entry 的映射的变量（在文章中叫做状态变量，state variable)；两个事件，一个代表新加入合约，另一个代表更新加入合约。以及添加和更新的函数。

首先，某个事件都跟随的是 entries 变量的变化，因此我们写出：

1

/// @notice tracks-changes-in entries

tracks-changes-in 关键字所说明的事实是：事件被触发当且仅当被跟踪的变量改变。由于数据经常以多步过程的形式改变（如例子中，函数依次更新了 Entry 结构中的两个数据），或者数据更新存在某种条件，因此事件不会总是立刻跟在某个追踪变量的改动后。因此，文章提出了前/后检查点的概念。前检查点是由事件所追踪的变量的第一次改变所动态的定义的。相对的，后检查点是一个静态边界，一般是循环或交易的边缘。说白了就是，你的事件必须要在你跟的变量第一次改变之后，离开程序之前进行一次激发。

在跟随变量以外，事件也可以被用 predicates 来注释，它是用状态变量和事件的参数来定义的，并且有两种，preconditions 和 postconditions。前置条件在前检查点前捕捉状态变量的值，而后置条件对应着事件被发送的时刻。

举例来说，对于 new_entry 事件，其要求用户一开始不处于 entries，即set 布尔类型为假，且事件发出后用户属于entries，data 被赋值。

1
2
3

/// @notice precondition !entries[at].set
/// @notice postcondition entries[at].set && entries[at].data == value 
event new_entry(address at, int value);

最后，发射事件的函数必须被标记处发射了何等事件：

1
2
3
4

/// @notice emits updated_entry
function update(int value) public {
...
}

基于函数的形式化规约和基于事件的有很多相似之处（并且是南大78004870课程所讲述的模式），只是把修改变量的规约放在函数（与合约、循环）前。并且由于函数可以对值进行修改，而非像事件一样仅展现变化，所以会比基于事件的规约增加其他的东西。请看下例：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24

/// @notice invariant x == y
contract Track {
	int x;
	int y;
	
	/// @notice precondition x == y
	/// @notice postcondition x == (y + n)
	/// @notice modifies x
	function add_to_x(int n) internal {
		x = x + n;
		require(x >= y);
	}
	
	/// @notice modifies x if n > 0
	/// @notice modifies y if n > 0
	function add(int n) public {
		require(n >= 0);
		add_to_x(n);
		/// @notice invariant y<=x
		while(y < x) {
			y = y + 1;
		}
	}
}

由例子，我们可以总结出基本的语句：

• 如果某变量没有被改变，那么需要注明不变式：

  1	invariant <EXPRESSION>

  注意，不变式出现在循环，合约，函数前。

• 如果函数开始前/结束后必须满足某条件，那么需要注明前置条件/后置条件，与基于事件的一样。

• 如果函数执行改变了状态变量，那么需要注明修改规约：

  1	modifies <TARGET> [if <CONDITION>]

进阶的规约表达

课程同时给出了一些进阶的规约表达方式，例如：

• 聚合计算的表达：

  1	__verifier_sum_<TYPE>( ... )

  所代表了将 <TYPE> 相加所得到的结果。

• 复合数据类型判等：

  1	__verifier_eq(..., ...)

  其实就是更加复杂的 x == y。

• 变量旧值引用:

  1	__verifier_old_<TYPE>

  也许是在循环中引用上一次的值或者引用修改前的值。

• 谓词逻辑表达：

  1 2 3

  forall (<VARS>) <QUANTEXPR> exists (<VARS>) <QUANTEXPR>

  举例来说：

  1	forall (uint λ) !(λ >= 0 && λ < length)

形式化规约是一种让程序设计更加严谨的实现，而对于对准确度要求高的智能合约来说更加有用。即使没有检查器，掌握形式化合约也有助于形成良好的变量追踪与查询习惯。