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) 新的、可证实的、正确的算法优化。
相关内容
Merkle Tree，通常也被称作Hash Tree，顾名思义，就是存储hash值的一棵树。Merkle树的叶子是数据块(例如，文件或者文件的集合)的hash值。非叶节点是其对应子节点串联字符串的hash。
相关主题
相关VIP内容
相关资讯
相关论文
微信扫码咨询专知VIP会员