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

fix(certora): fix invariant that requests are started when slots filled

This commit is contained in:
r4bbit 2024-08-21 20:58:18 +02:00
parent 7c542e72b6
commit faeb808d41
1 changed files with 1 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
certora/specs/Marketplace.spec
View File

@ -136,7 +136,7 @@ invariant totalSupplyIsSumOfBalances()
to_mathint(Token.totalSupply()) == sumOfBalances;
invariant requestStartedWhenSlotsFilled(env e, Marketplace.RequestId requestId, Marketplace.SlotId slotId)
to_mathint(currentContract.requestContext(e, requestId).slotsFilled) == to_mathint(currentContract.getRequest(e, requestId).ask.slots) => currentContract.requestState(e, requestId) == Marketplace.RequestState.Started;
currentContract.requestState(e, requestId) == Marketplace.RequestState.Started => to_mathint(currentContract.getRequest(e, requestId).ask.slots) - to_mathint(currentContract.requestContext(e, requestId).slotsFilled) <= to_mathint(currentContract.getRequest(e, requestId).ask.maxSlotLoss);
// STATUS - verified
// https://prover.certora.com/output/6199/6e2383ea040347eabeeb1008bc257ae6?anonymousKey=e1a6a00310a44ed264b1f98b03fa29273e68fca9