From 09ca8481fb75e4fdb271d187c0bf76474b88538c Mon Sep 17 00:00:00 2001
From: r4bbit <445106+0x-r4bbit@users.noreply.github.com>
Date: Wed, 21 Aug 2024 21:12:26 +0200
Subject: [PATCH] fix(certora): fix rule that describes allowed request state
 changes

This broke due to a newly introduced signature for `fillSlot()`
---
 certora/specs/Marketplace.spec | 9 +++++++--
 1 file changed, 7 insertions(+), 2 deletions(-)

diff --git a/certora/specs/Marketplace.spec b/certora/specs/Marketplace.spec
index fa03bef..ff76595 100644
--- a/certora/specs/Marketplace.spec
+++ b/certora/specs/Marketplace.spec
@@ -120,12 +120,14 @@ function canStartRequest(method f) returns bool {
 }
 
 function canFinishRequest(method f) returns bool {
-    return f.selector == sig:freeSlot(Marketplace.SlotId, address, address).selector;
+    return f.selector == sig:freeSlot(Marketplace.SlotId, address, address).selector ||
+        f.selector == sig:freeSlot(Marketplace.SlotId).selector;
 }
 
 function canFailRequest(method f) returns bool {
     return f.selector == sig:markProofAsMissing(Marketplace.SlotId, Periods.Period).selector ||
-        f.selector == sig:freeSlot(Marketplace.SlotId, address, address).selector;
+        f.selector == sig:freeSlot(Marketplace.SlotId, address, address).selector ||
+        f.selector == sig:freeSlot(Marketplace.SlotId).selector;
 }
 
 /*--------------------------------------------
@@ -262,6 +264,9 @@ rule functionsCausingRequestStateChanges(env e, method f) {
     // RequestState.New -> RequestState.Started
     assert requestStateBefore == Marketplace.RequestState.New && requestStateAfter == Marketplace.RequestState.Started => canStartRequest(f);
 
+    // RequestState.New -> RequestState.Cancelled
+    assert requestStateBefore == Marketplace.RequestState.New && requestStateAfter == Marketplace.RequestState.Cancelled => canCancelRequest(f);
+
     // RequestState.Started -> RequestState.Finished
     assert requestStateBefore == Marketplace.RequestState.Started && requestStateAfter == Marketplace.RequestState.Finished => canFinishRequest(f);