Verification of the Incremental Merkle Tree Algorithm with Dafny. Cassez, F. CoRR, 2021. 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
{"_id":"Ppbn2vcgoEYhHWyAp","bibbaseid":"cassez-verificationoftheincrementalmerkletreealgorithmwithdafny-2021","author_short":["Cassez, F."],"bibdata":{"bibtype":"article","type":"article","title":"Verification of the Incremental Merkle Tree Algorithm with Dafny","author":[{"firstnames":["Franck"],"propositions":[],"lastnames":["Cassez"],"suffixes":[]}],"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","bibtex":"@article{DBLP:journals/corr/abs-2021,\n title={Verification of the Incremental Merkle Tree Algorithm with Dafny}, \n author={Franck Cassez},\n year={2021},\n eprint={2105.06009},\n archivePrefix={arXiv},\n primaryClass={cs.LO},\n abstract={\n 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.\n },\n journal = {CoRR},\n volume = {abs/2105.06009},\n url = {https://arxiv.org/abs/2105.06009}\n}\n \n","author_short":["Cassez, F."],"key":"DBLP:journals/corr/abs-2021","id":"DBLP:journals/corr/abs-2021","bibbaseid":"cassez-verificationoftheincrementalmerkletreealgorithmwithdafny-2021","role":"author","urls":{"Paper":"https://arxiv.org/abs/2105.06009"},"metadata":{"authorlinks":{}},"downloads":13,"html":""},"bibtype":"article","biburl":"https://franck44.github.io/publications/franck-pubs.bib","dataSources":["8742EsvjQfyP2fYBW"],"keywords":[],"search_terms":["verification","incremental","merkle","tree","algorithm","dafny","cassez"],"title":"Verification of the Incremental Merkle Tree Algorithm with Dafny","year":2021,"downloads":13}