Try   HackMD

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







%0



10

10



9

9



10->9





11

11



11->10





12

12



12->11





13

13



13->11






14

14



14->13





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
HS
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
LMDB=LMDS
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

LMD14=50 and
LMD12=40
.

For two different tips at

S and
S
with equal FFG information (that is equal justification and finalization checkpoints) we have
LMDS>LMDS
implies that
S
is preferred over
S
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

LMDS 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
LMD9=10
and
LMD13=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
vi
,
i=0,,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.







%0



1

1



0

0



1->0





2

2



2->1





3

...



3->2





97

97



97->3





In this case, the weight of the vote at slot

1 was removed from this slot and assigned to slot
33
when validator
v1
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
LMD97=320
(the total effective balance) and
LMD1=0
.

For a block

B with parent
P
, we will define
BALB=LMDBLMDP
. 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
BAL1=BAL33=BAL65=0
while
BAL97=10
.

More generally for a slot/block

S and its ancestor
T
we will write
LMDT,S:=LMDSLMDT
, that is, the relative weight of votes cast for blocks supporting
S
after
T
. In particular we have
BALS=LMDP,S
. In the last example above we have
LMD1,97=320
and
LMD95,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

β be percentage staked by malicious validators. We assume that
β<32PB640.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

S032 be the current slot,
E0:=S032
be the current epoch. The current canonical head is
H0=H(S0)
at slot
S0
, and its parent block is
B
at slot
S01
.

We assume that

E01 is justified, ie. the current justified checkpoint is of the form
(Root:R,Epoch:E01)
.

Let

γ 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

η 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
LMDT,Bmax(S01T,32)Totγη

Proof. This is simply the fact that the maximum possible number of votes is given by

max(S01T,32)η and from these votes the worst that can happen is that the attestations that weren't accounted for (ie
γ
) 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
LMDBLMDSmax(S01T,32)Totγ2η.

Proof. The proof is the same as Lemma 1, the only difference is the extra
η
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

κ be the highest LMD weight of any head contending with
B
or any ancestor of
B
(excluding
B
itself)
γ+κ+(2β1)Tot+PBTotLMDB.

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
SS0
.

If

S=S0, there is nothing to prove. Let
S>S0
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
HB
be the best head descending from
B
at the time
S
, and let
S
be the best head on the chain of
S
at slot
S01
, so that we have







%0



C

C



dots1

...



dots1->C





dots2

...



S1

S'



dots2->S1





HB

H
B




dots3

...



dots3->C






dots4

...



S0

S
0



dots4->S0





S1->dots1





B

B



S0->B





HB->dots4





S

S=H(S)



S->dots2





B->dots3






Here notice that

HB may not to descend from
S0
and the slot of
HB
is less than
S
.

Without loss of generality we may assume that

S is the minimal slot with this property. This implies that
S0+i
either was in the chain of
B
or was not the canonical head during
S0+i
. for all
i0
such that
S0+iS
.

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

  • both
    S
    and
    HB
    have the same justified checkpoint
    (R,E1)
    . In this case we must have
    LMD(S)>LMD(HB)
    .
  • All of
    C
    ,
    S
    and
    HB
    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,...,SS01, honest validators voted for the block
HS0+i
during
S0+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
S0
and
S1
are votes during epoch
E
. By our assumptions, their previous votes were cast during epoch
E1
, 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β)Tot(SS0)

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
βTot(SS0),
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
LMDHSLMDS´(1β)Tot(SS0)+γ+PBTot.

On the other hand the branch supporting

B will have weight at least
LMDHBLMDBβTot(SS0).

From

LMDHS>LMDHB it follows that
γ+LMDS+(2β1)Tot(SS0)+PBTot>LMDB

Since

2β<1 we obtain
γ+LMDS+(2β1)Tot+PBTot>LMDB.

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
HB
are all in the same epoch
E
. Let us suppose first that
C
and
S0
are on the same epoch
E
, but not necessarily is the case for
HB
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
S0
, the difference of LMD weight between the tip of the chain supporting
B
and the chain supporting
S
increases by an amount of
(12β)Tot>0
. Since
E1
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
HB.justified_checkpoint.EpochHS.justified_checkpoint.Epoch

This is because
β<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
(12β)Tot(32(E+1)S0)
(accounting for the slots between the
S0
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
(12β)Tot(C+132E)
.

Malicious validators that had voted during

E on the chain supporting
B
, that is between the slots
C+1
and
S01
, 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βT(S01C)
.

It follows that during a slot

S in epoch
E+1
we have
LMDHBLMDS
is at least
LMDBLMDS+(12β)Tot(33+CS0)2βTot(S01C)

By Lemma 2 we have

LMDBLMDS(S01C)Totγ2η.
From where we obtain that during epoch
E+1
we have
LMDHBLMDS32(12β)TotPBTot2γ2η

where we have added another
γ
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(γ+η)<(32(12β)PB)Tot,

which is guaranteed by our assumptions on
β
.

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.