Loading .
Settings
3
3

Chained isolated 3SF protocol

Casper-FFG revisited

Checkpoints

A checkpoint is a \((block, slot, slot)\) triple \((B,c,p)\) where \(p = slot(B)\), and \(c\) is the slot in which \(B\) is proposed for justification (corresponding to the epoch in Casper-FFG checkpoints). Other than for the genesis checkpoint \((G,0,0)\), we always have \(c > p\). We refer to \(p\) as the proposal slot of \(B\) and to \(c\) as the checkpoint slot of \((B,c,p)\).

FFG vote

An FFG vote is a link \((B_1,c_1, p_1) \to (B_2, c_2, p_2)\) between a source and a target checkpoint, with \(B_1 \preceq B_2\) and \(c_2 > c_1\).

Justification

The genesis checkpoint \((G, 0, 0)\) is justified. Any other checkpoint \((B,c,p)\) is justified if there is a set of 2/3+ FFG votes \((A_i, c_i, p_i) \to (B_i,c, p_i')\), where \(A_i \preceq B \preceq B_i\) and all sources \((A_i, c_i, p_i)\) are justified. Note that the source and target blocks can be different across votes.

Finalization

A checkpoint \((B,c,p)\) is finalized if it is justified and there is a set of 2/3+ FFG votes with source \((B,c,p)\) and target slot \(c+1\), i.e. votes \((B,c,p) \to (B_i, c+1, p_i)\). In this case only target blocks are allowed to be different as the target checkpoint slot must be \(c+1\).

Greatest justified checkpoint and fork-choice root

Letting \((c_1, p_1) < (c_2, p_2)\) be defined by lexicographic ordering, we define an ordering on checkpoints by \((B_1,c_1,p_1) \prec (B_2,c_2, p_2)\) if \((c_1, p_1) < (c_2, p_2)\). We often consider the greatest justified checkpoint, defined with respect to this order. If the greatest justified checkpoint is \((B,c,p)\) we refer to \(B\) as the fork-choice root.

The figure shows all justified checkpoints after 4 slots. From left to right, the checkpoint slot increases, and for a given checkpoint slot the the proposal slot decreases top to bottom. Here we assume that all justifications happen through votes that have the same source and target, indicated through the arrows. Blocks \(A,B,C,D\) are proposed at slot \(0,1,2,3\), respectively. At slot \(2\), votes with source \((A,1,0)\) and target \((B,2,1)\) justify both \((B,2,1)\) and \((A,2,0)\). Nothing is justified at slot \(3\), while at slot \(4\) checkpoints with blocks \(B,C,D\) are justified, by votes with source \((B,2,1)\) and target \((D,4,3)\). At this point, \((D,4,3)\) is the greatest justified checkpoint.

Note that the greatest justified checkpoint is very much related to the latest justified checkpoint in plain Casper-FFG (epoch vs slot terminology aside). The lexicographic ordering first considers the checkpoint slot \(c\), restricting our choice to justified checkpoints of latest checkpoint slot, which in Casper-FFG would already yield a unique checkpoint, precisely the latest justified. Instead, here it is possible to have multiple justified checkpoints with the same checkpoint slot, and we may need the extra step of choosing the one with the greatest proposal slot \(p\) among those, as per the ordering.

Slashing

Two different votes \((B_1,c_1, p_1) \to (B_2, c_2, p_2)\), \((B_1', c'_1, p'_1) \to (B_2', c'_2, p'_2)\) are slashable if:

Slashing can always be avoided by locally ensuring monotonicity of the greatest justified checkpoint, since this is what is used as the source of FFG votes (as in Casper-FFG, as we’ll see), i.e., only updating when receiving a new justified checkpoint which is greater with respect to \(\prec\).

The figure depicts an instance of surround voting on top, with the slashable votes in red, and the fork corresponding to it on the bottom, with finalized checkpoints in red. From slot 4 to slot 3, the source has been moved “back” from checkpoint \((C,3,2)\) to the lower checkpoint \((B,3,1)\). This is in particular a case of surround voting that’s unique to this protocol and not present in Casper-FFG, because the two source checkpoints have the same checkpoint slot. Due to this, \((C,3,2)\) is finalized but \((E,5,4)\), a greater conflicting checkpoint, is justified and then finalized.

Fork-choice and confirmation

Attestations

An attestation is a head vote and FFG vote pair, where a head vote is just a (reference to a) block. Each attestation has a slot associated to it, which is the slot in which it should be sent, and corresponds to the checkpoint slot of the FFG vote target it contains.

Fork-choice

At any time a node can run the fork choice by starting from the fork-choice root then running the RLMD-GHOST. The output is the canonical chain, and the tip of the canonical chain is the chain head. A block is canonical if part of the canonical chain.

Confirmation candidates

A node keeps a set of blocks which we refer to as confirmation candidates. In slot \(p\) a node adds a block \(B\) to its set of confirmation candidates if at time \(2\Delta\) into the slot it has 2/3+ head votes from slot \(p\) that are in the subtree rooted at \(B\).

Confirmation

At any given time, a node considers a block \(B\) confirmed if either \(B\) is the fork-choice root or \(B\) is a canonical confirmation candidate. Note that the fork-choice root is canonical by definition, so all confirmed blocks are canonical. Moreover, each node always knows of a unique highest confirmed block, since the fork-choice root is always confirmed and confirmed blocks do not conflict because they are all in the canonical chain.

Protocol

The structure at slot \(p\) is propose-attest-confirm-freeze:

Security analysis

Liveness theorem

Assume 2/3+ of the validators are honest and that the network is synchronous. If the proposer of slot \(t\) is honest and proposes block \(B\) then:

Proof:

Accountability

Proof: Let \((B,c, p)\) be finalized at slot \(t+1\). We assume that no checkpoint \((B',c, p')\) with \(B'\) conflicting with \(B\) is justified at slot \(c\), as that would clearly involve 1/3+ equivocation, because the votes which count for justification of \((B,c,p)\) must have target blocks in the subtree of \(B\) and the votes which count for justification of \((B',c, p')\) must have target blocks in the subtree of \(B'\), and these two subtrees are disjoint by assumption. Then, suppose \(c'\) is the smallest slot \(> c\) such that a checkpoint \((B', c', p')\) is justified and \(B \not \preceq B'\), i.e., either \(B'\) conflicts with \(B\) or it is a strict ancestor of it. Here we assume that one such slot exists, and argue by contradiction. Consider a vote \((A_i, c_i, p_i) \to (B_i, c', p_i)\) involved in the justification of \((B', c', p')\), by a validator which has also voted for \((B,c, p) \to (*, c+1)\), i.e. to finalize \((B,c, p)\). By definition of justification, \(A_i \preceq B' \preceq B_i\). There are a few cases:

Rationale