Browse Source

run scripts

Nick Armstrong 3 years ago
parent
commit
6c5d33ba22
2 changed files with 41 additions and 2 deletions
  1. 23 0
      certora/scripts/ERC20VotesRule.sh
  2. 18 2
      certora/scripts/verifyERC20Votes.sh

+ 23 - 0
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 \

+ 18 - 2
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}"