NoBey/openzeppelin-contracts
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

proposeInitialized done

Browse Source
This commit is contained in:
Aleksander Kryukov
2021-11-14 15:33:30 +02:00
parent 2baa9bd801
commit 54fa59f879
2 changed files with 9 additions and 4 deletions
Download Patch File Download Diff File Expand all files Collapse all files

5
certora/scripts/GovernorBasic.sh
View File

@ -1,8 +1,9 @@
certoraRun certora/harnesses/GovernorBasicHarness.sol \ certoraRun certora/harnesses/GovernorBasicHarness.sol \
--verify GovernorBasicHarness:certora/specs/GovernorBase.spec \ --verify GovernorBasicHarness:certora/specs/GovernorBase.spec \
--solc solc8.2 \ --solc solc8.2 \
--staging \ --staging uri/add_with_env_to_preserved_all \
--optimistic_loop \ --optimistic_loop \
--settings -copyLoopUnroll=4 \ --settings -copyLoopUnroll=4 \
--rule doubleVoting \ --disableLocalTypeChecking \
--rule proposalInitiated \
--msg "$1" --msg "$1"

8
certora/specs/GovernorBase.spec
View File

@ -47,12 +47,16 @@ methods {
*/ */
// start !0 !0 !0 // start !0 !0 !0
// end = !0 !0 !0 // end = !0 !0 !0
// exe = 0 0 1 1 // exe = 0 0 1 1
// can = 0 1 0 1 // can = 0 1 0 1
invariant proposalInitiated(uint256 pId) invariant proposalInitiated(uint256 pId)
(proposalSnapshot(pId) != 0 <=> proposalDeadline(pId) != 0) && (proposalSnapshot(pId) != 0 <=> proposalDeadline(pId) != 0) &&
(isCanceled(pId) => proposalSnapshot(pId) != 0) && (isCanceled(pId) => proposalSnapshot(pId) != 0) &&
(isExecuted(pId) => proposalSnapshot(pId) != 0) (isExecuted(pId) => proposalSnapshot(pId) != 0)
{ preserved with (env e){
require e.block.number > 0;
}}
/* /*