From ecebc5688dcdb6e3ea789f55b4716565836ff573 Mon Sep 17 00:00:00 2001 From: Hadrien Croubois Date: Tue, 28 Feb 2023 09:55:41 +0100 Subject: [PATCH] add --optimistic_hashing to governor scripts --- certora/scripts/passes/verifyGPLQ_deadlineCantBeUnextended.sh | 1 + certora/scripts/passes/verifyGPLQ_proposalInOneState.sh | 3 ++- certora/scripts/passes/verifyGPLQ_quorumReachedEffect.sh | 1 + certora/scripts/passes/verifyGovernor.sh | 1 + certora/scripts/passes/verifyGovernorCountingSimple.sh | 1 + 5 files changed, 6 insertions(+), 1 deletion(-) diff --git a/certora/scripts/passes/verifyGPLQ_deadlineCantBeUnextended.sh b/certora/scripts/passes/verifyGPLQ_deadlineCantBeUnextended.sh index a28e75967..ae3b2a55e 100644 --- a/certora/scripts/passes/verifyGPLQ_deadlineCantBeUnextended.sh +++ b/certora/scripts/passes/verifyGPLQ_deadlineCantBeUnextended.sh @@ -7,6 +7,7 @@ certoraRun \ --verify GovernorFullHarness:certora/specs/GovernorPreventLateQuorum.spec \ --link GovernorFullHarness:token=ERC20VotesHarness \ --optimistic_loop \ + --optimistic_hashing \ --rule deadlineCantBeUnextended \ --loop_iter 1 \ $@ diff --git a/certora/scripts/passes/verifyGPLQ_proposalInOneState.sh b/certora/scripts/passes/verifyGPLQ_proposalInOneState.sh index 94754778e..defb01802 100644 --- a/certora/scripts/passes/verifyGPLQ_proposalInOneState.sh +++ b/certora/scripts/passes/verifyGPLQ_proposalInOneState.sh @@ -7,7 +7,8 @@ certoraRun \ --verify GovernorFullHarness:certora/specs/GovernorPreventLateQuorum.spec \ --link GovernorFullHarness:token=ERC20VotesHarness \ --optimistic_loop \ + --optimistic_hashing \ --rule proposalInOneState \ - --settings -t=1000 \ --loop_iter 1 \ + --settings -t=1000 \ $@ diff --git a/certora/scripts/passes/verifyGPLQ_quorumReachedEffect.sh b/certora/scripts/passes/verifyGPLQ_quorumReachedEffect.sh index 2cbebae8f..06c3da897 100644 --- a/certora/scripts/passes/verifyGPLQ_quorumReachedEffect.sh +++ b/certora/scripts/passes/verifyGPLQ_quorumReachedEffect.sh @@ -7,6 +7,7 @@ certoraRun \ --verify GovernorFullHarness:certora/specs/GovernorPreventLateQuorum.spec \ --link GovernorFullHarness:token=ERC20VotesHarness \ --optimistic_loop \ + --optimistic_hashing \ --rule quorumReachedEffect \ --loop_iter 1 \ $@ diff --git a/certora/scripts/passes/verifyGovernor.sh b/certora/scripts/passes/verifyGovernor.sh index 02d2b3118..fe1e0387d 100644 --- a/certora/scripts/passes/verifyGovernor.sh +++ b/certora/scripts/passes/verifyGovernor.sh @@ -11,5 +11,6 @@ certoraRun \ --verify GovernorHarness:certora/specs/GovernorBase.spec \ --link GovernorHarness:token=ERC20VotesHarness \ --optimistic_loop \ + --optimistic_hashing \ --settings -copyLoopUnroll=4 \ $@ \ No newline at end of file diff --git a/certora/scripts/passes/verifyGovernorCountingSimple.sh b/certora/scripts/passes/verifyGovernorCountingSimple.sh index b774d5fc5..070d7379a 100644 --- a/certora/scripts/passes/verifyGovernorCountingSimple.sh +++ b/certora/scripts/passes/verifyGovernorCountingSimple.sh @@ -8,5 +8,6 @@ certoraRun \ --verify GovernorHarness:certora/specs/GovernorCountingSimple.spec \ --link GovernorHarness:token=ERC20VotesHarness \ --optimistic_loop \ + --optimistic_hashing \ --settings -copyLoopUnroll=4 \ $@