status-im
/
dagger-contracts
mirror of https://github.com/status-im/dagger-contracts.git
2
0
Fork 0
Code Issues Projects Releases Wiki Activity

chore(certora): slot's missed periods count should be equal to the count of slot's missing periods set to true (#155)

This commit is contained in:
Andrea Franz 2024-08-15 12:51:14 +02:00 committed by GitHub
parent a27da9738a
commit 29f39d52c7
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
2 changed files with 23 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

27
certora/specs/Marketplace.spec
View File

@ -50,17 +50,32 @@ hook TIMESTAMP uint v {
}
ghost mapping(MarketplaceHarness.SlotId => mapping(Periods.Period => bool)) _missingMirror {
init_state axiom forall MarketplaceHarness.SlotId a.
forall Periods.Period b.
init_state axiom forall MarketplaceHarness.SlotId a.
forall Periods.Period b.
_missingMirror[a][b] == false;
}
ghost mapping(MarketplaceHarness.SlotId => uint256) _missedMirror {
init_state axiom forall MarketplaceHarness.SlotId a.
_missedMirror[a] == 0;
}
ghost mapping(MarketplaceHarness.SlotId => mathint) _missedCalculated {
init_state axiom forall MarketplaceHarness.SlotId a.
_missedCalculated[a] == 0;
}
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;
_missedCalculated[slotId] = _missedCalculated[slotId] + 1;
}
hook Sstore _missed[KEY MarketplaceHarness.SlotId slotId] uint256 defaultValue {
_missedMirror[slotId] = defaultValue;
}
ghost mathint requestStateChangesCount {
@ -83,7 +98,6 @@ hook Sstore _slots[KEY Marketplace.SlotId slotId].state Marketplace.SlotState ne
}
}
/*--------------------------------------------
| Helper functions |
--------------------------------------------*/
@ -101,7 +115,7 @@ function canFinishRequest(method f) returns bool {
}
function canFailRequest(method f) returns bool {
return f.selector == sig:markProofAsMissing(Marketplace.SlotId, Periods.Period).selector ||
return f.selector == sig:markProofAsMissing(Marketplace.SlotId, Periods.Period).selector ||
f.selector == sig:freeSlot(Marketplace.SlotId).selector;
}
@ -115,6 +129,9 @@ 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;
invariant slotMissedShouldBeEqualToNumberOfMissedPeriods(env e, Marketplace.SlotId slotId)
to_mathint(_missedMirror[slotId]) == _missedCalculated[slotId];
// STATUS - verified
// can set missing if period was passed
// https://prover.certora.com/output/3106/026b36c118e44ad0824a51c50647c497/?anonymousKey=29879706f3d343555bb6122d071c9409d4e9876d
@ -219,7 +236,7 @@ rule slotStateChangesOnlyOncePerFunctionCall(env e, method f) {
mathint slotStateChangesCountBefore = slotStateChangesCount;
f(e, args);
mathint slotStateChangesCountAfter =slotStateChangesCount;
mathint slotStateChangesCountAfter =slotStateChangesCount;
assert slotStateChangesCountAfter <= slotStateChangesCountBefore + 1;
}

1
contracts/Proofs.sol
View File

@ -203,6 +203,7 @@ abstract contract Proofs is Periods {
* @dev Reverts when:
* - missedPeriod has not ended yet ended
* - missing proof was time-barred
* - proof was submitted
* - proof was not required for missedPeriod period
* - proof was already marked as missing
*/