Cardano中的半形式化开发方法 2018-06-07
翻译自：https://iohk.io/blog/semi-formal-development-the-cardano-wallet/
注解
把形式化的建模和QuickCheck的测试结合在一起，是开发高可信软件的一把利刃。 通过对不变量的测试来保证模型的一致性，通过和模型的比对来保证真实实现的正确性。
Well-Typed给IOHK做的咨询工作的一部分，就是和他们一起设计和开发Cardano虚拟货币钱包软件的全新版本。其中一个重要部分就是输出了一份关于钱包的 半形式化规范 ， 也就是一个描述钱包运行机制的数学模型以及相关的不变量和定理。
我们把它叫做“半形式化”是因为，虽然它描述了很多钱包的属性，也证明了其中一部分，但并没有证明其所有属性。 不过，就像我们后面会讲到的，我们可以使用 QuickCheck （译注：一个能自动生成测试数据对属性进行测试的工具） 通过生成反例的方式来测试这些属性。 它不仅能帮助我们开发形式规范本身。如果未来我们真的证明了所有属性的正确性，它也为我们测试真实实现提供重要指导。
本文将向大家介绍这份形式规范，以及它是如何驱动新版本钱包的开发和测试的。 我们会展示了这个形式化开发方法的一部分，让大家大致了解它是什么样的，但不会涉及太多细节。 本文的目的是向大家介绍这套开发方法及其优势, 而不是具体的数学理论。
注解
本文所有图表、不变量、章节编号都来自于 1.1版本的规范
背景知识：UTxO记账法
正常银行转账交易是从一个账户往另一个账户转移资产，比如张三给李四转账100元。 但是Cardano和比特币这种虚拟货币的交易略有不同。 交易的输出大体上差不多，唯一区别是可以有多个目标账号，比如一笔交易可以同时转70元给李四，30元给王五。 交易的输入就完全不同了，一笔交易的输入不是来自某个账户，而是来自其他交易。 举个例子，我们把这笔“给李四70元给王五30元”的交易叫做t1。
t1 输入: ... 输出: 70元给李四, 30元给王五
现在如果李四想给赵六转50元，他可以创建一笔新交易说：用掉交易t1的第一个输出，然后给赵六50元，剩下20元给自己。
t2 输入: t1的第一个输出 输出: 50元给赵六, 20元给李四
我们注意到李四需要把20元“找零”转回给自己，因为一个交易输出只能被使用(也就是用作另一笔交易的输入)一次。 这种风格的记账风格就叫做UTxO记账法。UTxO的意思就是未使用的交易输出。
而区块链就是许多这种交易组成的一个列表。对应的形式化定义差不多是这样的：
钱包
虚拟货币的钱包就是一个软件工具，它会监控区块链的状态，跟踪用户的资金（准确的说就是用户的UTxO），也支持往区块链发送新的交易请求。 普通用户主要通过钱包和区块链打交道。至于验证新交易的有效性以及决定是否打包到区块中，这些不是钱包的任务，也就不在本文讨论的范围内了。
钱包的形式规范是一个数学抽象，它只关心钱包最核心的功能，忽略无关的细节。在Cardano钱包的基本模型中，我们把钱包状态简化到只包含UTxO以及在途交易(pending transactions)。 这份规范简单到用一张纸就可以写完：
这个模型很简单，这样才方便进行更深入的研究，也方便提供相关属性的数学证明。 同时又足够精确，可以用来指导钱包的设计，也可以作为单元测试的基础，并驱动真实实现的开发。 他还可以用来研究可能存在的性能问题，以及如何来解决这些问题。
余额
钱包设计中有一些棘手的问题，余额的处理就是其中一个。 你可能觉得在钱包里展示余额应该是一件很简单的事情，但就算在传统银行账户中，也至少存在两种余额。比如张三给李四转100元之后，他的银行账户可能会说：
- 你当前余额为1000元
- 有一笔100元的在途交易，所以你的可用余额为900元
和传统银行交易不同，UTxO风格的交易多了一个找零的概念。 这就会产生三个余额的概念。我们还拿前面的t2交易为例，李四的钱包可能会这么汇报他的余额：
- 你的可用UTxO为1070元
- 有一笔在途交易t2，所以你的可用余额为1000元
- 交易t2会转回20元，所以你的总余额其实是1020元
注意到t2的找零只有当它被打包进区块链之后才可以使用。
目前为止，从钱包设计角度来看，问题还不算复杂，虽然用户界面的展示上可能还需要斟酌一下(要给用户展示哪个余额？)。真正的复杂性来自临时的区块分叉，也就是区块链上对于哪些交易需要被包含进来的分歧（分叉的产生以及如何解决不在本文探讨的范围）。
还是继续上面这个例子，假设t2在途，同时又出现了对t1的争议。争议解决后，钱包发现t1不在区块链中了（可能之后还会被重新包含进来）。 这个时候钱包的可用余额还是1000元，但是总余额如果还是1020元是否合理? 毕竟这样的话，总余额就大于可用UTxO了，倒不是说它一定不对，但总觉得不太舒服。
所以我们在形式规范中又定义了一个最小余额的概念：账户在各种可能出现的情况下，最小的那个余额。 在这个例子中，就是t1和t2都没有被打包进区块链的情况下，余额最小，为1000元 （注意不可能出现t2生效但t1不生效的情况，因为t2依赖t1）。 这个概念在直觉上似乎可行，但是为了让它更加精确并且可以计算，我们还需要引入另一个概念: ‘“预期UTxO”，也就是钱包期望包含进来但还没有被包含进来的UTxO。
当然，就算不通过形式化的方法，我们也可以提出最小余额的概念，并且想出对应的算法。但是有这份形式规范可以让我们对这些问题研究地更加透彻，排除掉真实实现过程中周边的细节问题，专注于最核心的概念。
内部一致性：不变量
当我们引入一个像“预期UTxO”这样的新鲜概念的时候，我们怎么知道它是对的？ 其实，既然新概念是我们自己定义的，再问它是否正确没有太大意义，我们应该问的是，它是否有用？
回答这个问题的一个办法就是找出不变量。不变量就是永远为真的属性。 比如上面展示的基本模型中就有这样一个不变量：
不变量3.4 txins pending ⊆ dom utxo
这个不变量是说，在途交易只能使用UTxO中的输出。这一点在直觉上貌似是显然的：钱包不能让用户使用它自己没有的资金。 然而，就像上面展示的，当我们开始考虑临时分叉的时候，这个不变量就不成立了。 李四提交的t2，使用了t1的一个输出，随后t1被回滚，这个时候他就使用了一个不在当前UTxO中的输出了。
这个时候我们又需要用上“预期UTxO”的概念了，在完整模型中，这个不变量需要改成这样：
不变量7.8 txins pending ⊆ dom (utxo expected)
换句话说，在途交易只能花费UTxO或者预期UTxO。
另一个不变量能够帮助我们巩固对“预期UTxO”这个概念的直觉理解： 一个输出不能既在UTxO中也在预期UTxO中。
不变量7.6 dom utxo 相交 dom expected = ∅
毕竟如果一个预期UTxO出现在当前UTxO里的话就很奇怪了。 列出这样的不变量可以让我们对新概念的直觉理解变得精确， 而证明他们的正确性也能为形式规范的合理性以及内部一致性提供很强的保证。
半形式化开发
形式化地证明上面这样的不变量不光很耗时，还需要专业的数学训练。 如果能够证明他们当然是最完美的，但本文想说的是，尽管我们没有去证明，这个方法依然为我们提供巨大的帮助。 毕竟，我们之所以选择用Haskell编程，就是因为我们可以很容易地在Haskell代码和数学语言之间来回转换。
为了把形式规范中的钱包模型翻译成Haskell，我们使用一个在之前文章中介绍过的方法： Haskell中的面向对象编程 (我们发明这个方法就是用来干这个的)。下面就是把基本模型翻译到Haskell代码的样子：
mkWallet :: (Hash h a, Ord a, Buildable st)
=> Ours a -> Lens' st (State h a) -> WalletConstr h a st
mkWallet ours l self st =
(mkDefaultWallet (l . statePending) self st) {
utxo = st ^. l . stateUtxo
, ours = ours
, applyBlock = \b -> self (st & l %~ applyBlock' ours b)
}
applyBlock' :: Hash h a
=> Ours a -> Block h a -> State h a -> State h a
applyBlock' ours b State{..} = State {
_stateUtxo = updateUtxo ours b _stateUtxo
, _statePending = updatePending b _statePending
}
updateUtxo :: forall h a. Hash h a
=> Ours a -> Block h a -> Utxo h a -> Utxo h a
updateUtxo p b = remSpent . addNew
where
addNew, remSpent :: Utxo h a -> Utxo h a
addNew = utxoUnion (utxoRestrictToOurs p (txOuts b))
remSpent = utxoRemoveInputs (txIns b)
updatePending :: Hash h a
=> Block h a -> Pending h a -> Pending h a
updatePending b = Map.filter $ \t -> disjoint (trIns t) (txIns b)
它比形式规范涉及到更多细节；比如它把具体的hash类型和地址类型抽象出去了。虽然它比规范稍微复杂一点，但也很接近了。 它依然是一个模型：没有处理任何网络或者存储方面的问题，可能也不是很高效，等等。也就是说，这个代码还不是真实钱包的设计。 但有这个模型还是有用的，两个原因，一个是我们可以用它来测试真实的钱包，我们会在下一节讨论这个话题； 另一个是我们可以用这个模型来测试不变量。比如下面的代码就是对上面提到的不变量7.8和7.6的Haskell翻译：
pendingInUtxoOrExpected :: WalletInv h a
pendingInUtxoOrExpected l e =
invariant (l <> "/pendingInUtxoOrExpected") e $ \w ->
checkSubsetOf
("txins pending",
txIns (pending w))
("utxo ∪ expected",
utxoDomain (utxo w) `Set.union` utxoDomain (expectedUtxo w))
utxoExpectedDisjoint :: WalletInv h a
utxoExpectedDisjoint l e =
invariant (l <> "/utxoExpectedDisjoint") e $ \w ->
checkDisjoint
("dom utxo",
utxoDomain (utxo w))
("dom expected",
utxoDomain (expectedUtxo w))
和刚才的钱包实现一样，Haskell代码比对应的形式规范涉及更多细节；比如上面这个代码和形式规范主要区别是可以在不变量不成立时提供详细的错误信息。除此之外，大体上还是对规范的直接翻译。
这样做的好处是，我们可以用QuickCheck来测试这些不变量。 我们为钱包生成随机(但有效)的事件（"应用这个区块"，"提交这笔新交易"，"切换到另一个分叉"），然后检查这些不变量在每一个时间点都成立。 比如规范发布第一个版本的时候就有一个低级错误：当钱包收到一个新区块时，它从预期UTxO里把该区块的输入移除了，而不是输出。一个很蠢的错误，但是如果人工审核的话很容易被忽视。 当然，证明的话可以发现这个问题，但是用QuickCheck也可以：
Wallet unit tests
Test pure wallets
Using Cardano model FAILED [1]
Failures:
test/unit/Test/Spec/Models.hs:36:
1) Wallet unit tests, Test pure wallets, Using Cardano model
predicate failed on: Invalid [] InvariantViolation {
name: full/utxoExpectedDisjoint
, evidence: NotSubsetOf {
dom utxo: ..
, dom expected: ..
, dom utxo `intersection` dom expected: ..
}
, events: {
state: ..
, action: ApplyBlock ..
, state: ..
, action: NewPending Transaction{ .. }
, state: ..
..
, action: Rollback
..
}
}
它不光告诉我们这个不变量不成立了；它还输出了能重现问题的事件序列以及相应的钱包状态（包括所有的中间状态），并且它还显示UTxO和预期UTxO的domain以及他们的交集是什么(他们的交集应该为空，却不为空)。
测试真实的实现
上面说到Haskell对钱包规范的翻译依然是一个模型，其中忽略了大量真实世界的复杂情况，而这些情况是完整的钱包实现必须处理的。 甚至模型中实现的数据类型也是真实版本的简化：交易中没有包含签名，区块只是一个交易列表而不是真实的区块等等。
尽管如此，我们还是可以用这个模型实现来测试真实实现。我们可以把简化版的类型转换到真实版本。既然我们已经有了针对简化类型的QuickCheck测试数据生成器，并且我们也已经能够对模型实现进行测试，我们就可以用下图的方式对真实实现进行测试：
我们先用QuickCheck生成器生成简化模型的钱包事件，然后：
- 在简化类型的测试数据上执行模型实现，然后把结果翻译到真实实现
- 我们先把测试数据翻译到真实类型，然后执行真实钱包的实现
我们可以比对两条执行路径的结果，如果相同的话，我们就可以认为真实钱包正确地实现了这个模型。 我们在每一步都去验证这一点，加上我们前面保证了模型实现中的不变量在每一步都成立，那么我们就能得出结论：不变量在真实实现中也在每一步都成立。
比如，如果真实钱包中有一个bug重复计算了在途交易的找零(比如一笔在途交易使用另一笔在途交易的找零作为输入，这只在分叉的情况下才会出现)，测试用例生成器就会找到一个反例，使得两条执行路径的结果不一致，并且告诉我们导致不一致的具体的钱包事件序列以及相应的钱包状态，以及不一致的具体值。
结论
软件的规范，就算存在，一般也都是些非形式化的文档，使用自然语言描述一下软件预期的功能。 这样的规范不能用来做校验，甚至对测试也用处不大。 另一方面，对所有属性都在数学上加以证明的完整的形式规范，成本很高也很耗时，而且需要相关领域的专家才能搞定。这种做的效果当然是最完美的，但是我们可以有这么一个折中的方案：形式化地描述模型及其属性，然后我们可以用QuickCheck对其属性进行测试。 另外，基于这个模型我们可以对核心功能进行分析，并最终和真实实现进行比对。
IOHK对新钱包的开发是开源的，相关代码可以在 Github 上找到。 有趣的是，IOHK最近还招了人去实现Coq版本的钱包规范，这会把整个规范建立在更加坚实的基础之上。当然，这不代表目前的工作就没有意义，虽然这样的话，在模型实现中去测试不变量不再必要，但是有QuickCheck生成器去测试真实实现还是很有价值的。另外，在实际去证明不变量之前先用QuickCheck测试一遍，如果这个不变量确实不成立的话，可以帮助我们提早发现问题，从而节省宝贵的时间。
