From ebdf9ed366a26cfe5b67ac3bed04f9837c7dca1a Mon Sep 17 00:00:00 2001
From: r4bbit <445106+0x-r4bbit@users.noreply.github.com>
Date: Wed, 21 Aug 2024 20:22:39 +0200
Subject: [PATCH] fix(certora): fix rule that missed slots == number of issed
 periods

---
 certora/harness/MarketplaceHarness.sol |  6 +++++-
 certora/specs/Marketplace.spec         | 13 ++++++++++++-
 2 files changed, 17 insertions(+), 2 deletions(-)

diff --git a/certora/harness/MarketplaceHarness.sol b/certora/harness/MarketplaceHarness.sol
index c2f118a..318c390 100644
--- a/certora/harness/MarketplaceHarness.sol
+++ b/certora/harness/MarketplaceHarness.sol
@@ -6,7 +6,7 @@ import {IERC20} from "@openzeppelin/contracts/token/ERC20/IERC20.sol";
 import {IGroth16Verifier} from "../../contracts/Groth16.sol";
 import {MarketplaceConfig} from "../../contracts/Configuration.sol";
 import {Marketplace} from "../../contracts/Marketplace.sol";
-import {RequestId} from "../../contracts/Requests.sol";
+import {RequestId, SlotId} from "../../contracts/Requests.sol";
 
 contract MarketplaceHarness is Marketplace {
     constructor(MarketplaceConfig memory config, IERC20 token, IGroth16Verifier verifier) Marketplace(config, token, verifier) {}
@@ -15,6 +15,10 @@ contract MarketplaceHarness is Marketplace {
         return _requestContexts[requestId];
     }
 
+    function slots(SlotId slotId) public returns (Marketplace.Slot memory) {
+        return _slots[slotId];
+    }
+
     function publicPeriodEnd(Period period) public view returns (uint256) {
         return _periodEnd(period);
     }
diff --git a/certora/specs/Marketplace.spec b/certora/specs/Marketplace.spec
index 26551d8..70b43e3 100644
--- a/certora/specs/Marketplace.spec
+++ b/certora/specs/Marketplace.spec
@@ -71,11 +71,20 @@ hook Sload bool defaultValue _missing[KEY MarketplaceHarness.SlotId slotId][KEY
 
 hook Sstore _missing[KEY MarketplaceHarness.SlotId slotId][KEY Periods.Period period] bool defaultValue {
     _missingMirror[slotId][period] = defaultValue;
-    _missedCalculated[slotId] = _missedCalculated[slotId] + 1;
+    if (defaultValue) {
+        _missedCalculated[slotId] = _missedCalculated[slotId] + 1;
+    }
+}
+
+hook Sload uint256 defaultValue _missed[KEY MarketplaceHarness.SlotId slotId] {
+    require _missedMirror[slotId] == defaultValue;
 }
 
 hook Sstore _missed[KEY MarketplaceHarness.SlotId slotId] uint256 defaultValue {
     _missedMirror[slotId] = defaultValue;
+    if (defaultValue == 0) {
+        _missedCalculated[slotId] = 0;
+    }
 }
 
 ghost mathint requestStateChangesCount {
@@ -129,6 +138,8 @@ invariant totalSupplyIsSumOfBalances()
 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;
 
+// STATUS - verified
+// https://prover.certora.com/output/6199/6e2383ea040347eabeeb1008bc257ae6?anonymousKey=e1a6a00310a44ed264b1f98b03fa29273e68fca9
 invariant slotMissedShouldBeEqualToNumberOfMissedPeriods(env e, Marketplace.SlotId slotId)
     to_mathint(_missedMirror[slotId]) == _missedCalculated[slotId];