From 7ce7a5dda0adaec9b65f03e208e8813fe1374a03 Mon Sep 17 00:00:00 2001
From: r4bbit <445106+0x-r4bbit@users.noreply.github.com>
Date: Wed, 21 Aug 2024 20:37:43 +0200
Subject: [PATCH] chore(certora): add invariant that cancelled requests are
 always expired

---
 certora/specs/Marketplace.spec | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/certora/specs/Marketplace.spec b/certora/specs/Marketplace.spec
index 70b43e3..079d1de 100644
--- a/certora/specs/Marketplace.spec
+++ b/certora/specs/Marketplace.spec
@@ -149,6 +149,13 @@ invariant slotMissedShouldBeEqualToNumberOfMissedPeriods(env e, Marketplace.Slot
 invariant cantBeMissedIfInPeriod(MarketplaceHarness.SlotId slotId, Periods.Period period)
     lastBlockTimestampGhost <= publicPeriodEnd(period) => !_missingMirror[slotId][period];
 
+// STATUS - verified
+// cancelled request is always expired
+// https://prover.certora.com/output/6199/36b12b897f3941faa00fb4ab6871be8e?anonymousKey=de98a02041b841fb2fa67af4222f29fac258249f
+invariant cancelledRequestAlwaysExpired(env e, Marketplace.RequestId requestId)
+    currentContract.requestState(e, requestId) == Marketplace.RequestState.Cancelled =>
+        currentContract.requestExpiry(e, requestId) < lastBlockTimestampGhost;
+
 /*--------------------------------------------
 |                 Properties                 |
 --------------------------------------------*/