[Certora] Revamp sentinel liveness

[QGarchery]

Based on #686

The motivation is to improve the rule sentinelCanDeallocate, by linking the corresponding adapters. So instead of summarizing the adapter.deallocate call, the underlying protocol withdrawal is summarized (inside adapter.deallocate). This allows to take into account the revert reasons that could potentially happen inside the function adapter.deallocate (other than the ones in the protocol withdrawal of course).

Also in this PR:

• revamp sentinel liveness (document rules, format, explain assumptions)
• link every deallocate requirement to a proven rule
  • underflows
  • overflow before
  • overflow after
  • unique ids
• linked version to show that reverts only happen on the underlying protocol
• remove VaultV2Harness

[QGarchery]

The 3 following requires give an upper limit to the allocation that is relative to max_int256.

1. require MorphoMarketV1Adapter.allocation(marketParams) <= max_int256()
2. require forall uint256 i. i < ids.length => currentContract.caps[ids[i]].allocation <= max_int256()
3. require forall uint256 i. i < ids.length => currentContract.caps[ids[i]].allocation + change <= max_int256()

Weirdly they are all needed.
Require 2 is needed because VaultV2 does int256(_caps.allocation) + change, so _caps.allocation == 2**255 and change == -1 would yield a revert in the vault for example (even with require 1 & 3).
Require 3 is needed because VaultV2 does (int256(_caps.allocation) + change).toUint256();. Note that this require is not proven elsewhere, so it's an assumption of the rule, and it is added as such in the description of that rule.
Require 1 is needed as well but it's less intuitive why as it's a special case of require 2. The reason is that when your rule calls a function with @withrevert, the require that are written after the function call are not taken into account yet. In this case, the deallocate call of the adapter could revert when doing int256(newAllocation) - int256(oldAllocation), with newAllocation == 0 and oldAllocation == type(int256).min