以太坊?2.0存款合同的正式驗(yàn)證

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

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

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

存款智能合約

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

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

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

增量Merkle樹算法的形式化驗(yàn)證

我們?cè)谶\(yùn)行驗(yàn)證時(shí)開始對(duì)存款合約進(jìn)行正式驗(yàn)證，今天我們很高興地宣布我們實(shí)現(xiàn)了第一個(gè)里程碑，即增量Merkle樹算法的形式驗(yàn)證。

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

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

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

讓我們?cè)敿?xì)闡述一下這個(gè)微妙的Bug。在我們被要求驗(yàn)證的合約版本中，當(dāng)Merkle樹的所有葉節(jié)點(diǎn)都充滿了存儲(chǔ)數(shù)據(jù)時(shí)，就會(huì)觸發(fā)這個(gè)bug，在這種情況下，合約（特別是get-deposit-root函數(shù)）錯(cuò)誤地計(jì)算樹的根哈希，返回零根哈希（即空Merkle樹的根哈希），而不考慮葉子節(jié)點(diǎn)的內(nèi)容。例如，假設(shè)我們有一個(gè)高度為2的Merkle樹，它有四個(gè)葉節(jié)點(diǎn)，并且每個(gè)葉節(jié)點(diǎn)都填充了某些存款數(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)不要填充最后一個(gè)葉節(jié)點(diǎn)，即只接受存放最多2^h-1個(gè)，其中h是樹的高度。但是，我們注意到，在當(dāng)前設(shè)置中觸發(fā)此Bug行為是不可行的，因?yàn)樽钚〕练e量為1以太，并且以太網(wǎng)的總供應(yīng)量小于130M，遠(yuǎn)小于2^32，因此填充32高度樹的所有葉子是不可行的。

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