@ -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 \
--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