Merge branch 'main' into ph/mbt-pss

.changelog/v4.0.0/summary.md

@@ -0,0 +1 @@
+*January 22, 2024*

CHANGELOG.md

@@ -1,5 +1,59 @@
 # CHANGELOG
 
+## v4.0.0
+
+*January 22, 2024*
+
+### API BREAKING
+
+- [Consumer](x/ccv/consumer)
+  - Fix a bug in consmer genesis file transform CLI command.
+    ([\#1458](https://github.com/cosmos/interchain-security/pull/1458))
+
+### BUG FIXES
+
+- General
+  - Fix a bug in consmer genesis file transform CLI command.
+    ([\#1458](https://github.com/cosmos/interchain-security/pull/1458))
+  - Improve validation of IBC packet data and provider messages. Also,
+    enable the provider to validate consumer packets before handling them.
+    ([\#1460](https://github.com/cosmos/interchain-security/pull/1460))
+- [Consumer](x/ccv/consumer)
+  - Avoid jailing validators immediately once they can no longer opt-out from
+    validating consumer chains.
+    ([\#1549](https://github.com/cosmos/interchain-security/pull/1549))
+  - Fix the validation of VSCPackets to not fail due to marshaling to string using Bech32.
+    ([\#1570](https://github.com/cosmos/interchain-security/pull/1570))
+
+### DEPENDENCIES
+
+- Bump Golang to v1.21 
+  ([\#1557](https://github.com/cosmos/interchain-security/pull/1557))
+- Bump [cosmos-sdk](https://github.com/cosmos/cosmos-sdk) to
+  [v0.47.7](https://github.com/cosmos/cosmos-sdk/releases/tag/v0.47.7).
+  ([\#1558](https://github.com/cosmos/interchain-security/pull/1558))
+- Bump [CometBFT](https://github.com/cometbft/cometbft) to
+  [v0.37.4](https://github.com/cometbft/cometbft/releases/tag/v0.37.4).
+  ([\#1558](https://github.com/cosmos/interchain-security/pull/1558))
+
+### FEATURES
+
+- [Provider](x/ccv/provider)
+  - Add the provider-side changes for jail throttling with retries (cf. ADR 008).
+    ([\#1321](https://github.com/cosmos/interchain-security/pull/1321))
+
+### STATE BREAKING
+
+- [Consumer](x/ccv/consumer)
+  - Avoid jailing validators immediately once they can no longer opt-out from
+    validating consumer chains.
+    ([\#1549](https://github.com/cosmos/interchain-security/pull/1549))
+  - Fix the validation of VSCPackets to not fail due to marshaling to string using Bech32.
+    ([\#1570](https://github.com/cosmos/interchain-security/pull/1570))
+- [Provider](x/ccv/provider)
+  - Add the provider-side changes for jail throttling with retries (cf. ADR 008).
+    ([\#1321](https://github.com/cosmos/interchain-security/pull/1321))
+
 ## v3.3.0
 
 *January 5, 2024*

Makefile

@@ -131,7 +131,8 @@ 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 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/e2e/actions_sovereign_chain.go

@@ -70,7 +70,7 @@ func (tr TestConfig) startSovereignChain(
 
 	isConsumer := chainConfig.BinaryName != "interchain-security-pd"
 	testScriptPath := target.GetTestScriptPath(isConsumer, "start-sovereign.sh")
-	cmd := target.ExecCommand("/bin/bash", testScriptPath, string(vals),
+	cmd := target.ExecCommand("/bin/bash", testScriptPath, chainConfig.BinaryName, string(vals),
 		string(chainConfig.ChainId), chainConfig.IpPrefix, genesisChanges,
 		tr.tendermintConfigOverride)
 

tests/mbt/model/ccv.qnt

@@ -712,6 +712,8 @@ module ccv {
     import extraSpells.* from "./libraries/extraSpells"
     import ccv_types.*
     import ccv_pss.* from "./ccv_pss"
+    import ccv_utils.* from "./ccv_utils"
+
 
     // ===================
     // PROTOCOL PARAMETERS

tests/mbt/model/ccv_boundeddrift.qnt

@@ -1,6 +1,7 @@
 module ccv_boundeddrift {
     import ccv_model.* from "ccv_model"
     import ccv_types as Ccvt from "ccv"
+    import ccv_utils.* from "ccv_utils"
     import ccv from "ccv"
     import Time.* from "./libraries/Time"
     import extraSpells.* from "./libraries/extraSpells"
@@ -80,8 +81,8 @@ module ccv_boundeddrift {
             val consumerStatus = currentState.providerState.consumerStatus
             nondet consumersToStart = oneOf(nonConsumers.powerset())
             // make it so we stop consumers only with small likelihood:
-            nondet stopConsumers = oneOf(1.to(100))
-            nondet consumersToStop = if (stopConsumers <= consumerStopChance) oneOf(runningConsumers.powerset()) else Set()
+            nondet stopConsumersRand = oneOf(1.to(100))
+            nondet consumersToStop = if (stopConsumersRand <= consumerStopChance) oneOf(runningConsumers.powerset()) else Set()
             nondet timeAdvancement = oneOf(possibleAdvancements)
             EndAndBeginBlockForProvider(timeAdvancement, consumersToStart, consumersToStop),
         }

tests/mbt/model/ccv_model.qnt

@@ -4,6 +4,7 @@ module ccv_model {
     import ccv_types.* from "./ccv"
     import Time.* from "./libraries/Time"
     import extraSpells.* from "./libraries/extraSpells"
+    import ccv_utils.* from "./ccv_utils"
 
     pure val consumerChainList = List("consumer1", "consumer2", "consumer3")
     pure val consumerChains = consumerChainList.toSet()
@@ -310,9 +311,11 @@ module ccv_model {
     // Every validator set on any consumer chain MUST either be or have been 
     // a validator set on the provider chain.
     val ValidatorSetHasExistedInv =
-        runningConsumers.forall(chain =>
+        runningConsumers.forall(chain => // for all running consumers
             currentState.consumerStates.get(chain).chainState.votingPowerHistory.toSet().forall(
+                // go through all its historical and current validator sets
                 validatorSet => providerValidatorHistory.toSet().contains(validatorSet)
+                // and check that they are also historical or current validator sets on the provider
             )
         )
 
@@ -330,10 +333,6 @@ module ccv_model {
             consumer => currentState.providerState.sentVscPacketsToConsumer.get(consumer).toSet().exists(
                 packet => packet.validatorSet == providerValSetInCurBlock
             )
-            // or the consumer was just started, which we detect by the consumer having a timestamp of 0
-            // and the consumer having the validator set that was just sent in the block
-            or 
-            (currentState.consumerStates.get(consumer).chainState.lastTimestamp == 0 and currentState.consumerStates.get(consumer).chainState.currentValidatorSet == providerValSetInCurBlock)
         )
 
     // Every consumer chain receives the same sequence of 
@@ -380,8 +379,11 @@ module ccv_model {
     val lastTimeAdvancement = trace[trace.length()-1].timeAdvancement
     val lastBlockTime = currentState.consumerStates.get(ConsumerWithPotentialMaturations).chainState.lastTimestamp - lastTimeAdvancement
     val MatureOnTimeInv =
+        // if a consumer ended a block
         MaturationPrecondition
         implies
+        // then all matured packets need to have been processed and removed from the packets
+        // waiting to mature
         currentState.consumerStates.get(ConsumerWithPotentialMaturations).maturationTimes.toSet().forall(
             pair => 
             val maturationTime = pair._2 
@@ -398,7 +400,7 @@ module ccv_model {
     val EventuallyMatureOnProviderInv =
         runningConsumers.forall(
             consumer => {
-                val sentPackets = currentState.providerState.sentVscPacketsToConsumer.get(consumer).toSet()
+                val sentPackets = currentState.providerState.sentVscPacketsToConsumer.getOrElse(consumer, List()).toSet()
                 sentPackets.forall(
                     packet =>
                         // consumer still has time to respond
@@ -442,7 +444,7 @@ module ccv_model {
     val CanSendVscPackets =
         not(ConsumerChains.exists(
             consumer => 
-                currentState.providerState.outstandingPacketsToConsumer.get(consumer).length() > 0
+                currentState.providerState.outstandingPacketsToConsumer.getOrElse(consumer, List()).length() > 0
         ))
 
     val CanReceiveVscPackets =
@@ -510,7 +512,7 @@ module ccv_model {
                     // consumer1 was started
                     assert(currentState.providerState.consumerStatus.get("consumer1") == RUNNING),
                     // but no packet was sent to consumer 1
-                    assert(currentState.providerState.outstandingPacketsToConsumer.get("consumer1").length() == 0),
+                    assert(currentState.providerState.outstandingPacketsToConsumer.getOrElse("consumer1", List()).length() == 0),
                     // the validator set on the provider was entered into the history
                     assert(currentState.providerState.chainState.votingPowerHistory == List(InitialValidatorSet.put("node1", 150), InitialValidatorSet)),
                     // change voting power on provider again
@@ -698,9 +700,11 @@ module ccv_model {
     val providerKeyAssignedValSetHistory = currentState.providerState.keyAssignedValSetHistory
 
     val ValidatorSetHasExistedKeyAssignmentInv =
-        runningConsumers.forall(chain =>
+        runningConsumers.forall(chain => // for every running consumer
             currentState.consumerStates.get(chain).chainState.votingPowerHistory.toSet().forall(
+                // for every validator set the consumer ever had
                 validatorSet => providerKeyAssignedValSetHistory.getOrElse(chain, List()).toSet().exists(
+                    // that validator set needs to also have existed on the provider
                     provValSet => removeZeroPowers(provValSet) == removeZeroPowers(validatorSet)
                 )
             )
@@ -723,10 +727,6 @@ module ccv_model {
                     packet.validatorSet == 
                     applyKeyAssignmentToValSet(providerState, consumer, providerValSetInCurBlock)
             )
-            // or the consumer was just started, which we detect by the consumer having a timestamp of 0
-            // and the consumer having the validator set that was just sent in the block
-            or 
-            (currentState.consumerStates.get(consumer).chainState.lastTimestamp == 0 and currentState.consumerStates.get(consumer).chainState.currentValidatorSet == providerValSetInCurBlock)
         )
 
     // Every consumer chain receives the same sequence of 
@@ -778,6 +778,8 @@ module ccv_model {
                                     packet.validatorSet)
                             }))
                         )
+                        // check that the packets between the common packets are equal
+                        // when key assignment is reversed
                         packetsBetween1noKeyAssignment == packetsBetween2noKeyAssignment
                     }
                 }

tests/mbt/model/ccv_test.qnt

@@ -5,6 +5,7 @@ module ccv_test {
     import ccv_types.* from "./ccv"
     import Time.* from "./libraries/Time"
     import extraSpells.* from "./libraries/extraSpells"
+    import ccv_utils.* from "./ccv_utils"
 
     pure val consumerChains = Set("sender", "receiver")
     pure val chains = consumerChains.union(Set(PROVIDER_CHAIN))