From 3a074abd208b2cd158879690bed3664090804cfa Mon Sep 17 00:00:00 2001
From: Andrea Franz <andrea@gravityblast.com>
Date: Thu, 29 Aug 2024 16:33:23 +0200
Subject: [PATCH] chore(certora): verify possible slot state transitions

---
 certora/harness/MarketplaceHarness.sol | 14 ++++++--
 certora/specs/Marketplace.spec         | 46 +++++++++++++++++++++++---
 2 files changed, 53 insertions(+), 7 deletions(-)

diff --git a/certora/harness/MarketplaceHarness.sol b/certora/harness/MarketplaceHarness.sol
index 51d757a..f61ac57 100644
--- a/certora/harness/MarketplaceHarness.sol
+++ b/certora/harness/MarketplaceHarness.sol
@@ -7,12 +7,22 @@ import {IGroth16Verifier} from "../../contracts/Groth16.sol";
 import {MarketplaceConfig} from "../../contracts/Configuration.sol";
 import {Marketplace} from "../../contracts/Marketplace.sol";
 import {RequestId, SlotId} from "../../contracts/Requests.sol";
+import {Requests} from "../../contracts/Requests.sol";
 
 contract MarketplaceHarness is Marketplace {
-    constructor(MarketplaceConfig memory config, IERC20 token, IGroth16Verifier verifier) Marketplace(config, token, verifier) {}
+    constructor(MarketplaceConfig memory config, IERC20 token, IGroth16Verifier verifier)
+        Marketplace(config, token, verifier)
+    {}
 
     function publicPeriodEnd(Period period) public view returns (uint256) {
         return _periodEnd(period);
     }
-}
 
+    function slots(SlotId slotId) public view returns (Slot memory) {
+        return _slots[slotId];
+    }
+
+    function generateSlotId(RequestId requestId, uint256 slotIndex) public pure returns (SlotId) {
+        return Requests.slotId(requestId, slotIndex);
+    }
+}
diff --git a/certora/specs/Marketplace.spec b/certora/specs/Marketplace.spec
index 541793e..1645cba 100644
--- a/certora/specs/Marketplace.spec
+++ b/certora/specs/Marketplace.spec
@@ -4,6 +4,7 @@ methods {
     function Token.balanceOf(address) external returns (uint256) envfree;
     function Token.totalSupply() external returns (uint256) envfree;
     function publicPeriodEnd(Periods.Period) external returns (uint256) envfree;
+    function generateSlotId(Marketplace.RequestId, uint256) external returns (Marketplace.SlotId) envfree;
 }
 
 /*--------------------------------------------
@@ -160,6 +161,22 @@ function canFailRequest(method f) returns bool {
         f.selector == sig:freeSlot(Marketplace.SlotId).selector;
 }
 
+function canMakeSlotPaid(method f) returns bool {
+    return f.selector == sig:freeSlot(Marketplace.SlotId, address, address).selector ||
+        f.selector == sig:freeSlot(Marketplace.SlotId).selector;
+}
+
+function canFillSlot(method f) returns bool {
+    return f.selector == sig:fillSlot(Marketplace.RequestId, uint256, Marketplace.Groth16Proof).selector;
+}
+
+// The slot identified by `slotId` must have requestId and slotIndex set to 0,
+// or to values that satisfied slotId == keccak(requestId, slotIndex)
+function slotAttributesAreConsistent(env e, Marketplace.SlotId slotId) {
+    require (currentContract.slots(e, slotId).requestId == to_bytes32(0) && currentContract.slots(e, slotId).slotIndex == 0) ||
+        slotId == currentContract.generateSlotId(e, currentContract.slots(e, slotId).requestId, currentContract.slots(e, slotId).slotIndex);
+}
+
 /*--------------------------------------------
 |                 Invariants                 |
 --------------------------------------------*/
@@ -274,7 +291,7 @@ rule allowedRequestStateChanges(env e, method f) {
 
     Marketplace.RequestId requestId = slotIdToRequestId[slotId];
 
-    // needed, otherwise it finds counter examples where 
+    // needed, otherwise it finds counter examples where
     // `SlotState.Cancelled` and `RequestState.New`
     requireInvariant cancelledSlotAlwaysHasCancelledRequest(e, slotId);
     // needed, otherwise it finds counter example where
@@ -286,11 +303,11 @@ rule allowedRequestStateChanges(env e, method f) {
     // However, `requestId == 0` enforces `SlotState.Free` in the `fillSlot` function regardless,
     // which ultimately results in counter examples where we have a state change
     // RequestState.Cancelled -> RequestState.Finished, which is forbidden.
-    // 
+    //
     // COUNTER EXAMPLE: https://prover.certora.com/output/6199/3a4f410e6367422ba60b218a08c04fae?anonymousKey=0d7003af4ee9bc18c0da0c80a216a6815d397370
-    // 
-    // The `require` below is a hack to ensure we exclude such cases as the code 
-    // reverts in `requestIsKnown()` modifier (simply `require requestId != 0` isn't 
+    //
+    // The `require` below is a hack to ensure we exclude such cases as the code
+    // reverts in `requestIsKnown()` modifier (simply `require requestId != 0` isn't
     // sufficient here)
     require requestId == to_bytes32(0) => currentContract._requests[requestId].client == 0;
 
@@ -341,6 +358,25 @@ rule functionsCausingRequestStateChanges(env e, method f) {
     assert requestStateBefore == Marketplace.RequestState.Started && requestStateAfter == Marketplace.RequestState.Failed => canFailRequest(f);
 }
 
+rule functionsCausingSlotStateChanges(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);
+
+    // SlotState.Finished -> SlotState.Paid
+    assert slotStateBefore == Marketplace.SlotState.Finished && slotStateAfter == Marketplace.SlotState.Paid => canMakeSlotPaid(f);
+
+    // SlotState.Free -> SlotState.Filled
+    assert slotStateBefore != Marketplace.SlotState.Filled && slotStateAfter == Marketplace.SlotState.Filled => canFillSlot(f);
+    assert slotStateBefore != Marketplace.SlotState.Filled && slotStateAfter == Marketplace.SlotState.Filled => slotStateBefore == Marketplace.SlotState.Free;
+}
+
 rule cancelledRequestsStayCancelled(env e, method f) {
 
     calldataarg args;