[DEPRECATED: The result in this directory is outdated. The deposit contract has been reimplemented in Solidity and reverified. The latest result can be found at https://github.com/runtimeverification/deposit-contract-verification.]
This directory presents our formalization of the incremental Merkle tree algorithm, especially the one employed in the deposit contract, and prove its correctness w.r.t. the original full-construction Merkle tree algorithm.
Documents:
Mechanized specifications and proofs in K:
- deposit.k: Formal model of the incremental Merkle tree algorithm
- deposit-spec.k: Correctness specifications
- deposit-symbolic.k: Lemmas (trusted)
To prove the specifications:
$ ./run.sh
Prerequisites:
- Install K: https://github.com/kframework/k/releases