3 ms·
A Coq development of a theory of lightweight cryptographic ledgers
- gtank 12y agoI've been interested in formal treatments of ledgers for a while now. Does anyone know if other work has been done in this area?
- socrates1024 12y agoI 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/
- deleted 12y ago[deleted]
- qarterd 12y agoIt'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. See Qointum: https://qointum.com https://qointum.com
- woah 12y agoWhere's the whitepaper?