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.

Sign up for GitHub

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

Jump to bottom

Formal verification: add owner related invariants #600

Merged
merged 2 commits into from
Jul 4, 2023
Merged

Formal verification: add owner related invariants #600

merged 2 commits into from
Jul 4, 2023

Conversation

mmv08
Copy link
Member

@mmv08 mmv08 commented Jul 3, 2023 •
edited
Loading

This PR checks for three properties:

  • threshold should be less than the number of owners
  • safe cannot be an owner of the self
  • safe owner cannot be the sentinel address

The PR is based on Akshay's rules that haven't been pushed to the main branch. I had to change the sentinel as an owner invariant to a rule because, as an invariant, it didn't pass the vacuity check. It also adds changes for the cli v2 and CVL 2

@github-actions
Copy link

github-actions bot commented Jul 3, 2023 •
edited
Loading

Pull Request Test Coverage Report for Build 5453384937

  • 0 of 0 changed or added relevant lines in 0 files are covered.
  • No unchanged relevant lines lost coverage.
  • Overall coverage remained the same at 94.059%
Totals Coverage Status
Change from base Build 5453355428: 0.0%
Covered Lines: 318
Relevant Lines: 333
💛 - Coveralls

@mmv08 mmv08 force-pushed the certora/treshold-ownercount branch 6 times, most recently from 1796284 to 44b44e1 Compare July 3, 2023 13:50
@mmv08 mmv08 changed the title Add owner related invariants Formal verification: add owner related invariants Jul 3, 2023
@mmv08 mmv08 force-pushed the certora/treshold-ownercount branch 2 times, most recently from bb2e9a7 to 15e7d27 Compare July 4, 2023 08:44
@mmv08 mmv08 force-pushed the certora/treshold-ownercount branch from 15e7d27 to d2d87c3 Compare July 4, 2023 08:46
@mmv08 mmv08 requested review from a team, rmeissner, Uxio0 and akshay-ap and removed request for a team July 4, 2023 09:15
@mmv08 mmv08 force-pushed the certora/treshold-ownercount branch from 33c87c5 to b2006f7 Compare July 4, 2023 10:01
akshay-ap
akshay-ap approved these changes Jul 4, 2023
View reviewed changes
Copy link
Member

@akshay-ap akshay-ap left a comment

Choose a reason for hiding this comment

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

LGTM

@mmv08 mmv08 merged commit 47a3620 into main Jul 4, 2023
12 checks passed
@mmv08 mmv08 deleted the certora/treshold-ownercount branch July 4, 2023 14:10
@github-actions github-actions bot locked and limited conversation to collaborators Jul 4, 2023
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Reviewers

@akshay-ap akshay-ap akshay-ap approved these changes

@rmeissner rmeissner Awaiting requested review from rmeissner rmeissner was automatically assigned from safe-global/safe-protocol

@Uxio0 Uxio0 Awaiting requested review from Uxio0 Uxio0 was automatically assigned from safe-global/safe-protocol

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
2 participants
@mmv08 @akshay-ap