From e04f8ae909b8c8054dad7728f7ec2b483d236481 Mon Sep 17 00:00:00 2001
From: r4bbit <445106+0x-r4bbit@users.noreply.github.com>
Date: Fri, 9 Aug 2024 09:30:15 +0200
Subject: [PATCH] chore(certora): add invariant that totalSupply is
 sumOfBalances

This invariant ensures that the total supply of the used token in the
contract is always greater equal to the sum of all balances within the
token combined.
---
 certora/specs/Marketplace.spec | 24 ++++++++++++++++++++++++
 1 file changed, 24 insertions(+)

diff --git a/certora/specs/Marketplace.spec b/certora/specs/Marketplace.spec
index 75dc1eb..43475d6 100644
--- a/certora/specs/Marketplace.spec
+++ b/certora/specs/Marketplace.spec
@@ -2,12 +2,25 @@ using ERC20A as Token;
 
 methods {
     function Token.balanceOf(address) external returns (uint256) envfree;
+    function Token.totalSupply() external returns (uint256) envfree;
 }
 
 /*--------------------------------------------
 |              Ghosts and hooks              |
 --------------------------------------------*/
 
+ghost mathint sumOfBalances {
+    init_state axiom sumOfBalances == 0;
+}
+
+hook Sload uint256 balance Token._balances[KEY address addr] {
+    require sumOfBalances >= to_mathint(balance);
+}
+
+hook Sstore Token._balances[KEY address addr] uint256 newValue (uint256 oldValue) {
+    sumOfBalances = sumOfBalances - oldValue + newValue;
+}
+
 ghost mathint totalReceived;
 
 hook Sload uint256 defaultValue currentContract._marketplaceTotals.received {
@@ -28,6 +41,10 @@ hook Sstore currentContract._marketplaceTotals.sent uint256 defaultValue (uint25
     totalSent = totalSent + defaultValue - defaultValue_old;
 }
 
+/*--------------------------------------------
+|              Helper functions              |
+--------------------------------------------*/
+
 function canCancelRequest(method f) returns bool {
     return f.selector == sig:withdrawFunds(Marketplace.RequestId).selector;
 }
@@ -45,6 +62,13 @@ function canFailRequest(method f) returns bool {
         f.selector == sig:freeSlot(Marketplace.SlotId).selector;
 }
 
+/*--------------------------------------------
+|                 Invariants                 |
+--------------------------------------------*/
+
+invariant totalSupplyIsSumOfBalances()
+    to_mathint(Token.totalSupply()) == sumOfBalances;
+
 invariant requestStartedWhenSlotsFilled(env e, Marketplace.RequestId requestId, Marketplace.SlotId slotId)
     to_mathint(currentContract.requestContext(e, requestId).slotsFilled) == to_mathint(currentContract.getRequest(e, requestId).ask.slots) => currentContract.requestState(e, requestId) == Marketplace.RequestState.Started;