Use Vault in Marketplace

.github/workflows/ci.yml

@@ -32,11 +32,6 @@ jobs:
           node-version: 18.15
       - run: npm install
       - run: npm test
-      - uses: actions/cache@v4
-        with:
-          path: fuzzing/corpus
-          key: fuzzing
-      - run: npm run fuzz
 
   verify:
     runs-on: ubuntu-latest

Readme.md

@@ -14,10 +14,6 @@ To run the tests, execute the following commands:
     npm install
     npm test
 
-You can also run fuzzing tests (using [Echidna][echidna]) on the contracts:
-
-    npm run fuzz
-
 To start a local Ethereum node with the contracts deployed, execute:
 
     npm start

certora/confs/Marketplace.conf

@@ -2,12 +2,14 @@
     "files": [
         "certora/harness/MarketplaceHarness.sol",
         "contracts/Marketplace.sol",
+        "contracts/Vault.sol",
         "contracts/Groth16Verifier.sol",
         "certora/helpers/ERC20A.sol",
     ],
     "parametric_contracts": ["MarketplaceHarness"],
     "link" : [
-        "MarketplaceHarness:_token=ERC20A",
+        "Vault:_token=ERC20A",
+        "MarketplaceHarness:_vault=Vault",
         "MarketplaceHarness:_verifier=Groth16Verifier"
     ],
     "msg": "Verifying MarketplaceHarness",
@@ -18,5 +20,3 @@
     "optimistic_hashing": true,
     "hashing_length_bound": "512",
 }
-
-

certora/confs/StateChanges.conf

@@ -2,12 +2,14 @@
     "files": [
         "certora/harness/MarketplaceHarness.sol",
         "contracts/Marketplace.sol",
+        "contracts/Vault.sol",
         "contracts/Groth16Verifier.sol",
         "certora/helpers/ERC20A.sol",
     ],
     "parametric_contracts": ["MarketplaceHarness"],
     "link" : [
-        "MarketplaceHarness:_token=ERC20A",
+        "Vault:_token=ERC20A",
+        "MarketplaceHarness:_vault=Vault",
         "MarketplaceHarness:_verifier=Groth16Verifier"
     ],
     "msg": "Verifying StateChanges",

certora/harness/MarketplaceHarness.sol

@@ -2,19 +2,20 @@
 
 pragma solidity ^0.8.28;
 
-import {IERC20} from "@openzeppelin/contracts/token/ERC20/IERC20.sol";
+import {Vault} from "../../contracts/Vault.sol";
 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";
