Formal verification of Account (7702+7579) #5785
Conversation
Amxx
added
ignore-changeset
formal-verification
|
|
These specs pass ! https://prover.certora.com/output/71959/de382212ccb3440e92693f187ca74e93?anonymousKey=5f06da9b8474ce1aaa13d57841d641d64db70476 @ernestognw WDYT ? |
| rule callInstallModule(env e, uint256 moduleTypeId, address module, bytes initData) { | ||
| require calls == 0; | ||
|
|
||
| installModule(e, moduleTypeId, module, initData); | ||
|
|
||
| assert calls == 1; | ||
| assert lastcall_target == module; | ||
| assert lastcall_selector == 0x6d61fe70; // onInstall(bytes) | ||
| assert lastcall_value == 0; | ||
| } |
There was a problem hiding this comment.
Isn't already verified here?
openzeppelin-contracts/certora/specs/Account.spec
Lines 245 to 250 in a6ecba8
There was a problem hiding this comment.
That part is not verifying the target (we cannot extract it from the args).
This rule's point is mostly to check the target of the call is the module. All other checks (calls == 1, selector, value) are duplicated. Would you remove them ?
No description provided.