Plausible liveness

This file proves the plausible-liveness theorem: under the standing hypotheses (no slashing, good votes, quorum nonemptiness, two-thirds-good validators, and blocks at arbitrary heights), the protocol state can always be extended with two new supermajority links that finalize a new block — without introducing any new slashing.

This formalises Casper FFG's Theorem 2 (Plausible Liveness) / Gasper's Theorem 6.1: regardless of any previous events, it is always possible for new blocks to be finalized, provided that new blocks can be created by the underlying blockchain. The emphasis is that honest validators are never forced to violate a slashing condition in order to make progress — the protocol cannot "deadlock" into a state where finalization requires voluntary slashing. This is a purely non-probabilistic property about the logic of the protocol, requiring no synchrony assumptions.

Structure

The proof proceeds in three stages:

1. No new slashing (no_new_double_vote_two_link_extension, no_new_surround_vote_two_link_extension, no_new_slashed_two_link_extension): adding two carefully-chosen vote batches at heights H + 1 and H + 2 (where H = \operatorname{highest\_target}(\sigma)) cannot create any new double-vote or surround-vote violation. The proof is a 3 \times 3 case matrix (old / link-1 / link-2 for each of the two conflicting votes), with each off-diagonal cell ruled out by a height argument. The key insight is that the two new target heights H + 1, H + 2 are strictly above every existing target height \le H, so they cannot collide with old votes (for (S1)) and cannot be surrounded by old votes (for (S2)).

2. Extension construction (plausible_liveness_construct_extension): assembles the extended state \sigma' from the highest justified block, two fresh quorums from two_thirds_good, and two new supermajority links built by supermajority_link_of_quorum_votes. Verifies all five conditions: vote inclusion, well-formedness, no new slashing, justification of the new finalized block, and the finalizing parent edge. This is a 1-finalization construction: the new finalized block \mathit{nf} is justified at height H + 1, and the finalizing link goes from (\mathit{nf}, H{+}1) to (\mathit{nc}, H{+}2), matching the definition of finalized at depth k = 1.

3. Coq-compatible wrapper (plausible_liveness_from_coq_blocks_exist): replaces the corrected block-existence hypothesis with the Coq-faithful one via blocks_exist_high_over_of_coq.

Non-goals of this file

This file proves plausible liveness only — it shows that finalization is always possible. It does not prove probabilistic liveness (that finalization is likely under synchrony assumptions), which is a separate, stronger result discussed in Gasper's Section 7 but not formalised in this development.

Height-transport helpers

The following private lemmas transport strict/non-strict inequalities and equalities across height-level identifications (e.g. th = H + 1). They are used in the 3 \times 3 case matrix of no_new_double_vote_two_link_extension and no_new_surround_vote_two_link_extension to derive contradictions when two votes from different height levels would need to share a target or source height.

Adding two links at heights H+1 and H+2 creates no new double vote

Statement

\operatorname{slashed\_double\_vote}\bigl(\sigma \uplus V_1 \uplus V_2,\; v\bigr) \;\implies\; \operatorname{slashed\_double\_vote}(\sigma, v)

where V_1 = \operatorname{votes\_for\_link}(q_1, s_1, t_1, s_{1,h}, H{+}1) and V_2 = \operatorname{votes\_for\_link}(q_2, s_2, t_2, H{+}1, H{+}2). Any double vote in the extended state was already a double vote in the original state.

Assumptions

• hBound — every vote in \sigma has target height \le H (target_height_bound);

• hdbl — the double-vote witness in the extended state.

Proof idea

Classify each of the two conflicting votes as old / from link 1 / from link 2 via vote_msg_extend_classify, yielding a 3 \times 3 case matrix. The three target-height levels are \le H (old votes, by target_height_bound), H + 1 (link 1), and H + 2 (link 2). A double vote requires a shared target height, so:

• old × old: the pre-existing double vote is returned.

• old × link or link × old (4 cells): the shared target height would force H + 1 \le H or H + 2 \le H, both absurd (Nat.not_add_one_le_self, not_add_two_le_self).

• link 1 × link 2 or link 2 × link 1 (2 cells): the shared target height would force H + 1 = H + 2, absurd (add_one_ne_add_two).

• link 1 × link 1 or link 2 × link 2 (2 cells): both votes target the same block, so t_1 = t_2 contradicts t_1 \ne t_2 (eq_of_eq_right).