Safe Head: happy case

Basic definitions and notation

We will use $S$ for slots, $B$ for blocks, $E$ for epochs. Often times we will use $S$ for the block at slot $S$ abusing notation when no confusion could arise. For example, a forkchoice diagram of the form

denotes a reorg where the block in slot 13 has the block in slot 11 as parent. We will say things like The parent of $S$ is $T$ to mean the parent of the block in slot $S$ is the block in slot $T$.

All our forkchoice diagrams will have time going from left to right, that is a block $T$ to the right of a block $S$ will correspond to a slot $T>S$.

For a slot $S$ we will denote by $H_S$ the canonical head during $S$. When this depends on the time withing the slot, eg. if the block has arrived or not, we will explicitly specify it.

LMD Weights
For a block $B$ at slot $S$, that is a leaf of the forkchoice tree, we will write $LM{D}_B=LM{D}_S$ to mean the LMD GHOST weight of the branch supporting this head. That is, in terms of the forkchoice implementation the node's weight*

For example, assuming that each node in the diagram above was voted by a single validator with 10ETH of effective balance, we would have $LM{D}_{14}=50$ and $LM{D}_{12}=40$.

For two different tips at $S$ and $S^{\prime }$ with equal FFG information (that is equal justification and finalization checkpoints) we have $LM{D}_S>LM{D}_{S^{\prime }}$ implies that $S$ is preferred over $S^{\prime }$ as the current canonical head. In the example above, the node at $14$ would be preferred over that at $12$.

We will abuse notation and also use $LM{D}_S$ to denote the LMD weight of a node even when it is not a tip of forkchoice. With the same assumptions as above we would have $LM{D}_9=10$ and $LM{D}_{13}=40$. Recall that when a validator cast a vote, its previous vote is removed from the corresponding forkchoice node's balance and weight. Consider a chain without any forks, there are exactly 32 validators $v_i$, $i=0,\dots ,31$ with 10 ETH effective balance and each has voted sequentially, that is validator $i$ voted at slot $i(32)$ for each one of the blocks.

In this case, the weight of the vote at slot $1$ was removed from this slot and assigned to slot $33$ when validator $v_1$ voted during epoch $1$. Then it was removed from block $33$ and assigned to $65$ during Epoch $2$ and finally removed from $65$ and assigned to $97$ during epoch $3$. We see that $LM{D}_{97}=320$ (the total effective balance) and $LM{D}_1=0$.

For a block $B$ with parent $P$, we will define $BA{L}_B=LM{D}_B-LM{D}_P$. That is the total stake that voted directly for $B$ and we will refer to it as the balance of $B$. In the first example above, the balance of every node is $10$. However, in the last example we have $BA{L}_1=BA{L}_{33}=BA{L}_{65}=0$ while $BA{L}_{97}=10$.

More generally for a slot/block $S$ and its ancestor $T$ we will write $LM{D}_{T,S}:=LM{D}_S-LM{D}_T$, that is, the relative weight of votes cast for blocks supporting $S$ after $T$. In particular we have $BA{L}_S=LM{D}_{P,S}$. In the last example above we have $LM{D}_{1,97}=320$ and $LM{D}_{95,97}=20$.

Safety Assumptions
Let $Tot$ be the total effective balance of validators divided by 32, this is roughly the total stake attesting per slot.

We use PB to denote the proposer boost weight, currently set on mainnet to $0.4$.

Let $\beta$ be percentage staked by malicious validators. We assume that $$\beta <\frac{32-PB}{64}\simeq 0.49.$$

We assume that validators are online and attesting, this is measured below by the amount of stake of missing attestations that we will keep at a minimum (eg below 5% of the total stake).

We assume that validators are equidistributed, each committee has the same proportion of honest/dishonest validators.

Safe Head definition

Setup
Let $S_0\ge 32$ be the current slot, $E_0:=\lfloor \frac{S_0}{32}\rfloor$ be the current epoch. The current canonical head is $H_0=H(S_0)$ at slot $S_0$, and its parent block is $B$ at slot $S_0-1$.

We assume that $E_0-1$ is justified, ie. the current justified checkpoint is of the form $(\text{Root:}R,\text{Epoch:}{E}_0-1)$.

