From 7c542e72b6a241655bd04322d4d1b96b22913c35 Mon Sep 17 00:00:00 2001
From: r4bbit <445106+0x-r4bbit@users.noreply.github.com>
Date: Wed, 21 Aug 2024 20:53:38 +0200
Subject: [PATCH] chore(certora); add rule to verify slot is failed or free
 when request has failed

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

diff --git a/certora/specs/Marketplace.spec b/certora/specs/Marketplace.spec
index 8a02025..41aa43d 100644
--- a/certora/specs/Marketplace.spec
+++ b/certora/specs/Marketplace.spec
@@ -222,6 +222,21 @@ rule totalSentCannotDecrease(env e, method f) {
     assert total_after >= total_before;
 }
 
+rule slotIsFailedOrFreeIfRequestHasFailed(env e, method f) {
+    calldataarg args;
+    Marketplace.SlotId slotId;
+
+    requireInvariant paidSlotAlwaysHasFinishedOrCancelledRequest(e, slotId);
+
+    require currentContract.requestState(e, currentContract.slots(e, slotId).requestId) != Marketplace.RequestState.Failed;
+    f(e, args);
+    require currentContract.requestState(e, currentContract.slots(e, slotId).requestId) == Marketplace.RequestState.Failed;
+
+    assert currentContract.slotState(e, slotId) == Marketplace.SlotState.Failed ||
+        currentContract.slotState(e, slotId) == Marketplace.SlotState.Free;
+}
+
+
 rule allowedRequestStateChanges(env e, method f) {
     calldataarg args;
     Marketplace.RequestId requestId;