-
Notifications
You must be signed in to change notification settings - Fork 16
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Documentation for Strong Invariants #278
Conversation
Co-authored-by: urikirsh <[email protected]>
Co-authored-by: urikirsh <[email protected]>
Co-authored-by: urikirsh <[email protected]>
docs/cvl/invariants.md
Outdated
|
||
```{note} | ||
An invariant that is neither declared as `strong` nor `weak` will be treated as a `weak` invariant by default. | ||
This behavior can be changed using the flag `--prover_args '-defaultInvariantType strong'`. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I don't think we should mention this flag:
- Adds complexity
- It means we will now have to officially support this prover args syntax
- If it is a useful option, it should be a flag - flags have better validation, better error messages, and they appear in the help message.
- The workaround is rather easy (just add
strong
when relevant)
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I can agree with not mentioning it, (but we should have a list of flags for ourselves)
But the idea was to keep the flag so that we can gather more experience, whether strong or weak is the better default.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Regarding flags for internal use:
I bookmarked these two links:
docs/cvl/invariants.md
Outdated
|
||
1. Assert that the invariant holds before the `c` - if the invariant does not hold due to some logic of the current method, this will yield a counter example. | ||
2. Assume the invariant holds after the call `c`. The semantics is that the call did not break the invariant. | ||
3. In the case `c` is a `delegatecall` havoc the current's contact storage and assert the invariant once more. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Not clear to me what exactly happens and why we do this. Does 3 replace step 2, or happens right after it?
Is there any realistic case where there is an invariant we can prove right after a havoc? (AFAIK resetting storage also resets ghosts)
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Step 3 is in addition and should provide soundness. A delegatecall can change storage, so we simulate this by havocing storage. We do this at the end, because we need to show that even after step 2, the delegator cannot break the invariant (we don't need it then after step 1, because the solver can always assume that step 2 does no change, so only checking after step 2 also catches the bug).
I think step3 does not havoc ghost (is this right?) The idea is that the delegator cannot change the ghost state or the state of any other contract, just the contract that it is called on.
This is mostly for invariants that don't even talk about the state of the contract. If the contract that does the delegate call is not the main contract we want to reason about, then delegatecalls from this contract are always okay.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think step3 does not havoc ghost (is this right?)
Correct.
I updated the description to be more meaningful. Is it better now?
invariant is sometimes called a "representation invariant". | ||
invariant is sometimes called a "representation invariant". A *strong* invariant is | ||
an invariant that also holds before and after execution of an unresolved call, i.e. a call that | ||
potentially calls to another contract which could modify the current contract's state. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This paragraph still doesn't explain when should we use strong invariants over weak invariants. Perhaps we should base on the first sentence from the example at https://github.com/Certora/Examples/blob/cli-beta/CVLByExample/StrongInvariants/README.md:
"Strong invariants are sure to hold whenever control is yielded to an external function, providing enhanced security, especially for contracts without global locks. However, they add additional checks that can result in longer run times or even halted jobs."
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
In general, linking to the example would be highly beneficial
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks - I linked the example and improved the wording.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Small suggestions
docs/cvl/invariants.md
Outdated
A strong invariant performs the same checks as a weak invariant - i.e. it will be checked for the constructor | ||
and for any other method it will be assumed before executing the method (pre-state) and asserted afterward execution of the method (post-state). | ||
In addition to these steps, a strong invariant also asserts and assumes the invariant _during_ method | ||
execution at location that potentially break the invariant. The invariant can be violated if there |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
execution at location that potentially break the invariant. The invariant can be violated if there | |
execution at locations that potentially break the invariant. The invariant can be violated if there |
docs/cvl/invariants.md
Outdated
@@ -75,6 +79,19 @@ and by {ref}`--parametric_contracts`. `View` and `pure` methods are excluded fro | |||
invariant checking as by definition they cannot change the state | |||
of their contract. | |||
|
|||
A strong invariant performs the same checks as a weak invariant - i.e. it will be checked for the constructor | |||
and for any other method it will be assumed before executing the method (pre-state) and asserted afterward execution of the method (post-state). |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
and for any other method it will be assumed before executing the method (pre-state) and asserted afterward execution of the method (post-state). | |
and for any other method, it will be assumed before executing the method (pre-state) and asserted afterward execution of the method (post-state). |
docs/cvl/invariants.md
Outdated
and for any other method it will be assumed before executing the method (pre-state) and asserted afterward execution of the method (post-state). | ||
In addition to these steps, a strong invariant also asserts and assumes the invariant _during_ method | ||
execution at location that potentially break the invariant. The invariant can be violated if there | ||
is an unresolved external call that is able to modify the state of the current contract. To verify the strong invariant, for every unresolved external call `c` |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
is an unresolved external call that is able to modify the state of the current contract. To verify the strong invariant, for every unresolved external call `c` | |
is an unresolved external call that can modify the state of the current contract. To verify the strong invariant, for every unresolved external call `c` |
…es/stronginvariants Conflicts: docs/cvl/invariants.md
This PR adds documentation for the upcoming strong invariant feature that will be part of beta version
>7.9.0
.To avoid merge conflicts, I drafted it on top of this PR which will be merged for the main release of version
7.9.0