[Certora] Verification of timelocks (WIP) #819
Conversation
Signed-off-by: MathisGD <[email protected]>
- Add ExecutableAt.spec and helpers for executable timing verification - Add RevertsTimelocked.spec and helpers for timelock revert verification - Update Timelocks.spec and configuration - Add corresponding .conf files for all three verification suites
There was a problem hiding this comment.
ExecutableAt and RevertsTimelocked share a lot of logic. I think it would be better if we merge the two into a single spec file, checking that the helper function reverts if and only if the original function reverts.
Then it would be more clear that what we checked is an equivalent function that "just" has the reverting statements (the require statements notably). And makes me wonder whether we should keep such verification job or just forget about it entirely
| // Check currentTime < min(time1, time2) | ||
| fb(e, args); |
There was a problem hiding this comment.
I think it's very important that it's clear that this min(time1, time2) is greater than the computed time in earliestExecutionTimeIncreases. This way we know that the function can't be called before that computed time, even with other interactions in between. (it was clear in the original spec in Metamorpho, because the same variable was used)
There was a problem hiding this comment.
btw just checking currentTime < time2 is enough, no ?
| } | ||
|
|
||
| // Abdicated functions cannot be called | ||
| rule abdicatedFunctionsMustRevert(env e, method f, calldataarg args) |
There was a problem hiding this comment.
This one is already verified in AbdicatedFunctions, although it's nice to factorize the functionTimelocked helper
| } | ||
|
|
||
| // Function must revert if not submitted for execution | ||
| rule mustRevertIfNotSubmitted(env e, method fb, method f, calldataarg args) |
There was a problem hiding this comment.
probably not necessary if we already have revert conditions (we know that it needs to be submitted)
| } | ||
|
|
||
| // Submit correctly sets executableAt based on timelock | ||
| rule submitSetsCorrectExecutableAt(env e, bytes data) { |
There was a problem hiding this comment.
It feels a little bit out of place in this spec file, instead it would be best in a file that checks that functions sets the expected variables IMO
| } | ||
|
|
||
| // Function must revert if revoked | ||
| rule revokePreventsFutureExecution(env e, method revokeFb, method f, calldataarg args) |
There was a problem hiding this comment.
same (almost), because essentially what we prove here is that revoke sets the executableAt at 0
|
Closing, I will split this work and reopen PRs |
Credits to the Certora team !