【摘要】 增量Merkle树算法的形式验证 证明存款合约在源代码级别是正确的
以太坊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字节码的行为是否如预期的那样。(原作者：Runtime Verification)