Finalization rule 3 is unreachable

[ChihChengLiang]

It's impossible to have 0b111 without triggering Rule 2. Observe the bit position of previous_epoch - 1,

1. Get left 1 justified
2. In the next epoch the position become previous_justified.
3. In the epoch to trigger rule 3, it trigger rule 2 first.

  j
0b10
  p
  j
0b111

Rule 2: Set state.finalized_epoch = state.previous_justified_epoch if (state.justification_bitfield >> 1) % 4 == 0b11 and state.previous_justified_epoch == previous_epoch - 1.
Rule 3: Set state.finalized_epoch = state.justified_epoch if (state.justification_bitfield >> 0) % 8 == 0b111 and state.justified_epoch == previous_epoch - 1.

Related:

• https://github.com/ethereum/trinity/pull/264/files#r255382122
• Finalization rule 3 would return True in no case #410

[ChihChengLiang]

Rule 1 might also have some issue, it can only finalize the epoch that was already finalized by Rule 2.

[vbuterin]

Suppose that at the end of epoch N+2, epoch N+1 is justified but epoch N+2 is not. Then, at the end of epoch N+3, epochs N+1, N+2 and N+3 are all justified, because of messages that were not yet included in the chain before.

[ChihChengLiang]

That case will trigger rule 2 before 3. because N+1 is now previous justified epoch and the bitfield in rule 3 is a special case of the bitfield in rule 2

[vbuterin]

Ok, try this:

• In epoch N+1, JE is N, prev JE is N-1, and not enough messages get in to do anything
• In epoch N+2, JE is N, prev JE is N, and enough messages from the previous epoch get in to justify N+1. N+1 now becomes the JE. Not enough messages from epoch N+2 itself get in to justify N+2.
• In epoch N+3, LJE is N+1, prev LJE is N, and enough messages get in to justify epochs N+2 and N+3.

Rule (2) does not get triggered because prev LJE is NOT previous_epoch - 1, but rule (3) does get triggered because LJE is previous_epoch - 1, the previous epoch is justified, and the current epoch is justified.

[ChihChengLiang]

Alright, finally find the problem. Some case could trigger two rules at the same time.

I made a wrong assumption and implement the spec wrong. The wrong implementation returns the finalized epoch when a rule is triggered, while in the correct one every rule must be checked.

A simulation in Trinity shows that:

• In epoch N+2, Rule 2 would finalize N.
• In epoch N+3, Rule 1 would first finalize N again, then Rule 3 finalize N+1.

A quick look into the different codebases.

• Prysm has the same style as my implementation, need a head up for this bug. cc @terenc3t.
• The Lighthouse is safe, cc @paulhauner.

Thank you v for the example ❤️

[paulhauner]

Thanks @hwwhww :)

I've drew up some diagrams a while ago and noticed the same thing about double-execution.

Something that I haven't quite got my head across is why rules #1,3 require there to be two justified epochs following the finalized epoch, whilst #2,4 only require one.

[vbuterin]

The meta-rule behind all four rules is that if there are two epochs B[1] and B[n], where both are justified and B[n] was justified using B[1] as a source, and all intermediate epochs B[2] ... B[n-1] are all also justified (no matter what source), then B[1] can be finalized.

Rules 1 and 3 cover the n=3 case (the difference between the two is that rule 1 assumes that the current epoch is n+1, and rule 3 assumes it's n),and rules 2 and 4 cover the n=2 case.

The reason why any rule except rule 4 (the only rule in the original FFG paper) is necessary is to cover the possibility that it takes an entire epoch for attestations to get included in the chain, and so epoch 1 can't get justified until the chain has already moved on to epoch 2.

[dankrad]

The meta-rule behind all four rules is that if there are two epochs B[1] and B[n], where both are justified and B[n] was justified using B[1] as a source, and all intermediate epochs B[2] ... B[n-1] are all also justified (no matter what source), then B[1] can be finalized.

Rules 1 and 3 cover the n=3 case (the difference between the two is that rule 1 assumes that the current epoch is n+1, and rule 3 assumes it's n),and rules 2 and 4 cover the n=2 case.

The reason why any rule except rule 4 (the only rule in the original FFG paper) is necessary is to cover the possibility that it takes an entire epoch for attestations to get included in the chain, and so epoch 1 can't get justified until the chain has already moved on to epoch 2.

So my understanding of the FFG paper was that justification can happen to any past epoch as well. But we only allow attestations to the current and previous epoch. So I guess that is why we have those two cases, whereas I would have expected that we need to check all past epochs for justification/finalisation?
Is there a description of the exact consensus algorithm that is used?

[djrtwo]

We have these limited cases because of a few reasons:

• We only allow attestations from previous and current epoch to be included on chain
• We only allow attestations with the expected justified epoch wrt the state at the time of attestation to be included on chain
• We eagerly try to process the current epoch attestations even though not all slot attestations have been given an entire epoch to be included

The combination of these three attributes create the 4 possible cases possible to satisfy the general rule described here #611 (comment)

If we allowed 3 epochs of inclusions rather than two, we would need to cover the n=4 case (or change the state a bit to handle things more generally).

There is a WIP academic paper describing this more general purpose finality rule and it's instantiation in a PoS chain similar to our beacon chain. Will share when there's a draft ready

[dankrad]

OK, thanks :) This helps me understand what's going on.