From 29f39d52c77b57dc9f1b41853cea2250dec1af01 Mon Sep 17 00:00:00 2001
From: Andrea Franz <andrea@gravityblast.com>
Date: Thu, 15 Aug 2024 12:51:14 +0200
Subject: [PATCH] chore(certora): slot's missed periods count should be equal
 to the count of slot's missing periods set to true (#155)

---
 certora/specs/Marketplace.spec | 27 ++++++++++++++++++++++-----
 contracts/Proofs.sol           |  1 +
 2 files changed, 23 insertions(+), 5 deletions(-)

diff --git a/certora/specs/Marketplace.spec b/certora/specs/Marketplace.spec
index b9feb97..21905e5 100644
--- a/certora/specs/Marketplace.spec
+++ b/certora/specs/Marketplace.spec
@@ -50,17 +50,32 @@ hook TIMESTAMP uint v {
 }
 
 ghost mapping(MarketplaceHarness.SlotId => mapping(Periods.Period => bool)) _missingMirror {
-    init_state axiom forall MarketplaceHarness.SlotId a. 
-            forall Periods.Period b. 
+    init_state axiom forall MarketplaceHarness.SlotId a.
+            forall Periods.Period b.
             _missingMirror[a][b] == false;
 }
 
+ghost mapping(MarketplaceHarness.SlotId => uint256) _missedMirror {
+    init_state axiom forall MarketplaceHarness.SlotId a.
+            _missedMirror[a] == 0;
+}
+
+ghost mapping(MarketplaceHarness.SlotId => mathint) _missedCalculated {
+    init_state axiom forall MarketplaceHarness.SlotId a.
+            _missedCalculated[a] == 0;
+}
+
 hook Sload bool defaultValue _missing[KEY MarketplaceHarness.SlotId slotId][KEY Periods.Period period] {
     require _missingMirror[slotId][period] == defaultValue;
 }
 
 hook Sstore _missing[KEY MarketplaceHarness.SlotId slotId][KEY Periods.Period period] bool defaultValue {
     _missingMirror[slotId][period] = defaultValue;
+    _missedCalculated[slotId] = _missedCalculated[slotId] + 1;
+}
+
+hook Sstore _missed[KEY MarketplaceHarness.SlotId slotId] uint256 defaultValue {
+    _missedMirror[slotId] = defaultValue;
 }
 
 ghost mathint requestStateChangesCount {
@@ -83,7 +98,6 @@ hook Sstore _slots[KEY Marketplace.SlotId slotId].state Marketplace.SlotState ne
     }
 }
 
-
 /*--------------------------------------------
 |              Helper functions              |
 --------------------------------------------*/
@@ -101,7 +115,7 @@ function canFinishRequest(method f) returns bool {
 }
 
 function canFailRequest(method f) returns bool {
-    return f.selector == sig:markProofAsMissing(Marketplace.SlotId, Periods.Period).selector || 
+    return f.selector == sig:markProofAsMissing(Marketplace.SlotId, Periods.Period).selector ||
         f.selector == sig:freeSlot(Marketplace.SlotId).selector;
 }
 
@@ -115,6 +129,9 @@ 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;
 
+invariant slotMissedShouldBeEqualToNumberOfMissedPeriods(env e, Marketplace.SlotId slotId)
+    to_mathint(_missedMirror[slotId]) == _missedCalculated[slotId];
+
 // STATUS - verified
 // can set missing if period was passed
 // https://prover.certora.com/output/3106/026b36c118e44ad0824a51c50647c497/?anonymousKey=29879706f3d343555bb6122d071c9409d4e9876d
@@ -219,7 +236,7 @@ rule slotStateChangesOnlyOncePerFunctionCall(env e, method f) {
 
     mathint slotStateChangesCountBefore = slotStateChangesCount;
     f(e, args);
-    mathint slotStateChangesCountAfter =slotStateChangesCount; 
+    mathint slotStateChangesCountAfter =slotStateChangesCount;
 
     assert slotStateChangesCountAfter <= slotStateChangesCountBefore + 1;
 }
diff --git a/contracts/Proofs.sol b/contracts/Proofs.sol
index 5453228..56b8447 100644
--- a/contracts/Proofs.sol
+++ b/contracts/Proofs.sol
@@ -203,6 +203,7 @@ abstract contract Proofs is Periods {
    * @dev Reverts when:
    *    - missedPeriod has not ended yet ended
    *    - missing proof was time-barred
+   *    - proof was submitted
    *    - proof was not required for missedPeriod period
    *    - proof was already marked as missing
    */