43 lines
2.0 KiB
Plaintext
43 lines
2.0 KiB
Plaintext
|
import "./shared.spec";
|
||
|
|
|
||
|
|
rule allowedRequestStateChanges(env e, method f) {
|
||
|
|
calldataarg args;
|
||
|
|
Marketplace.SlotId slotId;
|
||
|
|
|
||
|
|
Marketplace.RequestId requestId = slotIdToRequestId[slotId];
|
||
|
|
|
||
|
|
// needed, otherwise it finds counter examples where
|
||
|
|
// `SlotState.Cancelled` and `RequestState.New`
|
||
|
|
requireInvariant cancelledSlotAlwaysHasCancelledRequest(e, slotId);
|
||
|
|
// needed, otherwise it finds counter example where
|
||
|
|
// `SlotState.Finished` and `RequestState.New`
|
||
|
|
requireInvariant finishedSlotAlwaysHasFinishedRequest(e, slotId);
|
||
|
|
|
||
|
|
ensureValidRequestId(requestId);
|
||
|
|
|
||
|
|
Marketplace.RequestState requestStateBefore = currentContract.requestState(e, requestId);
|
||
|
|
|
||
|
|
// we need to check for `freeSlot(slotId)` here to ensure it's being called with
|
||
|
|
// the slotId we're interested in and not any other slotId (that may not pass the
|
||
|
|
// required invariants)
|
||
|
|
if (f.selector == sig:freeSlot(Marketplace.SlotId).selector || f.selector == sig:freeSlot(Marketplace.SlotId, address, address).selector) {
|
||
|
|
freeSlot(e, slotId);
|
||
|
|
} else {
|
||
|
|
f(e, args);
|
||
|
|
}
|
||
|
|
Marketplace.RequestState requestStateAfter = currentContract.requestState(e, requestId);
|
||
|
|
|
||
|
|
// RequestState.New -> RequestState.Started
|
||
|
|
assert requestStateBefore != requestStateAfter && requestStateAfter == Marketplace.RequestState.Started => requestStateBefore == Marketplace.RequestState.New;
|
||
|
|
|
||
|
|
// RequestState.Started -> RequestState.Finished
|
||
|
|
assert requestStateBefore != requestStateAfter && requestStateAfter == Marketplace.RequestState.Finished => requestStateBefore == Marketplace.RequestState.Started;
|
||
|
|
|
||
|
|
// RequestState.Started -> RequestState.Failed
|
||
|
|
assert requestStateBefore != requestStateAfter && requestStateAfter == Marketplace.RequestState.Failed => requestStateBefore == Marketplace.RequestState.Started;
|
||
|
|
|
||
|
|
// RequestState.New -> RequestState.Cancelled
|
||
|
|
assert requestStateBefore != requestStateAfter && requestStateAfter == Marketplace.RequestState.Cancelled => requestStateBefore == Marketplace.RequestState.New;
|
||
|
|
}
|
||
|
|
|