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.

[protolambda]

E.g. if a state is partially updated and later an assertion is failed, the partial state update should be kept.

This is wrong. If an assertion (or index error) is raised anywhere in the state transition, the transition is invalid, and the block should not be accepted. This is defined here: https://github.com/ethereum/eth2.0-specs/blob/dev/specs/core/0_beacon-chain.md#beacon-chain-state-transition-function

[djrtwo]

Agreed that a note could be added to the fork choice to make it clear that an assertion failure in a function should lead to no modifications to the store.

[franck44]

@ericsson49 @protolambda @djrtwo

This issue is related the use of asserts to define when a computation (or a block) is valid.
It is possible to define functionally what a valid block.
We have done it in our Dafny spec with the isValid function.

It is then easy to use this function as pre-condition to other functions (e.g. state_transition) to ensure they will never fail and no roll back is necessary.
See the example of state_transition here and on_block here.

Using functions what the result of an operation is, or what a pre-condtion may improve readability.
On top of that it enables to check at the beginning of the execution of a function whether it can go through without violating assert statements (no waste of computation time, no roll back).

it is also a good way to have a spec that FP folks can use to write their client.