#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