diff --git a/certora/scripts/ERC20VotesRule.sh b/certora/scripts/ERC20VotesRule.sh new file mode 100644 index 000000000..a29fd1ff9 --- /dev/null +++ b/certora/scripts/ERC20VotesRule.sh @@ -0,0 +1,23 @@ +if [ -z "$2" ] + then + echo "Incorrect number of arguments" + echo "" + echo "Usage: (from git root)" + echo " ./certora/scripts/`basename $0` [message describing the run] [rule or invariant]" + echo "" + exit 1 +fi + +rule=$1 +msg=$2 +shift 2 + +certoraRun \ + certora/harnesses/ERC20VotesHarness.sol \ + --verify ERC20VotesHarness:certora/specs/ERC20Votes.spec \ + --solc solc8.2 \ + --optimistic_loop \ + --rule ${rule} \ + --msg "${msg}" \ + --staging \ + # --rule_sanity \ \ No newline at end of file diff --git a/certora/scripts/verifyERC20Votes.sh b/certora/scripts/verifyERC20Votes.sh index bb8c8e749..15f282307 100644 --- a/certora/scripts/verifyERC20Votes.sh +++ b/certora/scripts/verifyERC20Votes.sh @@ -1,7 +1,23 @@ +make -C certora munged + +if [ -z "$1" ] + then + echo "Incorrect number of arguments" + echo "" + echo "Usage: (from git root)" + echo " ./certora/scripts/`basename $0` [message describing the run]" + echo "" + exit 1 +fi + +msg=$1 +shift 1 + certoraRun \ certora/harnesses/ERC20VotesHarness.sol \ --verify ERC20VotesHarness:certora/specs/ERC20Votes.spec \ --solc solc8.2 \ --optimistic_loop \ - --cloud \ - --msg "sanityVotes" + --loop_iter 4 \ + --staging \ + --msg "${msg}"