A Coq development of a theory of lightweight cryptographic ledgers(github.com)
github.com
A Coq development of a theory of lightweight cryptographic ledgers
https://github.com/billlwhite/ledgertheory
4 comments
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.
See Qointum: https://qointum.com
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
Where's the whitepaper?
I've been interested in formal treatments of ledgers for a while now. Does anyone know if other work has been done in this area?
[deleted]
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/