Skip to content

Commit

Permalink
chore(certora): add invariant that proofs cant be missing when in period
Browse files Browse the repository at this point in the history
This invariant verifies that any given proof cannot be marked as missing
if the slot period has not passed yet.
  • Loading branch information
0x-r4bbit committed Aug 13, 2024
1 parent e04f8ae commit 1d36256
Show file tree
Hide file tree
Showing 2 changed files with 32 additions and 0 deletions.
4 changes: 4 additions & 0 deletions certora/harness/MarketplaceHarness.sol
Original file line number Diff line number Diff line change
Expand Up @@ -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);
}
}

28 changes: 28 additions & 0 deletions certora/specs/Marketplace.spec
Original file line number Diff line number Diff line change
Expand Up @@ -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;
}

/*--------------------------------------------
Expand Down Expand Up @@ -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 |
--------------------------------------------*/
Expand Down Expand Up @@ -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 |
--------------------------------------------*/
Expand Down

0 comments on commit 1d36256

Please sign in to comment.