Merge branch 'ph/mbt-keyassignment' into ph/mbt-pss

tests/mbt/driver/mbt_test.go

@@ -124,7 +124,7 @@ func RunItfTrace(t *testing.T, path string) {
 	// generate keys that can be assigned on consumers, according to the ConsumerAddresses in the trace
 	consumerAddressesExpr := params["ConsumerAddresses"].Value.(itf.ListExprType)
 
-	consumerPrivVals, err := integration.CreateSigners(len(consumerAddressesExpr))
+	_, _, consumerPrivVals, err := integration.CreateValidators(len(consumerAddressesExpr))
 	require.NoError(t, err, "Error creating consumer signers")
 
 	consumerAddrNamesToPrivVals := make(map[string]cmttypes.PrivValidator, len(consumerAddressesExpr))

tests/mbt/model/README.md

@@ -31,6 +31,7 @@ All the logic in EndBlock/BeginBlock happens here, like updating the validator s
 * `EndAndBeginBlockForConsumer(chain: Chain, timeAdvancement: Time)`: On the consumer `chain`, ends the current block, and begins a new one. Again, all the logic in EndBlock/BeginBlock happens here, like validator set change maturations.
 * `DeliverVscPacket(receiver: Chain)`: Delivers a pending VSCPacket from the provider to the consumer `receiver`.
 * `DeliverVscMaturedPacket(receiver: Chain)`: Delivers a pending VSCMaturedPacket from the consumer `receiver` to the provider.
+* `KeyAssignment(chain: Chain, validator: Node, consumerAddr: ConsumerAddr)` (only when running with `--step stepKeyAssignment`): Assigns the `consumerAddr` to the `validator` on the `chain`. Note that we use "key" and "consumerAddr" pretty much interchangeably, as the model makes no differentiation between private keys, public keys, addresses, etc, as it doesn't model the cryptography.
 
 ### State machines
 
@@ -48,10 +49,6 @@ As an optional module, it can also include KeyAssignment.
 
 To run with key assignment, specify the step flag: `--step stepKeyAssignment`.
 
-Key assignment allows an additional action:
-
-* `KeyAssignment(chain: Chain, validator: Node, consumerAddr: ConsumerAddr)`: Assigns the `consumerAddr` to the `validator` on the `chain`. Note that we use "key" and "consumerAddr" pretty much interchangeably, as the model makes no differentiation between private keys, public keys, addresses, etc, as it doesn't model the cryptography.
-
 KeyAssignment also needs some different invariants, see below.
 
 #### ccv_boundeddrift.qnt
@@ -107,8 +104,8 @@ with a timestamp >= t + UnbondingPeriod on that consumer.
 that were running at the time the packet was sent (and are still running).
 
 Invariants only relevant when running with key assignment (`--step stepKeyAssignment`):
-- [X] ValidatorSetHasExistedKeyAssignmentInv: Replaces ValidatorSetHasExistedInv. Validator sets are checked for equality under key assignment when checking whether they have existed.
-- [X] SameVscPacketsKeyAssignmentInv: Replaces SameVscPacketsInv. VscPackets are checked for equality under key assignment when ensuring consumers receive the same ones.
+- [X] ValidatorSetHasExistedKeyAssignmentInv: Should replace ValidatorSetHasExistedInv when running with `--step stepKeyAssignment`. Validator sets are checked for equality under key assignment when checking whether they have existed.
+- [X] SameVscPacketsKeyAssignmentInv: Should replace SameVscPacketsInv when running with `--step stepKeyAssignment`. VscPackets are checked for equality under key assignment when ensuring consumers receive the same ones.
 - [X] KeyAssignmentRulesInv: Ensures the rules of key assignment are never violated. The two rules relevant for the model are: 1) validator A cannot assign consumer key K to consumer chain X if there is already a validator B (B!=A)
 using K on the provider, and 2) validator A cannot assign consumer key K to consumer chain X if there is already a validator B using K on X