以太坊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字節碼的行為是否如預期的那樣。