# Model based validator state testing

By Mikhail Kalinin (@mkalinin) and Alex Vlasov (@ericsson49)

[toc]

## Motivation
A number of different validator states that are distinguished by the protocol has been increased by Electra as it has introduced new withdrawal credential type, decoupled `MAX_EFFECTIVE_BALANCE` from the `MIN_ACTIVATION_BALANCE` and introduced EL triggered requests that can change a validator state under certain conditions.

The above increase of complexity suggests that we need a tool ensuring that a validator state reached via state transition is always correct, and a protocol operation takes into effect if and only if a certain validator state allows for that.

## Proposed approach

The existing testing framework already supports state transition test that allows to easility create new beacon chain [operations](https://github.com/ethereum/consensus-specs/tree/dev/tests/formats/operations) and [epoch processing](https://github.com/ethereum/consensus-specs/tree/dev/tests/formats/epoch_processing) tests which is sufficiently enough to cover all the protocol operations we need to test validator state modifications.

The proposal is to produce a test case for each combination of protocol operations and validator states and then yield test vectors for implementation testing by leveraging on the existing testing framework.

## Operations

This operation set is not limited to the beacon chain operations and include all pieces of state transition where the validator state can be modified

| # | Operation name | Function |
|:-|:-|:-|
| 1 | eligible for activation | `process_registry_updates` |
| 2 | activation | `process_registry_updates` |
| 3 | ejection | `process_registry_updates` |
| 4 | correlation penalty | `process_slashings` |
| 5 | pending top up | `process_pending_deposits` |
| 6 | pending consolidation | `process_pending_consolidations` |
| 7 | pending partial withdrawal | `process_withdrawals` |
| 8 | full withdrawal | `process_withdrawals` |
| 9 | sweep partial withdrawal | `process_withdrawals` |
| 10 | proposer slashing | `process_proposer_slashing` |
| 11 | attester slashing | `process_attester_slashing` |
| 12 | voluntary exit | `process_voluntary_exit` |
| 13 | bls to execution | `process_bls_to_execution` |
| 14 | top up request | `process_deposit_request` |
| 15 | full withdrawal request | `process_withdrawal_request` |
| 16 | partial withdrawal request | `process_withdrawal_request` |
| 17 | switch to compounding request | `process_consolidation_request` |
| 18 | consolidation request | `process_consolidation_request` |

## Validator state computation

We suggest to compute all potential validator states by defining a validator state model and running a constraint solver on it. The model we use is written in the [Minizinc](https://www.minizinc.org/) language and its code can be found in [Appendix A](#Appendix-A).

The validator state model consists of two parts: validator state profile (a set of properties) and a set of constraints. The validator state profile is summarized in the following table:
| Param 1 | Param 2 | Allowed values |
|-|-|-|
| `activation_eligibility_epoch` | `FAR_FUTURE_EPOCH` | `==`, `!=` |
| `activation_eligibility_epoch` | `finalized_epoch` | `<`, `>=` |
| `activation_epoch` | `FAR_FUTURE_EPOCH` | `==`, `!=` |
| `exit_epoch` | `FAR_FUTURE_EPOCH` | `==`, `!=` |
| `withdrawable_epoch` | `FAR_FUTURE_EPOCH` | `==`, `!=` |
| `slashed` | | `True`, `False` |
| `activation_epoch` | `activation_eligibility_epoch` | `>`, `<=` |
| `withdrawable_epoch` | `exit_epoch` | `>`, `<=` |
| `activation_epoch + SHARD_COMMITTEE_PERIOD` | `current_epoch` | `>`, `<=` |
| `activation_epoch` | `current_epoch` | `<`, `==`, `>` |
| `exit_epoch` | `current_epoch` | `<`, `==`, `>` |
| `withdrawable_epoch` | `current_epoch` | `<`, `==`, `>` |
| `balance` | `0` | `==`, `>` |
| `balance` | `effective_balance` | `<`, `==`, `>` |
| `effective_balance` | `EJECTION_BALANCE` | `<=`, `>` |
| `effective_balance` | `MIN_ACTIVATION_BALANCE` | `<`, `==`, `>` |
| `effective_balance` | `MAX_EFFECTIVE_BALANCE` | `<`, `==`, `>` |
| `withdrawal_credential_type` | | `BLS`, `ETH1`, `COMP`, `UNKNOWN` |
| `has_pending_withdrawal_request` | | `True`, `False` |
| `has_pending_consolidation_request` | | `True`, `False` |

The [Minizinc file](#Appendix-A) also contains a set of constraints which excludes states that are incorrect from the protocol perspective. For example, `exit_epoch != FAR_FUTURE_EPOCH <-> withdrawable_epoch != FAR_FUTURE_EPOCH` means that `exit_epoch` and `withdrawable_epoch` are either both set or none of them is set.

There are 1210 [validator state profiles](https://github.com/mkalinin/eth2.0-specs/blob/validator-state-tests/tests/core/pyspec/eth2spec/test/helpers/validator_state_profiles.py#L129) generated by the Gecode solver using the described model:

| Criteria | Number of solutions |
|-|-|
| `BLS`, `slashed == False` | 108 |
| `ETH1`, `slashed == False` | 112 |
| `COMP`, `slashed == False` | 372 |
| `UNKNOWN`, `slashed == False` | 108 |
| `slashed == True` | 510 |
| | **1,210** |

In the table above we see a significant increase in possible states for validators with COMPOUNDING withdrawal credentials which proves the intuition on the potential increase of different validator states by changes introduced by Electra.

Note that the number of profiles where validator is slashed is artificially reduced to a reasonably small value. Originally, it was _3,570_ which is huge and using all of them doesn't increase the test coverage that much. This reduction is achieved by introducing the following constraint: `slashed -> shard_committee_period_lte_current_epoch`, i.e. if validator is `slashed` then it must always be advanced to the state where `current_epoch > activation_epoch + SHARD_COMMITTEE_PERIOD`.

## Test case generation

Total number of test cases is supposed to be `18 x 1,210 = 21,780`. The algorithm to generate the test cases consists of the following steps, for each _p_ in validator state profiles and for each _o_ in protocol operations:
1. Apply validator state profile to a certain validator by calling [`prepare_validator_and_beacon_state(state, p, validator_index)`](https://github.com/mkalinin/eth2.0-specs/blob/validator-state-tests/tests/core/pyspec/eth2spec/test/helpers/validator_state.py#L144)
2. Check operation conditions and apply the operation, by calling `process_operation(state, validator_index)`
3. Check the outcome of processing the operation (vary from operation to operation)
4. Convert the validator state to a validator state profile and check that it belongs to the set of valid validator states.

Current progress:
* validator state profiles are generated
* `prepare_validator_and_beacon_state` is implemented
* [WIP] Operation processors

## Appendix A

% Use this editor as a MiniZinc scratch book

enum WithdrawalCredentialType = { BLS, ETH1, COMP, UNKNOWN };
enum ComparisonOp = { LT, EQ, GT };

type ValidatorStateProfile = record(
    % Lifecycle
    bool: activation_eligibility_epoch_set,
    bool: activation_eligibility_epoch_finalized,
    bool: activation_epoch_set,
    bool: exit_epoch_set,
    bool: withdrawable_epoch_set,
    bool: slashed,
    bool: activation_epoch_gt_activation_eligibility_epoch,
    bool: withdrawable_epoch_gt_exit_epoch,
    bool: shard_committee_period_lte_current_epoch,
    ComparisonOp: activation_epoch_to_current_epoch,
    ComparisonOp: exit_epoch_to_current_epoch,
    ComparisonOp: withdrawable_epoch_to_current_epoch,

    % Balance
    bool: balance_is_zero,
    ComparisonOp: balance_to_effective_balance,
    bool: effective_balance_lte_ejection_balance,
    ComparisonOp: effective_balance_to_min_activation_balance,
    ComparisonOp: effective_balance_to_max_effective_balance,
    
    % Credential type
    WithdrawalCredentialType: withdrawal_credential_type,
    
    % Operations
    bool: has_pending_withdrawal_request,
    bool: has_pending_consolidation_request,
);


var ValidatorStateProfile: p;

% Lifecycle
constraint p.slashed -> p.exit_epoch_set;
% exit_epoch != FAR_FUTURE_EPOCH -> slashed or (activation_epoch + SHARD_COMMITTEE_PERIOD <= current_epoch)
constraint p.exit_epoch_set -> p.slashed \/ p.shard_committee_period_lte_current_epoch;
% activation_epoch + SHARD_COMMITTEE_PERIOD <= current_epoch -> activation_epoch < current_epoch
constraint p.shard_committee_period_lte_current_epoch -> p.activation_epoch_to_current_epoch = LT;
% activation_epoch <= current_epoch -> activation_epoch != FAR_FUTURE_EPOCH
constraint p.activation_epoch_to_current_epoch != GT -> p.activation_epoch_set;
% activation_epoch != FAR_FUTURE_EPOCH -> activation_eligibility_epoch <= finalized_epoch
constraint p.activation_epoch_set -> p.activation_eligibility_epoch_finalized;
% activation_eligibility_epoch <= finalized_epoch -> activation_eligibility_epoch != FAR_FUTURE_EPOCH
constraint p.activation_eligibility_epoch_finalized -> p.activation_eligibility_epoch_set;
% activation_eligibility_epoch != FAR_FUTURE_EPOCH -> activation_eligibility_epoch < activation_epoch
constraint p.activation_eligibility_epoch_set <-> p.activation_epoch_gt_activation_eligibility_epoch;
% exit_epoch != FAR_FUTURE_EPOCH <-> withdrawable_epoch != FAR_FUTURE_EPOCH
constraint p.exit_epoch_set <-> p.withdrawable_epoch_set;
% withdrawable_epoch != FAR_FUTURE_EPOCH <-> withdrawable_epoch > exit_epoch
constraint p.withdrawable_epoch_set <-> p.withdrawable_epoch_gt_exit_epoch;
% withdrawable_epoch <= current_epoch -> exit_epoch < current_epoch
constraint p.withdrawable_epoch_to_current_epoch != GT -> p.exit_epoch_to_current_epoch = LT;
% withdrawable_epoch <= current_epoch -> withdrawable_epoch != FAR_FUTURE_EPOCH
constraint p.withdrawable_epoch_to_current_epoch != GT -> p.withdrawable_epoch_set;
% exit_epoch <= current_epoch -> exit_epoch != FAR_FUTURE_EPOCH
constraint p.exit_epoch_to_current_epoch != GT -> p.exit_epoch_set;

% Balance
% balance == 0 -> balance <= effective_balance
constraint p.balance_is_zero -> p.balance_to_effective_balance != GT;
% balance == 0 and balance == effective_balance -> effective_balance <= EJECTION_BALANCE
constraint p.balance_is_zero /\ p.balance_to_effective_balance = EQ -> p.effective_balance_lte_ejection_balance;
% effective_balance <= EJECTION_BALANCE -> effective_balance < MIN_ACTIVATION_BALANCE
constraint p.effective_balance_lte_ejection_balance -> p.effective_balance_to_min_activation_balance == LT;
% effective_balance <= max_effective_balance
constraint p.effective_balance_to_max_effective_balance != GT;
% not COMP -> max_effective_balance == MIN_ACTIVATION_BALANCE
constraint p.withdrawal_credential_type != COMP -> p.effective_balance_to_min_activation_balance == p.effective_balance_to_max_effective_balance;
% COMP and effective_balance <= MIN_ACTIVATION_BALANCE -> effective_balance < max_effective_balance
constraint p.withdrawal_credential_type == COMP /\ p.effective_balance_to_min_activation_balance != GT -> p.effective_balance_to_max_effective_balance == LT;
% balance == 0 -> slashed or withdrawable_epoch >= current_epoch
constraint p.balance_is_zero -> p.slashed \/ (p.withdrawable_epoch_to_current_epoch = LT /\ (p.withdrawal_credential_type = ETH1 \/ p.withdrawal_credential_type = COMP));

% Operations
% has_pending_withdrawal_request -> COMP
constraint p.has_pending_withdrawal_request -> p.withdrawal_credential_type == COMP;
% has_pending_withdrawal_request and not slashed -> exit_epoch == FAR_FUTURE_EPOCH
constraint p.has_pending_withdrawal_request /\ not p.slashed -> not p.exit_epoch_set;
% has_pending_consolidation_request -> COMP and exit_epoch != FAR_FUTURE_EPOCH
constraint p.has_pending_consolidation_request -> p.withdrawal_credential_type == COMP /\ p.exit_epoch_set;
% has_pending_consolidation_request -> not has_pending_withdrawal_request
constraint p.has_pending_consolidation_request -> not p.has_pending_withdrawal_request;
% has_pending_withdrawal_request -> not has_pending_consolidation_request
constraint p.has_pending_withdrawal_request -> not p.has_pending_consolidation_request;

% Constraints reasonably reducing testing space
constraint p.slashed -> p.shard_committee_period_lte_current_epoch;