Преглед изворни кода

enable ci test for some (passing) rules

Hadrien Croubois пре 3 година
родитељ
комит
634c37becf

+ 0 - 7
certora/scripts/noCI/Round3/verifyERC1155Burnable.sh

@@ -1,7 +0,0 @@
-certoraRun \
-    certora/harnesses/ERC1155/ERC1155BurnableHarness.sol \
-    --verify ERC1155BurnableHarness:certora/specs/ERC1155Burnable.spec \
-    --solc solc \
-    --optimistic_loop \
-    --loop_iter 3 \
-    --msg "ERC1155 Burnable verification all rules"

+ 0 - 7
certora/scripts/noCI/Round3/verifyERC1155Pausable.sh

@@ -1,7 +0,0 @@
-certoraRun \
-    certora/harnesses/ERC1155/ERC1155PausableHarness.sol \
-    --verify ERC1155PausableHarness:certora/specs/ERC1155Pausable.spec \
-    --solc solc \
-    --optimistic_loop \
-    --loop_iter 3 \
-    --msg "ERC1155 Pausable verification all rules"

+ 0 - 7
certora/scripts/noCI/Round3/verifyERC1155Supply.sh

@@ -1,7 +0,0 @@
-certoraRun \
-    certora/harnesses/ERC1155/ERC1155SupplyHarness.sol \
-    --verify ERC1155SupplyHarness:certora/specs/ERC1155Supply.spec \
-    --solc solc \
-    --optimistic_loop \
-    --loop_iter 3 \
-    --msg "ERC1155 Supply verification all rules"

+ 10 - 2
certora/scripts/noCI/Round3/verifyGovernorPreventLateQuorum.sh

@@ -1,7 +1,15 @@
+#!/usr/bin/env bash
+
+set -euxo pipefail
+
 certoraRun \
-    certora/harnesses/ERC721VotesHarness.sol certora/munged/governance/TimelockController.sol certora/harnesses/GovernorPreventLateQuorumHarness.sol \
+    certora/harnesses/ERC20VotesHarness.sol \
+    certora/harnesses/ERC721VotesHarness.sol \
+    certora/munged/governance/TimelockController.sol \
+    certora/harnesses/GovernorPreventLateQuorumHarness.sol \
     --verify GovernorPreventLateQuorumHarness:certora/specs/GovernorPreventLateQuorum.spec \
     --solc solc \
     --optimistic_loop \
     --loop_iter 1 \
-    --msg "GovernorPreventLateQuorum verification all rules" \
+    --rule_sanity advanced \
+    --msg "all sanity" \

+ 0 - 7
certora/scripts/noCI/Round3/verifyInitializable.sh

@@ -1,7 +0,0 @@
-certoraRun \
-    certora/harnesses/InitializableComplexHarness.sol \
-    --verify InitializableComplexHarness:certora/specs/Initializable.spec \
-    --solc solc \
-    --optimistic_loop \
-    --loop_iter 3 \
-    --msg "Initializable verificaiton all rules on complex harness" \

+ 0 - 11
certora/scripts/noCI/verifyERC1155All.sh

@@ -1,11 +0,0 @@
-#!/usr/bin/env bash
-
-set -euxo pipefail
-
-certoraRun \
-    certora/harnesses/ERC1155/ERC1155Harness.sol \
-    --verify ERC1155Harness:certora/specs/ERC1155.spec \
-    --solc solc \
-    --optimistic_loop \
-    --loop_iter 3 \
-    --msg "ERC1155 verification all rules "

+ 0 - 15
certora/scripts/noCI/verifyGovernorPreventLateQuorum.sh

@@ -1,15 +0,0 @@
-#!/usr/bin/env bash
-
-set -euxo pipefail
-
-certoraRun \
-    certora/harnesses/ERC20VotesHarness.sol \
-    certora/harnesses/ERC721VotesHarness.sol \
-    certora/munged/governance/TimelockController.sol \
-    certora/harnesses/GovernorPreventLateQuorumHarness.sol \
-    --verify GovernorPreventLateQuorumHarness:certora/specs/GovernorPreventLateQuorum.spec \
-    --solc solc \
-    --optimistic_loop \
-    --loop_iter 1 \
-    --rule_sanity advanced \
-    --msg "all sanity" \

+ 0 - 1
certora/scripts/noCI/Round2/verifyAccessControl.sh → certora/scripts/passes/verifyAccessControl.sh

@@ -7,5 +7,4 @@ certoraRun \
     --verify AccessControlHarness:certora/specs/AccessControl.spec \
     --solc solc \
     --optimistic_loop \
-    --msg "AccessControl verification" \
     $@

+ 0 - 1
certora/scripts/noCI/Round2/verifyERC1155.sh → certora/scripts/passes/verifyERC1155.sh

@@ -8,5 +8,4 @@ certoraRun \
     --solc solc \
     --optimistic_loop \
     --loop_iter 3 \
-    --msg "ERC1155" \
     $@

+ 1 - 1
certora/scripts/noCI/verifyERC1155Burnable.sh → certora/scripts/passes/verifyERC1155Burnable.sh

@@ -8,4 +8,4 @@ certoraRun \
     --solc solc \
     --optimistic_loop \
     --loop_iter 3 \
-    --msg "ERC1155 Burnable verification all rules"
+    $@

+ 1 - 1
certora/scripts/noCI/verifyERC1155Pausable.sh → certora/scripts/passes/verifyERC1155Pausable.sh

@@ -8,4 +8,4 @@ certoraRun \
     --solc solc \
     --optimistic_loop \
     --loop_iter 3 \
-    --msg "ERC1155 Pausable verification all rules"
+    $@

+ 1 - 1
certora/scripts/noCI/verifyERC1155Supply.sh → certora/scripts/passes/verifyERC1155Supply.sh

@@ -8,4 +8,4 @@ certoraRun \
     --solc solc \
     --optimistic_loop \
     --loop_iter 3 \
-    --msg "ERC1155 Supply verification all rules"
+    $@

+ 0 - 1
certora/scripts/noCI/Round2/verifyERC721Votes.sh → certora/scripts/passes/verifyERC721Votes.sh

@@ -9,5 +9,4 @@ certoraRun \
     --optimistic_loop \
     --disableLocalTypeChecking \
     --settings -copyLoopUnroll=4 \
-    --msg "ERC721Votes" \
     $@

+ 1 - 2
certora/scripts/noCI/verifyInitializable.sh → certora/scripts/passes/verifyInitializable.sh

@@ -8,5 +8,4 @@ certoraRun \
     --solc solc \
     --optimistic_loop \
     --loop_iter 3 \
-    --rule_sanity advanced \
-    --msg "all complex sanity" \
+    $@

+ 0 - 1
certora/scripts/noCI/Round2/verifyTimelock.sh → certora/scripts/passes/verifyTimelock.sh

@@ -9,5 +9,4 @@ certoraRun \
     --optimistic_loop \
     --loop_iter 3 \
     --settings -byteMapHashingPrecision=32 \
-    --msg "TimelockController verification" \
     $@

+ 1 - 1
certora/specs/ERC20.spec

@@ -1,4 +1,4 @@
-import "interfaces/erc20.spec"
+import "erc20.spec"
 
 /*
 ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐

+ 0 - 0
certora/specs/interfaces/erc20.spec → certora/specs/erc20.spec