[Certora] Allocations from adapters #686
Conversation
Signed-off-by: Colin | Morpho 🦋 <[email protected]>
|
|
||
| definition max_int256() returns int256 = (2 ^ 255) - 1; | ||
|
|
||
| strong invariant allocationIsInt256(bytes32 id) |
There was a problem hiding this comment.
Informational: this definition is here only to make it possible to require in other rules. Importing Invariants.spec makes the process fail for a yet to be explained reason.
There was a problem hiding this comment.
I suggest we track this in an issue and merge it as is until Certora comes up a fix/explanation.
There was a problem hiding this comment.
The reason is that storage analysis fails for this Certora run. It's ok as it's sound, but then it prevents to hook on storage. The problem comes from the fact that Invariants does hook on storage (but it's respective run doesn't fail storage analysis, so it goes through ok).
The current workaround works fine (it just duplicates an invariant).
An alternative is to separate the Invariants job into 2, one that does not hook on storage that we would import here, and another one with the hook on storage (to prove totalSupplyIsSumOfBalances). But in the end this may be even more overhead
Signed-off-by: Colin | Morpho 🦋 <[email protected]>
Signed-off-by: Colin | Morpho 🦋 <[email protected]>
…cs' into feat/verif/allocations-alt
QGarchery
changed the base branch from
main
to
certora/import-chainsecurity-specs
|
Looks good for us , munging is absolutely necessary since the real code uses the extsload function that we don’t support |
3 participants
Based on #621
Slack thread.
Replaces #617