以太坊2 0是一種新的分片PoS協(xié)議，在其早期階段(稱為階段0)與現(xiàn)有的PoW鏈(稱為Eth1鏈)并行共存。雖然Eth1鏈由礦工提供支持，但新的PoS鏈(稱
以太坊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用于生成隨機數(shù)。只要大多數(shù)驗證者在創(chuàng)建和驗證新區(qū)塊時誠實遵循協(xié)議，那么就可以保證鏈其所需的安全性和活躍性。
驗證者集群是動態(tài)變化的，這意味著新的驗證者可以選擇加入和舊驗證者可以隨時選擇退出。要成為(新)驗證者，需要通過將交易(通過Eth1網(wǎng)絡(luò))發(fā)送到指定的智能合約(稱為存款合同)來存入一定數(shù)量的以太幣作為“stake”。存款合約記錄存款歷史，由Beacon鏈檢索以維護動態(tài)驗證者集群。(不過此存款流程將在稍后階段發(fā)生變化。)
存款智能合約
用Vyper編寫的存款智能合約采用Merkle樹數(shù)據(jù)結(jié)構(gòu)來存儲存款歷史，其中每當(dāng)接收到新存款時Merkle樹將被動態(tài)更新(即從左到右依次遞增葉子節(jié)點)。合約中使用的Merkle樹預(yù)計非常大。實際上，在當(dāng)前版本的合約中實現(xiàn)了高度為32的Merkle樹，其可以存儲多達2^32個存款數(shù)量。由于Merkle樹的數(shù)據(jù)量是非常大，所以每次收到新的存款時都需要重建整棵Merkle樹是非常不切實際的。
為了減少時間和空間要求，從而節(jié)省gas成本，合約采用了增量Merkle樹算法。增量算法具有O(h)時間和空間復(fù)雜度來重建Merkle樹(更精確地，計算高度為h的Merkle樹的根)，而樸素算法將需要O(2^h)時間或空間復(fù)雜度。具體來說，該算法維護兩個長度為h的數(shù)組，并且更新Merkle樹的每次重建都需要僅計算從新葉(即新存款)到根的鏈，其中鏈的計算僅需要兩個數(shù)組，從而實現(xiàn)Merkle樹高的線性時間和空間復(fù)雜度。
然而，有效的增量算法導(dǎo)致存款合約的實施非常不透明，并且使得確保其正確性變得非常重要?？紤]到存款合約的重要性，需要進行形式驗證，而這也是最終保證合同正確性的唯一已知方式。
增量Merkle樹算法的形式化驗證
我們在運行驗證時開始對存款合約進行正式驗證，今天我們很高興地宣布我們實現(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成本。
讓我們詳細闡述一下這個微妙的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并非易事，因此我們提出了一種解決方法，只是強制永遠不要填充最后一個葉節(jié)點，即只接受存放最多2^h-1個，其中h是樹的高度。但是，我們注意到，在當(dāng)前設(shè)置中觸發(fā)此Bug行為是不可行的，因為最小沉積量為1以太，并且以太網(wǎng)的總供應(yīng)量小于130M，遠小于2^32，因此填充32高度樹的所有葉子是不可行的。
因此，現(xiàn)在我們確信增量Merkle樹算法及其存款合約的實現(xiàn)在源代碼級別是正確的，接下來，我們將繼續(xù)正式驗證其編譯的EVM字節(jié)碼的行為是否如預(yù)期的那樣。(原作者：Runtime Verification)
關(guān)鍵詞： 增量Merkle樹算法 形式驗證
