Overview

The ouroboros-high-assurance library contains formalizations related to the Ouroboros family of blockchain consensus protocols. Concretely, it comprises the following:

• A proof of the chain selection property
• Draft specifications of the following consensus protocols, using the Þ-calculus:
  • Ouroboros BFT
  • Ouroboros Praos
• A specification of the Chain-Sync mini-protocol, using the Þ-calculus
• A framework for specifying mini-protocols
• Specifications of the following mini-protocols, using the above-mentioned framework:
  • Chain-Sync
  • Ping-Pong
  • Request-Response

Requirements

You need Isabelle2022 to use this Isabelle library. You can obtain Isabelle2022 from the Isabelle website.

In addition, you need the following Isabelle sessions:

• Finite-Map-Extras
• Thorn_Calculus

Setup

To make this Isabelle library available to your Isabelle installation, add the path of the src directory to the file $ISABELLE_HOME_USER/ROOTS. You can find out the value of $ISABELLE_HOME_USER by running the following command:

isabelle getenv ISABELLE_HOME_USER

Building

Running make builds the PDF file that includes the documentation and the code and places it in $ISABELLE_BROWSER_INFO/IOG. You can find out the value of $ISABELLE_BROWSER_INFO by running the following command:

isabelle getenv ISABELLE_BROWSER_INFO

The makefile specifies two targets: properly, which is the default, and qnd. With properly, fake proofs (sorry) are not accepted; with qnd, quick-and-dirty mode is used and thus fake proofs are accepted.