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.
It's nice to see a formal proof of lightweight ledgers, but this concept of account states in a merkle tree with merkle path verified state deltas is nothing new.
As the author states, lightweight ledgers are well suited to proof of stake. I'm working on such a crypto 2.0 that also uses the Python VM for smart contracts and is multichain scalable with cross-chain contracts.
[+] [-] socrates1024|11 years ago|reply
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/
[+] [-] qarterd|11 years ago|reply
As the author states, lightweight ledgers are well suited to proof of stake. I'm working on such a crypto 2.0 that also uses the Python VM for smart contracts and is multichain scalable with cross-chain contracts.
See Qointum: https://qointum.com
[+] [-] woah|11 years ago|reply
[+] [-] gtank|11 years ago|reply
[+] [-] unknown|11 years ago|reply
[deleted]