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

Certora's Governance verification rules #2997

Merged
merged 138 commits into from
Dec 27, 2021
Merged

Certora's Governance verification rules #2997

merged 138 commits into from
Dec 27, 2021

Conversation

mdgeorge4153
Copy link
Contributor

@mdgeorge4153 mdgeorge4153 commented Dec 3, 2021 •
edited
Loading

This PR contains the verification rules developed by Certora for the governance contracts, along with scripts for rerunning the verification and documentation for the rules.

PR Checklist

  • Tests
  • Documentation
  • Changelog entry (no changes are made to the contracts)

shellygr and others added 30 commits September 26, 2021 00:21
@shellygr
start work on governor
2c08f85
@shellygr
Back to expected pattern?
f239fa5
@shellygr
fixes
fdc4b0c
@shellygr
fixes
4c1d5e0
@shellygr
rule drafts
22030f2
@RedLikeRosesss
ignore certora's generated files
6776cc6
@RedLikeRosesss
sanity rule preparations
cac49bf
@shellygr
multiple inheritance is tricky
72d4e9c
@RedLikeRosesss
multiple inheritance is tricky x2
a710435
@MichaelMorami
slight script changes and ghost fix
69f87ad
@MichaelMorami
Hooks fixed
e888ea4
@MichaelMorami
slight changes change for convenience + disableLocalTypeChecking flag…
6876df0 
… for the hooks
@MichaelMorami
Harness private to public
c00d951
@MichaelMorami
Harness private to public
d6e79f4
@MichaelMorami
slight changes in scripts + disableLocalTypeChecking
21b8434
@MichaelMorami
hooks fixed
a2960e2
@RedLikeRosesss
scripts settings added
f7cc254
@MichaelMorami
quotes on var in msg
bfa1dd3
@RedLikeRosesss
checkingInvariantsWithoutGhosts
f08ee56
@RedLikeRosesss
WorkInProgress
b133fee
@RedLikeRosesss
someCleaning
0ebc0d5
@shellygr
fix simple vote end before start
ac729e0
@MichaelMorami
added invariants if executed or canceled always revert
7a5bd86
@MichaelMorami
idea for sum of votes
ad7993d
@RedLikeRosesss
MoreRulesToTheGodOfRules
751277a
@MichaelMorami
fixed function revert if executed
37a4975
@MichaelMorami
added ghost and counter implementation for castWithReason and castBySig
c819e0b
@MichaelMorami
ghosts and invariant unfinished
34cb4bd
@MichaelMorami
cannot set if executed and canceled as rules (not working)
44a8fed
@RedLikeRosesss
FirstWizardHarness
07d6379
RedLikeRosesss and others added 20 commits November 24, 2021 17:53
@RedLikeRosesss
RulesCleaning
b3dd1e0
@RedLikeRosesss
CleaningAndScriptForAllAndReadme
37725a0
@RedLikeRosesss
cleaning in process
73080c7
@RedLikeRosesss
runAllwithoutTypeCheckAndPolishingIt
1d25a22
@RedLikeRosesss
executedImplyStartAndEndDateNonZero inv fix
43e37f0
@RedLikeRosesss
madeVeryfyAllMoreFlexible
f40c48a
@MichaelMorami
fix script
de59492
@RedLikeRosesss
NewFileForRulesInProgress
96c6120
@RedLikeRosesss
FixingScriptsToWorkWithNewChanges
dae72a7
@RedLikeRosesss
HarnessCleaning
7d0eeab
@mdgeorge4153
moved contract modifications into munged directory
749738f
@mdgeorge4153
created applyHarness
f308740
@mdgeorge4153
switched harnesses to use munged contracts
380b87d
@mdgeorge4153
tweaked script to run quickly
760edf9
@mdgeorge4153
filtered out timeouts
ec5d501
@mdgeorge4153
fixed executeOnly rule
5888bee
@mdgeorge4153
did some harnessing
d648695
@mdgeorge4153
harnessing fix
3c15095
@mdgeorge4153
Merge branch 'OpenZeppelin:master' into master
8c0684a
@mdgeorge4153
Merge branch 'master' into certora/governor
6bd525f 
Rerunning verification against current master to ensure clean PR
@mdgeorge4153 mdgeorge4153 marked this pull request as ready for review December 3, 2021 20:39
@mdgeorge4153
Copy link
Contributor Author

I filtered out the timing out rules mentioned in the document, and reran the verification after merging from master. All the rules are passing, which means it should be straightforward to integrate verification into CI.

frangio
frangio reviewed Dec 6, 2021
View reviewed changes
certora/README.md Outdated Show resolved Hide resolved
certora/applyHarness.patch Outdated Show resolved Hide resolved
certora/applyHarness.patch Outdated Show resolved Hide resolved
certora/README.md Show resolved Hide resolved
@mdgeorge4153 mdgeorge4153 requested a review from frangio December 17, 2021 14:00
frangio
frangio approved these changes Dec 27, 2021
View reviewed changes
Copy link
Contributor

@frangio frangio left a comment

Choose a reason for hiding this comment

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

Thank you!

@frangio frangio merged commit 915ca18 into OpenZeppelin:master Dec 27, 2021
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@frangio frangio frangio approved these changes

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

Successfully merging this pull request may close these issues.
5 participants
@mdgeorge4153 @frangio @shellygr @RedLikeRosesss @MichaelMorami