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

@@ -140,8 +140,11 @@ test-trace:
 # Note: this is *not* using the Quint models to test the system,
 # this tests/verifies the Quint models *themselves*.
 verify-models:
-	cd tests/mbt/model;\
-	../run_invariants.sh
+	quint test tests/mbt/model/ccv_test.qnt;\
+	quint test tests/mbt/model/ccv_model.qnt;\
+	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

@@ -51,6 +51,12 @@ 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:
 * It never allows consumer chains to drift more than `MaxDrift` time apart from each other.
@@ -75,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
 ```
 
@@ -131,4 +134,8 @@ The available sanity checks are:
 - CanSendVscPackets
 - CanSendVscMaturedPackets
 - CanAssignConsumerKey (only with `--step stepKeyAssignment`)
-- CanHaveConsumerAddresses (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`)

tests/mbt/model/ccv.qnt

@@ -89,6 +89,12 @@ 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],
 
@@ -120,7 +126,18 @@ module ccv_types {
             consumerAddrsToPrune: Chain -> VscId -> List[ConsumerAddr],
 
             // For every sent VSCPacket, stores the key assignments that were applied to send it.
-            keyAssignmentsForVSCPackets: VscId -> (Chain -> (Node -> ConsumerAddr))
+            keyAssignmentsForVSCPackets: VscId -> (Chain -> (Node -> ConsumerAddr)),
+
+            // For each consumer chain,
+            // stores the set of validators that are opted into running the chain.
+            optedInVals: Chain -> Set[Node],
+
+            // for each consumer, stores the top N for that consumer.
+            // The top N% of the validator set by voting power
+            // is obliged to run a topN chain.
+            // If the chain is a pure opt-in chain (where noone is forced to run it),
+            // this is 0.
+            topNByConsumer: Chain -> int,
         }
 
     // utility function: returns a provider state that is initialized minimally.
