Eth2.0-specs: Side effects in functions

[franck44]

The specs seem to use different types of signatures for functions. for instance:

Case 1:

def state_transition(state: BeaconState, signed_block: SignedBeaconBlock, validate_result: bool=True) -> BeaconState:
 block = signed_block.message
    # Process slots (including those with no blocks) since block
    process_slots(state, block.slot)
    # Verify signature
    if validate_result:
        assert verify_block_signature(state, signed_block)
    # Process block
    process_block(state, block)
    # Verify state root
    if validate_result:
        assert block.state_root == hash_tree_root(state)
    # Return post-state
    return state

and case 2:

def process_slots(state: BeaconState, slot: Slot) -> None:
    assert state.slot < slot
    while state.slot < slot:
        process_slot(state)
        # Process epoch on the start slot of the next epoch
        if (state.slot + 1) % SLOTS_PER_EPOCH == 0:
            process_epoch(state)
        state.slot = Slot(state.slot + 1)

In case 1, it seems redundant to return a BeaconState because the state variable is passed by reference (I am not Python expert, but AFAIK state is mutable and hence passed by reference.) But the fact that the function's return type is a BeaconState also gives a false sense of immutability of the input object state. The result is actually in state (side-effect and in the returned value.

In case 2, the mutability of the parameter state is used and instead of returning a state, process_slots modifies state, so the result is obtained by a side-effect on input parameter state (passed by reference).

Main question: How is the choice of a function signature determined in the specs?
Some functions rely on side-effects, and some may not.

Python parameters' passing and the interference with local storage is known to be rather cumbersome as described in the additional comment below, so a clear and principled way of specifying functions may help reducing of problems that can arise in implementations.

Additional comment
For instance (again, I am not a Python expert, so if this is wrong, please correct me), the following code may not have any side-effect on state and leave the input parameter (although passed by reference) state unchanged:

class BeaconState:
    def __init__(self, slot):
        self.slot = slot

def process_slots(state: BeaconState, slot: int) -> None:
    s = BeaconState(0)
    s.slot = state.slot
    # the value of s is the same as the initial value of state
    state = s
    while state.slot < slot:
        state.slot = (state.slot + 1)

# k is a BeaconState
k = BeaconState(2)
print (k.slot) # Result is 2
process_slots(k, 4)
print (k.slot) # result is still 2

The specs may benefit from a clearer definition of the functions (without side-effects).

[mratsim]

I wonder if there is a way to tag additional markers like var or mut in MyPy?

def state_transition(state: mut BeaconState, signed_block: SignedBeaconBlock, validate_result: bool=True) -> BeaconState:
 block = signed_block.message
    # Process slots (including those with no blocks) since block
    process_slots(state, block.slot)
    # Verify signature
    if validate_result:
        assert verify_block_signature(state, signed_block)
    # Process block
    process_block(state, block)
    # Verify state root
    if validate_result:
        assert block.state_root == hash_tree_root(state)
    # Return post-state
    return state

[hwwhww]

Yeah, I felt the same.
Old issue and some options: https://github.com/ethereum/eth2.0-specs/issues/1059

I feel it's a bit late to make it side-effect-free in phase 0, I'd defer to the client teams.

[franck44]

Sorry did not see there was another issue with the same topic.
Altogether, this is probably dangerous to delegate a lot to client teams, and it does not make their life easy, nor does it open the door to implementations in side-effect free languages like Haskell.

This seems to indicate that Python may not be the best candidate to develop easy-to-read and sound specifications.
There are lots of specification-friendly languages, in which we can write readable, verifiable, and documented specs, without bothering about Python specific side-effect problems.

An example is Dafny, and we have already written dozens of function specifications like state_transition, with a clear semantics, easy to read, documented and machine checked.

[adiasg]

@franck44
But the fact that the function's return type is a BeaconState also gives a false sense of immutability of the input object state. The result is actually in state (side-effect and in the returned value.

I agree with this. In fact, on a first reading of the spec, I also interpreted state_transition to be a pure function based just on it's signature.

@franck44
The specs may benefit from a clearer definition of the functions (without side-effects).

Again, I agree with this.
As a first step, I think that documenting the current behavior will largely help first-time readers to understand the spec swiftly & correctly. I also support the larger goal of making the spec more "functional" in it's behavior.

I'll bring up this issue in the next spec team call & post updates in this thread.

[franck44]

@adiasg if there is anything we can do to help in the discussion (e.g. present the work we are doing with Dafny) let me know.
We have written a functional formal spec for almost all of the functions and we are happy to share our experience.

[adiasg]

Update from spec team call:
The general view is that re-writing the Python specification to be more functional will change its structure significantly, and deviate from the primary goal of serving as an implementation guide for client teams. There are some things which are undesirable in the current version of the pyspec, such as the misleading function signature of state_transition, which should be rectified in the coming versions.

On the other hand, this Python specification should have a "how to use" manual that helps newcomers to correctly understand it.

For users that require a more formal specification, there is Runtime Verification's K model, and now a Dafny model from @franck44 & PegaSysEng.

[dankrad]

There are some things which are undesirable in the current version of the pyspec, such as the misleading function signature of state_transition, which should be rectified in the coming versions.

Just wanted to highlight that this should definitely be done. Reading some client code I found it very confusing and then saw that they copied one for one what the spec does. Doesn't look great.