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; + }} + /*