Browse Source

cleanup scripts/*.sh

Hadrien Croubois 3 years ago
parent
commit
cc7837fb46

+ 0 - 26
certora/run.sh

@@ -1,26 +0,0 @@
-#!/bin/bash
-
-for receipt in $(cat certora/matrix.json | jq -r ".[$1] | @base64")
-do
-    FILE=$(echo $receipt | base64 --decode | jq -r '.file')
-    NAME=$(echo $receipt | base64 --decode | jq -r '.name')
-    SPEC=$(echo $receipt | base64 --decode | jq -r '.spec')
-    ARGS=$(echo $receipt | base64 --decode | jq -r '.args//""')
-    DISABLED=$(echo $receipt | base64 --decode | jq -r '.disabled//false')
-
-
-    echo "Running $SPEC on $FILE:$NAME ..."
-    if [[ $DISABLED == 'true' ]];
-    then
-        echo "disabled"
-    else
-        certoraRun $FILE --verify $NAME:$SPEC --solc solc --optimistic_loop --loop_iter 3 $ARGS --cloud
-    fi
-done
-
-# [00] ERC1155.spec                   -- pass
-# [01] ERC1155Burnable.spec           -- pass
-# [02] ERC1155Pausable.spec           -- pass
-# [03] ERC1155Supply.spec             -- pass
-# [04] GovernorPreventLateQuorum.spec -- nope
-# [05] Initializable.spec             -- nope

+ 3 - 6
certora/scripts/verifyERC1155All.sh

@@ -1,11 +1,8 @@
-make -C certora munged
-
 certoraRun \
 certoraRun \
-    certora/munged/token/ERC1155/ERC1155.sol \
-    --verify ERC1155:certora/specs/ERC1155.spec \
-    --solc solc8.2 \
+    certora/harnesses/ERC1155/ERC1155Harness.sol \
+    --verify ERC1155Harness:certora/specs/ERC1155.spec \
+    --solc solc \
     --optimistic_loop \
     --optimistic_loop \
     --loop_iter 3 \
     --loop_iter 3 \
     --cloud \
     --cloud \
-    --send_only \
     --msg "ERC1155 verification all rules "
     --msg "ERC1155 verification all rules "

+ 1 - 5
certora/scripts/verifyERC1155Burnable.sh

@@ -1,12 +1,8 @@
-make -C certora munged
-
 certoraRun \
 certoraRun \
     certora/harnesses/ERC1155/ERC1155BurnableHarness.sol \
     certora/harnesses/ERC1155/ERC1155BurnableHarness.sol \
     --verify ERC1155BurnableHarness:certora/specs/ERC1155Burnable.spec \
     --verify ERC1155BurnableHarness:certora/specs/ERC1155Burnable.spec \
-    --solc solc8.2 \
+    --solc solc \
     --optimistic_loop \
     --optimistic_loop \
     --loop_iter 3 \
     --loop_iter 3 \
-    --send_only \
     --cloud \
     --cloud \
     --msg "ERC1155 Burnable verification all rules"
     --msg "ERC1155 Burnable verification all rules"
-    

+ 1 - 5
certora/scripts/verifyERC1155BurnableSpecific.sh

@@ -1,13 +1,9 @@
-make -C certora munged
-
 certoraRun \
 certoraRun \
     certora/harnesses/ERC1155/ERC1155BurnableHarness.sol \
     certora/harnesses/ERC1155/ERC1155BurnableHarness.sol \
     --verify ERC1155BurnableHarness:certora/specs/ERC1155Burnable.spec \
     --verify ERC1155BurnableHarness:certora/specs/ERC1155Burnable.spec \
-    --solc solc8.2 \
+    --solc solc \
     --optimistic_loop \
     --optimistic_loop \
     --loop_iter 3 \
     --loop_iter 3 \
     --cloud \
     --cloud \
-    --send_only \
     --rule $1 \
     --rule $1 \
     --msg "ERC1155 Burnable verification specific rule $1"
     --msg "ERC1155 Burnable verification specific rule $1"
-    

+ 1 - 4
certora/scripts/verifyERC1155Pausable.sh

@@ -1,11 +1,8 @@
-make -C certora munged
-
 certoraRun \
 certoraRun \
     certora/harnesses/ERC1155/ERC1155PausableHarness.sol \
     certora/harnesses/ERC1155/ERC1155PausableHarness.sol \
     --verify ERC1155PausableHarness:certora/specs/ERC1155Pausable.spec \
     --verify ERC1155PausableHarness:certora/specs/ERC1155Pausable.spec \
-    --solc solc8.2 \
+    --solc solc \
     --optimistic_loop \
     --optimistic_loop \
     --loop_iter 3 \
     --loop_iter 3 \
-    --send_only \
     --cloud \
     --cloud \
     --msg "ERC1155 Pausable verification all rules"
     --msg "ERC1155 Pausable verification all rules"

+ 1 - 5
certora/scripts/verifyERC1155Specific.sh

@@ -1,13 +1,9 @@
-make -C certora munged
-
 certoraRun \
 certoraRun \
     certora/munged/token/ERC1155/ERC1155.sol \
     certora/munged/token/ERC1155/ERC1155.sol \
     --verify ERC1155:certora/specs/ERC1155.spec \
     --verify ERC1155:certora/specs/ERC1155.spec \
-    --solc solc8.2 \
+    --solc solc \
     --optimistic_loop \
     --optimistic_loop \
     --loop_iter 3 \
     --loop_iter 3 \
     --cloud \
     --cloud \
-    --send_only \
     --rule $1 \
     --rule $1 \
     --msg "ERC1155 Burnable verification specific rule $1"
     --msg "ERC1155 Burnable verification specific rule $1"
-    

+ 1 - 4
certora/scripts/verifyERC1155Supply.sh

@@ -1,11 +1,8 @@
-make -C certora munged
-
 certoraRun \
 certoraRun \
     certora/harnesses/ERC1155/ERC1155SupplyHarness.sol \
     certora/harnesses/ERC1155/ERC1155SupplyHarness.sol \
     --verify ERC1155SupplyHarness:certora/specs/ERC1155Supply.spec \
     --verify ERC1155SupplyHarness:certora/specs/ERC1155Supply.spec \
-    --solc solc8.2 \
+    --solc solc \
     --optimistic_loop \
     --optimistic_loop \
     --loop_iter 3 \
     --loop_iter 3 \
     --cloud \
     --cloud \
-    --send_only \
     --msg "ERC1155 Supply verification all rules"
     --msg "ERC1155 Supply verification all rules"

+ 1 - 5
certora/scripts/verifyGovernorPreventLateQuorum.sh

@@ -3,10 +3,6 @@ certoraRun \
     --verify GovernorPreventLateQuorumHarness:certora/specs/GovernorPreventLateQuorum.spec \
     --verify GovernorPreventLateQuorumHarness:certora/specs/GovernorPreventLateQuorum.spec \
     --solc solc \
     --solc solc \
     --optimistic_loop \
     --optimistic_loop \
-    --rule_sanity advanced \
-    --send_only \
     --loop_iter 1 \
     --loop_iter 1 \
+    --rule_sanity advanced \
     --msg "all sanity" \
     --msg "all sanity" \
-
-
-

+ 1 - 5
certora/scripts/verifyInitializable.sh

@@ -3,10 +3,6 @@ certoraRun \
     --verify InitializableComplexHarness:certora/specs/Initializable.spec \
     --verify InitializableComplexHarness:certora/specs/Initializable.spec \
     --solc solc \
     --solc solc \
     --optimistic_loop \
     --optimistic_loop \
-    --send_only \
-    --rule_sanity advanced \
     --loop_iter 3 \
     --loop_iter 3 \
+    --rule_sanity advanced \
     --msg "all complex sanity" \
     --msg "all complex sanity" \
-
-
-