codex-storage
/
codex-contracts-eth
mirror of https://github.com/codex-storage/codex-contracts-eth.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

fix(certora): remove incorrect requirment in 

`paidSlotAlwaysHasCancelledOrFinishedRequest`

The mentioned invariant uses a `preserved` block with a `require
SlotState == Paid`, which essentially excludes all cases where
`SlotState != Paid`.

This was incorrectly applied. Removing that requirement causes the
prover to find a counter example where it starts with `RequestState == Started`
and `SlotState == Cancelled`.

This ultimately results in `SlotState == PAID` while `RequestState`
stays `Started`.

Counter example link: https://prover.certora.com/output/6199/a38c9bd665d544dabcffd07335c05420?anonymousKey=119a850a4d1d65ccbe8f95298615592835801d2b

A slot that is `Cancelled` however, can never belong to a request that
is `Started`. So requiring the invariant that
`cancelledSlotAlwaysHasCancelledRequest` fixes this and the rule is
passing.

Passing rule: https://prover.certora.com/output/6199/d0e165ed5d594f9fb477602af06cfeb1?anonymousKey=01ffaad46027786c38d78e5a41c03ce002032200

Closes #164
This commit is contained in:
r4bbit 2024-08-26 14:49:42 +02:00
parent cc0b2732ad
commit 38caabeee3
1 changed files with 2 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
certora/specs/Marketplace.spec
View File

@ -174,13 +174,12 @@ invariant finishedSlotAlwaysHasFinishedRequest(env e, Marketplace.SlotId slotId)
// STATUS - verified
// paid slot always has finished or cancelled request
// https://prover.certora.com/output/6199/6217a927ff2c43bea1124f6ae54a78fb?anonymousKey=d5e09d0d12658fd6b5f298fc04cea88da892c62d
// https://prover.certora.com/output/6199/d0e165ed5d594f9fb477602af06cfeb1?anonymousKey=01ffaad46027786c38d78e5a41c03ce002032200
invariant paidSlotAlwaysHasFinishedOrCancelledRequest(env e, Marketplace.SlotId slotId)
currentContract.slotState(e, slotId) == Marketplace.SlotState.Paid =>
currentContract.requestState(e, currentContract.slots(e, slotId).requestId) == Marketplace.RequestState.Finished || currentContract.requestState(e, currentContract.slots(e, slotId).requestId) == Marketplace.RequestState.Cancelled
{ preserved {
// ensures we start with a paid slot
require currentContract.slotState(e, slotId) == Marketplace.SlotState.Paid;
requireInvariant cancelledSlotAlwaysHasCancelledRequest(e, slotId);
}
}