EPIC: Expand MBT functionality

[p-offtermatt]

Problem

We want to expand the MBT model to cover more functionality.

Closing criteria

We are running MBT for at least the must-have features.

Problem details

For each of the features listed below, several main tasks have to be done:

1. Adjust the Quint model to include the feature
2. Add tests in Quint to test the feature
3. Make sure that the generated traces use the feature in non-trivial ways (or add new generation methods, i.e. invariants, that do)
4. Expand the driver to understand/utilize the new feature

Task list

Must have

Preview Give feedback

1. MBT: Add key assignment #1529
   S: Productivity scope: MBT scope: testing +3
   
2. MBT: Add slashing #1531
   S: Productivity scope: MBT scope: testing +3
   

Nice to have

Preview Give feedback

1. MBT: Add soft opt-out #1532
   S: Productivity scope: MBT scope: testing +3
   
2. MBT: Add reward distribution #1530
   S: Productivity scope: MBT scope: testing +3
   

Other nice-to-have tasks related to MBT

Preview Give feedback

1. difftest core: model and test Redelegate operations #318
   S: Productivity ccv-core scope: MBT scope: testing +4
2. difftest core: model and test Unjail operations #319
   S: Productivity ccv-core scope: MBT scope: testing +4
3. difftest core: Amend diff model with throttle changes once spec has been updated #534
   S: Productivity ccv-core scope: MBT scope: testing spec +5
4. diff-test core: improve tests to use cryptolib #691
   S: Productivity scope: MBT type: feature-request +3
5. test soft opt-out with diff testing #1044
   S: Productivity scope: testing +2
6. Improve coverage around starting/stopping/restarting #306
   S: Productivity question scope: testing +3
7. refactor difftest setup #1131
   S: Productivity scope: testing +2