From 38caabeee393b97c8f62e17ea0428d118c7a39f0 Mon Sep 17 00:00:00 2001
From: r4bbit <445106+0x-r4bbit@users.noreply.github.com>
Date: Mon, 26 Aug 2024 14:49:42 +0200
Subject: [PATCH] fix(certora): remove incorrect requirment in
 `paidSlotAlwaysHasCancelledOrFinishedRequest`

The mentioned invariant uses a `preserved` block with a `require
SlotState == Paid`, which essentially excludes all cases where
`SlotState != Paid`.

This was incorrectly applied. Removing that requirement causes the
prover to find a counter example where it starts with `RequestState == Started`
and `SlotState == Cancelled`.

This ultimately results in `SlotState == PAID` while `RequestState`
stays `Started`.

Counter example link: https://prover.certora.com/output/6199/a38c9bd665d544dabcffd07335c05420?anonymousKey=119a850a4d1d65ccbe8f95298615592835801d2b

A slot that is `Cancelled` however, can never belong to a request that
is `Started`. So requiring the invariant that
`cancelledSlotAlwaysHasCancelledRequest` fixes this and the rule is
passing.

Passing rule: https://prover.certora.com/output/6199/d0e165ed5d594f9fb477602af06cfeb1?anonymousKey=01ffaad46027786c38d78e5a41c03ce002032200

Closes #164
---
 certora/specs/Marketplace.spec | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/certora/specs/Marketplace.spec b/certora/specs/Marketplace.spec
index 0c1d939..17d3391 100644
--- a/certora/specs/Marketplace.spec
+++ b/certora/specs/Marketplace.spec
@@ -174,13 +174,12 @@ invariant finishedSlotAlwaysHasFinishedRequest(env e, Marketplace.SlotId slotId)
 
 // STATUS - verified
 // paid slot always has finished or cancelled request
-// https://prover.certora.com/output/6199/6217a927ff2c43bea1124f6ae54a78fb?anonymousKey=d5e09d0d12658fd6b5f298fc04cea88da892c62d
+// https://prover.certora.com/output/6199/d0e165ed5d594f9fb477602af06cfeb1?anonymousKey=01ffaad46027786c38d78e5a41c03ce002032200
 invariant paidSlotAlwaysHasFinishedOrCancelledRequest(env e, Marketplace.SlotId slotId)
      currentContract.slotState(e, slotId) == Marketplace.SlotState.Paid =>
          currentContract.requestState(e, currentContract.slots(e, slotId).requestId) == Marketplace.RequestState.Finished || currentContract.requestState(e, currentContract.slots(e, slotId).requestId) == Marketplace.RequestState.Cancelled
     { preserved {
-        // ensures we start with a paid slot
-        require currentContract.slotState(e, slotId) == Marketplace.SlotState.Paid;
+        requireInvariant cancelledSlotAlwaysHasCancelledRequest(e, slotId);
       }
     }