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
`SlotReservationsFull` event is emitted once a slot has reached its capacity for slot reservations (3 reservations at this time).
`SlotReservationsFull` event emists `requestId` and `slotIndex`.
* feat(slot-reservations): Allow slots to be reserved
Closes#175.
Allows reservation of slots, without an implementation of the expanding window.
- Add a function called `reserveSlot(address, SlotId)`, that allows three unique addresses per slot to be reserved, that returns bool if successful.
- Use `mapping(SlotId => EnumerableSet.AddressSet)`
- Return false if the address could not be added to the set (if `EnumerableSet.add` returns false)
- Add `canReserveSlot(address, SlotId)`
- Return `true` if set of reservations is less than 3 and the set doesn't already contain the address
- Return `true` otherwise (for now, later add in logic for checking the address is inside the expanding window)
- Call `canReserveSlot` from `reserveSlot` as a `require` or invariant
- Add `SlotReservations` configuration struct to the network-level config, with `maxReservations`
There is a missing check in `requestStorage()` on whether the `Request`
contains an `Ask` where its `slots` is `> 0`.
This allows for making storage request without slots. Not harmful but
not a valid state of the system either.
This commit adds that check and a test with batteries included.
The rule `slotIsFailedOrFreeIfRequestHasFailed` currently has violations
as it is vacuous for some functions in the `Marketplace` contract.
The rule being vacuous means that the function on which the rule is
tested either doesn't have a case where the required conditions work (it
reverts), or, in this case, where any given function doesn't have a case
where it reaches the required state change.
There's various functions where this applies because the rule requires
that the request being tested is first any state that is `!= Failed`,
then for any function `f`, when `f` is executed, the required state of
the request is `Failed`.
Prover run that confirms this: https://prover.certora.com/output/6199/82ed96aac5014cb9a7485fc3752fb399?anonymousKey=28c97adbbe14ead331dc8e4b8ed05e94528075a3
There's two options to go about this:
1. Either filter out all functions from the rule where the rule is
vacuous (this is dangerous because we'd exclude those functions
entirely from the rule)
2. Or, rewrite the rule such that the requirements are relaxed
This commit implements option 2.
Instead of requiring that the starting request state has to be `!=
Failed`, we simply assert that **if** it **was** not `Failed` and then
**is** `Failed`, the corresponding slot is either failed or free.
Prover run that passes: https://prover.certora.com/output/6199/16fa074bd23146e59c21964c98bbb3e0?anonymousKey=229d721cf35873bed5eae67696eed803ce75fd18
This should fix the bug of certora-cli not properly completing with non
zero exit codes on errors, which ultimately results in CI tasks to give
false positives.
* initial commit for splitting payouts
Collateral goes to slot's host address, while reward payouts go to the slot's host payoutAddress
* Add fillSlot overload to make payoutAddress "optional"
* add tests for payoutAddress
* add doc to patchFillSlotOverloads
* formatting
* remove optional payoutAddress parameter
* Move payoutAddress to freeSlot
- remove payoutAddress parameter from `fillSlot`
- remove `payoutAddress` from slot struct and storage
- add payoutAddress parameter to `freeSlot`, preventing the need for storage
* formatting
* update certora spec to match updated function signature
* Add withdrawAddress to withdrawFunds
- prevent erc20 msg.sender blacklisting
* Update tests for paying out to withdrawAddress
* formatting
* Add collateralRecipient
* refactor: change withdrawFunds and freeSlot overloads
- `withdrawFunds` now has an option withdrawRecipient parameter
- `freeSlot` now has two optional parameters: rewardRecipient, and collateralRecipient. Both or none must be specified.
* update certora spec for new sigs
This adds a rule to formally verify that the `SlotState` and
`RequestState` of any given `Slot` or `Request` does not change more
than once per function call.
Closes#129
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.
This commit adds CVL rule that formally verifies the state changes of
any given request in relation to the functions of the contract that can
cause them.
Closes#128
r4bbit
Slava
Andrea Franz
Adam Uhlíř
Eric
Ben Bierens
Giuliano Mega
Jaremy Creechley
Mark Spanbroek