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

chore(certora): contract balance increases when new storage requests are added

This commit is contained in:
Andrea Franz 2024-08-27 11:08:33 +02:00
parent 6d319c76b9
commit 1e5c8df2fb
No known key found for this signature in database
GPG Key ID: 5514DDE0D12C9316
2 changed files with 72 additions and 7 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
certora/harness/MarketplaceHarness.sol
View File

@ -7,9 +7,12 @@ 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 {Request} 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 requestContext(RequestId requestId) public returns (Marketplace.RequestContext memory) {
return _requestContexts[requestId];
@ -23,4 +26,3 @@ contract MarketplaceHarness is Marketplace {
return _periodEnd(period);
}
}

63
certora/specs/Marketplace.spec
View File

@ -14,6 +14,14 @@ ghost mathint sumOfBalances {
init_state axiom sumOfBalances == 0;
}
ghost mathint requestsCount {
init_state axiom requestsCount == 0;
}
ghost mathint sumOfAllRequestPrices {
init_state axiom sumOfAllRequestPrices == 0;
}
hook Sload uint256 balance Token._balances[KEY address addr] {
require sumOfBalances >= to_mathint(balance);
}
@ -95,8 +103,22 @@ hook Sstore _requestContexts[KEY Marketplace.RequestId requestId].state Marketpl
if (oldState != newState) {
requestStateChangesCount = requestStateChangesCount + 1;
}
if (oldState == Marketplace.RequestState.New && newState == Marketplace.RequestState.Cancelled) {
uint256 duration = currentContract._requests[requestId].ask.duration;
uint256 slots = currentContract._requests[requestId].ask.slots;
uint256 reward = currentContract._requests[requestId].ask.reward;
sumOfAllRequestPrices = sumOfAllRequestPrices - reward * duration * slots;
}
}
hook Sstore _requests[KEY Marketplace.RequestId requestId].ask.reward uint256 value (uint256 oldValue) {
uint256 duration = currentContract._requests[requestId].ask.duration;
uint256 slots = currentContract._requests[requestId].ask.slots;
sumOfAllRequestPrices = sumOfAllRequestPrices + value * duration * slots;
}
ghost mathint slotStateChangesCount {
init_state axiom slotStateChangesCount == 0;
}
@ -107,6 +129,22 @@ hook Sstore _slots[KEY Marketplace.SlotId slotId].state Marketplace.SlotState ne
}
}
// hook Sstore _requests[KEY Marketplace.RequestId requestId].client address value (address oldValue) {
// if (oldValue == 0 && value != 0) {
// requestsCount = requestsCount + 1;
// }
// }
hook Sstore _requestsPerClient[KEY address client]._inner._values[INDEX uint i] bytes32 value (bytes32 oldValue) {
bytes32 zero = to_bytes32(0);
if (value != zero && oldValue == value) {
requestsCount = requestsCount + 1;
} else {
// commented out for now that we are only checking balance/requests increase
// requestsCount = requestsCount - 1;
}
}
/*--------------------------------------------
| Helper functions |
--------------------------------------------*/
@ -191,6 +229,9 @@ invariant cancelledSlotAlwaysHasCancelledRequest(env e, Marketplace.SlotId slotI
currentContract.slotState(e, slotId) == Marketplace.SlotState.Cancelled =>
currentContract.requestState(e, currentContract.slots(e, slotId).requestId) == Marketplace.RequestState.Cancelled;
invariant requestsCountIsGreaterOrEqualToZero()
requestsCount >= 0;
/*--------------------------------------------
| Properties |
--------------------------------------------*/
@ -374,3 +415,25 @@ rule slotStateChangesOnlyOncePerFunctionCall(env e, method f) {
assert slotStateChangesCountAfter <= slotStateChangesCountBefore + 1;
}
rule contractBalanceIncreasesWhenRequestsAmountIncreases(env e, method f) {
requireInvariant totalSupplyIsSumOfBalances();
requireInvariant requestsCountIsGreaterOrEqualToZero();
calldataarg args;
mathint balanceBefore = Token.balanceOf(e, currentContract);
mathint requestsCountBefore = requestsCount;
mathint sumOfAllRequestPricesBefore = sumOfAllRequestPrices;
require e.msg.sender != currentContract;
require e.msg.sender != 0;
f(e, args);
mathint balanceAfter = Token.balanceOf(e, currentContract);
mathint requestsCountAfter = requestsCount;
mathint sumOfAllRequestPricesAfter = sumOfAllRequestPrices;
assert requestsCountAfter > requestsCountBefore => sumOfAllRequestPricesAfter >= sumOfAllRequestPricesBefore;
assert requestsCountAfter > requestsCountBefore => balanceAfter >= balanceBefore + (sumOfAllRequestPricesAfter - sumOfAllRequestPricesBefore);
}