Remove special treatment of 0 voting power

cosmos · Oct 11, 2023 · f294eec · f294eec
1 parent d75d5c5
commit f294eec
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 11 deletions.
diff --git a/tests/difference/core/quint_model/ccv.qnt b/tests/difference/core/quint_model/ccv.qnt
@@ -254,7 +254,7 @@ module ccv {
                 Err("Voting power changes must be nonnegative")
             } else {
                 pure val currentValidatorSet = currentState.providerState.chainState.currentValidatorSet
-                pure val newValidatorSet = getUpdatedValidatorSet(currentValidatorSet, validator, amount)
+                pure val newValidatorSet = currentValidatorSet.put(validator, amount)
                 // set the validator set changed flag
                 val newProviderState = currentState.providerState.with(
                     "providerValidatorSetChangedInThisBlock", true
@@ -737,14 +737,6 @@ module ccv {
         newState
     }
 
-    // Updates the given oldValidatorSet by setting the validator to newVotingPower.
-    // If newVotingPower is zero, the validator is removed.
-    pure def getUpdatedValidatorSet(oldValidatorSet: ValidatorSet, validator: Node, newVotingPower: int): ValidatorSet =
-        if (newVotingPower > 0) 
-        oldValidatorSet.put(validator, newVotingPower)
-        else
-        oldValidatorSet.mapRemove(validator)
-
     // Returns a ProtocolState where the current validator set on the provider is set to 
     // newValidatorSet.
     pure def setProviderValidatorSet(currentState: ProtocolState, newValidatorSet: ValidatorSet): ProtocolState = {

diff --git a/tests/difference/core/quint_model/ccv_test.qnt b/tests/difference/core/quint_model/ccv_test.qnt
@@ -35,7 +35,7 @@ module ccv_test {
         result.newState.providerState.chainState.currentValidatorSet.get("validator") == 5
     }
 
-    // validators that get zero voting power are removed
+    // voting power of 0 is allowed and applied as usual
     run VotingPowerZeroTest =
     {
         val tmpResult = votingPowerChange(
@@ -49,7 +49,7 @@ module ccv_test {
             0
         )
         not(finalResult.hasError) and
-        not(finalResult.newState.providerState.chainState.currentValidatorSet.keys().contains("validator"))
+        finalResult.newState.providerState.chainState.currentValidatorSet.get("validator") == 0
     }
 
     run VotingPowerSetsFlagTest =