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

…#1627) * Port changes from branch to main * Add model analysis changes to Makefile
cosmos · Mar 12, 2024 · ee65399 · ee65399
1 parent 6e2618b
commit ee65399
Show file tree

Hide file tree

Showing 4 changed files with 14 additions and 8 deletions.
diff --git a/tests/mbt/model/README.md b/tests/mbt/model/README.md
@@ -138,4 +138,8 @@ The available sanity checks are:
 - 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`)
+<<<<<<< HEAD
 - CanHaveOptIn (only with `--step stepBoundedDriftKeyAndPSS` on `ccv_boundeddrift.qnt`)
+=======
+- CanHaveOptIn (only with `--step stepBoundedDriftKeyAndPSS` on `ccv_boundeddrift.qnt`)
+>>>>>>> 6e075652 (test: MBT: Add partial set security to model (feature branch version) (#1627))
diff --git a/tests/mbt/model/ccv_boundeddrift.qnt b/tests/mbt/model/ccv_boundeddrift.qnt
@@ -115,11 +115,6 @@ module ccv_boundeddrift {
         StepOptOut,
     }
 
-    action stepBoundedDriftKeyAssignment = any {
-        stepBoundedDrift,
-        nondetKeyAssignment,
-    }
-
     // INVARIANT
     // The maxDrift between chains is never exceeded.
     // This *should* be ensured by the step function.

diff --git a/tests/mbt/model/ccv_model.qnt b/tests/mbt/model/ccv_model.qnt
@@ -740,11 +740,11 @@ module ccv_model {
     // and the key assignment of each validator should be applied in that VSCPacket.
     val ValidatorUpdatesArePropagatedKeyAssignmentInv = 
         // when the provider has just entered a validator set into a block...
-        ValUpdatePrecondition and CurrentBlockEndsEpoch
+        ValUpdatePrecondition and currentState.providerState.providerValidatorSetChangedInThisBlock
             implies
         val providerValSetInCurBlock = providerValidatorHistory.head()
         // ... for each consumer that is running then ...
-        currentState.providerState.consumersWithPowerChangesInThisEpoch.forall(
+        runningConsumers.forall(
             // ...the validator set under key assignment is in a sent packet...
             val providerState = currentState.providerState
             consumer => providerState.sentVscPacketsToConsumer.get(consumer).toSet().exists(

diff --git a/tests/mbt/model/run_invariants.sh b/tests/mbt/model/run_invariants.sh
@@ -1,5 +1,6 @@
 #!/bin/bash
 
+<<<<<<< HEAD
 # to stop on any errors
 set -e
 
@@ -38,4 +39,10 @@ run_invariant "CanSendVscPackets" "" '[violation]'
 run_invariant "CanSendVscMaturedPackets" "" '[violation]'
 run_invariant "CanAssignConsumerKey" "stepKeyAssignment" '[violation]'
 run_invariant "CanHaveConsumerAddresses" "stepKeyAssignment" '[violation]'
-run_invariant "CanReceiveMaturations" "stepKeyAssignment" '[violation]'
+run_invariant "CanReceiveMaturations" "stepKeyAssignment" '[violation]'
+=======
+quint test ccv_model.qnt
+quint test ccv_test.qnt
+quint run --invariant "all{ValidatorUpdatesArePropagatedInv,ValidatorSetHasExistedInv,SameVscPacketsInv,MatureOnTimeInv,EventuallyMatureOnProviderInv}" ccv_model.qnt --max-steps 200 --max-samples 200
+quint run --invariant "all{ValidatorUpdatesArePropagatedKeyAssignmentInv,ValidatorSetHasExistedKeyAssignmentInv,SameVscPacketsKeyAssignmentInv,MatureOnTimeInv,EventuallyMatureOnProviderInv,KeyAssignmentRulesInv}" ccv_model.qnt --step stepKeyAssignment --max-steps 200 --max-samples 200
+>>>>>>> 6e075652 (test: MBT: Add partial set security to model (feature branch version) (#1627))