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

fix(certora): fix rule that missed slots == number of issed periods

This commit is contained in:
r4bbit 2024-08-21 20:22:39 +02:00
parent 92ab1e50dd
commit ebdf9ed366
2 changed files with 17 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
certora/harness/MarketplaceHarness.sol
View File

@ -6,7 +6,7 @@ import {IERC20} from "@openzeppelin/contracts/token/ERC20/IERC20.sol";
import {IGroth16Verifier} from "../../contracts/Groth16.sol"; import {IGroth16Verifier} from "../../contracts/Groth16.sol";
import {MarketplaceConfig} from "../../contracts/Configuration.sol"; import {MarketplaceConfig} from "../../contracts/Configuration.sol";
import {Marketplace} from "../../contracts/Marketplace.sol"; import {Marketplace} from "../../contracts/Marketplace.sol";
import {RequestId} from "../../contracts/Requests.sol"; import {RequestId, SlotId} from "../../contracts/Requests.sol";
contract MarketplaceHarness is Marketplace { 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) {}
@ -15,6 +15,10 @@ contract MarketplaceHarness is Marketplace {
return _requestContexts[requestId]; return _requestContexts[requestId];
} }
function slots(SlotId slotId) public returns (Marketplace.Slot memory) {
return _slots[slotId];
}
function publicPeriodEnd(Period period) public view returns (uint256) { function publicPeriodEnd(Period period) public view returns (uint256) {
return _periodEnd(period); return _periodEnd(period);
} }

13
certora/specs/Marketplace.spec
View File

@ -71,11 +71,20 @@ hook Sload bool defaultValue _missing[KEY MarketplaceHarness.SlotId slotId][KEY
hook Sstore _missing[KEY MarketplaceHarness.SlotId slotId][KEY Periods.Period period] bool defaultValue { hook Sstore _missing[KEY MarketplaceHarness.SlotId slotId][KEY Periods.Period period] bool defaultValue {
_missingMirror[slotId][period] = defaultValue; _missingMirror[slotId][period] = defaultValue;
_missedCalculated[slotId] = _missedCalculated[slotId] + 1; if (defaultValue) {
_missedCalculated[slotId] = _missedCalculated[slotId] + 1;
}
}
hook Sload uint256 defaultValue _missed[KEY MarketplaceHarness.SlotId slotId] {
require _missedMirror[slotId] == defaultValue;
} }
hook Sstore _missed[KEY MarketplaceHarness.SlotId slotId] uint256 defaultValue { hook Sstore _missed[KEY MarketplaceHarness.SlotId slotId] uint256 defaultValue {
_missedMirror[slotId] = defaultValue; _missedMirror[slotId] = defaultValue;
if (defaultValue == 0) {
_missedCalculated[slotId] = 0;
}
} }
ghost mathint requestStateChangesCount { ghost mathint requestStateChangesCount {
@ -129,6 +138,8 @@ invariant totalSupplyIsSumOfBalances()
invariant requestStartedWhenSlotsFilled(env e, Marketplace.RequestId requestId, Marketplace.SlotId slotId) invariant requestStartedWhenSlotsFilled(env e, Marketplace.RequestId requestId, Marketplace.SlotId slotId)
to_mathint(currentContract.requestContext(e, requestId).slotsFilled) == to_mathint(currentContract.getRequest(e, requestId).ask.slots) => currentContract.requestState(e, requestId) == Marketplace.RequestState.Started; to_mathint(currentContract.requestContext(e, requestId).slotsFilled) == to_mathint(currentContract.getRequest(e, requestId).ask.slots) => currentContract.requestState(e, requestId) == Marketplace.RequestState.Started;
// STATUS - verified
// https://prover.certora.com/output/6199/6e2383ea040347eabeeb1008bc257ae6?anonymousKey=e1a6a00310a44ed264b1f98b03fa29273e68fca9
invariant slotMissedShouldBeEqualToNumberOfMissedPeriods(env e, Marketplace.SlotId slotId) invariant slotMissedShouldBeEqualToNumberOfMissedPeriods(env e, Marketplace.SlotId slotId)
to_mathint(_missedMirror[slotId]) == _missedCalculated[slotId]; to_mathint(_missedMirror[slotId]) == _missedCalculated[slotId];