Ledger Theory Coq Development

[HostFat]

https://github.com/billlwhite/ledgertheory

Ledger Theory Coq Development
This 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 Paper
There 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.pdf

Abstract
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

[1715570216]

1715570216

[1715570216]

1715570216

[1715570216]

1715570216

[1715570216]

1715570216

[1715570216]

1715570216

[1715570216]

1715570216

[ffe]

Still reading through this and so far it's very interesting but I wanted to make one comment. The paper should make clear up front that your use of the term "forge" is related to mining a block and not related to creating an illegal block.  You mean forge as in create not forgery.

[tzpardi]

This seems really interesting.

[kanzure]

Above hyperlink is 404, an alternative link seems to be https://github.com/bitemyapp/ledgertheory