diff --git a/certora/confs/Marketplace.conf b/certora/confs/Marketplace.conf index 658f55c..2dc6fe4 100644 --- a/certora/confs/Marketplace.conf +++ b/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", - "Marketplace:_verifier=Groth16Verifier" + "MarketplaceHarness:_token=ERC20A", + "MarketplaceHarness:_verifier=Groth16Verifier" ], - "msg": "Verifying Marketplace", + "msg": "Verifying MarketplaceHarness", "rule_sanity": "basic", "verify": "MarketplaceHarness:certora/specs/Marketplace.spec", "optimistic_loop": true, diff --git a/certora/harness/MarketplaceHarness.sol b/certora/harness/MarketplaceHarness.sol index c2f118a..318c390 100644 --- a/certora/harness/MarketplaceHarness.sol +++ b/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); } diff --git a/certora/specs/Marketplace.spec b/certora/specs/Marketplace.spec index b9feb97..e9571dd 100644 --- a/certora/specs/Marketplace.spec +++ b/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 - assert requestStateBefore == Marketplace.RequestState.New && requestStateAfter == Marketplace.RequestState.Cancelled => canCancelRequest(f); + // RequestState.Finished -> RequestState.Started + 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; diff --git a/contracts/Marketplace.sol b/contracts/Marketplace.sol index e6763ce..a999848 100644 --- a/contracts/Marketplace.sol +++ b/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;