From 5b5a3c9e2e69273e14d891ed4d4be222a99cfac9 Mon Sep 17 00:00:00 2001
From: r4bbit <445106+0x-r4bbit@users.noreply.github.com>
Date: Wed, 21 Aug 2024 20:45:49 +0200
Subject: [PATCH] chore(certora): introduce invariant that failed requests are
 always ended

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

diff --git a/certora/specs/Marketplace.spec b/certora/specs/Marketplace.spec
index 079d1de..69ab266 100644
--- a/certora/specs/Marketplace.spec
+++ b/certora/specs/Marketplace.spec
@@ -156,6 +156,13 @@ invariant cancelledRequestAlwaysExpired(env e, Marketplace.RequestId requestId)
     currentContract.requestState(e, requestId) == Marketplace.RequestState.Cancelled =>
         currentContract.requestExpiry(e, requestId) < lastBlockTimestampGhost;
 
+// STATUS - verified
+// failed request is always ended
+// https://prover.certora.com/output/6199/902ffe4a83a9438e9860655446b46a74?anonymousKey=47b344024bbfe84a649bd1de44d7d243ce8dbc21
+invariant failedRequestAlwaysEnded(env e, Marketplace.RequestId requestId)
+    currentContract.requestState(e, requestId) == Marketplace.RequestState.Failed =>
+        currentContract.requestContext(e, requestId).endsAt < lastBlockTimestampGhost;
+
 /*--------------------------------------------
 |                 Properties                 |
 --------------------------------------------*/