From 26926c1d5e37f4f475012df911795ddaf2e3578f Mon Sep 17 00:00:00 2001
From: Andrea Franz <andrea@gravityblast.com>
Date: Tue, 11 Mar 2025 08:24:57 +0100
Subject: [PATCH] test(certora): Karma.totalDistributorAllocation can only
 increase (#166)

---
 certora/specs/Karma.spec | 19 ++++++++++++++++++-
 1 file changed, 18 insertions(+), 1 deletion(-)

diff --git a/certora/specs/Karma.spec b/certora/specs/Karma.spec
index 124350e..be7b0a4 100644
--- a/certora/specs/Karma.spec
+++ b/certora/specs/Karma.spec
@@ -2,10 +2,10 @@ using Karma as karma;
 
 methods {
     function owner() external returns (address) envfree;
+    function totalDistributorAllocation() external returns (uint256) envfree;
 }
 
 // TODO:
-// totalDistributorAllocation can only increase
 // totalDistributorAllocation == sum of all distributor allocations
 // sum of external supply <= total supply
 
@@ -44,3 +44,20 @@ rule ownableFuncsOnlyCallableByOwner(method f) {
 
     assert isOwnableFunction(f) && !isOwner => isReverted;
 }
+
+rule totalDistributorAllocationCanOnlyIncrease(method f) filtered { f ->
+     f.selector != sig:karma.upgradeToAndCall(address, bytes).selector
+     && !isERC20TransferFunction(f)
+    } {
+    env e;
+    calldataarg args;
+
+
+    uint256 totalDistributorAllocationBefore = totalDistributorAllocation();
+
+    f(e, args);
+
+    uint256 totalDistributorAllocationAfter = totalDistributorAllocation();
+
+    assert totalDistributorAllocationAfter >= totalDistributorAllocationBefore;
+}