diff --git a/certora/harness/MarketplaceHarness.sol b/certora/harness/MarketplaceHarness.sol index 272fe9c..c2f118a 100644 --- a/certora/harness/MarketplaceHarness.sol +++ b/certora/harness/MarketplaceHarness.sol @@ -14,5 +14,9 @@ contract MarketplaceHarness is Marketplace { function requestContext(RequestId requestId) public returns (Marketplace.RequestContext memory) { return _requestContexts[requestId]; } + + function publicPeriodEnd(Period period) public view returns (uint256) { + return _periodEnd(period); + } } diff --git a/certora/specs/Marketplace.spec b/certora/specs/Marketplace.spec index 43475d6..eab3619 100644 --- a/certora/specs/Marketplace.spec +++ b/certora/specs/Marketplace.spec @@ -3,6 +3,7 @@ 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 (uint256) envfree; } /*-------------------------------------------- @@ -41,6 +42,27 @@ hook Sstore currentContract._marketplaceTotals.sent uint256 defaultValue (uint25 totalSent = totalSent + defaultValue - defaultValue_old; } +ghost uint256 lastBlockTimestampGhost; + +hook TIMESTAMP uint v { + require lastBlockTimestampGhost <= v; + lastBlockTimestampGhost = v; +} + +ghost mapping(MarketplaceHarness.SlotId => mapping(Periods.Period => bool)) _missingMirror { + init_state axiom forall MarketplaceHarness.SlotId a. + forall Periods.Period b. + _missingMirror[a][b] == false; +} + +hook Sload bool defaultValue _missing[KEY MarketplaceHarness.SlotId slotId][KEY Periods.Period period] { + require _missingMirror[slotId][period] == defaultValue; +} + +hook Sstore _missing[KEY MarketplaceHarness.SlotId slotId][KEY Periods.Period period] bool defaultValue { + _missingMirror[slotId][period] = defaultValue; +} + /*-------------------------------------------- | Helper functions | --------------------------------------------*/ @@ -72,6 +94,12 @@ invariant totalSupplyIsSumOfBalances() 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; +// STATUS - verified +// can set missing if period was passed +// https://prover.certora.com/output/3106/026b36c118e44ad0824a51c50647c497/?anonymousKey=29879706f3d343555bb6122d071c9409d4e9876d +invariant cantBeMissedIfInPeriod(MarketplaceHarness.SlotId slotId, Periods.Period period) + lastBlockTimestampGhost <= publicPeriodEnd(period) => !_missingMirror[slotId][period]; + /*-------------------------------------------- | Properties | --------------------------------------------*/