https://github.com/billlwhite/ledgertheoryLedger Theory Coq DevelopmentThis repository contains a Coq development of a theory of lightweight cryptographic ledgers. The files should be compiled in the following order (see also the file coqcompile):
Prelude.v Addrs.v CryptoHashes.v CryptoSignatures.v Assets.v Transactions.v LedgerStates.v MTrees.v CTrees.v CTreeGrafting.v Blocks.v
White PaperThere is also a white paper lightcrypto.pdf providing a high level description and overview of what is here. More detailed descriptions of the various parts will hopefully be written soon.
https://github.com/billlwhite/ledgertheory/blob/master/lightcrypto.pdfAbstract
We present representations for cryptographic ledgers which do not
require storing excessive information about transaction histories. Such
representations may allow for the creation of cryptocurrencies which do
not suffer from so-called “block chain bloat.” A corresponding theory
has been formalized in the proof assistant Coq. We give a high level
description and a simplified example. We then give some of the main
definitions and theorems which can be found in the formal development.
I'm not the author