Our formalization of the incremental Merkle tree algorithm, especially the one employed in the deposit contract, and its correctness proof w.r.t. the original full-construction Merkle tree algorithm can be found in the final report.
The correctness proof presented in the report has also been mechanized in K:
- deposit.k: Formal model of the incremental Merkle tree algorithm
- deposit-spec.k: Correctness specifications
- deposit-symbolic.k: Lemmas (trusted)
To run the mechanized proof:
$ make deps
$ make build
$ make test
Prerequisites:
- Install K: https://github.com/kframework/k/releases