Verification of the Incremental Merkle Tree Algorithm with Dafny. Cassez, F. CoRR, 2021.
Verification of the Incremental Merkle Tree Algorithm with Dafny [link]Paper  abstract   bibtex   13 downloads  
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.
@article{DBLP:journals/corr/abs-2021,
    title={Verification of the Incremental Merkle Tree Algorithm with Dafny}, 
    author={Franck Cassez},
    year={2021},
    eprint={2105.06009},
    archivePrefix={arXiv},
    primaryClass={cs.LO},
    abstract={
    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.
    },
  journal   = {CoRR},
  volume    = {abs/2105.06009},
  url       = {https://arxiv.org/abs/2105.06009}
}

Downloads: 13