The Deposit Smart Contract (DSC) is an instrumental component of the Ethereum 2.0 Phase 0 infrastructure. We have developed the first machine-checkable version of the incremental Merkle tree algorithm used in the DSC. We present our new and original correctness proof of the algorithm along with the Dafny machine-checkable version. The main results are: 1) a new proof of total correctness; 2) a software artefact with the proof in the form of the complete Dafny code base and 3) new provably correct optimisations of the algorithm.

翻译：存款智能合同(DSC)是Etheum 2.0阶段0基础设施的一个工具部分。 我们开发了DSC中采用的递增的Merkle树算法的第一个机器可检查版本。 我们提供了我们新的和原始的算法正确性证明,以及Dafny机器可检查版本。 主要结果是:1) 新的完全正确性证明;2) 软件精品,以完整的 Dafny 代码基数为形式提供证明;3) 新的、可证实的、正确的算法优化。