reorganized governance verification in preparation for erc20 verification

This commit is contained in:
Michael George
2021-12-17 09:22:06 -05:00
parent 7912b1af7d
commit b5980a569c
8 changed files with 1 additions and 43 deletions

View File

@ -1,10 +0,0 @@
make -C certora munged
certoraRun certora/harnesses/ERC20VotesHarness.sol certora/harnesses/GovernorHarness.sol \
--verify GovernorHarness:certora/specs/GovernorBase.spec \
--solc solc8.0 \
--staging shelly/forSasha \
--optimistic_loop \
--settings -copyLoopUnroll=4 \
--rule voteStartBeforeVoteEnd \
--msg "$1"

View File

@ -1,10 +0,0 @@
make -C certora munged
certoraRun certora/harnesses/ERC20VotesHarness.sol certora/harnesses/GovernorBasicHarness.sol \
--verify GovernorBasicHarness:certora/specs/GovernorCountingSimple.spec \
--solc solc8.2 \
--staging shelly/forSasha \
--optimistic_loop \
--settings -copyLoopUnroll=4 \
--rule hasVotedCorrelation \
--msg "$1"

View File

@ -1,12 +0,0 @@
make -C certora munged
certoraRun certora/harnesses/ERC20VotesHarness.sol certora/harnesses/WizardControlFirstPriority.sol \
--link WizardControlFirstPriority:token=ERC20VotesHarness \
--verify WizardControlFirstPriority:certora/specs/GovernorBase.spec \
--solc solc8.2 \
--disableLocalTypeChecking \
--staging shelly/forSasha \
--optimistic_loop \
--settings -copyLoopUnroll=4 \
--rule canVoteDuringVotingPeriod \
--msg "$1"

View File

@ -1,10 +0,0 @@
make -C certora munged
certoraRun certora/harnesses/ERC20VotesHarness.sol certora/harnesses/WizardFirstTry.sol \
--verify WizardFirstTry:certora/specs/GovernorBase.spec \
--solc solc8.2 \
--staging shelly/forSasha \
--optimistic_loop \
--disableLocalTypeChecking \
--settings -copyLoopUnroll=4 \
--msg "$1"

View File

@ -4,7 +4,7 @@ make -C certora munged
for contract in certora/harnesses/Wizard*.sol;
do
for spec in certora/specs/*.spec;
for spec in certora/specs/governor*.spec;
do
contractFile=$(basename $contract)
specFile=$(basename $spec)