Browse Source

add --optimistic_hashing to governor scripts

Hadrien Croubois 2 years ago
parent
commit
ecebc5688d

+ 1 - 0
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 \
     $@

+ 2 - 1
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 \
     $@

+ 1 - 0
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 \
     $@

+ 1 - 0
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 \
     $@

+ 1 - 0
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 \
     $@