Add restriction to only consider `single_node_state`s where each block in `view_blocks` is a complete chain.

freespek / ssf-mc

EF project Exploring Automatic Model-Checking of the Ethereum specification

Apache License 2.0

4 stars 0 forks source link

Add restriction to only consider `single_node_state`s where each block in `view_blocks` is a complete chain. #15

Open saltiniroberto opened 3 months ago

saltiniroberto commented 3 months ago

This is to reduce the initial state space. I would suggest encoding this constraint outside of IsValidNodeState as a node state that has incomplete chains is still valid, but just not relevant for accountable safety.