chore: formally verify request state changes

This commit adds CVL rule that formally verifies the state changes of
any given request in relation to the functions of the contract that can
cause them.

Closes #128

certora/confs/Marketplace.conf

@@ -1,5 +1,6 @@
 {
     "files": [
+        "certora/harness/MarketplaceHarness.sol",
         "contracts/Marketplace.sol",
         "contracts/Groth16Verifier.sol",
         "certora/helpers/ERC20A.sol",
@@ -11,7 +12,7 @@
     ],
     "msg": "Verifying Marketplace",
     "rule_sanity": "basic",
-    "verify": "Marketplace:certora/specs/Marketplace.spec",
+    "verify": "MarketplaceHarness:certora/specs/Marketplace.spec",
     "optimistic_loop": true,
     "loop_iter": "3",
     "optimistic_hashing": true,

certora/harness/MarketplaceHarness.sol

@@ -0,0 +1,18 @@
+// SPDX-License-Identifier: MIT
+
+pragma solidity ^0.8.23;
+
+import {IERC20} from "@openzeppelin/contracts/token/ERC20/IERC20.sol";
+import {IGroth16Verifier} from "../../contracts/Groth16.sol";
+import {MarketplaceConfig} from "../../contracts/Configuration.sol";
+import {Marketplace} from "../../contracts/Marketplace.sol";
+import {RequestId} from "../../contracts/Requests.sol";
+
+contract MarketplaceHarness is Marketplace {
+    constructor(MarketplaceConfig memory config, IERC20 token, IGroth16Verifier verifier) Marketplace(config, token, verifier) {}
+
+    function requestContext(RequestId requestId) public returns (Marketplace.RequestContext memory) {
+        return _requestContexts[requestId];
+    }
+}
+

certora/specs/Marketplace.spec

@@ -1,5 +1,9 @@
 using ERC20A as Token;
 
+methods {
+    function Token.balanceOf(address) external returns (uint256) envfree;
+}
+
 /*--------------------------------------------
 |              Ghosts and hooks              |
 --------------------------------------------*/
@@ -24,6 +28,26 @@ hook Sstore currentContract._marketplaceTotals.sent uint256 defaultValue (uint25
     totalSent = totalSent + defaultValue - defaultValue_old;
 }
 
+function canCancelRequest(method f) returns bool {
+    return f.selector == sig:withdrawFunds(Marketplace.RequestId).selector;
+}
+
+function canStartRequest(method f) returns bool {
+    return f.selector == sig:fillSlot(Marketplace.RequestId, uint256, Marketplace.Groth16Proof).selector;
+}
+
+function canFinishRequest(method f) returns bool {
+    return 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).selector;
+}
+
+invariant requestStartedWhenSlotsFilled(env e, Marketplace.RequestId requestId, Marketplace.SlotId slotId)
+    to_mathint(currentContract.requestContext(e, requestId).slotsFilled) == to_mathint(currentContract.getRequest(e, requestId).ask.slots) => currentContract.requestState(e, requestId) == Marketplace.RequestState.Started;
+
 /*--------------------------------------------
 |                 Properties                 |
 --------------------------------------------*/
@@ -56,3 +80,51 @@ rule totalSentCannotDecrease(env e, method f) {
 
     assert total_after >= total_before;
 }
+
+rule allowedRequestStateChanges(env e, method f) {
+    calldataarg args;
+    Marketplace.RequestId requestId;
+
+    Marketplace.RequestState requestStateBefore = currentContract.requestState(e, requestId);
+    f(e, args);
+    Marketplace.RequestState requestStateAfter = currentContract.requestState(e, requestId);
+
+    assert requestStateBefore != requestStateAfter && requestStateAfter == Marketplace.RequestState.Started => requestStateBefore == Marketplace.RequestState.New;
+    assert requestStateBefore != requestStateAfter && requestStateAfter == Marketplace.RequestState.Finished => requestStateBefore == Marketplace.RequestState.Started;
+    assert requestStateBefore != requestStateAfter && requestStateAfter == Marketplace.RequestState.Failed => requestStateBefore == Marketplace.RequestState.Started;
+    assert requestStateBefore != requestStateAfter && requestStateAfter == Marketplace.RequestState.Cancelled => requestStateBefore == Marketplace.RequestState.New;
+}
+
+rule functionsCausingRequestStateChanges(env e, method f) {
+    calldataarg args;
+    Marketplace.RequestId requestId;
+
+    Marketplace.RequestState requestStateBefore = currentContract.requestState(e, requestId);
+    f(e, args);
+    Marketplace.RequestState requestStateAfter = currentContract.requestState(e, requestId);
+
+    // RequestState.New -> RequestState.Started
+    assert requestStateBefore == Marketplace.RequestState.New && requestStateAfter == Marketplace.RequestState.Started => canStartRequest(f);
+
+    // RequestState.Started -> RequestState.Finished
+    assert requestStateBefore == Marketplace.RequestState.Started && requestStateAfter == Marketplace.RequestState.Finished => canFinishRequest(f);
+
+    // RequestState.Started -> RequestState.Failed
+    assert requestStateBefore == Marketplace.RequestState.Started && requestStateAfter == Marketplace.RequestState.Failed => canFailRequest(f);
+
+    // RequestState.New -> RequestState.Cancelled
+    assert requestStateBefore == Marketplace.RequestState.New && requestStateAfter == Marketplace.RequestState.Cancelled => canCancelRequest(f);
+}
+
+rule finishedRequestCannotBeStartedAgain(env e, method f) {
+
+    calldataarg args;
+    Marketplace.RequestId requestId;
+
+    Marketplace.RequestState requestStateBefore = currentContract.requestState(e, requestId);
+    require requestStateBefore == Marketplace.RequestState.Finished;
+    f(e, args);
+    Marketplace.RequestState requestStateAfter = currentContract.requestState(e, requestId);
+
+    assert requestStateBefore == requestStateAfter;
+}

contracts/Marketplace.sol

@@ -19,7 +19,7 @@ contract Marketplace is Proofs, StateRetrieval, Endian {
   MarketplaceConfig private _config;
 
   mapping(RequestId => Request) private _requests;
-  mapping(RequestId => RequestContext) private _requestContexts;
+  mapping(RequestId => RequestContext) internal _requestContexts;
   mapping(SlotId => Slot) internal _slots;
 
   MarketplaceTotals internal _marketplaceTotals;