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

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

diff --git a/certora/specs/Marketplace.spec b/certora/specs/Marketplace.spec
index 914b5f7..8a02025 100644
--- a/certora/specs/Marketplace.spec
+++ b/certora/specs/Marketplace.spec
@@ -182,6 +182,13 @@ invariant paidSlotAlwaysHasFinishedOrCancelledRequest(env e, Marketplace.SlotId
       }
     }
 
+// STATUS - verified
+// cancelled slot always belongs to cancelled request
+// https://prover.certora.com/output/6199/80d5dc73d406436db166071e277283f1?anonymousKey=d5d175960dc40f72e22ba8e31c6904a488277e57
+invariant cancelledSlotAlwaysHasCancelledRequest(env e, Marketplace.SlotId slotId)
+    currentContract.slotState(e, slotId) == Marketplace.SlotState.Cancelled =>
+        currentContract.requestState(e, currentContract.slots(e, slotId).requestId) == Marketplace.RequestState.Cancelled;
+
 /*--------------------------------------------
 |                 Properties                 |
 --------------------------------------------*/