I wrote a paper called "Authenticated Data Structures, Generically" [1] that's closely related to this. It shows how to automatically make a "merkleized" versio

I wrote a paper called "Authenticated Data Structures, Generically" [1] that's closely related to this. It shows how to automatically make a "merkleized" version of any (pure functional) data structure. The original motivation (and a case study in the paper) is making Bitcoin verifiers that don't require much storage, similar to this. I don't fully understand the compact tree proposed here. I used balanced red-black trees, and others have suggested tries since the element size is fixed (160-bit address, or 256-bit tx hashes). I think you're basically proposing a trie. It would be possible to make invalid addresses that incur the worst-case cost to check (00001, 00002, 00010, 00020, and so on) but this is maybe splitting hairs. Anyway, this is awesome to use Coq for formal verification of cryptocurrency components. We need way more of this. [1] http://www.cs.umd.edu/~amiller/gpads/ http://www.cs.umd.edu/~amiller/gpads/