test: MBT: Add partial set security to model (feature branch version) (…

…#1627)

* Port changes from branch to main

* Add model analysis changes to Makefile

Makefile

@@ -131,7 +131,9 @@ test-trace:
 verify-models:
 	quint test tests/mbt/model/ccv_test.qnt;\
 	quint test tests/mbt/model/ccv_model.qnt;\
-	quint run --invariant "all{ValidatorUpdatesArePropagatedInv,ValidatorSetHasExistedInv,SameVscPacketsInv,MatureOnTimeInv,EventuallyMatureOnProviderInv}" tests/mbt/model/ccv_model.qnt --max-steps 200 --max-samples 200
+	quint test tests/mbt/model/ccv_pss_test.qnt;\
+	quint run --invariant "all{ValidatorUpdatesArePropagatedInv,ValidatorSetHasExistedInv,SameVscPacketsInv,MatureOnTimeInv,EventuallyMatureOnProviderInv}" tests/mbt/model/ccv_model.qnt --max-steps 200 --max-samples 200;\
+	quint run --invariant "all{ValidatorUpdatesArePropagatedKeyAssignmentInv,ValidatorSetHasExistedKeyAssignmentInv,SameVscPacketsKeyAssignmentInv,MatureOnTimeInv,EventuallyMatureOnProviderInv,KeyAssignmentRulesInv}" tests/mbt/model/ccv_model.qnt --step stepKeyAssignment --max-steps 200 --max-samples 200
 
 
 

tests/mbt/model/README.md

@@ -31,16 +31,31 @@ 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
 
 There are 3 different "state machine layers" that can be put on top of the core logic.
+Some layers include extra logic, need other invariants, ...
 
 #### ccv_model.qnt
 This is the most general state machine layer. It allows the most behaviour,
 in particular it allows abitrary clock drift between chains, it allows starting and
 stopping consumer chains during runtime, etc.
 This layer is most useful for model checking, because it encompasses the most behaviour.
+As an optional module, it can also include KeyAssignment.
+
+##### KeyAssignment
+
+To run with key assignment, specify the step flag: `--step stepKeyAssignment`.
+
+KeyAssignment also needs some different invariants, see below.
+
+#### Partial Set Security
+
+To run with Partial Set Security, specify the step flag `--step stepBoundedDriftKeyAndPSS`.
+This runs both PSS and Key Assignment.
+It also requires running with `ccv_boundeddrift.qnt`, see below.
 
 #### ccv_boundeddrift.qnt
 This state machine layer is more restricted to generate more interesting traces:
@@ -66,10 +81,7 @@ traces are not very useful for testing.
 
 To run unit tests, run 
 ```
-quint test ccv_test.qnt
-```
-and 
-```
+quint test ccv_test.qnt;
 quint test ccv_model.qnt
 ```
 
@@ -94,6 +106,13 @@ with a timestamp >= t + UnbondingPeriod on that consumer.
 - [X] EventuallyMatureOnProviderInv: If we send a VscPacket, this is eventually responded to by all consumers
 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: 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
+
+
 Invariants can also be model-checked by Apalache, using this command:
 ```
 quint verify --invariant ValidatorUpdatesArePropagatedInv,ValidatorSetHasExistedInv,SameVscPacketsInv,MatureOnTimeInv,EventuallyMatureOnProviderInv \
@@ -113,4 +132,10 @@ The available sanity checks are:
 - CanStopConsumer
 - CanTimeoutConsumer
 - CanSendVscPackets
-- CanSendVscMaturedPackets
+- CanSendVscMaturedPackets
+- CanAssignConsumerKey (only with `--step stepKeyAssignment`)
+- CanHaveConsumerAddresses (only with `--step stepKeyAssignment`)
+- CanOptIn (only with `--step stepBoundedDriftKeyAndPSS` on `ccv_boundeddrift.qnt`)
+- CanOptOut (only with `--step stepBoundedDriftKeyAndPSS` on `ccv_boundeddrift.qnt`)
+- CanFailOptOut (only with `--step stepBoundedDriftKeyAndPSS` on `ccv_boundeddrift.qnt`)
+- CanHaveOptIn (only with `--step stepBoundedDriftKeyAndPSS` on `ccv_boundeddrift.qnt`)