r4bbit b413d776cc

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

2024-10-21 12:04:20 +02:00

..

confs

chore(certora): set MarketplaceHarness as parametric_contract config value

2024-08-19 14:07:05 +02:00

harness

chore(certora): verify possible slot state transitions

2024-09-30 12:53:06 +02:00

helpers

Set up certora and implement first rules (#122)

2024-07-24 18:50:18 +02:00

specs

chore(certora): add invariant that totalSent is <= totalReceived

2024-10-21 12:04:20 +02:00