You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
85 lines
3.6 KiB
85 lines
3.6 KiB
#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
|