以太坊​2.0存款合同的正式验证

以太坊2.0是一种新的分片PoS协议，在其早期阶段（称为阶段0）与现有的PoW链（称为Eth1链）并行共存。虽然Eth1链由矿工提供支持，但新的PoS链（称为Beacon链）将由验证者驱动。

在Beacon链中，验证者的作用是创建（称为propose）和验证（称为attest）新区块。Beacon链的共识协议建立在重要小工具之上，Casper FFG用于最终区块化，LMD GHOST用于分叉选择规则，RANDAO用于生成随机数。只要大多数验证者在创建和验证新区块时诚实遵循协议，那么就可以保证链其所需的安全性和活跃性。

验证者集群是动态变化的，这意味着新的验证者可以选择加入和旧验证者可以随时选择退出。要成为（新）验证者，需要通过将交易（通过Eth1网络）发送到指定的智能合约（称为存款合同）来存入一定数量的以太币作为“stake”。存款合约记录存款历史，由Beacon链检索以维护动态验证者集群。（不过此存款流程将在稍后阶段发生变化。）

存款智能合约

用Vyper编写的存款智能合约采用Merkle树数据结构来存储存款历史，其中每当接收到新存款时Merkle树将被动态更新（即从左到右依次递增叶子节点）。合约中使用的Merkle树预计非常大。实际上，在当前版本的合约中实现了高度为32的Merkle树，其可以存储多达2^32个存款数量。由于Merkle树的数据量是非常大，所以每次收到新的存款时都需要重建整棵Merkle树是非常不切实际的。

为了减少时间和空间要求，从而节省gas成本，合约采用了增量Merkle树算法。增量算法具有O（h）时间和空间复杂度来重建Merkle树（更精确地，计算高度为h的Merkle树的根），而朴素算法将需要O（2^h）时间或空间复杂度。具体来说，该算法维护两个长度为h的数组，并且更新Merkle树的每次重建都需要仅计算从新叶（即新存款）到根的链，其中链的计算仅需要两个数组，从而实现Merkle树高的线性时间和空间复杂度。

然而，有效的增量算法导致存款合约的实施非常不透明，并且使得确保其正确性变得非常重要。考虑到存款合约的重要性，需要进行形式验证，而这也是最终保证合同正确性的唯一已知方式。

增量Merkle树算法的形式化验证

我们在运行验证时开始对存款合约进行正式验证，今天我们很高兴地宣布我们实现了第一个里程碑，即增量Merkle树算法的形式验证。

具体来说，我们首先严格形式化了增量Merkle树算法。然后，我们提取了存款合约中使用的算法的伪代码实现，并正式证明了伪代码实现的正确性。这意味着存款合约在源代码级别是正确的，也就是说，如果Vyper编译器或EVM字节码级功能正确性没有引入编译时错误，它将以增量方式正确计算Merkle树根。 （实际上，我们的下一个任务是确保字节码级别的正确性。）

意外发现

在我们的形式化和正确性证明工作的过程中，我们发现存款合同的一个微妙的Bug，但已在最新版本中修复以及一些重构建议，可以提高代码可读性和降低gas成本。

让我们详细阐述一下这个微妙的Bug。在我们被要求验证的合约版本中，当Merkle树的所有叶节点都充满了存储数据时，就会触发这个bug，在这种情况下，合约（特别是get-deposit-root函数）错误地计算树的根哈希，返回零根哈希（即空Merkle树的根哈希），而不考虑叶子节点的内容。例如，假设我们有一个高度为2的Merkle树，它有四个叶节点，并且每个叶节点都填充了某些存款数据，分别为D1，D2，D3和D4。虽然树的正确根哈希是hash（hash（D1，D2），hash（D3，D4）），但get_deposit_root函数返回hash（hash（0，0），hash（0，0）），这是不正确的。

由于代码的逻辑复杂，在不重写代码的情况下正确修复此Bug并非易事，因此我们提出了一种解决方法，只是强制永远不要填充最后一个叶节点，即只接受存放最多2^h-1个，其中h是树的高度。但是，我们注意到，在当前设置中触发此Bug行为是不可行的，因为最小沉积量为1以太，并且以太网的总供应量小于130M，远小于2^32，因此填充32高度树的所有叶子是不可行的。

因此，现在我们确信增量Merkle树算法及其存款合约的实现在源代码级别是正确的，接下来，我们将继续正式验证其编译的EVM字节码的行为是否如预期的那样。