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

chore(certora): verify possible slot state transitions

This commit is contained in:
Andrea Franz 2024-08-29 16:33:23 +02:00
parent a5aa19453e
commit 3a074abd20
2 changed files with 53 additions and 7 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

14
certora/harness/MarketplaceHarness.sol
View File

@ -7,12 +7,22 @@ import {IGroth16Verifier} from "../../contracts/Groth16.sol";
import {MarketplaceConfig} from "../../contracts/Configuration.sol";
import {Marketplace} from "../../contracts/Marketplace.sol";
import {RequestId, SlotId} from "../../contracts/Requests.sol";
import {Requests} from "../../contracts/Requests.sol";
contract MarketplaceHarness is Marketplace {
constructor(MarketplaceConfig memory config, IERC20 token, IGroth16Verifier verifier) Marketplace(config, token, verifier) {}
constructor(MarketplaceConfig memory config, IERC20 token, IGroth16Verifier verifier)
Marketplace(config, token, verifier)
{}
function publicPeriodEnd(Period period) public view returns (uint256) {
return _periodEnd(period);
}
}
function slots(SlotId slotId) public view returns (Slot memory) {
return _slots[slotId];
}
function generateSlotId(RequestId requestId, uint256 slotIndex) public pure returns (SlotId) {
return Requests.slotId(requestId, slotIndex);
}
}

36
certora/specs/Marketplace.spec
View File

@ -4,6 +4,7 @@ methods {
function Token.balanceOf(address) external returns (uint256) envfree;
function Token.totalSupply() external returns (uint256) envfree;
function publicPeriodEnd(Periods.Period) external returns (uint256) envfree;
function generateSlotId(Marketplace.RequestId, uint256) external returns (Marketplace.SlotId) envfree;
}
/*--------------------------------------------
@ -160,6 +161,22 @@ function canFailRequest(method f) returns bool {
f.selector == sig:freeSlot(Marketplace.SlotId).selector;
}
function canMakeSlotPaid(method f) returns bool {
return f.selector == sig:freeSlot(Marketplace.SlotId, address, address).selector ||
f.selector == sig:freeSlot(Marketplace.SlotId).selector;
}
function canFillSlot(method f) returns bool {
return f.selector == sig:fillSlot(Marketplace.RequestId, uint256, Marketplace.Groth16Proof).selector;
}
// The slot identified by `slotId` must have requestId and slotIndex set to 0,
// or to values that satisfied slotId == keccak(requestId, slotIndex)
function slotAttributesAreConsistent(env e, Marketplace.SlotId slotId) {
require (currentContract.slots(e, slotId).requestId == to_bytes32(0) && currentContract.slots(e, slotId).slotIndex == 0) ||
slotId == currentContract.generateSlotId(e, currentContract.slots(e, slotId).requestId, currentContract.slots(e, slotId).slotIndex);
}
/*--------------------------------------------
| Invariants |
--------------------------------------------*/
@ -341,6 +358,25 @@ rule functionsCausingRequestStateChanges(env e, method f) {
assert requestStateBefore == Marketplace.RequestState.Started && requestStateAfter == Marketplace.RequestState.Failed => canFailRequest(f);
}
rule functionsCausingSlotStateChanges(env e, method f) {
calldataarg args;
Marketplace.SlotId slotId;
slotAttributesAreConsistent(e, slotId);
Marketplace.Slot slot = currentContract.slots(e, slotId);
Marketplace.SlotState slotStateBefore = currentContract.slotState(e, slotId);
f(e, args);
Marketplace.SlotState slotStateAfter = currentContract.slotState(e, slotId);
// SlotState.Finished -> SlotState.Paid
assert slotStateBefore == Marketplace.SlotState.Finished && slotStateAfter == Marketplace.SlotState.Paid => canMakeSlotPaid(f);
// SlotState.Free -> SlotState.Filled
assert slotStateBefore != Marketplace.SlotState.Filled && slotStateAfter == Marketplace.SlotState.Filled => canFillSlot(f);
assert slotStateBefore != Marketplace.SlotState.Filled && slotStateAfter == Marketplace.SlotState.Filled => slotStateBefore == Marketplace.SlotState.Free;
}
rule cancelledRequestsStayCancelled(env e, method f) {
calldataarg args;