[WIP] spec: The contract has enough funds to pay back everything #169
Conversation
gravityblast
force-pushed
the
contract-balance-spec
branch
3 times, most recently
from
412a285 to
854ad2d
Compare
| @@ -191,6 +228,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; | |||
There was a problem hiding this comment.
@gravityblast did we see counter examples where we had a negative request count?
Wondering otherwise how useful this invariant is.
There was a problem hiding this comment.
@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
|
@gravityblast can you rebase this on top of latest |
gravityblast
force-pushed
the
contract-balance-spec
branch
from
854ad2d to
0d0215e
Compare
gravityblast
force-pushed
the
contract-balance-spec
branch
from
0d0215e to
1e5c8df
Compare
|
Is this ready for review or not? On one hand it is marked as ready for review but at the same time there is |
Part of #127
Add a spec to check that the contract balance increases when new storage requests are added.
certora run started from local command:
https://prover.certora.com/output/27938/7c09c206648f4d8d9e26ed839d14f0b1?anonymousKey=40b24d364cac6b8df280b8b9e2bc62551c3bdfdc