基于 Dafny 的增量默克尔树算法验证
计算机科学中的逻辑
2021-09-01 v3
摘要
存款智能合约（DSC）是以太坊 2.0 第 0 阶段基础设施的关键组成部分。我们开发了 DSC 中使用的增量默克尔树算法的首个机器可检验版本。我们提出了该算法全新的原创正确性证明以及 Dafny 机器可检验版本。主要结果包括：1）全新的完全正确性证明；2）以完整 Dafny 代码库形式呈现的带证明的软件制品；3）算法新的可证明正确的优化。
引用
@article{arxiv.2105.06009,
title = {Verification of the Incremental Merkle Tree Algorithm with Dafny},
author = {Franck Cassez},
journal= {arXiv preprint arXiv:2105.06009},
year = {2021}
}
备注
16 pages