mirror of
https://github.com/tendermint/tendermint.git
synced 2026-01-07 13:55:17 +00:00
34 lines
1.9 KiB
Markdown
34 lines
1.9 KiB
Markdown
# Ivy Proofs
|
|
|
|
```copyright
|
|
Copyright (c) 2020 Galois, Inc.
|
|
SPDX-License-Identifier: Apache-2.0
|
|
```
|
|
|
|
## Contents
|
|
|
|
This folder contains:
|
|
|
|
* `tendermint.ivy`, a specification of Tendermint algorithm as described in *The latest gossip on BFT consensus* by E. Buchman, J. Kwon, Z. Milosevic.
|
|
* `abstract_tendermint.ivy`, a more abstract specification of Tendermint that is more verification-friendly.
|
|
* `classic_safety.ivy`, a proof that Tendermint satisfies the classic safety property of BFT consensus: if every two quorums have a well-behaved node in common, then no two well-behaved nodes ever disagree.
|
|
* `accountable_safety_1.ivy`, a proof that, assuming every quorum contains at least one well-behaved node, if two well-behaved nodes disagree, then there is evidence demonstrating at least f+1 nodes misbehaved.
|
|
* `accountable_safety_2.ivy`, a proof that, regardless of any assumption about quorums, well-behaved nodes cannot be framed by malicious nodes. In other words, malicious nodes can never construct evidence that incriminates a well-behaved node.
|
|
* `network_shim.ivy`, the network model and a convenience `shim` object to interface with the Tendermint specification.
|
|
* `domain_model.ivy`, a specification of the domain model underlying the Tendermint specification, i.e. rounds, value, quorums, etc.
|
|
|
|
All specifications and proofs are written in [Ivy](https://github.com/kenmcmil/ivy).
|
|
|
|
The license above applies to all files in this folder.
|
|
|
|
|
|
## Building and running
|
|
|
|
The easiest way to check the proofs is to use [Docker](https://www.docker.com/).
|
|
|
|
1. Install [Docker](https://docs.docker.com/get-docker/) and [Docker Compose](https://docs.docker.com/compose/install/).
|
|
2. Build a Docker image: `docker-compose build`
|
|
3. Run the proofs inside the Docker container: `docker-compose run
|
|
tendermint-proof`. This will check all the proofs with the `ivy_check`
|
|
command and write the output of `ivy_check` to a subdirectory of `./output/'
|