以太坊2.0是一種新的分片PoS協(xié)議，在其早期階段（稱為階段0）與現(xiàn)有的PoW鏈（稱為Eth1鏈）并行共存。雖然Eth1鏈由礦工提供支持，但新的PoS鏈（稱為Beacon鏈）將由驗證者驅(qū)動。

在Beacon鏈中，驗證者的作用是創(chuàng)建（稱為propose）和驗證（稱為attest）新區(qū)塊。Beacon鏈的共識協(xié)議建立在重要小工具之上，Casper FFG用于最終區(qū)塊化，LMD GHOST用于分叉選擇規(guī)則，RANDAO用于生成隨機(jī)數(shù)。只要大多數(shù)驗證者在創(chuàng)建和驗證新區(qū)塊時誠實遵循協(xié)議，那么就可以保證鏈其所需的安全性和活躍性。

驗證者集群是動態(tài)變化的，這意味著新的驗證者可以選擇加入和舊驗證者可以隨時選擇退出。要成為（新）驗證者，需要通過將交易（通過Eth1網(wǎng)絡(luò)）發(fā)送到指定的智能合約（稱為存款合同）來存入一定數(shù)量的以太幣作為“stake”。存款合約記錄存款歷史，由Beacon鏈檢索以維護(hù)動態(tài)驗證者集群。（不過此存款流程將在稍后階段發(fā)生變化。）

存款智能合約

用Vyper編寫的存款智能合約采用Merkle樹數(shù)據(jù)結(jié)構(gòu)來存儲存款歷史，其中每當(dāng)接收到新存款時Merkle樹將被動態(tài)更新（即從左到右依次遞增葉子節(jié)點）。合約中使用的Merkle樹預(yù)計非常大。實際上，在當(dāng)前版本的合約中實現(xiàn)了高度為32的Merkle樹，其可以存儲多達(dá)2^32個存款數(shù)量。由于Merkle樹的數(shù)據(jù)量是非常大，所以每次收到新的存款時都需要重建整棵Merkle樹是非常不切實際的。

為了減少時間和空間要求，從而節(jié)省gas成本，合約采用了增量Merkle樹算法。增量算法具有O（h）時間和空間復(fù)雜度來重建Merkle樹（更精確地，計算高度為h的Merkle樹的根），而樸素算法將需要O（2^h）時間或空間復(fù)雜度。具體來說，該算法維護(hù)兩個長度為h的數(shù)組，并且更新Merkle樹的每次重建都需要僅計算從新葉（即新存款）到根的鏈，其中鏈的計算僅需要兩個數(shù)組，從而實現(xiàn)Merkle樹高的線性時間和空間復(fù)雜度。

然而，有效的增量算法導(dǎo)致存款合約的實施非常不透明，并且使得確保其正確性變得非常重要。考慮到存款合約的重要性，需要進(jìn)行形式驗證，而這也是最終保證合同正確性的唯一已知方式。

增量Merkle樹算法的形式化驗證

我們在運行驗證時開始對存款合約進(jìn)行正式驗證，今天我們很高興地宣布我們實現(xiàn)了第一個里程碑，即增量Merkle樹算法的形式驗證。

具體來說，我們首先嚴(yán)格形式化了增量Merkle樹算法。然后，我們提取了存款合約中使用的算法的偽代碼實現(xiàn)，并正式證明了偽代碼實現(xiàn)的正確性。這意味著存款合約在源代碼級別是正確的，也就是說，如果Vyper編譯器或EVM字節(jié)碼級功能正確性沒有引入編譯時錯誤，它將以增量方式正確計算Merkle樹根。 （實際上，我們的下一個任務(wù)是確保字節(jié)碼級別的正確性。）

意外發(fā)現(xiàn)

在我們的形式化和正確性證明工作的過程中，我們發(fā)現(xiàn)存款合同的一個微妙的Bug，但已在最新版本中修復(fù)以及一些重構(gòu)建議，可以提高代碼可讀性和降低gas成本。

讓我們詳細(xì)闡述一下這個微妙的Bug。在我們被要求驗證的合約版本中，當(dāng)Merkle樹的所有葉節(jié)點都充滿了存儲數(shù)據(jù)時，就會觸發(fā)這個bug，在這種情況下，合約（特別是get-deposit-root函數(shù)）錯誤地計算樹的根哈希，返回零根哈希（即空Merkle樹的根哈希），而不考慮葉子節(jié)點的內(nèi)容。例如，假設(shè)我們有一個高度為2的Merkle樹，它有四個葉節(jié)點，并且每個葉節(jié)點都填充了某些存款數(shù)據(jù)，分別為D1，D2，D3和D4。雖然樹的正確根哈希是hash（hash（D1，D2），hash（D3，D4）），但get_deposit_root函數(shù)返回hash（hash（0，0），hash（0，0）），這是不正確的。

由于代碼的邏輯復(fù)雜，在不重寫代碼的情況下正確修復(fù)此Bug并非易事，因此我們提出了一種解決方法，只是強(qiáng)制永遠(yuǎn)不要填充最后一個葉節(jié)點，即只接受存放最多2^h-1個，其中h是樹的高度。但是，我們注意到，在當(dāng)前設(shè)置中觸發(fā)此Bug行為是不可行的，因為最小沉積量為1以太，并且以太網(wǎng)的總供應(yīng)量小于130M，遠(yuǎn)小于2^32，因此填充32高度樹的所有葉子是不可行的。

因此，現(xiàn)在我們確信增量Merkle樹算法及其存款合約的實現(xiàn)在源代碼級別是正確的，接下來，我們將繼續(xù)正式驗證其編譯的EVM字節(jié)碼的行為是否如預(yù)期的那樣。