codex-storage
/
codex-contracts-eth
mirror of https://github.com/codex-storage/codex-contracts-eth.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

WIP

This commit is contained in:
Andrea Franz 2024-08-16 18:11:24 +02:00
parent e45724f825
commit ba42fb3428
No known key found for this signature in database
GPG Key ID: 5514DDE0D12C9316
2 changed files with 34 additions and 11 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
certora/confs/Marketplace.conf
View File

@ -17,6 +17,7 @@
"loop_iter": "3",
"optimistic_hashing": true,
"hashing_length_bound": "512",
"rule": "requestContextStateCanChangeToFailedOnlyWhenSlotIsFilled"
}

44
certora/specs/Marketplace.spec
View File

@ -173,16 +173,16 @@ rule totalSentCannotDecrease(env e, method f) {
assert total_after >= total_before;
}
rule slotFilledIFRequestIsFailed(env e, method f) {
calldataarg args;
Marketplace.SlotId slotId;
require currentContract.requestState(e, currentContract.slots(slotId).requestId) != Marketplace.RequestState.Failed;
f(e, args);
require currentContract.requestState(e, currentContract.slots(slotId).requestId) == Marketplace.RequestState.Failed;
assert currentContract.slotState(slotId) == Marketplace.SlotState.Failed;
}
//rule slotFilledIFRequestIsFailed(env e, method f) {
// calldataarg args;
// Marketplace.SlotId slotId;
//
// require currentContract.requestState(e, currentContract.slots(slotId).requestId) != Marketplace.RequestState.Failed;
// f(e, args);
// require currentContract.requestState(e, currentContract.slots(slotId).requestId) == Marketplace.RequestState.Failed;
//
// assert currentContract.slotState(slotId) == Marketplace.SlotState.Failed;
//}
rule allowedRequestStateChanges(env e, method f) {
@ -275,7 +275,29 @@ rule slotStateChangesOnlyOncePerFunctionCall(env e, method f) {
mathint slotStateChangesCountBefore = slotStateChangesCount;
f(e, args);
mathint slotStateChangesCountAfter =slotStateChangesCount;
mathint slotStateChangesCountAfter =slotStateChangesCount;
assert slotStateChangesCountAfter <= slotStateChangesCountBefore + 1;
}
rule requestContextStateCanChangeToFailedOnlyWhenSlotIsFilled(env e, method f) {
calldataarg args;
Marketplace.SlotId slotId;
Marketplace.RequestId requestId = currentContract.slots(e, slotId).requestId;
// check only cases where the request is not already failed
Marketplace.RequestState requestStateBefore = currentContract.requestState(e, requestId);
require requestStateBefore != Marketplace.RequestState.Failed;
Marketplace.SlotState slotComputedStateBefore = currentContract.slotState(e, slotId);
require slotComputedStateBefore != Marketplace.SlotState.Failed &&
slotComputedStateBefore != Marketplace.SlotState.Cancelled &&
slotComputedStateBefore != Marketplace.SlotState.Finished;
f(e, args);
// check if the slotState function returns Failed (the actual storage variable won't be failed)
assert currentContract.slotState(e, slotId) == Marketplace.SlotState.Failed => slotComputedStateBefore == Marketplace.SlotState.Filled;
//assert currentContract.slotState(e, slotId) == Marketplace.SlotState.Failed => currentContract.requestState(e, requestId) == Marketplace.RequestState.Failed;
//assert currentContract.slotState(e, slotId) == Marketplace.SlotState.Failed => currentContract.requestContext(e, requestId).state == Marketplace.RequestState.Failed;
}