From f294eecabb5a3aee2b592316d4df353645311a9d Mon Sep 17 00:00:00 2001
From: Philip Offtermatt <p.offtermatt@gmail.com>
Date: Wed, 11 Oct 2023 14:45:32 +0200
Subject: [PATCH] Remove special treatment of 0 voting power

---
 tests/difference/core/quint_model/ccv.qnt      | 10 +---------
 tests/difference/core/quint_model/ccv_test.qnt |  4 ++--
 2 files changed, 3 insertions(+), 11 deletions(-)

diff --git a/tests/difference/core/quint_model/ccv.qnt b/tests/difference/core/quint_model/ccv.qnt
index 606574c42b..ac1f1f4959 100644
--- 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
index 4262c4c386..eb832603e6 100644
--- 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 =