From 9a342eb766a741738e847418d60b7dad23d7bf20 Mon Sep 17 00:00:00 2001
From: 0xb337r007 <0xe4e5@proton.me>
Date: Thu, 6 Jun 2024 10:51:28 +0200
Subject: [PATCH] add harness and marketplace totals rules

---
 certora/harness/MarketplaceHarness.sol | 22 +++++++++++++++++
 certora/scripts/verify-marketplace.sh  |  3 ++-
 certora/specs/Marketplace.spec         | 34 ++++++++++++++++++++++++--
 3 files changed, 56 insertions(+), 3 deletions(-)
 create mode 100644 certora/harness/MarketplaceHarness.sol

diff --git a/certora/harness/MarketplaceHarness.sol b/certora/harness/MarketplaceHarness.sol
new file mode 100644
index 00000000..5d611efd
--- /dev/null
+++ b/certora/harness/MarketplaceHarness.sol
@@ -0,0 +1,22 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.8;
+
+import "@openzeppelin/contracts/token/ERC20/IERC20.sol";
+import {Marketplace} from "../../contracts/Marketplace.sol";
+import {MarketplaceConfig} from "../../contracts/Configuration.sol";
+
+contract MarketplaceHarness is Marketplace {
+    constructor(IERC20 token_, MarketplaceConfig memory configuration) Marketplace(token_, configuration) {}
+
+    function totalReceived() public view returns (uint256) {
+        return _marketplaceTotals.received;
+    }
+
+    function totalSent() public view returns (uint256) {
+        return _marketplaceTotals.sent;
+    }
+
+    function tokenBalance() public view returns (uint256) {
+        return token.balanceOf(address(this));
+    }
+}
diff --git a/certora/scripts/verify-marketplace.sh b/certora/scripts/verify-marketplace.sh
index 1dde17ee..7a2f8700 100755
--- a/certora/scripts/verify-marketplace.sh
+++ b/certora/scripts/verify-marketplace.sh
@@ -10,7 +10,8 @@ fi
 
 certoraRun \
   contracts/Marketplace.sol \
---verify Marketplace:certora/specs/Marketplace.spec \
+  certora/harness/MarketplaceHarness.sol \
+--verify MarketplaceHarness:certora/specs/Marketplace.spec \
 --optimistic_loop \
 --loop_iter 3 \
 --rule_sanity "basic" \
diff --git a/certora/specs/Marketplace.spec b/certora/specs/Marketplace.spec
index 54c4fc51..d7c1b125 100644
--- a/certora/specs/Marketplace.spec
+++ b/certora/specs/Marketplace.spec
@@ -1,3 +1,33 @@
-rule test {
-    assert(true);
+methods {
+  function totalReceived() external returns (uint) envfree;
+  function totalSent() external returns (uint) envfree;
+  function tokenBalance() external returns (uint) envfree;
+}
+
+rule sanity(env e, method f) {
+    calldataarg args;
+    f(e, args);
+    satisfy true;
+}
+
+rule totalReceivedCannotDecrease(env e, method f) {
+  mathint total_before = totalReceived();
+
+  calldataarg args;
+  f(e, args);
+
+  mathint total_after = totalReceived();
+
+  assert total_after >= total_before;
+}
+
+rule totalSentCannotDecrease(env e, method f) {
+  mathint total_before = totalSent();
+
+  calldataarg args;
+  f(e, args);
+
+  mathint total_after = totalSent();
+
+  assert total_after >= total_before;
 }