add Ivy proofs (#210)

* add Ivy proofs

* fix docker-compose command

ivy-proofs/Dockerfile

@@ -0,0 +1,37 @@
+# we need python2 support, which was dropped after buster:
+FROM debian:buster
+
+RUN echo 'debconf debconf/frontend select Noninteractive' | debconf-set-selections
+RUN apt-get update
+RUN apt-get install -y apt-utils
+
+# Install and configure locale `en_US.UTF-8`
+RUN apt-get install -y locales && \
+    sed -i -e "s/# $en_US.*/en_US.UTF-8 UTF-8/" /etc/locale.gen && \
+    dpkg-reconfigure --frontend=noninteractive locales && \
+    update-locale LANG=en_US.UTF-8
+ENV LANG=en_US.UTF-8
+
+RUN apt-get update
+RUN apt-get install -y git python2 python-pip g++ cmake python-ply python-tk tix pkg-config libssl-dev python-setuptools
+
+# create a user:
+RUN useradd -ms /bin/bash user
+USER user
+WORKDIR /home/user
+
+RUN git clone --recurse-submodules https://github.com/kenmcmil/ivy.git
+WORKDIR /home/user/ivy/
+RUN git checkout 271ee38980699115508eb90a0dd01deeb750a94b
+
+RUN python2.7 build_submodules.py
+RUN mkdir -p "/home/user/python/lib/python2.7/site-packages"
+ENV PYTHONPATH="/home/user/python/lib/python2.7/site-packages"
+# need to install pyparsing manually because otherwise wrong version found
+RUN pip install pyparsing
+RUN python2.7 setup.py install --prefix="/home/user/python/"
+ENV PATH=$PATH:"/home/user/python/bin/"
+WORKDIR /home/user/tendermint-proof/
+
+ENTRYPOINT ["/home/user/tendermint-proof/check_proofs.sh"]
+

ivy-proofs/README.md

@@ -0,0 +1,27 @@
+```
+Copyright (c) 2020 Galois, Inc.
+SPDX-License-Identifier: Apache-2.0
+```
+
+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/'

ivy-proofs/abstract_tendermint.ivy

@@ -0,0 +1,173 @@
+#lang ivy1.7
+# ---
+# layout: page
+# title: Abstract specification of Tendermint in Ivy
+# ---
+
+# Here we define an abstract version of the Tendermint specification. We use
+# two main forms of abstraction: a) We abstract over how information is
+# transmitted (there is no network). b) We abstract functions using relations.
+# For example, we abstract over a node's current round, instead only tracking
+# with a relation which rounds the node has left. We do something similar for
+# the `lockedRound` variable. This is in order to avoid using a function from
+# node to round, and it allows us to emit verification conditions that are
+# efficiently solvable by Z3.
+
+# This specification also defines the observations that are used to adjudicate
+# misbehavior. Well-behaved nodes faithfully observe every message that they
+# use to take a step, while Byzantine nodes can fake observations about
+# themselves (including withholding observations). Misbehavior is defined using
+# the collection of all observations made (in reality, those observations must
+# be collected first, but we do not model this process).
+
+include domain_model
+
+module abstract_tendermint = {
+
+# Protocol state
+# ##############
+
+    relation left_round(N:node, R:round)
+    relation prevoted(N:node, R:round, V:value)
+    relation precommitted(N:node, R:round, V:value)
+    relation decided(N:node, R:round, V:value)
+    relation locked(N:node, R:round, V:value)
+
+# Accountability relations
+# ########################
+
+    relation observed_prevoted(N:node, R:round, V:value)
+    relation observed_precommitted(N:node, R:round, V:value)
+
+# relations that are defined in terms of the previous two:
+    relation observed_equivocation(N:node)
+    relation observed_unlawful_prevote(N:node)
+    relation agreement
+
+    object defs = { # we hide those definitions and use them only when needed
+        private {
+            definition [observed_equivocation_def] observed_equivocation(N) = exists V1,V2,R .
+                V1 ~= V2 & (observed_precommitted(N,R,V1) & observed_precommitted(N,R,V2) | observed_prevoted(N,R,V1) & observed_prevoted(N,R,V2))
+
+            definition [observed_unlawful_prevote_def] observed_unlawful_prevote(N) = exists V1,V2,R1,R2 .
+                V1 ~= value.nil & V2 ~= value.nil & V1 ~= V2 & R1 < R2 & observed_precommitted(N,R1,V1) & observed_prevoted(N,R2,V2)
+                & forall Q,R . R1 <= R & R < R2 & nset.is_quorum(Q) -> exists N2 . nset.member(N2,Q) & ~observed_prevoted(N2,R,V2)
+
+            definition [agreement_def] agreement = forall N1,N2,R1,R2,V1,V2 . well_behaved(N1) & well_behaved(N2) & decided(N1,R1,V1) & decided(N2,R2,V2) -> V1 = V2
+        }
+    }
+
+# Protocol transitions
+# ####################
+
+    after init {
+        left_round(N,R) := R < 0;
+        prevoted(N,R,V) := false;
+        precommitted(N,R,V) := false;
+        decided(N,R,V) := false;
+        locked(N,R,V) := false;
+
+        observed_prevoted(N,R,V) := false;
+        observed_precommitted(N,R,V) := false;
+    }
+
+# Actions are named after the corresponding line numbers in the Tendermint
+# arXiv paper.
+
+    action l_11(n:node, r:round) = { # start round r
+        require ~left_round(n,r);
+        left_round(n,R) := R < r;
+    }
+
+    action l_22(n:node, rp:round, v:value) = {
+        require ~left_round(n,rp);
+        require ~prevoted(n,rp,V) & ~precommitted(n,rp,V);
+        require (forall R,V . locked(n,R,V) -> V = v) | v = value.nil;
+        prevoted(n, rp, v) := true;
+        left_round(n, R) := R < rp; # leave all lower rounds.
+
+        observed_prevoted(n, rp, v) := observed_prevoted(n, rp, v) | well_behaved(n); # the node observes itself
+    }
+
+    action l_28(n:node, rp:round, v:value, vr:round, q:nset) = {
+        require ~left_round(n,rp) & ~prevoted(n,rp,V);
+        require ~prevoted(n,rp,V) & ~precommitted(n,rp,V);
+        require vr < rp;
+        require nset.is_quorum(q) & (forall N . nset.member(N,q) -> (prevoted(N,vr,v) | ~well_behaved(N)));
+        var proposal:value;
+        if value.valid(v) & ((forall R0,V0 . locked(n,R0,V0) -> R0 <= vr) | (forall R,V . locked(n,R,V) -> V = v)) {
+            proposal := v;
+        }
+        else {
+            proposal := value.nil;
+        };
+        prevoted(n, rp, proposal) := true;
+        left_round(n, R) := R < rp; # leave all lower rounds
+
+        observed_prevoted(N, vr, v) := observed_prevoted(N, vr, v) | (well_behaved(n) & nset.member(N,q)); # the node observes the prevotes of quorum q
+        observed_prevoted(n, rp, proposal) := observed_prevoted(n, rp, proposal) | well_behaved(n); # the node observes itself
+    }
+
+    action l_36(n:node, rp:round, v:value, q:nset) = {
+        require v ~= value.nil;
+        require ~left_round(n,rp);
+        require exists V . prevoted(n,rp,V);
+        require ~precommitted(n,rp,V);
+        require nset.is_quorum(q) & (forall N . nset.member(N,q) -> (prevoted(N,rp,v) | ~well_behaved(N)));
+        precommitted(n, rp, v) := true;
+        left_round(n, R) := R < rp; # leave all lower rounds
+        locked(n,R,V) := R <= rp & V = v;
+
+        observed_prevoted(N, rp, v) := observed_prevoted(N, rp, v) | (well_behaved(n) & nset.member(N,q)); # the node observes the prevotes of quorum q
+        observed_precommitted(n, rp, v) := observed_precommitted(n, rp, v) | well_behaved(n); # the node observes itself
+    }
+
+    action l_44(n:node, rp:round, q:nset) = {
+        require ~left_round(n,rp);
+        require ~precommitted(n,rp,V);
+        require nset.is_quorum(q) & (forall N .nset.member(N,q) -> (prevoted(N,rp,value.nil) | ~well_behaved(N)));
+        precommitted(n, rp, value.nil) := true;
+        left_round(n, R) := R < rp; # leave all lower rounds
+
+        observed_prevoted(N, rp, value.nil) := observed_prevoted(N, rp, value.nil) | (well_behaved(n) & nset.member(N,q)); # the node observes the prevotes of quorum q
+        observed_precommitted(n, rp, value.nil) := observed_precommitted(n, rp, value.nil) | well_behaved(n); # the node observes itself
+    }
+
+    action l_57(n:node, rp:round) = {
+        require ~left_round(n,rp);
+        require ~prevoted(n,rp,V);
+        prevoted(n, rp, value.nil) := true;
+        left_round(n, R) := R < rp; # leave all lower rounds
+
+        observed_prevoted(n, rp, value.nil) := observed_prevoted(n, rp, value.nil) | well_behaved(n); # the node observes itself
+    }
+
+    action l_61(n:node, rp:round) = {
+        require ~left_round(n,rp);
+        require ~precommitted(n,rp,V);
+        precommitted(n, rp, value.nil) := true;
+        left_round(n, R) := R < rp; # leave all lower rounds
+
+        observed_precommitted(n, rp, value.nil) := observed_precommitted(n, rp, value.nil) | well_behaved(n); # the node observes itself
+    }
+
+    action decide(n:node, r:round, v:value, q:nset) = {
+        require v ~= value.nil;
+        require nset.is_quorum(q) & (forall N . nset.member(N, q) -> (precommitted(N, r, v) | ~well_behaved(N)));
+        decided(n, r, v) := true;
+
+        observed_precommitted(N, r, v) := observed_precommitted(N, r, v) | (well_behaved(n) & nset.member(N,q)); # the node observes the precommits of quorum q
+
+    }
+
+    action misbehave = {
+# Byzantine nodes can claim they observed whatever they want about themselves,
+# but they cannot remove observations.
+        observed_prevoted(N,R,V) := *;
+        assume (old observed_prevoted(N,R,V)) -> observed_prevoted(N,R,V);
+        assume well_behaved(N) -> old observed_prevoted(N,R,V) = observed_prevoted(N,R,V);
+        observed_precommitted(N,R,V) := *;
+        assume (old observed_precommitted(N,R,V)) -> observed_precommitted(N,R,V);
+        assume well_behaved(N) -> old observed_precommitted(N,R,V) = observed_precommitted(N,R,V);
+    }
+}

ivy-proofs/accountable_safety_1.ivy

@@ -0,0 +1,144 @@
+#lang ivy1.7
+# ---
+# layout: page
+# title: Proof of Classic Safety
+# ---
+
+include tendermint
+include abstract_tendermint
+
+# Here we prove the first accountability property: if two well-behaved nodes
+# disagree, then there are two quorums Q1 and Q2 such that all members of the
+# intersection of Q1 and Q2 have violated the accountability properties.
+
+# The proof is done in two steps: first we prove the abstract specification
+# satisfies the property, and then we show by refinement that this property
+# also holds in the concrete specification.
+
+# To see what is checked in the refinement proof, use `ivy_show isolate=accountable_safety_1 accountable_safety_1.ivy`
+# To see what is checked in the abstract correctness proof, use `ivy_show isolate=abstract_accountable_safety_1 accountable_safety_1.ivy`
+# To check the whole proof, use `ivy_check accountable_safety_1.ivy`.
+
+
+# Proof of the accountability property in the abstract specification
+# ==================================================================
+
+# We prove with tactics (see `lemma_1` and `lemma_2`) that, if some basic
+# invariants hold (see `invs` below), then the accountability property holds.
+
+isolate abstract_accountable_safety = {
+
+    instantiate abstract_tendermint
+
+# The main property
+# -----------------
+
+# If there is disagreement, then there is evidence that a third of the nodes
+# have violated the protocol:
+    invariant [accountability] agreement | exists Q1,Q2 . nset.is_quorum(Q1) & nset.is_quorum(Q2) & (forall N . nset.member(N,Q1) & nset.member(N,Q2) -> observed_equivocation(N) | observed_unlawful_prevote(N))
+    proof {
+        apply lemma_2.thm # this reduces to goal to three subgoals: p1, p2, and p3 (see their definition below)
+        proof [p1] {
+            assume invs.inv1
+        }
+        proof [p2] {
+            assume invs.inv2
+        }
+        proof [p3] {
+            assume invs.inv3
+        }
+    }
+
+# The invariants
+# --------------
+
+    isolate invs = {
+
+        # well-behaved nodes observe their own actions faithfully:
+        invariant [inv1] well_behaved(N) -> (observed_precommitted(N,R,V) = precommitted(N,R,V))
+        # if a value is precommitted by a well-behaved node, then a quorum is observed to prevote it:
+        invariant [inv2] (exists N . well_behaved(N) & precommitted(N,R,V)) & V ~= value.nil  -> exists Q . nset.is_quorum(Q) & forall N2 . nset.member(N2,Q) -> observed_prevoted(N2,R,V)
+        # if a value is decided by a well-behaved node, then a quorum is observed to precommit it:
+        invariant [inv3] (exists N . well_behaved(N) & decided(N,R,V)) -> 0 <= R & V ~= value.nil & exists Q . nset.is_quorum(Q) & forall N2 . nset.member(N2,Q) -> observed_precommitted(N2,R,V)
+        private {
+            invariant (precommitted(N,R,V) | prevoted(N,R,V)) -> 0 <= R
+            invariant R < 0 -> left_round(N,R)
+        }
+
+    } with this, nset, round, accountable_bft.max_2f_byzantine
+
+# The theorems proved with tactics
+# --------------------------------
+
+# Using complete induction on rounds, we prove that, assuming that the
+# invariants inv1, inv2, and inv3 hold, the accountability property holds.
+
+# For technical reasons, we separate the proof in two steps
+    isolate lemma_1 = {
+
+# complete induction is not built-in, so we introduce it with an axiom. Note that this only holds for a type where 0 is the smallest element
+        axiom [complete_induction] {
+            relation p(X:round)
+            { # base case
+                property p(0)
+            }
+            { # inductive step: show that if the property is true for all X lower or equal to x and y=x+1, then the property is true of y
+                individual a:round
+                individual b:round
+                property (forall X. 0 <= X & X <= a -> p(X)) & round.succ(a,b) -> p(b)
+            }
+            #--------------------------
+            property forall X . 0 <= X -> p(X)
+        }
+
+# the main lemma: if inv1 and inv2 below hold and a quorum is observed to
+# precommit V1 at R1 and another quorum is observed to precommit V2~=V1 at
+# R2>=R1, then the intersection of two quorums (i.e. f+1 nodes) is observed to
+# violate the protocol
+        theorem [thm] {
+            property [p1] forall N,R,V . well_behaved(N) -> (observed_precommitted(N,R,V) = precommitted(N,R,V))
+            property [p2] forall R,V . (exists N . well_behaved(N) & precommitted(N,R,V)) -> V = value.nil | exists Q . nset.is_quorum(Q) & forall N2 . nset.member(N2,Q) -> observed_prevoted(N2,R,V)
+            #-----------------------------------------------------------------------------------------------------------------------
+            property forall R2. 0 <= R2  -> ((exists V2,Q1,R1,V1,Q1 . V1 ~= value.nil & V2 ~= value.nil & V1 ~= V2 & 0 <= R1 & R1 <= R2 & nset.is_quorum(Q1) & (forall N . nset.member(N,Q1) -> observed_precommitted(N,R1,V1)) & (exists Q2 . nset.is_quorum(Q2) & forall N . nset.member(N,Q2) -> observed_prevoted(N,R2,V2))) -> exists Q1,Q2 . nset.is_quorum(Q1) & nset.is_quorum(Q2) & forall N . nset.member(N,Q1) & nset.member(N,Q2) -> observed_equivocation(N) | observed_unlawful_prevote(N))
+        }
+        proof {
+            apply complete_induction # the two subgoals (base case and inductive case) are then discharged automatically
+        }
+    } with this, round, nset, accountable_bft.max_2f_byzantine, defs.observed_equivocation_def, defs.observed_unlawful_prevote_def
+
+# Now we put lemma_1 in a form that matches exactly the accountability property
+# we want to prove. This is a bit cumbersome and could probably be improved.
+    isolate lemma_2 = {
+
+        theorem [thm] {
+            property [p1] forall N,R,V . well_behaved(N) -> (observed_precommitted(N,R,V) = precommitted(N,R,V))
+            property [p2] forall R,V . (exists N . well_behaved(N) & precommitted(N,R,V)) & V ~= value.nil  -> exists Q . nset.is_quorum(Q) & forall N2 . nset.member(N2,Q) -> observed_prevoted(N2,R,V)
+            property [p3] forall R,V. (exists N . well_behaved(N) & decided(N,R,V)) -> 0 <= R & V ~= value.nil & exists Q . nset.is_quorum(Q) & forall N2 . nset.member(N2,Q) -> observed_precommitted(N2,R,V)
+            #-------------------------------------------------------------------------------------------------------------------------------------------
+            property agreement | exists Q1,Q2 . nset.is_quorum(Q1) & nset.is_quorum(Q2) & forall N . nset.member(N,Q1) & nset.member(N,Q2) -> observed_equivocation(N) | observed_unlawful_prevote(N)
+        }
+        proof {
+            assume lemma_1.thm
+        }
+
+    } with this, round,  defs.agreement_def, lemma_1, nset, accountable_bft.max_2f_byzantine
+
+} with round
+
+# The final proof
+# ===============
+
+isolate accountable_safety_1 = {
+
+# First we instantiate the concrete protocol:
+    instantiate tendermint(abstract_accountable_safety)
+
+# We then define what we mean by agreement
+    relation agreement
+    definition [agreement_def] agreement = forall N1,N2. well_behaved(N1) & well_behaved(N2) & server.decision(N1) ~= value.nil & server.decision(N2) ~= value.nil -> server.decision(N1) = server.decision(N2)
+
+    invariant abstract_accountable_safety.agreement -> agreement
+
+    invariant [accountability] agreement | exists Q1,Q2 . nset.is_quorum(Q1) & nset.is_quorum(Q2) & forall N . nset.member(N,Q1) & nset.member(N,Q2) -> abstract_accountable_safety.observed_equivocation(N) | abstract_accountable_safety.observed_unlawful_prevote(N)
+
+} with value, round, proposers, shim, abstract_accountable_safety, abstract_accountable_safety.defs.agreement_def, accountable_safety_1.agreement_def

ivy-proofs/accountable_safety_2.ivy

@@ -0,0 +1,52 @@
+#lang ivy1.7
+
+include tendermint
+include abstract_tendermint
+
+# Here we prove the second accountability property: no well-behaved node is
+# every observed to violate the accountability properties.
+
+# The proof is done in two steps: first we prove the the abstract specification
+# satisfies the property, and then we show by refinement that this property
+# also holds in the concrete specification.
+
+# To see what is checked in the refinement proof, use `ivy_show isolate=accountable_safety_2 accountable_safety_2.ivy`
+# To see what is checked in the abstract correctness proof, use `ivy_show isolate=abstract_accountable_safety_2 accountable_safety_2.ivy`
+# To check the whole proof, use `ivy_check accountable_safety_2.ivy`.
+
+# Proof that the property holds in the abstract specification
+# ============================================================
+
+isolate abstract_accountable_safety_2 = {
+
+    instantiate abstract_tendermint
+
+# the main property:
+    invariant [wb_never_punished] well_behaved(N) -> ~(observed_equivocation(N) | observed_unlawful_prevote(N))
+
+# the main invariant for proving wb_not_punished:
+    invariant well_behaved(N) & precommitted(N,R,V) & ~locked(N,R,V) & V ~= value.nil -> exists R2,V2 . V2 ~= value.nil & R < R2 & precommitted(N,R2,V2) & locked(N,R2,V2)
+
+    invariant (exists N . well_behaved(N) & precommitted(N,R,V) & V ~= value.nil) -> exists Q . nset.is_quorum(Q) & forall N . nset.member(N,Q) -> observed_prevoted(N,R,V)
+
+    invariant well_behaved(N) -> (observed_prevoted(N,R,V) <-> prevoted(N,R,V))
+    invariant well_behaved(N) -> (observed_precommitted(N,R,V) <-> precommitted(N,R,V))
+
+# nodes stop prevoting or precommitting in lower rounds when doing so in a higher round:
+    invariant well_behaved(N) & prevoted(N,R2,V2) & R1 < R2 -> left_round(N,R1)
+    invariant well_behaved(N) & locked(N,R2,V2) & R1 < R2 -> left_round(N,R1)
+
+    invariant [precommit_unique_per_round] well_behaved(N) & precommitted(N,R,V1) & precommitted(N,R,V2) -> V1 = V2
+
+} with nset, round, abstract_accountable_safety_2.defs.observed_equivocation_def, abstract_accountable_safety_2.defs.observed_unlawful_prevote_def
+
+# Proof that the property holds in the concrete specification
+# ===========================================================
+
+isolate accountable_safety_2 = {
+
+    instantiate tendermint(abstract_accountable_safety_2)
+
+    invariant well_behaved(N) -> ~(abstract_accountable_safety_2.observed_equivocation(N) | abstract_accountable_safety_2.observed_unlawful_prevote(N))
+
+} with round, value, shim, abstract_accountable_safety_2, abstract_accountable_safety_2.defs.observed_equivocation_def, abstract_accountable_safety_2.defs.observed_unlawful_prevote_def

ivy-proofs/check_proofs.sh

@@ -0,0 +1,38 @@
+#!/bin/bash
+
+# returns non-zero error code if any proof fails
+
+success=0
+log_dir=$(cat /dev/urandom | tr -cd 'a-f0-9' | head -c 6)
+mkdir -p output/$log_dir
+
+echo "Checking classic safety:"
+res=$(ivy_check classic_safety.ivy | tee "output/$log_dir/classic_safety.txt" | tail -n 1)
+if [ "$res" = "OK" ]; then
+  echo "OK"
+else
+  echo "FAILED"
+  success=1
+fi
+
+echo "Checking accountable safety 1:"
+res=$(ivy_check complete=fo accountable_safety_1.ivy | tee "output/$log_dir/accountable_safety_1.txt" | tail -n 1)
+if [ "$res" = "OK" ]; then
+  echo "OK"
+else
+  echo "FAILED"
+  success=1
+fi
+
+echo "Checking accountable safety 2:"
+res=$(ivy_check complete=fo accountable_safety_2.ivy | tee "output/$log_dir/accountable_safety_2.txt" | tail -n 1)
+if [ "$res" = "OK" ]; then
+  echo "OK"
+else
+  echo "FAILED"
+  success=1
+fi
+
+echo
+echo "See ivy_check output in the output/ folder"
+exit $success

ivy-proofs/classic_safety.ivy

@@ -0,0 +1,85 @@
+#lang ivy1.7
+# ---
+# layout: page
+# title: Proof of Classic Safety
+# ---
+
+include tendermint
+include abstract_tendermint
+
+# Here we prove the classic safety property: assuming that every two quorums
+# have a well-behaved node in common, no two well-behaved nodes ever disagree.
+
+# The proof is done in two steps: first we prove the the abstract specification
+# satisfies the property, and then we show by refinement that this property
+# also holds in the concrete specification.
+
+# To see what is checked in the refinement proof, use `ivy_show isolate=classic_safety classic_safety.ivy`
+# To see what is checked in the abstract correctness proof, use `ivy_show isolate=abstract_classic_safety classic_safety.ivy`
+
+# To check the whole proof, use `ivy_check classic_safety.ivy`.
+
+# Note that all the verification conditions sent to Z3 for this proof are in
+# EPR.
+
+# Classic safety in the abstract model
+# ====================================
+
+# We start by proving that classic safety holds in the abstract model.
+
+isolate abstract_classic_safety = {
+
+    instantiate abstract_tendermint
+
+    invariant [classic_safety] classic_bft.quorum_intersection & decided(N1,R1,V1) & decided(N2,R2,V2) -> V1 = V2
+
+# The notion of choosable value
+# -----------------------------
+
+    relation choosable(R:round, V:value)
+    definition choosable(R,V) = exists Q . nset.is_quorum(Q) & forall N . well_behaved(N) & nset.member(N,Q) -> ~left_round(N,R) | precommitted(N,R,V)
+
+# Main invariants
+# ---------------
+
+# `classic_safety` is inductive relative to those invariants
+
+    invariant [decision_is_quorum_precommit] (exists N1 . decided(N1,R,V)) -> exists Q. nset.is_quorum(Q) & forall N2. well_behaved(N2) & nset.member(N2, Q) -> precommitted(N2,R,V)
+
+    invariant [precommitted_is_quorum_prevote] V ~= value.nil & (exists N1 . precommitted(N1,R,V)) -> exists Q. nset.is_quorum(Q) & forall N2. well_behaved(N2) & nset.member(N2, Q) -> prevoted(N2,R,V)
+
+    invariant [prevote_unique_per_round] prevoted(N,R,V1) & prevoted(N,R,V2) -> V1 = V2
+
+# This is the core invariant: as long as a precommitted value is still choosable, it remains protected by a lock and prevents any new value from being prevoted:
+    invariant [locks] classic_bft.quorum_intersection & V ~= value.nil & precommitted(N,R,V) & choosable(R,V) -> locked(N,R,V) & forall R2,V2 . R < R2 & prevoted(N,R2,V2) -> V2 = V | V2 = value.nil
+
+# Supporting invariants
+# ---------------------
+
+# The main invariants are inductive relative to those
+
+    invariant decided(N,R,V) -> V ~= value.nil
+
+    invariant left_round(N,R2) & R1 < R2 -> left_round(N,R1) # if a node left round R2>R1, then it also left R1:
+
+    invariant prevoted(N,R2,V2) & R1 < R2 -> left_round(N,R1)
+    invariant precommitted(N,R2,V2) & R1 < R2 -> left_round(N,R1)
+
+} with round, nset, classic_bft.quorum_intersection_def
+
+# The refinement proof
+# ====================
+
+# Now, thanks to the refinement relation that we establish in
+# `concrete_tendermint.ivy`, we prove that classic safety transfers to the
+# concrete specification:
+isolate classic_safety = {
+
+    # We instantiate the `tendermint` module providing `abstract_classic_safety` as abstract model.
+    instantiate tendermint(abstract_classic_safety)
+
+    # We prove that if every two quorums have a well-behaved node in common,
+    # then well-behaved nodes never disagree:
+    invariant [classic_safety] classic_bft.quorum_intersection & server.decision(N1) ~= value.nil & server.decision(N2) ~= value.nil -> server.decision(N1) = server.decision(N2)
+
+} with value, round, proposers, shim, abstract_classic_safety # here we list all the specifications that we rely on for this proof

ivy-proofs/docker-compose.yml

@@ -0,0 +1,8 @@
+version: '3'
+services:
+  tendermint-proof:
+    build: .
+    volumes:
+      - ./:/home/user/tendermint-proof:ro
+      - ./output:/home/user/tendermint-proof/output:rw
+

ivy-proofs/domain_model.ivy

@@ -0,0 +1,90 @@
+#lang ivy1.7
+# ---
+# layout: page
+# title: Proof of Classic Safety
+# ---
+
+include order # this is a file from the standard library (`ivy/ivy/include/1.7/order.ivy`)
+
+isolate round = {
+    type this
+    individual minus_one:this
+    relation succ(R1:round, R2:round)
+    action incr(i:this) returns (j:this)
+    specification {
+# to simplify verification, we treat rounds as an abstract totally ordered set with a successor relation.
+        instantiate totally_ordered(this)
+        property minus_one < 0
+        property succ(X,Z) -> (X < Z & ~(X < Y & Y < Z))
+        after incr {
+            ensure succ(i,j)
+        }
+    }
+    implementation {
+# here we prove that the abstraction is sound.
+        interpret this -> int # rounds are integers in the Tendermint specification.
+        definition minus_one = 0-1
+        definition succ(R1,R2) = R2 = R1 + 1
+        implement incr {
+            j := i+1;
+        }
+    }
+}
+
+instance node : iterable # nodes are a set with an order, that can be iterated over (see order.ivy in the standard library)
+relation well_behaved(N:node) # whether a node is well-behaved or not. NOTE: Use only in the proof! Nodes do know know that.
+
+isolate proposers = {
+    # each round has a unique proposer in Tendermint. In order to avoid a
+    # function from round to node (which makes verification more difficult), we
+    # abstract over this function using a relation.
+    relation is_proposer(N:node, R:round)
+    action get_proposer(r:round) returns (n:node)
+    specification {
+        property is_proposer(N1,R) & is_proposer(N2,R) -> N1 = N2
+        after get_proposer {
+            ensure is_proposer(n,r);
+        }
+    }
+    implementation {
+    # here we prove that the abstraction is sound
+        function f(R:round):node
+        definition is_proposer(N,R) = N = f(R)
+        implement get_proposer {
+            n := f(r);
+        }
+    }
+}
+
+isolate value = { # the type of values
+    type this
+    relation valid(V:value)
+    individual nil:value
+    specification {
+        property ~valid(nil)
+    }
+    implementation {
+        definition valid(V) = V ~= nil
+    }
+}
+
+object nset = { # the type of node sets
+    type this # a set of N=3f+i nodes for 0<i<=3
+    relation member(N:node, S:nset) # set-membership relation
+    relation is_quorum(S:nset) # intent: sets of cardinality at least 2f+i+1
+    relation is_blocking(S:nset) # intent: at least f+1 nodes
+}
+
+object classic_bft = {
+    relation quorum_intersection
+    private {
+        definition [quorum_intersection_def] quorum_intersection = forall Q1,Q2. exists N. well_behaved(N) & nset.member(N, Q1) & nset.member(N, Q2) # every two quorums have a well-behaved node in common
+    }
+}
+
+trusted isolate accountable_bft = {
+    # this is our baseline assumption about quorums:
+    private {
+        property [max_2f_byzantine] exists N . well_behaved(N) & nset.member(N,Q) # every quorum has a well-behaved member
+    }
+}# with nset

ivy-proofs/network_shim.ivy

@@ -0,0 +1,140 @@
+#lang ivy1.7
+# ---
+# layout: page
+# title: Network model and network shim
+# ---
+
+# Here we define a network module, which is our model of the network, and a
+# shim module that sits on top of the network and which, upon receiving a
+# message, calls the appropriate protocol handler.
+
+include domain_model
+
+# Here we define an enumeration type for identifying the 3 different types of
+# messages that nodes send.
+object msg_kind = { # TODO: merge with step_t
+    type this = {proposal, prevote, precommit}
+}
+
+# Here we define the type of messages `msg`. Its members are structs with the fields described below.
+object msg = {
+    type this = struct {
+        m_kind : msg_kind,
+        m_src  : node,
+        m_round : round,
+        m_value : value,
+        m_vround : round
+    }
+}
+
+# This is our model of the network:
+trusted isolate net = {
+# `trusted` indicates to Ivy that this is a trusted object, i.e. we assume
+# without proof that receive is only called when its requirement is true.
+
+    export action recv(dst:node,v:msg)
+    action send(src:node,dst:node,v:msg)
+    # Note that the `recv` action is exported, meaning that it can be called
+    # non-deterministically by the environment any time it is enabled. In other
+    # words, a packet that is in flight can be received at any time. In this
+    # sense, the network is fully asynchronous. Moreover, there is no
+    # requirement that a given message will be received at all.
+
+    specification {
+
+        # The state of the network consists of all the packets that have been
+        # sent so far, along with their destination.
+        relation sent(V:msg, N:node)
+
+        after init {
+            sent(V, N) := false
+        }
+
+        before send {
+            sent(v,dst) := true
+        }
+
+        before recv {
+            require sent(v,dst) # only sent messages can be received.
+        }
+    }
+
+}
+
+# The network shim sits on top of the network and, upon receiving a message,
+# calls the appropriate protocol handler. It also exposes a `broadcast` action
+# that sends to all nodes.
+
+isolate shim = {
+
+    # In order not repeat the same code for each handler, we use a handler
+    # module parameterized by the type of message it will handle. Below we
+    # instantiate this module for the 3 types of messages of Tendermint
+    module handler(p_kind) = {
+        action handle(dst:node,m:msg)
+        object spec = {
+            before handle {
+                assert sent(m,dst) & m.m_kind = p_kind
+            }
+        }
+    }
+
+    instance proposal_handler : handler(msg_kind.proposal)
+    instance prevote_handler : handler(msg_kind.prevote)
+    instance precommit_handler : handler(msg_kind.precommit)
+
+    relation sent(M:msg,N:node)
+
+    action broadcast(src:node,m:msg)
+    action send(src:node,dst:node,m:msg)
+
+    specification {
+        after init {
+            sent(M,D) := false;
+        }
+        before broadcast {
+            sent(m,D) := true
+        }
+        before send {
+            sent(m,dst) := true
+        }
+    }
+
+    # In contrast to the network object, the shim is not a trusted component.
+    # Here we give an implementation of it that satisfies its specification:
+    implementation {
+
+        implement net.recv(dst:node,m:msg) {
+
+            if m.m_kind = msg_kind.proposal {
+                call proposal_handler.handle(dst,m)
+            }
+            else if m.m_kind = msg_kind.prevote {
+                call prevote_handler.handle(dst,m)
+            }
+            else if m.m_kind = msg_kind.proposal {
+                call precommit_handler.handle(dst,m)
+            }
+        }
+
+        implement broadcast { # broadcast sends to all nodes, including the sender.
+            var iter := node.iter.create(0);
+            while ~iter.is_end
+            invariant net.sent(M,D) -> sent(M,D)
+            {
+                var n := iter.val;
+                call net.send(src,n,m);
+                iter := iter.next;
+            }
+        }
+
+        implement send {
+            call net.send(src,dst,m)
+        }
+
+        private {
+            invariant net.sent(M,D) -> sent(M,D)
+        }
+    }
+
+} with net, node # to prove that the shim implementation satisfies the shim specification, we rely on the specification of net and node.

ivy-proofs/output/.gitignore

@@ -0,0 +1,4 @@
+# Ignore everything in this directory
+*
+# Except this file
+!.gitignore

ivy-proofs/tendermint.ivy

@@ -0,0 +1,430 @@
+#lang ivy1.7
+# ---
+# layout: page
+# title: Specification of Tendermint in Ivy
+# ---
+
+# This specification closely follows the pseudo-code given in "The latest
+# gossip on BFT consensus" by E. Buchman, J. Kwon, Z. Milosevic
+# <https://arxiv.org/abs/1807.04938>
+
+include domain_model
+include network_shim
+
+# We model the Tendermint protocol as an Ivy object. Like in Object-Oriented
+# Programming, the basic structuring unit in Ivy is the object. Objects have
+# internal state and actions (i.e. methods in OO parlance) that modify their
+# state. We model Tendermint as an object whose actions represent steps taken
+# by individual nodes in the protocol. Actions in Ivy can have preconditions,
+# and a valid execution is a sequence of actions whose preconditions are all
+# satisfied in the state in which they are called.
+
+# For technical reasons, we define below a `tendermint` module instead of an
+# object. Ivy modules are a little bit like classes in OO programs, and like
+# classes they can be instantiated to obtain objects. To instantiate the
+# `tendermint` module, we must provide an abstract-protocol object. This allows
+# us to use different abstract-protocol objects for different parts of the
+# proof, and to do so without too much notational burden (we could have used
+# Ivy monitors, but then we would need to prefix every variable name by the
+# name of the object containing it, which clutters things a bit compared to the
+# approach we took).
+
+# The abstract-protocol object is called by the resulting tendermint object so
+# as to run the abstract protocol alongside the concrete protocol. This allows
+# us to transfer properties proved of the abstract protocol to the concrete
+# protocol, as follows. First, we prove that running the abstract protocol in
+# this way results in a valid execution of the abstract protocol. This is done
+# by checking that all preconditions of the abstract actions are satisfied at
+# their call sites. Second, we establish a relation between abstract state and
+# concrete state (in the form of invariants of the resulting, two-object
+# transition system) that allow us to transfer properties proved in the
+# abstract protocol to the concrete protocol (for example, we prove that any
+# decision made in the Tendermint protocol is also made in the abstract
+# protocol; if the abstract protocol satisfies the agreement property, this
+# allows us to conclude that the Tendermint protocol also does).
+
+# The abstract protocol object that we will use is always the same, and only
+# the abstract properties that we prove about it change in the different
+# instantiations of the `tendermint` module. Thus we provide common invariants
+# that a) allow to prove that the abstract preconditions are met, and b)
+# provide a refinement relation (see end of the module) relating the state of
+# Tendermint to the state of the abstract protocol.
+
+# In the model, Byzantine nodes can send whatever messages they want, except
+# that they cannot forge sender identities. This reflects the fact that, in
+# practice, nodes use public key cryptography to sign their messages.
+
+# Finally, note that the observations that serve to adjudicate misbehavior are
+# defined only in the abstract protocol (they happen in the abstract actions).
+
+module tendermint(abstract_protocol) = {
+
+    # the initial value of a node:
+    parameter init_val(N:node): value
+
+    # the three type of steps
+    object step_t = {
+        type this = {propose, prevote, precommit}
+    } # refer to those e.g. as step_t.propose
+
+    object server(n:node) = {
+
+        # the current round of a node
+        individual round_p: round
+
+        individual step: step_t
+
+        individual decision: value
+
+        individual lockedValue: value
+        individual lockedRound: round
+
+        individual validValue: value
+        individual validRound: round
+
+
+        relation done_l34(R:round)
+        relation done_l36(R:round, V:value)
+        relation done_l47(R:round)
+
+        # variables for scheduling request
+        relation propose_timer_scheduled(R:round)
+        relation prevote_timer_scheduled(R:round)
+        relation precommit_timer_scheduled(R:round)
+
+        relation _recved_proposal(Sender:node, R:round, V:value, VR:round)
+        relation _recved_prevote(Sender:node, R:round, V:value)
+        relation _recved_precommit(Sender:node, R:round, V:value)
+
+        relation _has_started
+
+        after init {
+            round_p := 0;
+            step := step_t.propose;
+            decision := value.nil;
+
+            lockedValue := value.nil;
+            lockedRound := round.minus_one;
+
+            validValue := value.nil;
+            validRound := round.minus_one;
+
+            done_l34(R) := false;
+            done_l36(R, V) := false;
+            done_l47(R) := false;
+
+            propose_timer_scheduled(R) := false;
+            prevote_timer_scheduled(R) := false;
+            precommit_timer_scheduled(R) := false;
+
+            _recved_proposal(Sender, R, V, VR) := false;
+            _recved_prevote(Sender, R, V) := false;
+            _recved_precommit(Sender, R, V) := false;
+
+            _has_started := false;
+        }
+
+        action getValue returns (v:value) = {
+            v := init_val(n)
+        }
+
+        export action start = {
+            assume ~_has_started;
+            _has_started := true;
+            # line 10
+            call startRound(0);
+        }
+
+        # line 11-21
+        action startRound(r:round) = {
+            # line 12
+            round_p := r;
+
+            # line 13
+            step := step_t.propose;
+
+            var proposal : value;
+
+            # line 14
+            if (proposers.get_proposer(r) = n) {
+                if validValue ~= value.nil {      # line 15
+                    proposal := validValue; # line 16
+                } else {
+                    proposal := getValue();   # line 18
+                };
+                call broadcast_proposal(r, proposal, validRound); # line 19
+            } else {
+                propose_timer_scheduled(r) := true; # line 21
+            };
+
+            call abstract_protocol.l_11(n, r);
+        }
+
+        # This action, as not exported, can only be called at specific call sites.
+        action broadcast_proposal(r:round, v:value, vr:round) = {
+            var m: msg;
+            m.m_kind := msg_kind.proposal;
+            m.m_src := n;
+            m.m_round := r;
+            m.m_value := v;
+            m.m_vround := vr;
+            call shim.broadcast(n,m);
+        }
+
+
+        implement shim.proposal_handler.handle(msg:msg) {
+            _recved_proposal(msg.m_src, msg.m_round, msg.m_value, msg.m_vround) := true;
+        }
+
+
+        # line 22-27
+        export action l_22(v:value) = {
+            assume _has_started;
+            assume _recved_proposal(proposers.get_proposer(round_p), round_p, v, round.minus_one);
+            assume step = step_t.propose;
+
+            if (value.valid(v) & (lockedRound = round.minus_one | lockedValue = v)) {
+                call broadcast_prevote(round_p, v); # line 24
+                call abstract_protocol.l_22(n, round_p, v);
+            } else {
+                call broadcast_prevote(round_p, value.nil); # line 26
+                call abstract_protocol.l_22(n, round_p, value.nil);
+            };
+
+            # line 27
+            step := step_t.prevote;
+        }
+
+
+
+        # line 28-33
+        export action l_28(r:round, v:value, vr:round, q:nset) = {
+            assume _has_started;
+            assume r = round_p;
+            assume _recved_proposal(proposers.get_proposer(r), r, v, vr);
+            assume nset.is_quorum(q);
+            assume nset.member(N,q) -> _recved_prevote(N,vr,v);
+            assume step = step_t.propose;
+            assume vr >= 0 & vr < r;
+
+            # line 29
+            if (value.valid(v) & (lockedRound <= vr | lockedValue = v)) {
+                call broadcast_prevote(r, v);
+            } else {
+                call broadcast_prevote(r, value.nil);
+            };
+
+            call abstract_protocol.l_28(n,r,v,vr,q);
+            step := step_t.prevote;
+        }
+
+        action broadcast_prevote(r:round, v:value) = {
+            var m: msg;
+            m.m_kind := msg_kind.prevote;
+            m.m_src := n;
+            m.m_round := r;
+            m.m_value := v;
+            call shim.broadcast(n,m);
+        }
+
+        implement shim.prevote_handler.handle(msg:msg) {
+            assume msg.m_vround = round.minus_one;
+            _recved_prevote(msg.m_src, msg.m_round, msg.m_value) := true;
+        }
+
+
+        # line 34-35
+        export action l_34(r:round, q:nset) = {
+            assume _has_started;
+            assume round_p = r;
+            assume nset.is_quorum(q);
+            assume exists V . nset.member(N,q) -> _recved_prevote(N,r,V);
+            assume step = step_t.prevote;
+            assume ~done_l34(r);
+            done_l34(r) := true;
+
+            prevote_timer_scheduled(r) := true;
+        }
+
+
+        # line 36-43
+        export action l_36(r:round, v:value, q:nset) = {
+            assume _has_started;
+            assume r = round_p;
+            assume exists VR . _recved_proposal(proposers.get_proposer(r), r, v, VR);
+            assume nset.is_quorum(q);
+            assume nset.member(N,q) -> _recved_prevote(N,r,v);
+            assume value.valid(v);
+            assume step = step_t.prevote | step = step_t.precommit;
+
+            assume ~done_l36(r,v);
+            done_l36(r, v) := true;
+
+            if step = step_t.prevote {
+                lockedValue := v; # line 38
+                lockedRound := r; # line 39
+                call broadcast_precommit(r, v); # line 40
+                step := step_t.precommit; # line 41
+                call abstract_protocol.l_36(n, r, v, q);
+            };
+
+            validValue := v; # line 42
+            validRound := r; # line 43
+
+        }
+
+
+        # line 44-46
+        export action l_44(r:round, q:nset) = {
+            assume _has_started;
+            assume r = round_p;
+            assume nset.is_quorum(q);
+            assume nset.member(N,q) -> _recved_prevote(N,r,value.nil);
+            assume step = step_t.prevote;
+
+            call broadcast_precommit(r, value.nil); # line 45
+            step := step_t.precommit; # line 46
+
+            call abstract_protocol.l_44(n, r, q);
+        }
+
+        action broadcast_precommit(r:round, v:value) = {
+            var m: msg;
+            m.m_kind := msg_kind.precommit;
+            m.m_src := n;
+            m.m_round := r;
+            m.m_value := v;
+            m.m_vround := round.minus_one;
+            call shim.broadcast(n,m);
+        }
+
+        implement shim.precommit_handler.handle(msg:msg) {
+            assume msg.m_vround = round.minus_one;
+            _recved_precommit(msg.m_src, msg.m_round, msg.m_value) := true;
+        }
+
+
+        # line 47-48
+        export action l_47(r:round, q:nset) = {
+            assume _has_started;
+            assume round_p = r;
+            assume nset.is_quorum(q);
+            assume nset.member(N,q) -> exists V . _recved_precommit(N,r,V);
+            assume ~done_l47(r);
+            done_l47(r) := true;
+
+            precommit_timer_scheduled(r) := true;
+        }
+
+
+        # line 49-54
+        export action l_49_decide(r:round, v:value, q:nset) = {
+            assume _has_started;
+            assume exists VR . _recved_proposal(proposers.get_proposer(r), r, v, VR);
+            assume nset.is_quorum(q);
+            assume nset.member(N,q) -> _recved_precommit(N,r,v);
+            assume decision = value.nil;
+
+            if value.valid(v) {
+                decision := v;
+                # MORE for next height
+                call abstract_protocol.decide(n, r, v, q);
+            }
+        }
+
+        # line 55-56
+        export action l_55(r:round, b:nset) = {
+            assume _has_started;
+            assume nset.is_blocking(b);
+            assume nset.member(N,b) -> exists V,VR . _recved_proposal(N,r,V,VR) | _recved_prevote(N,r,V) | _recved_precommit(N,r,V);
+            assume r > round_p;
+            call startRound(r); # line 56
+        }
+
+        # line 57-60
+        export action onTimeoutPropose(r:round) = {
+            assume _has_started;
+            assume propose_timer_scheduled(r);
+            assume r = round_p;
+            assume step = step_t.propose;
+            call broadcast_prevote(r,value.nil);
+            step := step_t.prevote;
+
+            call abstract_protocol.l_57(n,r);
+
+            propose_timer_scheduled(r) := false;
+        }
+
+        # line 61-64
+        export action onTimeoutPrevote(r:round) = {
+            assume _has_started;
+            assume prevote_timer_scheduled(r);
+            assume r = round_p;
+            assume step = step_t.prevote;
+            call broadcast_precommit(r,value.nil);
+            step := step_t.precommit;
+
+            call abstract_protocol.l_61(n,r);
+
+            prevote_timer_scheduled(r) := false;
+        }
+
+
+        # line 65-67
+        export action onTimeoutPrecommit(r:round) = {
+            assume _has_started;
+            assume precommit_timer_scheduled(r);
+            assume r = round_p;
+            call startRound(round.incr(r));
+
+            precommit_timer_scheduled(r) := false;
+        }
+
+# The Byzantine actions
+# ---------------------
+
+# Byzantine nodes can send whatever they want, but they cannot send
+# messages on behalf of well-behaved nodes. In practice this is implemented
+# using cryprography (e.g. public-key cryptography).
+
+        export action byzantine_send = {
+            assume ~well_behaved(n);
+            var m:msg;
+            var dst:node;
+            assume ~well_behaved(m.m_src); # cannot forge the identity of well-behaved nodes
+            call shim.send(n,dst,m);
+        }
+
+# Byzantine nodes can also report fake observations, as defined in the abstract protocol.
+        export action fake_observations = {
+            call abstract_protocol.misbehave
+        }
+
+# Invariants
+# ----------
+
+# We provide common invariants that a) allow to prove that the abstract
+# preconditions are met, and b) provide a refinement relation.
+
+
+        invariant 0 <= round_p
+        invariant abstract_protocol.left_round(n,R) <-> R < round_p
+
+        invariant lockedRound ~= round.minus_one -> forall R,V . abstract_protocol.locked(n,R,V) <-> R <= lockedRound & lockedValue = V
+        invariant lockedRound = round.minus_one -> forall R,V . ~abstract_protocol.locked(n,R,V)
+
+        invariant forall M:msg . well_behaved(M.m_src) & M.m_kind = msg_kind.prevote & shim.sent(M,N) -> abstract_protocol.prevoted(M.m_src,M.m_round,M.m_value)
+        invariant well_behaved(N) & _recved_prevote(N,R,V) -> abstract_protocol.prevoted(N,R,V)
+        invariant forall M:msg . well_behaved(M.m_src) & M.m_kind = msg_kind.precommit & shim.sent(M,N) -> abstract_protocol.precommitted(M.m_src,M.m_round,M.m_value)
+        invariant well_behaved(N) & _recved_precommit(N,R,V) -> abstract_protocol.precommitted(N,R,V)
+
+        invariant (step = step_t.prevote | step = step_t.propose) -> ~abstract_protocol.precommitted(n,round_p,V)
+        invariant step = step_t.propose -> ~abstract_protocol.prevoted(n,round_p,V)
+        invariant step = step_t.prevote -> exists V . abstract_protocol.prevoted(n,round_p,V)
+
+        invariant round_p < R -> ~(abstract_protocol.prevoted(n,R,V) | abstract_protocol.precommitted(n,R,V))
+        invariant ~_has_started -> step = step_t.propose & ~(abstract_protocol.prevoted(n,R,V) | abstract_protocol.precommitted(n,R,V)) & round_p = 0
+
+        invariant decision ~= value.nil -> exists R . abstract_protocol.decided(n,R,decision)
+    }
+}