驗證者叢集是動態變化的，這意味著新的驗證者可以選擇加入和舊驗證者可以隨時選擇退出。要成為（新）驗證者，需要透過將交易（透過Eth2網路）傳送到指定的智慧合約（稱為存款合同）來存入一定數量的以太幣作為“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
