From 38d21cab86c3c87ac86fecb6364af8350a0a3275 Mon Sep 17 00:00:00 2001 From: Hadrien Croubois Date: Thu, 22 Sep 2022 18:56:59 +0200 Subject: [PATCH] update scripts --- certora/.gitignore | 1 + certora/applyHarness.patch | 6 --- .../harnesses/WizardControlFirstPriority.sol | 4 +- certora/munged/.gitignore | 2 - certora/scripts/Round1/Governor.sh | 14 ++++--- .../Round1/GovernorCountingSimple-counting.sh | 13 +++--- certora/scripts/Round1/sanity.sh | 20 ++++----- certora/scripts/Round1/sanityGovernor.sh | 14 ++++--- certora/scripts/Round1/sanityTokens.sh | 10 ++--- certora/scripts/Round1/verifyAll.sh | 41 +++++++++---------- certora/scripts/Round1/verifyGovernor.sh | 40 +++++++++--------- certora/scripts/verifyERC1155All.sh | 5 ++- certora/scripts/verifyERC1155Burnable.sh | 5 ++- .../scripts/verifyERC1155BurnableSpecific.sh | 9 ---- certora/scripts/verifyERC1155Pausable.sh | 5 ++- certora/scripts/verifyERC1155Specific.sh | 9 ---- certora/scripts/verifyERC1155Supply.sh | 5 ++- .../verifyGovernorPreventLateQuorum.sh | 4 ++ certora/scripts/verifyInitializable.sh | 4 ++ certora/specs/sanity.spec | 1 - 20 files changed, 106 insertions(+), 106 deletions(-) create mode 100644 certora/.gitignore delete mode 100644 certora/munged/.gitignore delete mode 100644 certora/scripts/verifyERC1155BurnableSpecific.sh delete mode 100644 certora/scripts/verifyERC1155Specific.sh diff --git a/certora/.gitignore b/certora/.gitignore new file mode 100644 index 000000000..d632c9acc --- /dev/null +++ b/certora/.gitignore @@ -0,0 +1 @@ +munged diff --git a/certora/applyHarness.patch b/certora/applyHarness.patch index 834c2b40b..c69692496 100644 --- a/certora/applyHarness.patch +++ b/certora/applyHarness.patch @@ -10,12 +10,6 @@ diff -ruN access/AccessControl.sol access/AccessControl.sol _checkRole(role, _msgSender()); } -diff -ruN .gitignore .gitignore ---- .gitignore 1970-01-01 01:00:00.000000000 +0100 -+++ .gitignore 2022-09-20 14:34:08.626268788 +0200 -@@ -0,0 +1,2 @@ -+* -+!.gitignore diff -ruN governance/extensions/GovernorCountingSimple.sol governance/extensions/GovernorCountingSimple.sol --- governance/extensions/GovernorCountingSimple.sol 2022-09-20 11:01:10.432848512 +0200 +++ governance/extensions/GovernorCountingSimple.sol 2022-09-20 14:34:08.632935582 +0200 diff --git a/certora/harnesses/WizardControlFirstPriority.sol b/certora/harnesses/WizardControlFirstPriority.sol index 856b688fd..8fdce291e 100644 --- a/certora/harnesses/WizardControlFirstPriority.sol +++ b/certora/harnesses/WizardControlFirstPriority.sol @@ -9,7 +9,7 @@ import "../munged/governance/extensions/GovernorTimelockControl.sol"; import "../munged/governance/extensions/GovernorProposalThreshold.sol"; import "../munged/token/ERC20/extensions/ERC20Votes.sol"; -/* +/* Wizard options: ProposalThreshhold = 10 ERC20Votes @@ -106,7 +106,7 @@ contract WizardControlFirstPriority is function getVotes(address account, uint256 blockNumber) public view - override(IGovernor, GovernorVotes) + override(IGovernor, Governor) returns (uint256) { return super.getVotes(account, blockNumber); diff --git a/certora/munged/.gitignore b/certora/munged/.gitignore deleted file mode 100644 index d6b7ef32c..000000000 --- a/certora/munged/.gitignore +++ /dev/null @@ -1,2 +0,0 @@ -* -!.gitignore diff --git a/certora/scripts/Round1/Governor.sh b/certora/scripts/Round1/Governor.sh index 5ca0f239b..525731d97 100755 --- a/certora/scripts/Round1/Governor.sh +++ b/certora/scripts/Round1/Governor.sh @@ -1,10 +1,12 @@ -make -C certora munged +#!/usr/bin/env bash -certoraRun certora/harnesses/ERC20VotesHarness.sol certora/harnesses/GovernorHarness.sol \ - --verify GovernorHarness:certora/specs/GovernorBase.spec \ +set -euxo pipefail + +# Changed: GovernorHarness → GovernorPreventLateQuorumHarness +certoraRun \ + certora/harnesses/ERC20VotesHarness.sol certora/harnesses/GovernorPreventLateQuorumHarness.sol \ + --verify GovernorPreventLateQuorumHarness:certora/specs/GovernorBase.spec \ --solc solc \ - --staging shelly/forSasha \ --optimistic_loop \ --settings -copyLoopUnroll=4 \ - --rule voteStartBeforeVoteEnd \ - --msg "$1" + --rule voteStartBeforeVoteEnd diff --git a/certora/scripts/Round1/GovernorCountingSimple-counting.sh b/certora/scripts/Round1/GovernorCountingSimple-counting.sh index 2d209d3f9..2ead5ae58 100644 --- a/certora/scripts/Round1/GovernorCountingSimple-counting.sh +++ b/certora/scripts/Round1/GovernorCountingSimple-counting.sh @@ -1,8 +1,11 @@ -make -C certora munged +#!/usr/bin/env bash -certoraRun certora/harnesses/ERC20VotesHarness.sol certora/harnesses/GovernorBasicHarness.sol \ - --verify GovernorBasicHarness:certora/specs/GovernorCountingSimple.spec \ +set -euxo pipefail + +# Changed: GovernorBasicHarness → GovernorPreventLateQuorumHarness +certoraRun \ + certora/harnesses/ERC20VotesHarness.sol certora/harnesses/GovernorPreventLateQuorumHarness.sol \ + --verify GovernorPreventLateQuorumHarness:certora/specs/GovernorCountingSimple.spec \ --solc solc \ --optimistic_loop \ - --settings -copyLoopUnroll=4 \ - --msg "$1" + --settings -copyLoopUnroll=4 diff --git a/certora/scripts/Round1/sanity.sh b/certora/scripts/Round1/sanity.sh index be8f404a6..8deed442f 100644 --- a/certora/scripts/Round1/sanity.sh +++ b/certora/scripts/Round1/sanity.sh @@ -1,16 +1,19 @@ -# make -C certora munged +#!/usr/bin/env bash + +set -euxo pipefail # for f in certora/harnesses/Wizard*.sol # do # echo "Processing $f" # file=$(basename $f) # echo ${file%.*} -# certoraRun certora/harnesses/$file \ -# --verify ${file%.*}:certora/specs/sanity.spec "$@" \ -# --solc solc --staging shelly/forSasha \ -# --optimistic_loop \ -# --msg "checking sanity on ${file%.*}" -# --settings -copyLoopUnroll=4 +# certoraRun \ +# certora/harnesses/$file \ +# --verify ${file%.*}:certora/specs/sanity.spec "$@" \ +# --solc solc \ +# --optimistic_loop \ +# --settings -copyLoopUnroll=4 \ +# --msg "checking sanity on ${file%.*}" # done # TimelockController @@ -19,16 +22,13 @@ certoraRun \ --verify TimelockControllerHarness:certora/specs/sanity.spec \ --solc solc \ --optimistic_loop \ - --cloud \ --msg "sanity and keccak check" - # Votes # certoraRun \ # certora/harnesses/VotesHarness.sol \ # --verify VotesHarness:certora/specs/sanity.spec \ # --solc solc \ # --optimistic_loop \ -# --cloud \ # --settings -strictDecompiler=false,-assumeUnwindCond \ # --msg "sanityVotes" diff --git a/certora/scripts/Round1/sanityGovernor.sh b/certora/scripts/Round1/sanityGovernor.sh index f979dd364..50d9adb59 100755 --- a/certora/scripts/Round1/sanityGovernor.sh +++ b/certora/scripts/Round1/sanityGovernor.sh @@ -1,4 +1,6 @@ -make -C certora munged +#!/usr/bin/env bash + +set -euxo pipefail for f in certora/harnesses/Wizard*.sol do @@ -6,9 +8,9 @@ do file=$(basename $f) echo ${file%.*} certoraRun certora/harnesses/$file \ - --verify ${file%.*}:certora/specs/sanity.spec "$@" \ - --solc solc --staging shelly/forSasha \ - --optimistic_loop \ - --msg "checking sanity on ${file%.*}" - --settings -copyLoopUnroll=4 + --verify ${file%.*}:certora/specs/sanity.spec "$@" \ + --solc solc \ + --optimistic_loop \ + --settings -copyLoopUnroll=4 \ + --msg "checking sanity on ${file%.*}" done diff --git a/certora/scripts/Round1/sanityTokens.sh b/certora/scripts/Round1/sanityTokens.sh index 308a00623..c0de4260f 100755 --- a/certora/scripts/Round1/sanityTokens.sh +++ b/certora/scripts/Round1/sanityTokens.sh @@ -1,6 +1,6 @@ -#!/bin/bash +#!/usr/bin/env bash -make -C certora munged +set -euxo pipefail for f in certora/harnesses/ERC20{Votes,Permit,Wrapper}Harness.sol do @@ -9,8 +9,8 @@ do echo ${file%.*} certoraRun certora/harnesses/$file \ --verify ${file%.*}:certora/specs/sanity.spec "$@" \ - --solc solc --staging \ + --solc solc \ --optimistic_loop \ - --msg "checking sanity on ${file%.*}" \ - --settings -copyLoopUnroll=4,-strictDecompiler=false + --settings -copyLoopUnroll=4,-strictDecompiler=false \ + --msg "checking sanity on ${file%.*}" done diff --git a/certora/scripts/Round1/verifyAll.sh b/certora/scripts/Round1/verifyAll.sh index d770a8963..a7d3c8ed2 100644 --- a/certora/scripts/Round1/verifyAll.sh +++ b/certora/scripts/Round1/verifyAll.sh @@ -1,11 +1,10 @@ -#!/bin/bash - -make -C certora munged - +#!/usr/bin/env bash +set -euxo pipefail for contract in certora/harnesses/Wizard*.sol; do + # NOTE: some spec wile are not governor related, and should be run on Wizard*.sol for spec in certora/specs/*.spec; do contractFile=$(basename $contract) @@ -15,24 +14,24 @@ do echo "Processing ${contractFile%.*} with $specFile" if [[ "${contractFile%.*}" = *"WizardControl"* ]]; then - certoraRun certora/harnesses/ERC20VotesHarness.sol certora/harnesses/$contractFile \ - --link ${contractFile%.*}:token=ERC20VotesHarness \ - --verify ${contractFile%.*}:certora/specs/$specFile "$@" \ - --solc solc \ - --staging shelly/forSasha \ - --disableLocalTypeChecking \ - --optimistic_loop \ - --settings -copyLoopUnroll=4 \ - --msg "checking $specFile on ${contractFile%.*}" + certoraRun \ + certora/harnesses/ERC20VotesHarness.sol certora/harnesses/$contractFile \ + --link ${contractFile%.*}:token=ERC20VotesHarness \ + --verify ${contractFile%.*}:certora/specs/$specFile "$@" \ + --solc solc \ + --optimistic_loop \ + --disableLocalTypeChecking \ + --settings -copyLoopUnroll=4 \ + --msg "checking $specFile on ${contractFile%.*}" else - certoraRun certora/harnesses/ERC20VotesHarness.sol certora/harnesses/$contractFile \ - --verify ${contractFile%.*}:certora/specs/$specFile "$@" \ - --solc solc \ - --staging shelly/forSasha \ - --disableLocalTypeChecking \ - --optimistic_loop \ - --settings -copyLoopUnroll=4 \ - --msg "checking $specFile on ${contractFile%.*}" + certoraRun \ + certora/harnesses/ERC20VotesHarness.sol certora/harnesses/$contractFile \ + --verify ${contractFile%.*}:certora/specs/$specFile "$@" \ + --solc solc \ + --optimistic_loop \ + --disableLocalTypeChecking \ + --settings -copyLoopUnroll=4 \ + --msg "checking $specFile on ${contractFile%.*}" fi fi done diff --git a/certora/scripts/Round1/verifyGovernor.sh b/certora/scripts/Round1/verifyGovernor.sh index 0ce0eb1e5..7f01f3acc 100755 --- a/certora/scripts/Round1/verifyGovernor.sh +++ b/certora/scripts/Round1/verifyGovernor.sh @@ -1,10 +1,10 @@ -#!/bin/bash +#!/usr/bin/env bash -make -C certora munged +set -euxo pipefail for contract in certora/harnesses/Wizard*.sol; do - for spec in certora/specs/governor*.spec; + for spec in certora/specs/Governor*.spec; do contractFile=$(basename $contract) specFile=$(basename $spec) @@ -13,24 +13,24 @@ do echo "Processing ${contractFile%.*} with $specFile" if [[ "${contractFile%.*}" = *"WizardControl"* ]]; then - certoraRun certora/harnesses/ERC20VotesHarness.sol certora/harnesses/$contractFile \ - --link ${contractFile%.*}:token=ERC20VotesHarness \ - --verify ${contractFile%.*}:certora/specs/$specFile "$@" \ - --solc solc \ - --staging shelly/forSasha \ - --disableLocalTypeChecking \ - --optimistic_loop \ - --settings -copyLoopUnroll=4 \ - --msg "checking $specFile on ${contractFile%.*}" + certoraRun \ + certora/harnesses/ERC20VotesHarness.sol certora/harnesses/$contractFile \ + --link ${contractFile%.*}:token=ERC20VotesHarness \ + --verify ${contractFile%.*}:certora/specs/$specFile "$@" \ + --solc solc \ + --optimistic_loop \ + --disableLocalTypeChecking \ + --settings -copyLoopUnroll=4 \ + --msg "checking $specFile on ${contractFile%.*}" else - certoraRun certora/harnesses/ERC20VotesHarness.sol certora/harnesses/$contractFile \ - --verify ${contractFile%.*}:certora/specs/$specFile "$@" \ - --solc solc \ - --staging shelly/forSasha \ - --disableLocalTypeChecking \ - --optimistic_loop \ - --settings -copyLoopUnroll=4 \ - --msg "checking $specFile on ${contractFile%.*}" + certoraRun \ + certora/harnesses/ERC20VotesHarness.sol certora/harnesses/$contractFile \ + --verify ${contractFile%.*}:certora/specs/$specFile "$@" \ + --solc solc \ + --optimistic_loop \ + --disableLocalTypeChecking \ + --settings -copyLoopUnroll=4 \ + --msg "checking $specFile on ${contractFile%.*}" fi fi done diff --git a/certora/scripts/verifyERC1155All.sh b/certora/scripts/verifyERC1155All.sh index baa0b5684..26484e9dc 100644 --- a/certora/scripts/verifyERC1155All.sh +++ b/certora/scripts/verifyERC1155All.sh @@ -1,8 +1,11 @@ +#!/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 \ - --cloud \ --msg "ERC1155 verification all rules " \ No newline at end of file diff --git a/certora/scripts/verifyERC1155Burnable.sh b/certora/scripts/verifyERC1155Burnable.sh index 275466a0a..73763aae4 100644 --- a/certora/scripts/verifyERC1155Burnable.sh +++ b/certora/scripts/verifyERC1155Burnable.sh @@ -1,8 +1,11 @@ +#!/usr/bin/env bash + +set -euxo pipefail + certoraRun \ certora/harnesses/ERC1155/ERC1155BurnableHarness.sol \ --verify ERC1155BurnableHarness:certora/specs/ERC1155Burnable.spec \ --solc solc \ --optimistic_loop \ --loop_iter 3 \ - --cloud \ --msg "ERC1155 Burnable verification all rules" diff --git a/certora/scripts/verifyERC1155BurnableSpecific.sh b/certora/scripts/verifyERC1155BurnableSpecific.sh deleted file mode 100644 index d43dc8fb0..000000000 --- a/certora/scripts/verifyERC1155BurnableSpecific.sh +++ /dev/null @@ -1,9 +0,0 @@ -certoraRun \ - certora/harnesses/ERC1155/ERC1155BurnableHarness.sol \ - --verify ERC1155BurnableHarness:certora/specs/ERC1155Burnable.spec \ - --solc solc \ - --optimistic_loop \ - --loop_iter 3 \ - --cloud \ - --rule $1 \ - --msg "ERC1155 Burnable verification specific rule $1" diff --git a/certora/scripts/verifyERC1155Pausable.sh b/certora/scripts/verifyERC1155Pausable.sh index 0b99acc45..3870f979c 100755 --- a/certora/scripts/verifyERC1155Pausable.sh +++ b/certora/scripts/verifyERC1155Pausable.sh @@ -1,8 +1,11 @@ +#!/usr/bin/env bash + +set -euxo pipefail + certoraRun \ certora/harnesses/ERC1155/ERC1155PausableHarness.sol \ --verify ERC1155PausableHarness:certora/specs/ERC1155Pausable.spec \ --solc solc \ --optimistic_loop \ --loop_iter 3 \ - --cloud \ --msg "ERC1155 Pausable verification all rules" diff --git a/certora/scripts/verifyERC1155Specific.sh b/certora/scripts/verifyERC1155Specific.sh deleted file mode 100644 index 97b387710..000000000 --- a/certora/scripts/verifyERC1155Specific.sh +++ /dev/null @@ -1,9 +0,0 @@ -certoraRun \ - certora/munged/token/ERC1155/ERC1155.sol \ - --verify ERC1155:certora/specs/ERC1155.spec \ - --solc solc \ - --optimistic_loop \ - --loop_iter 3 \ - --cloud \ - --rule $1 \ - --msg "ERC1155 Burnable verification specific rule $1" diff --git a/certora/scripts/verifyERC1155Supply.sh b/certora/scripts/verifyERC1155Supply.sh index 6008d615a..153963c4c 100755 --- a/certora/scripts/verifyERC1155Supply.sh +++ b/certora/scripts/verifyERC1155Supply.sh @@ -1,8 +1,11 @@ +#!/usr/bin/env bash + +set -euxo pipefail + certoraRun \ certora/harnesses/ERC1155/ERC1155SupplyHarness.sol \ --verify ERC1155SupplyHarness:certora/specs/ERC1155Supply.spec \ --solc solc \ --optimistic_loop \ --loop_iter 3 \ - --cloud \ --msg "ERC1155 Supply verification all rules" diff --git a/certora/scripts/verifyGovernorPreventLateQuorum.sh b/certora/scripts/verifyGovernorPreventLateQuorum.sh index 363335e0e..53e24a999 100644 --- a/certora/scripts/verifyGovernorPreventLateQuorum.sh +++ b/certora/scripts/verifyGovernorPreventLateQuorum.sh @@ -1,3 +1,7 @@ +#!/usr/bin/env bash + +set -euxo pipefail + certoraRun \ certora/harnesses/ERC721VotesHarness.sol certora/munged/governance/TimelockController.sol certora/harnesses/GovernorPreventLateQuorumHarness.sol \ --verify GovernorPreventLateQuorumHarness:certora/specs/GovernorPreventLateQuorum.spec \ diff --git a/certora/scripts/verifyInitializable.sh b/certora/scripts/verifyInitializable.sh index 30a0e7436..00358e18a 100644 --- a/certora/scripts/verifyInitializable.sh +++ b/certora/scripts/verifyInitializable.sh @@ -1,3 +1,7 @@ +#!/usr/bin/env bash + +set -euxo pipefail + certoraRun \ certora/harnesses/InitializableComplexHarness.sol \ --verify InitializableComplexHarness:certora/specs/Initializable.spec \ diff --git a/certora/specs/sanity.spec b/certora/specs/sanity.spec index bd184841a..7bc91aff3 100644 --- a/certora/specs/sanity.spec +++ b/certora/specs/sanity.spec @@ -6,7 +6,6 @@ How it works: - If all execution paths are reverting, we never call the assertion, and the method will pass this rule vacuously. */ - rule sanity(method f) { env e; calldataarg arg;