From 54fa59f87957222e5d9cc26a15f70695e02fcf95 Mon Sep 17 00:00:00 2001 From: Aleksander Kryukov Date: Sun, 14 Nov 2021 15:33:30 +0200 Subject: [PATCH] proposeInitialized done --- certora/scripts/GovernorBasic.sh | 5 +++-- certora/specs/GovernorBase.spec | 8 ++++++-- 2 files changed, 9 insertions(+), 4 deletions(-) diff --git a/certora/scripts/GovernorBasic.sh b/certora/scripts/GovernorBasic.sh index b720c28ec..8a6b48373 100644 --- a/certora/scripts/GovernorBasic.sh +++ b/certora/scripts/GovernorBasic.sh @@ -1,8 +1,9 @@ certoraRun certora/harnesses/GovernorBasicHarness.sol \ --verify GovernorBasicHarness:certora/specs/GovernorBase.spec \ --solc solc8.2 \ - --staging \ + --staging uri/add_with_env_to_preserved_all \ --optimistic_loop \ --settings -copyLoopUnroll=4 \ - --rule doubleVoting \ + --disableLocalTypeChecking \ + --rule proposalInitiated \ --msg "$1" \ No newline at end of file diff --git a/certora/specs/GovernorBase.spec b/certora/specs/GovernorBase.spec index 88fe278f8..1a6580d40 100644 --- a/certora/specs/GovernorBase.spec +++ b/certora/specs/GovernorBase.spec @@ -47,12 +47,16 @@ methods { */ // start !0 !0 !0 // end = !0 !0 !0 - // exe = 0 0 1 1 - // can = 0 1 0 1 + // exe = 0 0 1 1 + // can = 0 1 0 1 invariant proposalInitiated(uint256 pId) (proposalSnapshot(pId) != 0 <=> proposalDeadline(pId) != 0) && (isCanceled(pId) => proposalSnapshot(pId) != 0) && (isExecuted(pId) => proposalSnapshot(pId) != 0) + { preserved with (env e){ + require e.block.number > 0; + }} + /*