Let $\gamma$ be the total stake of attestations that could have been cast in the last 32 slots and have not been acounted for, that is, those attestations have not been seen yet either over gossip nor included in any block that is currently in forkchoice.

Let $\eta$ be the total stake of attestations (only the last possible vote of each validator) that have been cast for non-canonical blocks.

Lemma 1. Let $T$ be any ancestor of $B$, we have that
$$LM{D}_{T,B}\ge max(S_0-1-T,32)\cdot Tot-\gamma -\eta$$

Proof. This is simply the fact that the maximum possible number of votes is given by $max(S_0-1-T,32)-\eta$ and from these votes the worst that can happen is that the attestations that weren't accounted for (ie $\gamma$) are given to non-canonical blocks.

QED

A simple variation of this Lemma is
Lemma 2. Let $S$ be any contending block of $B$ with common ancestor $T$, then
$$LM{D}_B-LM{D}_S\ge max(S_0-1-T,32)\cdot Tot-\gamma -2\eta .$$
Proof. The proof is the same as Lemma 1, the only difference is the extra $\eta$ votes that not only do not count for $B$ but may count for the contending branch of $S$.

QED

Theorem 2. Under the above conditions, let $\kappa$ be the highest LMD weight of any head contending with $B$ or any ancestor of $B$ (excluding $B$ itself)
$$\gamma +\kappa +(2\beta -1)\cdot Tot+PB\cdot Tot\le LM{D}_B.$$

the block $B$ is final.

Proof. We want to prove the following. For any slot $S$, let $H(S)$ be the canonical head (from the point of view of an honest validator) at $S$. Then $H(S)$ is a descendant of $B$ for $S\ge S_0$.

If $S=S_0$, there is nothing to prove. Let $S>S_0$ be a slot that does not satisfy the hipothesis, that is $H(S)$ does not descend from $B$. Let $C$ be the slot of their common ancestor, let $H_B$ be the best head descending from $B$ at the time $S$, and let $S^{\prime }$ be the best head on the chain of $S$ at slot $S_0-1$, so that we have

Here notice that $H_B$ may not to descend from $S_0$ and the slot of $H_B$ is less than $S$.

Without loss of generality we may assume that $S$ is the minimal slot with this property. This implies that $S_0+i$ either was in the chain of $B$ or was not the canonical head during $S_0+i$. for all $i\ge 0$ such that $S_0+i\le S$.

For simplicity of exposition, let us first make the following assumptions:

• both $S$ and $H_B$ have the same justified checkpoint $(R,E-1)$. In this case we must have $LMD(S)>LMD(H_B)$.
• All of $C$, $S$ and $H_B$ are slots in the same epoch $E$.
• There are only two viable heads at all times (that is, we have a simple fork)

For each $i=0,...,S-S_0-1$, honest validators voted for the block $H_{S_0+i}$ during $S_0+i$, and this block is a descendant of $B$ by hypothesis. Some of these votes however may have been supporting the $S$ branch before, that is, any vote from an honest validator that was before $C$ would have supported the branch $S$ and no longer does. Honest validators votes on slots between $C+1$ and $B$ however, were not supporting the chain of $S$ before, and will therefore not change the difference in the LMD weight of the chain of $B$ with respect to that of $S$. On the other hand, all validators that vote between slots $S_0$ and $S-1$ are votes during epoch $E$. By our assumptions, their previous votes were cast during epoch $E-1$, therefore before slot $C$. The votes that are added to the chain of $B$ (not changing its weight) and subtracted from the chain of $S$ are then
$$(1-\beta )\cdot Tot\cdot (S-S_0)$$

On the other hand, malicious validators would be voting for the contending branch of $S$, and for each vote they cast that was previously voting for the B branch, it would now count towards $S$. In the worst case scenario, every single malicious vote, shifts from the B branch to the S branch. These votes, with total weight
$$\beta \cdot Tot\cdot (S-S_0),$$ will be removed from the $B$ branch and added to the LMD weight of the $S$ branch (without changing its weight since they were already counted towards $S$).