@@ -130,6 +147,7 @@ module ccv_types {
             outstandingPacketsToConsumer: Map(),
             receivedMaturations: Set(),
             sentVscPacketsToConsumer: Map(),
+            providerValidatorSetChangedInThisBlock: false,
             consumersWithPowerChangesInThisEpoch: Set(),
             consumerStatus: Map(),
             runningVscId: 0,
@@ -138,7 +156,9 @@ module ccv_types {
             consumerAddrToValidator: Map(),
             consumerAddrsToPrune: Map(),
             keyAssignmentsForVSCPackets: Map(),
-            consumersWithAddrAssignmentChangesInThisEpoch: Set()
+            consumersWithAddrAssignmentChangesInThisEpoch: Set(),
+            optedInVals: Map(),
+            topNByConsumer: Map(),
         }
 
 
@@ -226,6 +246,33 @@ module ccv_types {
     // given as a pure val so that we can switch cases based on
     // whether a chain is the provider or not
     pure val PROVIDER_CHAIN = "provider"
+
+    // A record that keeps the information needed to add a new consumer.
+    // In particular, holds:
+    // the chain name/identifier,
+    // and the top N factor for the chain.
+    type ConsumerAdditionMsg = {
+        chain: Chain,
+        topN: int
+    }
+
+    // Creates a new ConsumerAdditionMsg with a given top N.
+    pure def NewTopNConsumer(chain: Chain, topN: int): ConsumerAdditionMsg = {
+        {
+            chain: chain,
+            topN: topN
+        }
+    }
+
+    // Creates a new ConsumerAdditionMsg with topN = 0.
+    pure def NewOptInConsumer(chain: Chain): ConsumerAdditionMsg = {
+        NewTopNConsumer(chain, 0)
+    }
+
+    // Creates a new ConsumerAdditionMsg with top N = 100%.
+    pure def NewFullConsumer(chain: Chain): ConsumerAdditionMsg = {
+        NewTopNConsumer(chain, 100)
+    }
 }
 
 module ccv {
@@ -246,6 +293,7 @@ module ccv {
     import Time.* from "./libraries/Time"
     import extraSpells.* from "./libraries/extraSpells"
     import ccv_types.*
+    import ccv_pss.* from "./ccv_pss"
     import ccv_utils.* from "./ccv_utils"
 
 
@@ -417,41 +465,26 @@ module ccv {
         // i.e. the timestamp for the next block is oldTimestamp + timeAdvancement
         timeAdvancement: Time,
         // a set of consumers that were not consumers before, but should be set to running now.
-        consumersToStart: Set[Chain],
+        consumersToStart: Set[ConsumerAdditionMsg],
         // a set of consumers that were running before, but should be set to stopped now.
         // This argument only needs to contain "voluntary" stops -
         // forced stops, e.g. because a consumer timed out,
         // will be added automatically. 
         consumersToStop: Set[Chain]): Result = {
         val currentProviderState = currentState.providerState
+        val curValSet = currentProviderState.chainState.currentValidatorSet
 
         // check for vsc timeouts
         val timedOutConsumers = getRunningConsumers(currentProviderState).filter(
             consumer => 
             val res = TimeoutDueToVscTimeout(currentState, consumer, VscTimeout)
             res._1
         )
-
-        // for each consumer chain, apply the key assignment to the current validator set
-        val currentValSets = ConsumerChains.mapBy(
-            (consumer) => 
-            currentProviderState.applyKeyAssignmentToValSet(
-                consumer, 
-                currentProviderState.chainState.currentValidatorSet
-            )
-        )
-        // store the current validator set with the key assignments applied in the history
-        val newKeyAssignedValSetHistory = currentValSets.keys().mapBy(
-            (consumer) => 
-            currentProviderState.keyAssignedValSetHistory
-                .getOrElse(consumer, List()) // get the existing history (empty list if no history yet)
-                .prepend(currentValSets.get(consumer)) // prepend the current validator set with key assignments applied
-        )
 
         // run the shared core chainState logic
         val newChainState = currentProviderState.chainState.endAndBeginBlockShared(timeAdvancement)
         val providerStateAfterTimeAdvancement = 
-            {...currentProviderState, chainState: newChainState, keyAssignedValSetHistory: newKeyAssignedValSetHistory}
+            {...currentProviderState, chainState: newChainState}
         val tmpState = currentState.with(
             "providerState", providerStateAfterTimeAdvancement
         )
@@ -472,41 +505,62 @@ module ccv {
 
 
         // start/stop chains
-        val res = providerStateAfterSending.consumerStatus.StartStopConsumers(
+        val res = providerStateAfterSending.StartStopConsumers(
             consumersToStart,
             consumersToStop,
             timedOutConsumers
         )
-        val newConsumerStatus = res._1
+        val providerStateAfterConsumerAdvancement = res._1.with("providerValidatorSetChangedInThisBlock", false)
         val err = res._2
-        val providerStateAfterConsumerAdvancement = providerStateAfterSending.with(
-            "consumerStatus", newConsumerStatus
-        )
+
+        val consumerAdditions = consumersToStart.map(consumer => consumer.chain)
+
+        // for each running consumer chain, opt in validators that are in the top N
+        val providerStateAfterPSS = providerStateAfterConsumerAdvancement.endBlockPSS()
 
         if (err != "") {
             Err(err)
         } else {
-            // for each consumer we just set to running, set its initial validator set to be the current one on the provider...
-            val valSet = providerStateAfterConsumerAdvancement.chainState.currentValidatorSet
+            // for each consumer chain, apply the key assignment to the current validator set
+            val currentValSets = getRunningConsumers(providerStateAfterPSS).mapBy(
+                (consumer) => 
+                providerStateAfterPSS.applyKeyAssignmentToValSet(
+                    consumer,
+                    // get the validator set after partial set security has been applied
+                    GetPSSValidatorSet(providerStateAfterPSS, curValSet, consumer)
+                )
+            )
+
+            // store the current validator set with the key assignments applied in the history
+            val newKeyAssignedValSetHistory = currentValSets.keys().mapBy(
+                (consumer) => 
+                providerStateAfterPSS.keyAssignedValSetHistory
+                    .getOrElse(consumer, List()) // get the existing history (empty list if no history yet)
+                    .prepend(currentValSets.get(consumer)) // prepend the current validator set with key assignments applied
+            )
+
+            val providerStateAfterStoringValSets = providerStateAfterPSS.with(
+                "keyAssignedValSetHistory", newKeyAssignedValSetHistory
+            )
+
             val newConsumerStateMap =
                 tmpState.consumerStates.keys().mapBy(
                     (consumer) => 
-                    if (consumersToStart.contains(consumer)) {
-                        // ...modified by the key assignments for the consumer
-                        val consValSet = applyKeyAssignmentToValSet(providerStateAfterConsumerAdvancement, consumer, valSet)
+                    if (consumerAdditions.contains(consumer)) {
                         val currentConsumerState: ConsumerState = tmpState.consumerStates.get(consumer)
+                        // correctly set the state for the new consumer
                         val newConsumerState: ConsumerState = currentConsumerState.with(
                             "chainState", currentConsumerState.chainState.with(
-                                "currentValidatorSet", consValSet
+                                "currentValidatorSet", currentValSets.get(consumer)
                             ).with(
                                 "votingPowerHistory",
-                                List(consValSet)
+                                List(currentValSets.get(consumer))
                             ).with(
                                 "lastTimestamp", 
-                                providerStateAfterConsumerAdvancement.chainState.lastTimestamp
+                                providerStateAfterStoringValSets.chainState.lastTimestamp
                             ).with(
                                 "runningTimestamp", 
-                                providerStateAfterConsumerAdvancement.chainState.runningTimestamp
+                                providerStateAfterStoringValSets.chainState.runningTimestamp
                             )
                         )
                         newConsumerState
@@ -515,7 +569,7 @@ module ccv {
                     }
                 )
             val newState = tmpState.with(
-                "providerState", providerStateAfterConsumerAdvancement
+                "providerState", providerStateAfterStoringValSets
             ).with(
                 "consumerStates", newConsumerStateMap
             )

tests/mbt/model/ccv_boundeddrift.qnt

@@ -5,6 +5,7 @@ module ccv_boundeddrift {
     import ccv from "ccv"
     import Time.* from "./libraries/Time"
     import extraSpells.* from "./libraries/extraSpells"
+    import ccv_pss_model.* from "ccv_pss_model"
 
 
     // The boundeddrift module has its own step function.
@@ -60,34 +61,60 @@ module ccv_boundeddrift {
         stepCommon, // allow actions that do not influence time
 
         // advance a block for a consumer
-        all {
-            runningConsumers.size() > 0, // ensure there is a running consumer, otherwise this action does not make sense
-            nondet chain = runningConsumers.oneOf()
-            val maxAdv = findMaxTimeAdvancement(GetChainState(chain), GetOtherChainStates(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
-                nondet timeAdvancement = possibleAdvancements.oneOf()
-                EndAndBeginBlockForConsumer(chain, timeAdvancement),
-            }
-        },
+        stepBoundedDriftConsumer,
 
         // advance a block for the provider
+        stepBoundedDriftProvider
+    }
+
+    action stepBoundedDriftProvider: bool = {
+        stepBoundedDriftProvider_helper(allFullConsumers)
+    }
+
+    action stepBoundedDriftProviderPSS: bool = {
+        stepBoundedDriftProvider_helper(variousPossibleTopN)
+    }
+
+    // As an argument, takes a function that, when invoked, gives a top N value to use for a new consumer chain.
+    action stepBoundedDriftProvider_helper(topNOracle: Set[int]): bool = {
         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())
+            nondet topN = oneOf(topNOracle)
+            nondet consumerAdditions = consumersToStart.map(c => Ccvt::NewTopNConsumer(c, topN))
             // 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),
+            EndAndBeginBlockForProvider(timeAdvancement, consumerAdditions, consumersToStop),
         }
     }
 
+    action stepBoundedDriftConsumer = all {
+        runningConsumers.size() > 0, // ensure there is a running consumer, otherwise this action does not make sense
+            nondet chain = runningConsumers.oneOf()
+            val maxAdv = findMaxTimeAdvancement(GetChainState(chain), GetOtherChainStates(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
+                nondet timeAdvancement = possibleAdvancements.oneOf()
+                EndAndBeginBlockForConsumer(chain, timeAdvancement),
+            }
+    }
+
+    action stepBoundedDriftKeyAndPSS = any {
+        stepCommon,
+        stepBoundedDriftProviderPSS,
+        stepBoundedDriftConsumer,
+        nondetKeyAssignment,
+        StepOptIn,
+        StepOptOut,
+    }
+
     action stepBoundedDriftKeyAssignment = any {
         stepBoundedDrift,
         nondetKeyAssignment,