add harness and marketplace totals rules

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));
+    }
+}

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" \

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;
 }