Synchronous specification

[Kukovec]

Alternate version of the specification, where voting is slot-restricted. For any n, once current_slot > n we will never see a vote targeting a checkpoint with slot n, so we know that any checkpoint with slot < current_slot is either already justified, or it will never become justified. This allows justified_checkpoints to be computed incrementally.

Changes:

• current_slot added to the state
• MayAdvanceSlot added to Next: With any action, the current_slot may increase (or remain the same)
• CastVotes changed to incrementally update justified_checkpoints
• Removed the \E-quantified target slot or block slot in Next and replaced it with current_slot

[konnov]

Since we have a lot of other specifications and experiments, we have decided to abandon this branch of research.