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

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

diff --git a/certora/specs/Marketplace.spec b/certora/specs/Marketplace.spec
index 69ab266..55a8857 100644
--- a/certora/specs/Marketplace.spec
+++ b/certora/specs/Marketplace.spec
@@ -163,6 +163,13 @@ invariant failedRequestAlwaysEnded(env e, Marketplace.RequestId requestId)
     currentContract.requestState(e, requestId) == Marketplace.RequestState.Failed =>
         currentContract.requestContext(e, requestId).endsAt < lastBlockTimestampGhost;
 
+// STATUS - verified
+// finished slot always has finished request
+// https://prover.certora.com/output/6199/3371ee4f80354ac9b05b1c84c53b6154?anonymousKey=eab83785acb61ccd31ed0c9d5a2e9e2b24099156
+invariant finishedSlotAlwaysHasFinishedRequest(env e, Marketplace.SlotId slotId)
+    currentContract.slotState(e, slotId) == Marketplace.SlotState.Finished =>
+        currentContract.requestState(e, currentContract.slots(e, slotId).requestId) == Marketplace.RequestState.Finished;
+
 /*--------------------------------------------
 |                 Properties                 |
 --------------------------------------------*/