Skip to content
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

Merged
merged 11 commits into from
Jul 25, 2024
Merged

Conversation

johspaeth
Copy link
Contributor

@johspaeth johspaeth commented Jul 9, 2024

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

@johspaeth johspaeth changed the base branch from master to johspaeth-patch-4 July 9, 2024 09:51
@johspaeth johspaeth requested a review from jhoenicke July 9, 2024 09:53
@johspaeth johspaeth added the release documentation for an upcoming release label Jul 15, 2024

```{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'`.
Copy link
Contributor

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:

  1. Adds complexity
  2. It means we will now have to officially support this prover args syntax
  3. 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.
  4. The workaround is rather easy (just add strong when relevant)

Copy link
Contributor

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.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.


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.
Copy link
Contributor

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)

Copy link
Contributor

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.

Copy link
Contributor Author

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.
Copy link
Contributor

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."

Copy link
Contributor

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

Copy link
Contributor Author

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.

docs/cvl/invariants.md Outdated Show resolved Hide resolved
@johspaeth johspaeth requested a review from urikirsh July 17, 2024 15:59
Copy link
Contributor

@urikirsh urikirsh left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Small suggestions

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
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
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

@@ -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).
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
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).

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`
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
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`

Base automatically changed from johspaeth-patch-4 to master July 25, 2024 08:18
…es/stronginvariants

Conflicts:
	docs/cvl/invariants.md
@urikirsh urikirsh merged commit bf7ce3e into master Jul 25, 2024
2 checks passed
@urikirsh urikirsh deleted the johannes/stronginvariants branch July 25, 2024 10:48
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
release documentation for an upcoming release
Projects
None yet
Development

Successfully merging this pull request may close these issues.

4 participants