fix(certora): fix rule that describes allowed request state changes

This broke due to a newly introduced signature for `fillSlot()`
This commit is contained in:
r4bbit 2024-08-21 21:12:26 +02:00
parent faeb808d41
commit 09ca8481fb
1 changed files with 7 additions and 2 deletions

View File

@ -120,12 +120,14 @@ function canStartRequest(method f) returns bool {
}
function canFinishRequest(method f) returns bool {
return f.selector == sig:freeSlot(Marketplace.SlotId, address, address).selector;
return f.selector == sig:freeSlot(Marketplace.SlotId, address, address).selector ||
f.selector == sig:freeSlot(Marketplace.SlotId).selector;
}
function canFailRequest(method f) returns bool {
return f.selector == sig:markProofAsMissing(Marketplace.SlotId, Periods.Period).selector ||
f.selector == sig:freeSlot(Marketplace.SlotId, address, address).selector;
f.selector == sig:freeSlot(Marketplace.SlotId, address, address).selector ||
f.selector == sig:freeSlot(Marketplace.SlotId).selector;
}
/*--------------------------------------------
@ -262,6 +264,9 @@ rule functionsCausingRequestStateChanges(env e, method f) {
// RequestState.New -> RequestState.Started
assert requestStateBefore == Marketplace.RequestState.New && requestStateAfter == Marketplace.RequestState.Started => canStartRequest(f);
// RequestState.New -> RequestState.Cancelled
assert requestStateBefore == Marketplace.RequestState.New && requestStateAfter == Marketplace.RequestState.Cancelled => canCancelRequest(f);
// RequestState.Started -> RequestState.Finished
assert requestStateBefore == Marketplace.RequestState.Started && requestStateAfter == Marketplace.RequestState.Finished => canFinishRequest(f);