Conversation
bhargavbh
changed the title
bhargavbh
changed the title
bhargavbh
force-pushed
the
certora/forceDeallocate
branch
from
39fe08a to
98940a5
Compare
certora/specs/ForceDeallocate.spec
Outdated
|
|
||
| // Post-conditions on the returned ids and change that ensures forceDeallocate with Zero does not revert: | ||
| require forall uint256 i. i < ids.length => currentContract.caps[ids[i]].allocation > 0; | ||
| require forall uint256 i. i < ids.length => currentContract.caps[ids[i]].allocation <= max_int256(); |
There was a problem hiding this comment.
is this last one required ?
There was a problem hiding this comment.
yes, its required. prover link when you remove it. its similar to the requirement of the deallocate revert condition in AllocateDeallocateReverts.spec
There was a problem hiding this comment.
sorry I meant the last one in the code highlighted, so the second one of the block:
require forall uint256 i. i < ids.length => currentContract.caps[ids[i]].allocation <= max_int256();
There was a problem hiding this comment.
this condition is also necessary: prover link.
forceDeallocate calls deallocateInternal, so any condition on the adapter's deallocate which makes deallocateInternal revert would also be required here. Calling with assets=0 does not reduce the assumptions.
4 participants
assume the adapter's deallocate does not revert and show forceDeallocate with assets=0 does not revert.