Context

This commit adds a condition to guarantee that in state_transition(state,block), state.slot < block.slot.
It is related to the spec update v0.11.3.

It is supposed to fix a problem "process without progress".
It is unclear to me what it actually fixes.

Progress with state_transition

As far as I understand, the fix guarantees that, for a sequence of state_transitions, the slot number progresses. In other words it prevents executions like (I write s - b -> s' for s' = state_transition(s,b))

s0 - b0 -> s1 - b1 -> s2 ...

with b0.slot == b1.slot == b2.slot.

This seems to assume that progress is made by executing state_transition successively, and each time using the previously computed state.

Progress with on_block

However this does not seem to align with how state_transition is used in the Beacon chain.
As far as I can tell, state_transition is only called in on_block(b) with b a block.
In on_block(b), the pre_state that b claims to attach to is computed.
And later state_transition(pre_state,b) is called.

So if I am correct, nothing prevents me from calling on_block(b) many times with the same block.
This will trigger a computation with state_transition to compute the successor state of pre_state with b , state_transition(pre_state,b).
Now assume the store is S, and b has already been added to the store (it is in S.blocks).
There seems to be a possibility of an infinite sequence of on_block(b) without the store being modified (because b is already in):

S - on_block(b) -> S - on_block(b) -> S .....

Security vulnerability

An exploit may be a DoS attack by sending the same block b many many times.

How the issues can be mitigated

First the change in the commit that adds a condition to guarantee that in state_transition(state,block), state.slot < block.slot may be pushed upwards to on_block by requesting that pre_state.slot < b.slot in the pre-conditions of this function. This avoids the needs for all the asserts on the slot number that are below on_block (a formal proof can be established using our Dafny specification of the eth2,0 specs).

Second, to avoid the possibility of processing the same block again and again in on_block without progress on the store, we may require that the block b (or its hash) is not already in the store's keys, and add the pre-condition

on_block(b)
   requires hash_tree_root(b) !in S

to on_block(b).

How the issues was uncovered

Issue was uncovered while specifying and proving some invariants on the Dafny specification of the Eth2.0 specs.