Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[WIP] spec: The contract has enough funds to pay back everything #169

Draft
wants to merge 1 commit into
base: master
Choose a base branch
from
Draft

[WIP] spec: The contract has enough funds to pay back everything #169

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 4 additions & 2 deletions certora/harness/MarketplaceHarness.sol
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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];
Expand All @@ -23,4 +26,3 @@ contract MarketplaceHarness is Marketplace {
return _periodEnd(period);
}
}

73 changes: 68 additions & 5 deletions certora/specs/Marketplace.spec
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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);
}
Expand Down Expand Up @@ -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;
}
Expand All @@ -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 |
--------------------------------------------*/
Expand Down Expand Up @@ -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;
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@gravityblast did we see counter examples where we had a negative request count?
Wondering otherwise how useful this invariant is.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@0x-r4bbit yes we had a run with requestsCount starting with -1 because the init_state axiom works only with invariants, so as discussed with the Certora team we need this invariant to make sure it's not a negative number in the rule


/*--------------------------------------------
| Properties |
--------------------------------------------*/
Expand Down Expand Up @@ -244,7 +285,7 @@ rule allowedRequestStateChanges(env e, method f) {

Marketplace.RequestId requestId = currentContract.slots(e, slotId).requestId;

// needed, otherwise it finds counter examples where
// needed, otherwise it finds counter examples where
// `SlotState.Cancelled` and `RequestState.New`
requireInvariant cancelledSlotAlwaysHasCancelledRequest(e, slotId);
// needed, otherwise it finds counter example where
Expand All @@ -256,11 +297,11 @@ rule allowedRequestStateChanges(env e, method f) {
// However, `requestId == 0` enforces `SlotState.Free` in the `fillSlot` function regardless,
// which ultimately results in counter examples where we have a state change
// RequestState.Cancelled -> RequestState.Finished, which is forbidden.
//
//
// COUNTER EXAMPLE: https://prover.certora.com/output/6199/3a4f410e6367422ba60b218a08c04fae?anonymousKey=0d7003af4ee9bc18c0da0c80a216a6815d397370
//
// The `require` below is a hack to ensure we exclude such cases as the code
// reverts in `requestIsKnown()` modifier (simply `require requestId != 0` isn't
//
// The `require` below is a hack to ensure we exclude such cases as the code
// reverts in `requestIsKnown()` modifier (simply `require requestId != 0` isn't
// sufficient here)
require requestId == to_bytes32(0) => currentContract._requests[requestId].client == 0;

Expand Down Expand Up @@ -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);
}
Loading