FV for Safe v1.5 Audit #3
Conversation
|
CLA Assistant Lite bot: I have read the CLA Document and I hereby sign the CLA Derek Sorensen seems not to be a GitHub user. You need a GitHub account to be able to sign the CLA. If you have already a GitHub account, please add the email address used for this commit to your account. |
…le guards; this commit ports a rule from Safe.spec so that rules on guards are in the same spec, adds some functionality to the Safe harness, and makes two mocks for the module and transaction guards.
… and all its expected functionality
Pull Request Test Coverage Report for Build 12796391062Details
💛 - Coveralls |
… an enabled module before making the successful call, and adds documentation that refers to an added function to the Safe Harness
|
All the rules are passing now, this codebase also incorporates changes suggested by @nd-certora on the previous draft PR. |
…but for execTransactionFromModuleReturnData
…s both of which are passing
certora/specs/Safe.spec
Outdated
There was a problem hiding this comment.
The rule guardAddressChange was moved from Safe.spec to Guards.spec so that all the rules about guards are in one place.
…anity on the invariant fallbackHanlderNeverSelf, adding the static Dummy to the spec, and strengthening from satisfy to assert
…n and txnGuardCalled are vioalted otherwise
…olve some CVL issues, filter the invariant fallbackHanlderNeverSelf for sanity, etc. overall improvement of rules for fallback
…d) and it's our problem. will update if we can resolve it
… is never self nor the zero address, and now the Prover is misbehaving. Committing here and opening a ticket
…position that the correct guard is called
…ization, and adding all the specs to the spec folder and all the confs to the conf folder
…ausing timeout in a rule
|
merging in preparation for PR to client |
Summary
This is a draft PR to make it easy to get code review on the new rules being written.
Files
The new spec and conf files are located in respective
v1.5files, in order to keep the new spec separate (for now) from the old spec.Note
This is a rebased version of a the previous working branch,
derek/audit, onto a more recent commit given by the customer.