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): verify SlotState and RequestState changes count 

This adds a rule to formally verify that the `SlotState` and
`RequestState` of any given `Slot` or `Request` does not change more
than once per function call.

Closes #129
This commit is contained in:
r4bbit 2024-08-13 14:16:12 +02:00
parent ed428767b3
commit a27da9738a
1 changed files with 43 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

43
certora/specs/Marketplace.spec
View File

@ -63,6 +63,27 @@ hook Sstore _missing[KEY MarketplaceHarness.SlotId slotId][KEY Periods.Period pe
_missingMirror[slotId][period] = defaultValue;
}
ghost mathint requestStateChangesCount {
init_state axiom requestStateChangesCount == 0;
}
hook Sstore _requestContexts[KEY Marketplace.RequestId requestId].state Marketplace.RequestState newState (Marketplace.RequestState oldState) {
if (oldState != newState) {
requestStateChangesCount = requestStateChangesCount + 1;
}
}
ghost mathint slotStateChangesCount {
init_state axiom slotStateChangesCount == 0;
}
hook Sstore _slots[KEY Marketplace.SlotId slotId].state Marketplace.SlotState newState (Marketplace.SlotState oldState) {
if (oldState != newState) {
slotStateChangesCount = slotStateChangesCount + 1;
}
}
/*--------------------------------------------
| Helper functions |
--------------------------------------------*/
@ -180,3 +201,25 @@ rule finishedRequestCannotBeStartedAgain(env e, method f) {
assert requestStateBefore == requestStateAfter;
}
rule requestStateChangesOnlyOncePerFunctionCall(env e, method f) {
calldataarg args;
Marketplace.RequestId requestId;
mathint requestStateChangesCountBefore = requestStateChangesCount;
f(e, args);
mathint requestStateChangesCountAfter = requestStateChangesCount;
assert requestStateChangesCountAfter <= requestStateChangesCountBefore + 1;
}
rule slotStateChangesOnlyOncePerFunctionCall(env e, method f) {
calldataarg args;
Marketplace.SlotId slotId;
mathint slotStateChangesCountBefore = slotStateChangesCount;
f(e, args);
mathint slotStateChangesCountAfter =slotStateChangesCount;
assert slotStateChangesCountAfter <= slotStateChangesCountBefore + 1;
}