Change semantics of VotingPowerChange to take change amount, not new …

…total
cosmos · Nov 8, 2023 · b8640d9 · b8640d9
1 parent e9d7107
commit b8640d9
Show file tree

Hide file tree

Showing 3 changed files with 20 additions and 19 deletions.
diff --git a/tests/difference/core/quint_model/ccv.qnt b/tests/difference/core/quint_model/ccv.qnt
@@ -245,14 +245,15 @@ module ccv {
     // functions here roughly correspond to API calls that can be triggered from external sources
     // ===================
 
-    // the power of a validator on the provider chain is changed to the given amount. We do not care how this happens,
+    // the power of a validator on the provider chain is changed by the given amount. We do not care how this happens,
     // e.g. via undelegations, or delegations, ...
     pure def votingPowerChange(currentState: ProtocolState, validator: Node, amount: int): Result = {
-            if (amount < 0) {
-                Err("Voting power changes must be nonnegative")
+            pure val currentValidatorSet = currentState.providerState.chainState.currentValidatorSet
+            pure val oldVotingPower = if (currentValidatorSet.keys().contains(validator)) currentValidatorSet.get(validator) else 0
+            if (amount == 0) {
+                Err("Voting power cannot change by zero!")
             } else {
-                pure val currentValidatorSet = currentState.providerState.chainState.currentValidatorSet
-                pure val newValidatorSet = currentValidatorSet.put(validator, amount)
+                pure val newValidatorSet = currentValidatorSet.put(validator, oldVotingPower + amount)
                 // set the validator set changed flag
                 val newProviderState = currentState.providerState.with(
                     "providerValidatorSetChangedInThisBlock", true

diff --git a/tests/difference/core/quint_model/ccv_model.qnt b/tests/difference/core/quint_model/ccv_model.qnt
@@ -43,7 +43,7 @@ module ccv_model {
             consumersToStart: Set[Chain],
             consumersToStop: Set[Chain],
             validator: Node,
-            newVotingPower: int,
+            changeAmount: int,
         }
 
 
@@ -64,7 +64,7 @@ module ccv_model {
                 consumersToStart: Set(),
                 consumersToStop: Set(),
                 validator: "",
-                newVotingPower: 0,
+                changeAmount: 0,
             }
 
     // step allows the most generic nondeterminism, in particular it becomes relatively likely
@@ -149,12 +149,12 @@ module ccv_model {
         }
     }
 
-    action VotingPowerChange(validator: Node, newVotingPower: int): bool = 
-        val result = votingPowerChange(currentState, validator, newVotingPower)
+    action VotingPowerChange(validator: Node, changeAmount: int): bool = 
+        val result = votingPowerChange(currentState, validator, changeAmount)
         all {
             result.hasError() == false,
             currentState' = result.newState,
-            trace' = trace.append(emptyAction.with("kind", "VotingPowerChange").with("validator", validator).with("newVotingPower", newVotingPower)),
+            trace' = trace.append(emptyAction.with("kind", "VotingPowerChange").with("validator", validator).with("changeAmount", changeAmount)),
             params' = params,
         }
 
@@ -448,7 +448,7 @@ module ccv_model {
             .then(
             all {
                 // the validator set has changed
-                assert(currentState.providerState.chainState.currentValidatorSet == InitialValidatorSet.put("node1", 50)),
+                assert(currentState.providerState.chainState.currentValidatorSet == InitialValidatorSet.put("node1", 150)),
                 // start consumer1
                 EndAndBeginBlockForProvider(1 * Second, Set("consumer1"), Set())
             })
@@ -459,7 +459,7 @@ module ccv_model {
                     // a packet was sent to consumer1
                     assert(currentState.providerState.outstandingPacketsToConsumer.get("consumer1").length() == 1),
                     // the validator set on the provider was entered into the history
-                    assert(currentState.providerState.chainState.votingPowerHistory == List(InitialValidatorSet.put("node1", 50), InitialValidatorSet)),
+                    assert(currentState.providerState.chainState.votingPowerHistory == List(InitialValidatorSet.put("node1", 150), InitialValidatorSet)),
                     // deliver the packet
                     DeliverVscPacket("consumer1")
                 }
@@ -471,7 +471,7 @@ module ccv_model {
                     // ensure the maturation time was entered on the consumer
                     assert(currentState.consumerStates.get("consumer1").maturationTimes.keys().size() == 1),
                     // the validator set was put as the current validator set
-                    assert(currentState.consumerStates.get("consumer1").chainState.currentValidatorSet == InitialValidatorSet.put("node1", 50)),
+                    assert(currentState.consumerStates.get("consumer1").chainState.currentValidatorSet == InitialValidatorSet.put("node1", 150)),
                     // advance time on provider until the unbonding period is over
                     EndAndBeginBlockForProvider(UnbondingPeriodPerChain.get("consumer1"), Set(), Set()),
                 }

diff --git a/tests/difference/core/quint_model/ccv_test.qnt b/tests/difference/core/quint_model/ccv_test.qnt
@@ -13,13 +13,13 @@ module ccv_test {
 
     import ccv(VscTimeout = 5 * Week, CcvTimeout = ccvTimeouts, UnbondingPeriodPerChain = unbondingPeriods, ConsumerChains = consumerChains).* from "./ccv"
 
-    // negative voting powers give an error
-    run VotingPowerNegativeTest =
+    // changing voting power by zero gives an error
+    run VotingPowerZeroChangeTest =
     {
         votingPowerChange(
             GetEmptyProtocolState,
             "validator",
-            -1
+            0
         ).hasError()
     }
 
@@ -46,7 +46,7 @@ module ccv_test {
         val finalResult = votingPowerChange(
             tmpResult.newState,
             "validator",
-            0
+            -5
         )
         not(finalResult.hasError()) and
         finalResult.newState.providerState.chainState.currentValidatorSet.get("validator") == 0
@@ -64,7 +64,7 @@ module ccv_test {
         val finalResult = votingPowerChange(
             tmpResult.newState,
             "validator",
-            0
+            -5
         )
         // still should set the flag
         not(finalResult.hasError()) and
@@ -78,7 +78,7 @@ module ccv_test {
         val result = votingPowerChange(
             GetEmptyProtocolState,
             "validator",
-            0
+            2
         )
         not(result.hasError()) and
         result.newState.providerState.chainState.votingPowerHistory == List()