@@ -4,4 +4,6 @@ certoraRun certora/harnesses/GovernorHarness.sol \
--staging \
--msg $1 \
--disableLocalTypeChecking \
- --rule voteStartBeforeVoteEnd
+ --optimistic_loop \
+ --settings -copyLoopUnroll=4
+ --rule sanityCheckVoteStart
@@ -5,7 +5,8 @@ do
echo ${file%.*}
certoraRun certora/harnesses/$file \
--verify ${file%.*}:certora/specs/sanity.spec "$@" \
- --solc solc8.0 \
- --staging \
- --msg "sanity ${file}"
+ --solc solc8.0 --staging \
+ --msg "checking sanity on ${file%.*}"
done
@@ -32,7 +32,6 @@ hook Sload uint64 value _proposals[KEY uint256 pId].voteStart._deadline STORAGE
require proposalVoteStart(pId) == value;
}
-
hook Sstore _proposals[KEY uint256 pId].voteEnd._deadline uint64 newValue STORAGE {
havoc proposalVoteEnd assuming (
proposalVoteEnd@new(pId) == newValue