From 2e3f775a0da8a3b7d5d018233176563f888a41cf Mon Sep 17 00:00:00 2001
From: r4bbit <445106+0x-r4bbit@users.noreply.github.com>
Date: Mon, 5 Aug 2024 16:27:20 +0200
Subject: [PATCH] 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         |  3 +-
 certora/harness/MarketplaceHarness.sol | 18 +++++++
 certora/specs/Marketplace.spec         | 72 ++++++++++++++++++++++++++
 contracts/Marketplace.sol              |  2 +-
 4 files changed, 93 insertions(+), 2 deletions(-)
 create mode 100644 certora/harness/MarketplaceHarness.sol

diff --git a/certora/confs/Marketplace.conf b/certora/confs/Marketplace.conf
index 5caa384..658f55c 100644
--- a/certora/confs/Marketplace.conf
+++ b/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,
diff --git a/certora/harness/MarketplaceHarness.sol b/certora/harness/MarketplaceHarness.sol
new file mode 100644
index 0000000..272fe9c
--- /dev/null
+++ b/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];
+    }
+}
+
diff --git a/certora/specs/Marketplace.spec b/certora/specs/Marketplace.spec
index af013bc..75dc1eb 100644
--- a/certora/specs/Marketplace.spec
+++ b/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;
+}
diff --git a/contracts/Marketplace.sol b/contracts/Marketplace.sol
index 4ea1b6f..e6763ce 100644
--- a/contracts/Marketplace.sol
+++ b/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;