freespek / ssf-mc

EF project Exploring Automatic Model-Checking of the Ethereum specification
Apache License 2.0
4 stars 0 forks source link

Consider genesis checkpoint a valid checkpoint #29

Closed thpani closed 3 months ago

thpani commented 3 months ago

Currently, Init requires that all checkpoints c in view_votes satisfy c.chkp_slot > c.block_slot.

However, the checkpoint associated with the genesis block is defined as [ chkp_slot |-> 0, block_slot |-> 0, ... ].

Following offline discussion with Roberto, we make an exemption for the genesis checkpoint.