From ee653997beebe141303cb9fd1a5c418b259d5739 Mon Sep 17 00:00:00 2001
From: Philip Offtermatt <57488781+p-offtermatt@users.noreply.github.com>
Date: Thu, 8 Feb 2024 10:39:49 +0100
Subject: [PATCH] test: MBT: Add partial set security to model (feature branch
 version) (#1627)

* Port changes from branch to main

* Add model analysis changes to Makefile
---
 tests/mbt/model/README.md            | 4 ++++
 tests/mbt/model/ccv_boundeddrift.qnt | 5 -----
 tests/mbt/model/ccv_model.qnt        | 4 ++--
 tests/mbt/model/run_invariants.sh    | 9 ++++++++-
 4 files changed, 14 insertions(+), 8 deletions(-)

diff --git a/tests/mbt/model/README.md b/tests/mbt/model/README.md
index df994b7f84..dac613337e 100644
--- 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
index b067ca79b2..37fcd5a15b 100644
--- 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
index b3b487d113..3dc0ea1861 100644
--- 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
index afe079387e..e232bcce8b 100755
--- 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]'
\ No newline at end of file
+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))