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): add invariant that totalSent is <= totalReceived 

This commit adds an invariant that verifies `marketplaceTotals.sent <=
marketplceTotals.received`.

The invariant relies on the `Token.totalSupply()` which has previously
been verified to be the sum of all balances.

The invariant uses `<=` as there could be donations sent to the
marketplace.

Closes #132
This commit is contained in:
r4bbit 2024-08-09 09:58:39 +02:00
parent 6d319c76b9
commit 018ed2567f
No known key found for this signature in database
GPG Key ID: E95F1E9447DC91A9
1 changed files with 16 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

16
certora/specs/Marketplace.spec
View File

@ -191,6 +191,22 @@ invariant cancelledSlotAlwaysHasCancelledRequest(env e, Marketplace.SlotId slotI
currentContract.slotState(e, slotId) == Marketplace.SlotState.Cancelled => currentContract.slotState(e, slotId) == Marketplace.SlotState.Cancelled =>
currentContract.requestState(e, currentContract.slots(e, slotId).requestId) == Marketplace.RequestState.Cancelled; currentContract.requestState(e, currentContract.slots(e, slotId).requestId) == Marketplace.RequestState.Cancelled;
// STATUS - in progress (fails on constructor state due to a strange behaviour in the tool)
// _marketplaceTotals.received - _marketplaceTotals.sent == tokenBalanceOfContract
// https://prover.certora.com/output/3106/4e6cac8055ac45bb92840e14d9b095eb/?anonymousKey=655a42ca6306a023db78914d5a188d8ec2882771
invariant totalSentIsLessThanOrEqualTotalReceived()
totalReceived - totalSent <= to_mathint(Token.balanceOf(currentContract))
{
preserved fillSlot(MarketplaceHarness.RequestId requestId, uint256 slotIndex, MarketplaceHarness.Groth16Proof proof) with (env e2) {
require e2.msg.sender != currentContract;
requireInvariant totalSupplyIsSumOfBalances();
}
preserved requestStorage(MarketplaceHarness.Request request) with (env e3) {
require e3.msg.sender != currentContract;
requireInvariant totalSupplyIsSumOfBalances();
}
}
/*-------------------------------------------- /*--------------------------------------------
| Properties | | Properties |
--------------------------------------------*/ --------------------------------------------*/