Fix merging ccv model

tests/mbt/model/README.md

@@ -50,12 +50,15 @@ As an optional module, it can also include KeyAssignment.
 To run with key assignment, specify the step flag: `--step stepKeyAssignment`.
 
 KeyAssignment also needs some different invariants, see below.
+<<<<<<< HEAD
 
 #### 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.
+=======
+>>>>>>> main
 
 #### ccv_boundeddrift.qnt
 This state machine layer is more restricted to generate more interesting traces:

tests/mbt/model/ccv.qnt

@@ -89,12 +89,6 @@ module ccv_types {
             // Stores VscPackets which have been sent but where the provider has *not received a response yet*.
             sentVscPacketsToConsumer: Chain -> List[VscPacket],
 
-            // stores whether, in this block, the validator set has changed.
-            // this is needed because the validator set might be considered to have changed, even though
-            // it is still technically identical at our level of abstraction, e.g. a validator power change on the provider
-            // might leave the validator set the same because a delegation and undelegation cancel each other out.
-            providerValidatorSetChangedInThisBlock: bool,
-
             // stores for which consumer chains, in this epoch, the validator set is considered to have changed and we thus need to send a VscPacket to the consumer chains.
             consumersWithPowerChangesInThisEpoch: Set[Chain],
 
@@ -147,7 +141,6 @@ module ccv_types {
             outstandingPacketsToConsumer: Map(),
             receivedMaturations: Set(),
             sentVscPacketsToConsumer: Map(),
-            providerValidatorSetChangedInThisBlock: false,
             consumersWithPowerChangesInThisEpoch: Set(),
             consumerStatus: Map(),
             runningVscId: 0,
@@ -156,9 +149,9 @@ module ccv_types {
             consumerAddrToValidator: Map(),
             consumerAddrsToPrune: Map(),
             keyAssignmentsForVSCPackets: Map(),
-            consumersWithAddrAssignmentChangesInThisEpoch: Set(),
             optedInVals: Map(),
             topNByConsumer: Map(),
+            consumersWithAddrAssignmentChangesInThisEpoch: Set()
         }
 
 
@@ -510,7 +503,7 @@ module ccv {
             consumersToStop,
             timedOutConsumers
         )
-        val providerStateAfterConsumerAdvancement = res._1.with("providerValidatorSetChangedInThisBlock", false)
+        val providerStateAfterConsumerAdvancement = res._1
         val err = res._2
 
         val consumerAdditions = consumersToStart.map(consumer => consumer.chain)

tests/mbt/model/ccv_boundeddrift.qnt

@@ -104,6 +104,12 @@ module ccv_boundeddrift {
                 nondet timeAdvancement = possibleAdvancements.oneOf()
                 EndAndBeginBlockForConsumer(chain, timeAdvancement),
             }
+<<<<<<< HEAD
+    }
+
+    action stepBoundedDriftKeyAssignment = any {
+        stepBoundedDrift,
+        nondetKeyAssignment,
     }
 
     action stepBoundedDriftKeyAndPSS = any {
@@ -113,6 +119,24 @@ module ccv_boundeddrift {
         nondetKeyAssignment,
         StepOptIn,
         StepOptOut,
+=======
+        },
+
+        // advance a block for the provider
+        val maxAdv = findMaxTimeAdvancement(GetChainState(Ccvt::PROVIDER_CHAIN), GetOtherChainStates(Ccvt::PROVIDER_CHAIN), maxDrift)
+        val possibleAdvancements = timeAdvancements.filter(t => t <= maxAdv)
+        all {
+            possibleAdvancements.size() > 0, // ensure there is a possible advancement, otherwise this action does not make sense
+            // advance a block for the provider
+            val consumerStatus = currentState.providerState.consumerStatus
+            nondet consumersToStart = oneOf(nonConsumers.powerset())
+            // make it so we stop consumers only with small likelihood:
+            nondet stopConsumersRand = oneOf(1.to(100))
+            nondet consumersToStop = if (stopConsumersRand <= consumerStopChance) oneOf(runningConsumers.powerset()) else Set()
+            nondet timeAdvancement = oneOf(possibleAdvancements)
+            EndAndBeginBlockForProvider(timeAdvancement, consumersToStart, consumersToStop),
+        }
+>>>>>>> main
     }
 
     action stepBoundedDriftKeyAssignment = any {

tests/mbt/model/ccv_model.qnt

@@ -109,7 +109,7 @@ module ccv_model {
         val consumerStates = ConsumerChains.mapBy(chain => GetEmptyConsumerState)
         val providerStateWithConsumers = providerState.with(
             "consumerStatus", 
-            ConsumerChains.mapBy(chain =>  NOT_CONSUMER)
+            ConsumerChains.mapBy(chain => NOT_CONSUMER)
         ).with(
             "outstandingPacketsToConsumer", 
             ConsumerChains.mapBy(chain => List())
@@ -255,7 +255,7 @@ module ccv_model {
     // As a a `Run`, it is only used in tests, not during simulation or verification.
     run EndProviderEpoch(
         timeAdvancement: Time,
-        consumersToStart: Set[ConsumerAdditionMsg],
+        consumersToStart: Set[Chain],
         consumersToStop: Set[Chain]
     ): bool =
         epochLength.reps(
@@ -270,7 +270,6 @@ module ccv_model {
     // ==================
     // UTILITY FUNCTIONS
     // ==================
-
     pure def oldest(packets: Set[VscPacket]): VscPacket =
         val newestPossiblePacket: VscPacket = {
             id: 0,
@@ -740,11 +739,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 currentState.providerState.providerValidatorSetChangedInThisBlock
+        ValUpdatePrecondition and CurrentBlockEndsEpoch
             implies
         val providerValSetInCurBlock = providerValidatorHistory.head()
         // ... for each consumer that is running then ...
-        runningConsumers.forall(
+        currentState.providerState.consumersWithPowerChangesInThisEpoch.forall(
             // ...the validator set under key assignment is in a sent packet...
             val providerState = currentState.providerState
             consumer => providerState.sentVscPacketsToConsumer.get(consumer).toSet().exists(