meta.yml

---
fullname: PoS-NSB
shortname: PoS-NSB
opam_name: coq-pos-nsb
organization: AU-COBRA
community: false
dune: true
action: true

synopsis: Coq formalization of a proof-of-stake Nakamoto-style blockchain

description: |-
  This repository contains a formalization of Proof-of-Stake (PoS)
  Nakamoto-style blockchain (NSB). Assuming a synchronous network
  with a static set of corrupted parties we prove chain growth,
  chain quality, and common prefix.

publications:
- pub_url: https://arxiv.org/abs/2007.12105
  pub_title: Formalizing Nakamoto-Style Proof of Stake

authors:
- name: Søren Eller Thomsen
- name: Bas Spitters

opam-file-maintainer: palmskog@gmail.com

opam-file-version: dev

license:
  fullname: MIT License
  identifier: MIT

supported_coq_versions:
  text: '8.11 or later'
  opam: '{>= "8.11" & < "8.13~"}'

tested_coq_opam_versions:
- version: '1.11.0-coq-8.12'
  repo: 'mathcomp/mathcomp'
- version: '1.11.0-coq-8.11'
  repo: 'mathcomp/mathcomp' 

dependencies:
- opam:
    name: coq-mathcomp-ssreflect
    version: '{>= "1.11" & < "1.12~"}'
  description: |-
    [MathComp ssreflect 1.11.0](https://math-comp.github.io)
- opam:
    name: coq-mathcomp-finmap
    version: '{>= "1.5"}'
  description: |-
    [MathComp finmap 1.5.0](https://github.com/math-comp/finmap)
- opam:
    name: coq-equations
    version: '{>= "1.2.2"}'
  description: |-
    [Equations 1.2.2](https://github.com/mattam82/Coq-Equations)
- opam:
    name: coq-record-update
  description: |-
    [Coq record update](https://github.com/tchajed/coq-record-update)

namespace: AUChain

keywords:
- name: blockchain
- name: consensus

categories:
- name: Computer Science/Concurrent Systems and Protocols/Theory of concurrent systems

build: |-
  ## Building
  The requirements can be installed via [OPAM](https://opam.ocaml.org/doc/Install.html):
  ```
  opam repo add coq-released https://coq.inria.fr/opam/released
  opam install coq.8.11.2 coq-mathcomp-ssreflect.1.11.0 \
    coq-mathcomp-finmap coq-equations coq-record-update
  ```
  Then, run `make clean; make` from the root folder. This will build all
  the libraries and check all the proofs.

documentation: |-
  ## Project Structure

  The top-level structure consists of the following folders:
  
  - `Protocol` - parameters for the development, implementation of the
    actual protocol and definition of a block tree.
  - `Model` - definition of the network, global state, and definition of
    reachable global states.
  - `Properties` - proved properties about the protocol. `CG.v` contains
    the chain growth theorem, `CQ.v` contains the chain quality theorem,
    and `CP.v` contains the common prefix theorem.

  Below is a depiction of the dependencies between the files.

  <p align="center">
   <img src="deps.svg" width="500" title="File dependencies" />
  </p>
---