mirror of
https://github.com/status-im/dagger-contracts.git
synced 2025-01-09 22:05:50 +00:00
e04f8ae909
This invariant ensures that the total supply of the used token in the contract is always greater equal to the sum of all balances within the token combined.
155 lines
5.7 KiB
Ruby
155 lines
5.7 KiB
Ruby
using ERC20A as Token;
|
|
|
|
methods {
|
|
function Token.balanceOf(address) external returns (uint256) envfree;
|
|
function Token.totalSupply() external returns (uint256) envfree;
|
|
}
|
|
|
|
/*--------------------------------------------
|
|
| Ghosts and hooks |
|
|
--------------------------------------------*/
|
|
|
|
ghost mathint sumOfBalances {
|
|
init_state axiom sumOfBalances == 0;
|
|
}
|
|
|
|
hook Sload uint256 balance Token._balances[KEY address addr] {
|
|
require sumOfBalances >= to_mathint(balance);
|
|
}
|
|
|
|
hook Sstore Token._balances[KEY address addr] uint256 newValue (uint256 oldValue) {
|
|
sumOfBalances = sumOfBalances - oldValue + newValue;
|
|
}
|
|
|
|
ghost mathint totalReceived;
|
|
|
|
hook Sload uint256 defaultValue currentContract._marketplaceTotals.received {
|
|
require totalReceived >= to_mathint(defaultValue);
|
|
}
|
|
|
|
hook Sstore currentContract._marketplaceTotals.received uint256 defaultValue (uint256 defaultValue_old) {
|
|
totalReceived = totalReceived + defaultValue - defaultValue_old;
|
|
}
|
|
|
|
ghost mathint totalSent;
|
|
|
|
hook Sload uint256 defaultValue currentContract._marketplaceTotals.sent {
|
|
require totalSent >= to_mathint(defaultValue);
|
|
}
|
|
|
|
hook Sstore currentContract._marketplaceTotals.sent uint256 defaultValue (uint256 defaultValue_old) {
|
|
totalSent = totalSent + defaultValue - defaultValue_old;
|
|
}
|
|
|
|
/*--------------------------------------------
|
|
| Helper functions |
|
|
--------------------------------------------*/
|
|
|
|
function canCancelRequest(method f) returns bool {
|
|
return f.selector == sig:withdrawFunds(Marketplace.RequestId).selector;
|
|
}
|
|
|
|
function canStartRequest(method f) returns bool {
|
|
return f.selector == sig:fillSlot(Marketplace.RequestId, uint256, Marketplace.Groth16Proof).selector;
|
|
}
|
|
|
|
function canFinishRequest(method f) returns bool {
|
|
return f.selector == sig:freeSlot(Marketplace.SlotId).selector;
|
|
}
|
|
|
|
function canFailRequest(method f) returns bool {
|
|
return f.selector == sig:markProofAsMissing(Marketplace.SlotId, Periods.Period).selector ||
|
|
f.selector == sig:freeSlot(Marketplace.SlotId).selector;
|
|
}
|
|
|
|
/*--------------------------------------------
|
|
| Invariants |
|
|
--------------------------------------------*/
|
|
|
|
invariant totalSupplyIsSumOfBalances()
|
|
to_mathint(Token.totalSupply()) == sumOfBalances;
|
|
|
|
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;
|
|
|
|
/*--------------------------------------------
|
|
| Properties |
|
|
--------------------------------------------*/
|
|
|
|
rule sanity(env e, method f) {
|
|
calldataarg args;
|
|
f(e, args);
|
|
assert true;
|
|
satisfy true;
|
|
}
|
|
|
|
rule totalReceivedCannotDecrease(env e, method f) {
|
|
mathint total_before = totalReceived;
|
|
|
|
calldataarg args;
|
|
f(e, args);
|
|
|
|
mathint total_after = totalReceived;
|
|
|
|
assert total_after >= total_before;
|
|
}
|
|
|
|
rule totalSentCannotDecrease(env e, method f) {
|
|
mathint total_before = totalSent;
|
|
|
|
calldataarg args;
|
|
f(e, args);
|
|
|
|
mathint total_after = totalSent;
|
|
|
|
assert total_after >= total_before;
|
|
}
|
|
|
|
rule allowedRequestStateChanges(env e, method f) {
|
|
calldataarg args;
|
|
Marketplace.RequestId requestId;
|
|
|
|
Marketplace.RequestState requestStateBefore = currentContract.requestState(e, requestId);
|
|
f(e, args);
|
|
Marketplace.RequestState requestStateAfter = currentContract.requestState(e, requestId);
|
|
|
|
assert requestStateBefore != requestStateAfter && requestStateAfter == Marketplace.RequestState.Started => requestStateBefore == Marketplace.RequestState.New;
|
|
assert requestStateBefore != requestStateAfter && requestStateAfter == Marketplace.RequestState.Finished => requestStateBefore == Marketplace.RequestState.Started;
|
|
assert requestStateBefore != requestStateAfter && requestStateAfter == Marketplace.RequestState.Failed => requestStateBefore == Marketplace.RequestState.Started;
|
|
assert requestStateBefore != requestStateAfter && requestStateAfter == Marketplace.RequestState.Cancelled => requestStateBefore == Marketplace.RequestState.New;
|
|
}
|
|
|
|
rule functionsCausingRequestStateChanges(env e, method f) {
|
|
calldataarg args;
|
|
Marketplace.RequestId requestId;
|
|
|
|
Marketplace.RequestState requestStateBefore = currentContract.requestState(e, requestId);
|
|
f(e, args);
|
|
Marketplace.RequestState requestStateAfter = currentContract.requestState(e, requestId);
|
|
|
|
// RequestState.New -> RequestState.Started
|
|
assert requestStateBefore == Marketplace.RequestState.New && requestStateAfter == Marketplace.RequestState.Started => canStartRequest(f);
|
|
|
|
// RequestState.Started -> RequestState.Finished
|
|
assert requestStateBefore == Marketplace.RequestState.Started && requestStateAfter == Marketplace.RequestState.Finished => canFinishRequest(f);
|
|
|
|
// RequestState.Started -> RequestState.Failed
|
|
assert requestStateBefore == Marketplace.RequestState.Started && requestStateAfter == Marketplace.RequestState.Failed => canFailRequest(f);
|
|
|
|
// RequestState.New -> RequestState.Cancelled
|
|
assert requestStateBefore == Marketplace.RequestState.New && requestStateAfter == Marketplace.RequestState.Cancelled => canCancelRequest(f);
|
|
}
|
|
|
|
rule finishedRequestCannotBeStartedAgain(env e, method f) {
|
|
|
|
calldataarg args;
|
|
Marketplace.RequestId requestId;
|
|
|
|
Marketplace.RequestState requestStateBefore = currentContract.requestState(e, requestId);
|
|
require requestStateBefore == Marketplace.RequestState.Finished;
|
|
f(e, args);
|
|
Marketplace.RequestState requestStateAfter = currentContract.requestState(e, requestId);
|
|
|
|
assert requestStateBefore == requestStateAfter;
|
|
}
|