Unclear atomicity semantics of the beacon chain spec

[ericsson49]

In the beacon chain specs state updates are sometimes intertwined with assertions within a function. An executable python spec is also constructed from such code fragments. The executability of the specs suggests such functions should not be treated as atomic state updates (assuming python semantics). E.g. if a state is partially updated and later an assertion is failed, the partial state update should be kept. However, such view contradicts the intention expressed in other functions.

For example, consider the fork choice/on_block function. A block store is updated with a new block. Some checks are preformed after (including state_transition ones). And then, a block_state store is updated with the corresponding block state.

If any of in-between assertions failed, then store.blocks would contain the block, while store.block_states wouldn't. That seems to be a problem. For example, if an attestation referencing the block arrives later, the on_attestation is called. Which first checks if the referenced block is present (which will succeed) and later accesses the block's state, which is absent. So, the piece of code implicitly assumes the changes made by on_block are atomic, i.e. either both block and it's state are stored or none of them (or maybe some weaker form like, if a block is stored then it's state also should). Which seems pretty reasonable, since ensuring consistency of block/state updates with python code would be more verbose and makes the specs more clumsy.

Besides storage updates, an analogous problem exists with beacon state updates. For example, in process_attestation function, either state.current_epoch_attestations or state.previous_epoch_attestations is updated, followed by some assertion checks. If any of the assertion failed, the update will be kept.

While it's a minor issue from a human being point of view, it's not so from a machine's perspective. For example, we would like to develop a test suit to test fork choice against the specs. In case of negative tests, it becomes important, so that we can base our tests on a stable ground.

Another point is that we'd like eventually to use formal methods like bounded model checking or formal proofs to check/verify properties of the beacon chain specs.

Based on the above, we propose:

• to add clarification to the beacon chain specs, regarding atomicity semantics of the fork choice functions (on_block, on_attestation). I.e. should multiple store updates be performed in all or none fashion. Or the python execution semantics are assumed.
• Optionally, to clarify beacon state updates atomicity semantics.
• Optionally, to modify the executable python spec to comply the changes.

[ericsson49]

Opened https://github.com/ethereum/eth2.0-specs/issues/1409

[ericsson49]

Closing this, as there exists a corresponding eth2.0-specs issue.