We can assume also that all of the witheld attestations were malicious, were valid, and could be added to the $S$ branch, and that also the block at $S$ was timely, thus proposer boosted. This accounts for a total LMD weight for the branch of $S$ at the start of its slot of at most
$$LM{D}_{H_S}\le LM{D}_{S´}-(1-\beta )\cdot Tot\cdot (S-S_0)+\gamma +PB\cdot Tot.$$

On the other hand the branch supporting $B$ will have weight at least
$$LM{D}_{H_B}\ge LM{D}_B-\beta \cdot Tot\cdot (S-S_0).$$

From $LM{D}_{H_S}>LM{D}_{H_B}$ it follows that
$$\gamma +LM{D}_{S^{\prime }}+(2\beta -1)\cdot Tot\cdot (S-S_0)+PB\cdot Tot>LM{D}_B$$

Since $2\beta <1$ we obtain
$$\gamma +LM{D}_{S^{\prime }}+(2\beta -1)\cdot Tot+PB\cdot Tot>LM{D}_B.$$

We now have reduced the problem to prove that our assumptions above were not necessary. Let us first deal with the second assumption, that is that $C$, $S$ and $H_B$ are all in the same epoch $E$. Let us suppose first that $C$ and $S_0$ are on the same epoch $E$, but not necessarily is the case for $H_B$ and $S$, that is, the fork is long enough to cross epoch boundaries but the common ancestor is close to the block $B$ which we want to prove is final. Notice that for each slot during epoch $E$ and after slot $S_0$, the difference of LMD weight between the tip of the chain supporting $B$ and the chain supporting $S$ increases by an amount of $(1-2\beta )\cdot Tot>0$. Since $E-1$ was justified, and all votes during $E$ are for the same target, when crossing the epoch boundary to $E+1$ we have that the justification of the $B$ chain is at least the justification of the $S$ chain, that is
$$H_B.\text{justified\_checkpoint.Epoch}\ge H_S.\text{justified\_checkpoint.Epoch}$$
This is because $\beta <0.5$ and honest validators are attesting on the $B$ chain. It follows that honest validators will continue voting during $E+1$ on the $B$ chain, while malicious validators can continue voting on the $S$ chain. At the start of epoch $E+1$, the difference on LMD weights of both chains has increased by $(1-2\beta )\cdot Tot\cdot (32(E+1)-S_0)$ (accounting for the slots between the $S_0$ and the start of $E+1$).

During $E+1$, validators that had voted up to slot $C$ during $E$ will account for a difference in LMD weights of $(1-2\beta )\cdot Tot\cdot (C+1-32E)$.

Malicious validators that had voted during $E$ on the chain supporting $B$, that is between the slots $C+1$ and $S_0-1$, can shift their vote during $E+1$ to the chain of $S$, these will increase the weight on $S$ and decrease it from $B$, the maximum difference caused by these is $2\beta \cdot T\cdot (S_0-1-C)$.

It follows that during a slot $S$ in epoch $E+1$ we have $LM{D}_{H_B}-LM{D}_S$ is at least $$LM{D}_B-LM{D}_{S^{\prime }}+(1-2\beta )\cdot Tot\cdot (33+C-S_0)-2\beta \cdot Tot\cdot (S_0-1-C)$$

By Lemma 2 we have
$$LM{D}_B-LM{D}_{S^{\prime }}\ge (S_0-1-C)\cdot Tot-\gamma -2\eta .$$
From where we obtain that during epoch $E+1$ we have
$$LM{D}_{H_B}-LM{D}_S\ge 32(1-2\beta )\cdot Tot-PB\cdot Tot-2\gamma -2\eta$$
where we have added another $\gamma$ terms of withdeld votes that counted for the $S$ branch and proposer boost to the last block produced by the malicious branch. We see that the RHS is positive if
$$2(\gamma +\eta )<(32(1-2\beta )-PB)\cdot Tot,$$
which is guaranteed by our assumptions on $\beta$.

If the slot $S$ is in an epoch higher than $E+1$, the situation does not change, since malicious validators have already been accounted for the branch $S$ and honest validators for the branch $B$, thus the LMD difference will continue to increase, and the same argument can be applied for justification.