WIP

certora/confs/Marketplace.conf

@@ -5,12 +5,12 @@
         "contracts/Groth16Verifier.sol",
         "certora/helpers/ERC20A.sol",
     ],
-    "parametric_contracts": ["Marketplace"],
+    "parametric_contracts": ["MarketplaceHarness"],
     "link" : [
-        "Marketplace:_token=ERC20A",
+        "MarketplaceHarness:_token=ERC20A",
-        "Marketplace:_verifier=Groth16Verifier"
+        "MarketplaceHarness:_verifier=Groth16Verifier"
     ],
-    "msg": "Verifying Marketplace",
+    "msg": "Verifying MarketplaceHarness",
     "rule_sanity": "basic",
     "verify": "MarketplaceHarness:certora/specs/Marketplace.spec",
     "optimistic_loop": true,

certora/harness/MarketplaceHarness.sol

@@ -6,7 +6,7 @@ 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";
+import {RequestId, SlotId} from "../../contracts/Requests.sol";
 
 contract MarketplaceHarness is Marketplace {
     constructor(MarketplaceConfig memory config, IERC20 token, IGroth16Verifier verifier) Marketplace(config, token, verifier) {}
@@ -15,6 +15,10 @@ contract MarketplaceHarness is Marketplace {
         return _requestContexts[requestId];
     }
 
+    function slots(SlotId slotId) public returns (Marketplace.Slot memory) {
+        return _slots[slotId];
+    }
+
     function publicPeriodEnd(Period period) public view returns (uint256) {
         return _periodEnd(period);
     }

certora/specs/Marketplace.spec

@@ -93,7 +93,8 @@ function canCancelRequest(method f) returns bool {
 }
 
 function canStartRequest(method f) returns bool {
-    return f.selector == sig:fillSlot(Marketplace.RequestId, uint256, Marketplace.Groth16Proof).selector;
+    return f.selector == sig:fillSlot(Marketplace.RequestId, uint256, Marketplace.Groth16Proof).selector ||
+        f.selector == sig:freeSlot(Marketplace.SlotId).selector;
 }
 
 function canFinishRequest(method f) returns bool {
@@ -113,7 +114,11 @@ invariant totalSupplyIsSumOfBalances()
     to_mathint(Token.totalSupply()) == sumOfBalances;
 
 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;
+    currentContract.requestState(e, requestId) == Marketplace.RequestState.Started => to_mathint(currentContract.getRequest(e, requestId).ask.slots) - to_mathint(currentContract.requestContext(e, requestId).slotsFilled) <= to_mathint(currentContract.getRequest(e, requestId).ask.maxSlotLoss);
+//     { preserved {
+//         require to_mathint(currentContract.requestContext(e, requestId).slotsFilled) <= to_mathint(currentContract.getRequest(e, requestId).ask.slots);
+//     }
+// }
 
 // STATUS - verified
 // can set missing if period was passed
@@ -121,6 +126,20 @@ invariant requestStartedWhenSlotsFilled(env e, Marketplace.RequestId requestId,
 invariant cantBeMissedIfInPeriod(MarketplaceHarness.SlotId slotId, Periods.Period period)
     lastBlockTimestampGhost <= publicPeriodEnd(period) => !_missingMirror[slotId][period];
 
+// STATUS - verified
+// cancelled request is always expired
+// https://prover.certora.com/output/6199/df88c16b9fb144ec88292df2346adb21?anonymousKey=2c76bd226b246bdd1b667d16c387519beaf94487
+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                 |
 --------------------------------------------*/
@@ -154,10 +173,28 @@ rule totalSentCannotDecrease(env e, method f) {
     assert total_after >= total_before;
 }
 
+rule slotFilledIFRequestIsFailed(env e, method f) {
+    calldataarg args;
+    Marketplace.SlotId slotId;
+
+    require currentContract.requestState(e, currentContract.slots(slotId).requestId) != Marketplace.RequestState.Failed;
+    f(e, args);
+    require currentContract.requestState(e, currentContract.slots(slotId).requestId) == Marketplace.RequestState.Failed;
+
+    assert currentContract.slotState(slotId) == Marketplace.SlotState.Failed;
+}
+
+
 rule allowedRequestStateChanges(env e, method f) {
     calldataarg args;
     Marketplace.RequestId requestId;
 
+    //requireInvariant cancelledRequestAlwaysExpired(e, requestId);
+    // requireInvariant failedRequestAlwaysEnded(e, requestId);
+    //require currentContract.requestContext(e, requestId).expiresAt < currentContract.requestContext(e, requestId).endsAt;
+
+    // require currentContract.slotState(e, slotId) == Marketplace.SlotState.Finished => currentContract.requestState(e, requestId) == Marketplace.RequestState.Finished;
+
     Marketplace.RequestState requestStateBefore = currentContract.requestState(e, requestId);
     f(e, args);
     Marketplace.RequestState requestStateAfter = currentContract.requestState(e, requestId);
@@ -179,17 +216,36 @@ rule functionsCausingRequestStateChanges(env e, method f) {
     // RequestState.New -> RequestState.Started
     assert requestStateBefore == Marketplace.RequestState.New && requestStateAfter == Marketplace.RequestState.Started => canStartRequest(f);
 
+    // RequestState.New -> RequestState.Cancelled
+    assert requestStateBefore == Marketplace.RequestState.New && requestStateAfter == Marketplace.RequestState.Cancelled => canCancelRequest(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
+    // RequestState.Finished -> RequestState.Started
-    assert requestStateBefore == Marketplace.RequestState.New && requestStateAfter == Marketplace.RequestState.Cancelled => canCancelRequest(f);
+    assert requestStateBefore == Marketplace.RequestState.Finished && requestStateAfter == Marketplace.RequestState.Started => canStartRequest(f);
 }
 
-rule finishedRequestCannotBeStartedAgain(env e, method f) {
+rule cancelledRequestsStayCancelled(env e, method f) {
+
+    calldataarg args;
+    Marketplace.RequestId requestId;
+
+    Marketplace.RequestState requestStateBefore = currentContract.requestState(e, requestId);
+
+    require requestStateBefore == Marketplace.RequestState.Cancelled;
+    requireInvariant cancelledRequestAlwaysExpired(e, requestId);
+
+    f(e, args);
+    Marketplace.RequestState requestStateAfter = currentContract.requestState(e, requestId);
+
+    assert requestStateAfter == requestStateBefore;
+}
+
+rule finishedRequestsStayFinished(env e, method f) {
 
     calldataarg args;
     Marketplace.RequestId requestId;

contracts/Marketplace.sol

@@ -118,7 +118,7 @@ contract Marketplace is Proofs, StateRetrieval, Endian {
     RequestId requestId,
     uint256 slotIndex,
     Groth16Proof calldata proof
-  ) public requestIsKnown(requestId) {
+  ) public requestIsKnown(requestId) requestNotFinished(requestId) {
     Request storage request = _requests[requestId];
     require(slotIndex < request.ask.slots, "Invalid slot");
 
@@ -127,7 +127,7 @@ contract Marketplace is Proofs, StateRetrieval, Endian {
     slot.requestId = requestId;
     slot.slotIndex = slotIndex;
 
-    require(slotState(slotId) == SlotState.Free, "Slot is not free");
+    require(slotState(slotId) == SlotState.Free, "Slot is not free"); // revert
 
     _startRequiringProofs(slotId, request.ask.proofProbability);
     submitProof(slotId, proof);
@@ -251,7 +251,7 @@ contract Marketplace is Proofs, StateRetrieval, Endian {
       context.state == RequestState.Started
     ) {
       context.state = RequestState.Failed;
-      context.endsAt = block.timestamp - 1;
+      context.endsAt = block.timestamp - 1; // Ended
       emit RequestFailed(requestId);
 
       // TODO: send client remaining funds
@@ -331,6 +331,14 @@ contract Marketplace is Proofs, StateRetrieval, Endian {
     _;
   }
 
+  modifier requestNotFinished(RequestId requestId) {
+    require(
+      _requestContexts[requestId].state != RequestState.Finished,
+      "Request is cancelled or finished"
+    );
+    _;
+  }
+
   function getRequest(
     RequestId requestId
   ) public view requestIsKnown(requestId) returns (Request memory) {
@@ -377,32 +385,32 @@ contract Marketplace is Proofs, StateRetrieval, Endian {
   function requestState(
     RequestId requestId
   ) public view requestIsKnown(requestId) returns (RequestState) {
-    RequestContext storage context = _requestContexts[requestId];
+    RequestContext storage context = _requestContexts[requestId]; // Cancelled
     if (
       context.state == RequestState.New &&
       block.timestamp > requestExpiry(requestId)
     ) {
       return RequestState.Cancelled;
     } else if (
-      context.state == RequestState.Started && block.timestamp > context.endsAt
+      (context.state == RequestState.Started || context.state == RequestState.New) && block.timestamp > context.endsAt
     ) {
       return RequestState.Finished;
     } else {
-      return context.state;
+      return context.state; // Cancelled
     }
   }
 
   function slotState(SlotId slotId) public view override returns (SlotState) {
-    Slot storage slot = _slots[slotId];
+    Slot storage slot = _slots[slotId]; // Free
     if (RequestId.unwrap(slot.requestId) == 0) {
       return SlotState.Free;
     }
-    RequestState reqState = requestState(slot.requestId);
     if (slot.state == SlotState.Paid) {
       return SlotState.Paid;
     }
+    RequestState reqState = requestState(slot.requestId); // Failed
     if (reqState == RequestState.Cancelled) {
-      return SlotState.Cancelled;
+      return SlotState.Cancelled; // Cancelled
     }
     if (reqState == RequestState.Finished) {
       return SlotState.Finished;