From 2a1bef52552e7bd5d32f6c254719394140d85119 Mon Sep 17 00:00:00 2001
From: Andrea Franz <andrea@gravityblast.com>
Date: Fri, 4 Oct 2024 11:38:25 +0200
Subject: [PATCH] chore(certora): verify slots transitions and that a slot can
 be paid only once

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

diff --git a/certora/specs/Marketplace.spec b/certora/specs/Marketplace.spec
index f7f2e2c..9e00376 100644
--- a/certora/specs/Marketplace.spec
+++ b/certora/specs/Marketplace.spec
@@ -378,6 +378,31 @@ rule functionsCausingSlotStateChanges(env e, method f) {
 
     // SlotState.Free -> SlotState.Filled
     assert slotStateBefore != Marketplace.SlotState.Filled && slotStateAfter == Marketplace.SlotState.Filled => canFillSlot(f);
+}
+
+rule allowedSlotStateChanges(env e, method f) {
+    calldataarg args;
+    Marketplace.SlotId slotId;
+
+    slotAttributesAreConsistent(e, slotId);
+
+    Marketplace.Slot slot = currentContract.slots(e, slotId);
+    Marketplace.SlotState slotStateBefore = currentContract.slotState(e, slotId);
+    f(e, args);
+    Marketplace.SlotState slotStateAfter = currentContract.slotState(e, slotId);
+
+    // Cannot change from Paid
+    assert slotStateBefore == Marketplace.SlotState.Paid => slotStateAfter == Marketplace.SlotState.Paid;
+
+    // SlotState.Cancelled -> SlotState.Cancelled || SlotState.Failed || Finished || Paid
+    assert slotStateBefore == Marketplace.SlotState.Cancelled => (
+            slotStateAfter == Marketplace.SlotState.Cancelled ||
+            slotStateAfter == Marketplace.SlotState.Failed ||
+            slotStateAfter == Marketplace.SlotState.Finished ||
+            slotStateAfter == Marketplace.SlotState.Paid
+            );
+
+    // SlotState.Filled only from Free
     assert slotStateBefore != Marketplace.SlotState.Filled && slotStateAfter == Marketplace.SlotState.Filled => slotStateBefore == Marketplace.SlotState.Free;
 }
 
@@ -435,3 +460,21 @@ rule slotStateChangesOnlyOncePerFunctionCall(env e, method f) {
 
     assert slotStateChangesCountAfter <= slotStateChangesCountBefore + 1;
 }
+
+rule slotCanBeFreedAndPaidOnce {
+  env e;
+  Marketplace.SlotId slotId;
+  address rewardRecipient;
+  address collateralRecipient;
+
+  Marketplace.SlotState slotStateBefore = currentContract.slotState(e, slotId);
+  require slotStateBefore != Marketplace.SlotState.Paid;
+  freeSlot(e, slotId, rewardRecipient, collateralRecipient);
+
+  Marketplace.SlotState slotStateAfter = currentContract.slotState(e, slotId);
+  require slotStateAfter == Marketplace.SlotState.Paid;
+
+  freeSlot@withrevert(e, slotId, rewardRecipient, collateralRecipient);
+
+  assert lastReverted;
+}