test(certora): add rule to check Karma externalSupply is always <= totalDistributorAllocation

certora/specs/Karma.spec

@@ -3,6 +3,8 @@ using Karma as karma;
 methods {
     function owner() external returns (address) envfree;
     function totalDistributorAllocation() external returns (uint256) envfree;
+    function totalSupply() external returns (uint256) envfree;
+    function externalSupply() external returns (uint256) envfree;
     function _.setReward(uint256, uint256) external => HAVOC_ECF;
 }
 
@@ -20,11 +22,14 @@ invariant totalDistributorAllocationIsSumOfDistributorAllocations()
         f -> !isUpgradeFunction(f)
     }
 
-// TODO:
-// sum of external supply <= total supply
+rule externalSupplyIsLessOrEqThanTotalDistributorAllocation() {
+    assert externalSupply() <= totalDistributorAllocation();
+}
+
 
 definition isUpgradeFunction(method f) returns bool = (
-  f.selector == sig:karma.upgradeToAndCall(address, bytes).selector
+  f.selector == sig:karma.upgradeToAndCall(address, bytes).selector ||
+  f.selector == sig:karma.upgradeTo(address).selector
 );
 
 definition isERC20TransferFunction(method f) returns bool = (

src/Karma.sol

@@ -163,12 +163,13 @@ contract Karma is Initializable, ERC20Upgradeable, Ownable2StepUpgradeable, UUPS
         for (uint256 i = 0; i < rewardDistributors.length(); i++) {
             IRewardDistributor distributor = IRewardDistributor(rewardDistributors.at(i));
             uint256 supply = distributor.totalRewardsSupply();
-            if (supply > rewardDistributorAllocations[address(distributor)]) {
-                supply = rewardDistributorAllocations[address(distributor)];
-            }
-
             externalSupply += supply;
         }
+
+        if (externalSupply > totalDistributorAllocation) {
+            return totalDistributorAllocation;
+        }
+
         return externalSupply;
     }
 
@@ -230,4 +231,13 @@ contract Karma is Initializable, ERC20Upgradeable, Ownable2StepUpgradeable, UUPS
     function allowance(address, address) public pure override returns (uint256) {
         return 0;
     }
+
+    /**
+     * @notice Returns the external supply of the token.
+     * @dev The external supply is the sum of the rewards from all reward distributors.
+     * @return The external supply of the token.
+     */
+    function externalSupply() public view returns (uint256) {
+        return _externalSupply();
+    }
 }