+import {Timestamp} from "../../contracts/Timestamps.sol";
 
 contract MarketplaceHarness is Marketplace {
-    constructor(MarketplaceConfig memory config, IERC20 token, IGroth16Verifier verifier)
-        Marketplace(config, token, verifier)
+    constructor(MarketplaceConfig memory config, Vault vault, IGroth16Verifier verifier)
+        Marketplace(config, vault, verifier)
     {}
 
-    function publicPeriodEnd(Period period) public view returns (uint64) {
+    function publicPeriodEnd(Period period) public view returns (Timestamp) {
         return _periodEnd(period);
     }
 

certora/specs/Marketplace.spec

@@ -3,54 +3,20 @@ import "./shared.spec";
 using ERC20A as Token;
 
 methods {
-    function Token.balanceOf(address) external returns (uint256) envfree;
-    function Token.totalSupply() external returns (uint256) envfree;
-    function publicPeriodEnd(Periods.Period) external returns (uint64) envfree;
+    function publicPeriodEnd(Periods.Period) external returns (Marketplace.Timestamp) envfree;
     function generateSlotId(Marketplace.RequestId, uint64) external returns (Marketplace.SlotId) envfree;
 }
 
 /*--------------------------------------------
 |              Ghosts and hooks              |
 --------------------------------------------*/
 
-ghost mathint sumOfBalances {
-    init_state axiom sumOfBalances == 0;
-}
-
-hook Sload uint256 balance Token._balances[KEY address addr] {
-    require sumOfBalances >= to_mathint(balance);
-}
-
-hook Sstore Token._balances[KEY address addr] uint256 newValue (uint256 oldValue) {
-    sumOfBalances = sumOfBalances - oldValue + newValue;
-}
-
-ghost mathint totalReceived;
-
-hook Sload uint256 defaultValue currentContract._marketplaceTotals.received {
-    require totalReceived >= to_mathint(defaultValue);
-}
-
-hook Sstore currentContract._marketplaceTotals.received uint256 defaultValue (uint256 defaultValue_old) {
-    totalReceived = totalReceived + defaultValue - defaultValue_old;
-}
-
-ghost mathint totalSent;
-
-hook Sload uint256 defaultValue currentContract._marketplaceTotals.sent {
-    require totalSent >= to_mathint(defaultValue);
-}
-
-hook Sstore currentContract._marketplaceTotals.sent uint256 defaultValue (uint256 defaultValue_old) {
-    totalSent = totalSent + defaultValue - defaultValue_old;
-}
-
-ghost uint64 lastBlockTimestampGhost;
+ghost Marketplace.Timestamp lastBlockTimestampGhost;
 
 hook TIMESTAMP uint v {
-    require v < max_uint64;
-    require lastBlockTimestampGhost <= assert_uint64(v);
-    lastBlockTimestampGhost = assert_uint64(v);
+    require v < max_uint40;
+    require lastBlockTimestampGhost <= assert_uint40(v);
+    lastBlockTimestampGhost = assert_uint40(v);
 }
 
 ghost mapping(MarketplaceHarness.SlotId => mapping(Periods.Period => bool)) _missingMirror {
@@ -121,13 +87,13 @@ hook Sstore _requestContexts[KEY MarketplaceHarness.RequestId RequestId].slotsFi
     slotsFilledGhost[RequestId] = defaultValue;
 }
 
-ghost mapping(MarketplaceHarness.RequestId => uint64) endsAtGhost;
+ghost mapping(MarketplaceHarness.RequestId => Marketplace.Timestamp) endsAtGhost;
 
-hook Sload uint64 defaultValue _requestContexts[KEY MarketplaceHarness.RequestId RequestId].endsAt {
+hook Sload Marketplace.Timestamp defaultValue _requestContexts[KEY MarketplaceHarness.RequestId RequestId].endsAt {
     require endsAtGhost[RequestId] == defaultValue;
 }
 
-hook Sstore _requestContexts[KEY MarketplaceHarness.RequestId RequestId].endsAt uint64 defaultValue {
+hook Sstore _requestContexts[KEY MarketplaceHarness.RequestId RequestId].endsAt Marketplace.Timestamp defaultValue {
     endsAtGhost[RequestId] = defaultValue;
 }
 
@@ -144,18 +110,11 @@ function canStartRequest(method f) returns bool {
 }
 
 function canFinishRequest(method f) returns bool {
-    return f.selector == sig:freeSlot(Marketplace.SlotId, address, address).selector ||
-        f.selector == sig:freeSlot(Marketplace.SlotId).selector;
+    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, address, address).selector ||
-        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;
 }
 
@@ -174,9 +133,6 @@ function slotAttributesAreConsistent(env e, Marketplace.SlotId slotId) {
 |                 Invariants                 |
 --------------------------------------------*/
 
-invariant totalSupplyIsSumOfBalances()
-    to_mathint(Token.totalSupply()) == sumOfBalances;
-
 invariant requestStartedWhenSlotsFilled(env e, Marketplace.RequestId requestId, Marketplace.SlotId slotId)
     currentContract.requestState(e, requestId) == Marketplace.RequestState.Started => to_mathint(currentContract.getRequest(e, requestId).ask.slots) - slotsFilledGhost[requestId] <= to_mathint(currentContract.getRequest(e, requestId).ask.maxSlotLoss);
 
@@ -198,25 +154,6 @@ 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/3c5e57311e474f26aa7d9e9481c5880a?anonymousKey=36e39932ee488bb35fe23e38d8d4091190e047af
-invariant failedRequestAlwaysEnded(env e, Marketplace.RequestId requestId)
-    currentContract.requestState(e, requestId) == Marketplace.RequestState.Failed =>
-        endsAtGhost[requestId] < lastBlockTimestampGhost;
-
-// STATUS - verified
-// paid slot always has finished or cancelled request
-// 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, slotIdToRequestId[slotId]) == Marketplace.RequestState.Finished || currentContract.requestState(e, slotIdToRequestId[slotId]) == Marketplace.RequestState.Cancelled
-    { preserved {
-        requireInvariant cancelledSlotAlwaysHasCancelledRequest(e, slotId);
-      }
-    }
-
-
 /*--------------------------------------------
 |                 Properties                 |
 --------------------------------------------*/
@@ -228,35 +165,11 @@ rule sanity(env e, method f) {
     satisfy true;
 }
 
-rule totalReceivedCannotDecrease(env e, method f) {
-    mathint total_before = totalReceived;
-
-    calldataarg args;
-    f(e, args);
-
-    mathint total_after = totalReceived;
-
-    assert total_after >= total_before;
-}
-
-rule totalSentCannotDecrease(env e, method f) {
-    mathint total_before = totalSent;
-
-    calldataarg args;
-    f(e, args);
-
-    mathint total_after = totalSent;
-
-    assert total_after >= total_before;
-}
-
 // https://prover.certora.com/output/6199/0b56a7cdb3f9466db08f2a4677eddaac?anonymousKey=351ce9d5561f6c2aff1b38942e307735428bb83f
 rule slotIsFailedOrFreeIfRequestHasFailed(env e, method f) {
     calldataarg args;
     Marketplace.SlotId slotId;
 
-    requireInvariant paidSlotAlwaysHasFinishedOrCancelledRequest(e, slotId);
-
     Marketplace.RequestState requestStateBefore = currentContract.requestState(e, slotIdToRequestId[slotId]);
     f(e, args);
     Marketplace.RequestState requestAfter = currentContract.requestState(e, slotIdToRequestId[slotId]);
@@ -298,9 +211,6 @@ rule functionsCausingSlotStateChanges(env e, method f) {
     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.Free || slotStateBefore == Marketplace.SlotState.Repair) && slotStateAfter == Marketplace.SlotState.Filled => canFillSlot(f);
 }
@@ -316,15 +226,11 @@ rule allowedSlotStateChanges(env e, method f) {
     f(e, args);
     Marketplace.SlotState slotStateAfter = currentContract.slotState(e, slotId);
 
-    // Cannot change from Paid
-    assert slotStateBefore == Marketplace.SlotState.Paid => slotStateAfter == Marketplace.SlotState.Paid;
-
-    // SlotState.Cancelled -> SlotState.Cancelled || SlotState.Failed || Finished || Paid
+    // SlotState.Cancelled -> SlotState.Cancelled || SlotState.Failed || Finished
     assert slotStateBefore == Marketplace.SlotState.Cancelled => (
             slotStateAfter == Marketplace.SlotState.Cancelled ||
             slotStateAfter == Marketplace.SlotState.Failed ||
-            slotStateAfter == Marketplace.SlotState.Finished ||
-            slotStateAfter == Marketplace.SlotState.Paid
+            slotStateAfter == Marketplace.SlotState.Finished
             );
 
     // SlotState.Filled only from Free or Repair
@@ -385,21 +291,3 @@ rule slotStateChangesOnlyOncePerFunctionCall(env e, method f) {
 
     assert slotStateChangesCountAfter <= slotStateChangesCountBefore + 1;
 }
-
-rule slotCanBeFreedAndPaidOnce {
-  env e;
-  Marketplace.SlotId slotId;
-  address rewardRecipient;
-  address collateralRecipient;
-
-  Marketplace.SlotState slotStateBefore = currentContract.slotState(e, slotId);
-  require slotStateBefore != Marketplace.SlotState.Paid;
-  freeSlot(e, slotId, rewardRecipient, collateralRecipient);
-
-  Marketplace.SlotState slotStateAfter = currentContract.slotState(e, slotId);
-  require slotStateAfter == Marketplace.SlotState.Paid;
-
-  freeSlot@withrevert(e, slotId, rewardRecipient, collateralRecipient);
-
-  assert lastReverted;
-}

certora/specs/StateChanges.spec

@@ -20,7 +20,7 @@ rule allowedRequestStateChanges(env e, method f) {
     // we need to check for `freeSlot(slotId)` here to ensure it's being called with
     // the slotId we're interested in and not any other slotId (that may not pass the
     // required invariants)
-    if (f.selector == sig:freeSlot(Marketplace.SlotId).selector || f.selector == sig:freeSlot(Marketplace.SlotId, address, address).selector) {
+    if (f.selector == sig:freeSlot(Marketplace.SlotId).selector) {
         freeSlot(e, slotId);
     } else {
         f(e, args);

contracts/Configuration.sol

@@ -2,12 +2,13 @@
 pragma solidity 0.8.28;
 
 import "@openzeppelin/contracts/token/ERC20/IERC20.sol";
+import "./Timestamps.sol";
 
 struct MarketplaceConfig {
   CollateralConfig collateral;
   ProofConfig proofs;
   SlotReservationsConfig reservations;
-  uint64 requestDurationLimit;
+  Duration requestDurationLimit;
 }
 
 struct CollateralConfig {
@@ -19,8 +20,8 @@ struct CollateralConfig {
 }
 
 struct ProofConfig {
-  uint64 period; // proofs requirements are calculated per period (in seconds)
-  uint64 timeout; // mark proofs as missing before the timeout (in seconds)
+  Duration period; // proofs requirements are calculated per period (in seconds)
+  Duration timeout; // mark proofs as missing before the timeout (in seconds)
   uint8 downtime; // ignore this much recent blocks for proof requirements
   // Ensures the pointer does not remain in downtime for many consecutive
   // periods. For each period increase, move the pointer `pointerProduct`