From 018ed2567f163d3128199f47fe64663136305d6a Mon Sep 17 00:00:00 2001
From: r4bbit <445106+0x-r4bbit@users.noreply.github.com>
Date: Fri, 9 Aug 2024 09:58:39 +0200
Subject: [PATCH] chore(certora): add invariant that totalSent is <=
 totalReceived

This commit adds an invariant that verifies `marketplaceTotals.sent <=
marketplceTotals.received`.

The invariant relies on the `Token.totalSupply()` which has previously
been verified to be the sum of all balances.

The invariant uses `<=` as there could be donations sent to the
marketplace.

Closes #132
---
 certora/specs/Marketplace.spec | 16 ++++++++++++++++
 1 file changed, 16 insertions(+)

diff --git a/certora/specs/Marketplace.spec b/certora/specs/Marketplace.spec
index 0c1d939..49e2499 100644
--- a/certora/specs/Marketplace.spec
+++ b/certora/specs/Marketplace.spec
@@ -191,6 +191,22 @@ invariant cancelledSlotAlwaysHasCancelledRequest(env e, Marketplace.SlotId slotI
     currentContract.slotState(e, slotId) == Marketplace.SlotState.Cancelled =>
         currentContract.requestState(e, currentContract.slots(e, slotId).requestId) == Marketplace.RequestState.Cancelled;
 
+// STATUS - in progress (fails on constructor state due to a strange behaviour in the tool)
+// _marketplaceTotals.received - _marketplaceTotals.sent == tokenBalanceOfContract
+// https://prover.certora.com/output/3106/4e6cac8055ac45bb92840e14d9b095eb/?anonymousKey=655a42ca6306a023db78914d5a188d8ec2882771
+invariant totalSentIsLessThanOrEqualTotalReceived()
+    totalReceived - totalSent <= to_mathint(Token.balanceOf(currentContract))
+    {
+        preserved fillSlot(MarketplaceHarness.RequestId requestId, uint256 slotIndex, MarketplaceHarness.Groth16Proof proof) with (env e2) {
+            require e2.msg.sender != currentContract;
+            requireInvariant totalSupplyIsSumOfBalances();
+        }
+        preserved requestStorage(MarketplaceHarness.Request request) with (env e3) {
+            require e3.msg.sender != currentContract;
+            requireInvariant totalSupplyIsSumOfBalances();
+        }
+    }
+
 /*--------------------------------------------
 |                 Properties                 |
 --------------------------------------------*/