diff --git a/.github/workflows/formal-verification.yml b/.github/workflows/formal-verification.yml new file mode 100644 index 000000000..6c9935ad4 --- /dev/null +++ b/.github/workflows/formal-verification.yml @@ -0,0 +1,53 @@ +name: formal verification + +on: + push: + branches: + - master + - release-v* + pull_request: {} + workflow_dispatch: {} + +env: + PIP_VERSION: '3.10' + JAVA_VERSION: '11' + SOLC_VERSION: '0.8.19' + +jobs: + apply-diff: + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v3 + - name: Apply patches + run: make -C certora apply + + verify: + runs-on: ubuntu-latest + if: github.event_name != 'pull_request' || contains(github.event.pull_request.labels.*.name, 'formal-verification') + steps: + - uses: actions/checkout@v3 + - name: Set up environment + uses: ./.github/actions/setup + - name: Install python + uses: actions/setup-python@v4 + with: + python-version: ${{ env.PIP_VERSION }} + cache: 'pip' + - name: Install python packages + run: pip install -r requirements.txt + - name: Install java + uses: actions/setup-java@v3 + with: + distribution: temurin + java-version: ${{ env.JAVA_VERSION }} + - name: Install solc + run: | + wget https://github.com/ethereum/solidity/releases/download/v${{ env.SOLC_VERSION }}/solc-static-linux + sudo mv solc-static-linux /usr/local/bin/solc + chmod +x /usr/local/bin/solc + - name: Verify specification + run: | + make -C certora apply + node certora/run.js >> "$GITHUB_STEP_SUMMARY" + env: + CERTORAKEY: ${{ secrets.CERTORAKEY }} diff --git a/certora/.gitignore b/certora/.gitignore new file mode 100644 index 000000000..893adcd31 --- /dev/null +++ b/certora/.gitignore @@ -0,0 +1 @@ +patched diff --git a/certora/Makefile b/certora/Makefile index bbbddbcab..50fd6da08 100644 --- a/certora/Makefile +++ b/certora/Makefile @@ -1,24 +1,54 @@ default: help -PATCH = applyHarness.patch -CONTRACTS_DIR = ../contracts -MUNGED_DIR = munged +SRC := ../contracts +DST := patched +DIFF := diff +SRCS := $(shell find $(SRC) -type f) +DSTS := $(shell find $(DST) -type f) +DIFFS := $(shell find $(DIFF) -type f) +############################################################################### +# Apply all patches in the $DIFF folder to the $DST folder +apply: $(DST) $(patsubst $(DIFF)/%.patch,$(DST)/%,$(subst _,/,$(DIFFS))) + +# Reset the $DST folder +$(DST): FORCE + @rm -rf $@ + @cp -r $(SRC) $@ + +# Update a solidity file in the $DST directory using the corresponding patch +$(DST)/%.sol: FORCE + @echo Applying patch to $@ + @patch -p0 -d $(DST) < $(patsubst $(DST)_%,$(DIFF)/%.patch,$(subst /,_,$@)) + +############################################################################### +# Record all difference between $SRC and $DST in patches +record: $(DIFF) $(patsubst %,$(DIFF)/%.patch,$(subst /,_,$(subst $(SRC)/,,$(SRCS)) $(subst $(DST)/,,$(DSTS)))) + +# Create the $DIFF folder +$(DIFF): FORCE + @rm -rf $@ + @mkdir $@ + +# Create the patch file by comparing the source and the destination +$(DIFF)/%.patch: FORCE + @echo Generating patch $@ + @diff -ruN \ + $(patsubst $(DIFF)/%.patch,$(SRC)/%,$(subst _,/,$@)) \ + $(patsubst $(DIFF)/%.patch,$(DST)/%,$(subst _,/,$@)) \ + | sed 's+$(SRC)/++g' \ + | sed 's+$(DST)/++g' \ + > $@ + @[ -s $@ ] || rm $@ + +############################################################################### help: @echo "usage:" + @echo " make apply: create $(DST) directory by applying the patches to $(SRC)" + @echo " make record: record the patches capturing the differences between $(SRC) and $(DST)" @echo " make clean: remove all generated files (those ignored by git)" - @echo " make $(MUNGED_DIR): create $(MUNGED_DIR) directory by applying the patch file to $(CONTRACTS_DIR)" - @echo " make record: record a new patch file capturing the differences between $(CONTRACTS_DIR) and $(MUNGED_DIR)" - -munged: $(wildcard $(CONTRACTS_DIR)/*.sol) $(PATCH) - rm -rf $@ - cp -r $(CONTRACTS_DIR) $@ - patch -p0 -d $@ < $(PATCH) - -record: - diff -ruN $(CONTRACTS_DIR) $(MUNGED_DIR) | sed 's+../contracts/++g' | sed 's+munged/++g' > $(PATCH) clean: git clean -fdX - touch $(PATCH) +FORCE: ; diff --git a/certora/applyHarness.patch b/certora/applyHarness.patch deleted file mode 100644 index 0fbe9acad..000000000 --- a/certora/applyHarness.patch +++ /dev/null @@ -1,101 +0,0 @@ -diff -ruN .gitignore .gitignore ---- .gitignore 1969-12-31 19:00:00.000000000 -0500 -+++ .gitignore 2021-12-09 14:46:33.923637220 -0500 -@@ -0,0 +1,2 @@ -+* -+!.gitignore -diff -ruN governance/compatibility/GovernorCompatibilityBravo.sol governance/compatibility/GovernorCompatibilityBravo.sol ---- governance/compatibility/GovernorCompatibilityBravo.sol 2021-12-03 15:24:56.523654357 -0500 -+++ governance/compatibility/GovernorCompatibilityBravo.sol 2021-12-09 14:46:33.923637220 -0500 -@@ -245,7 +245,7 @@ - /** - * @dev See {Governor-_quorumReached}. In this module, only forVotes count toward the quorum. - */ -- function _quorumReached(uint256 proposalId) internal view virtual override returns (bool) { -+ function _quorumReached(uint256 proposalId) public view virtual override returns (bool) { // HARNESS: changed to public from internal - ProposalDetails storage details = _proposalDetails[proposalId]; - return quorum(proposalSnapshot(proposalId)) <= details.forVotes; - } -@@ -253,7 +253,7 @@ - /** - * @dev See {Governor-_voteSucceeded}. In this module, the forVotes must be scritly over the againstVotes. - */ -- function _voteSucceeded(uint256 proposalId) internal view virtual override returns (bool) { -+ function _voteSucceeded(uint256 proposalId) public view virtual override returns (bool) { // HARNESS: changed to public from internal - ProposalDetails storage details = _proposalDetails[proposalId]; - return details.forVotes > details.againstVotes; - } -diff -ruN governance/extensions/GovernorCountingSimple.sol governance/extensions/GovernorCountingSimple.sol ---- governance/extensions/GovernorCountingSimple.sol 2021-12-03 15:24:56.523654357 -0500 -+++ governance/extensions/GovernorCountingSimple.sol 2021-12-09 14:46:33.923637220 -0500 -@@ -64,7 +64,7 @@ - /** - * @dev See {Governor-_quorumReached}. - */ -- function _quorumReached(uint256 proposalId) internal view virtual override returns (bool) { -+ function _quorumReached(uint256 proposalId) public view virtual override returns (bool) { - ProposalVote storage proposalvote = _proposalVotes[proposalId]; - - return quorum(proposalSnapshot(proposalId)) <= proposalvote.forVotes + proposalvote.abstainVotes; -@@ -73,7 +73,7 @@ - /** - * @dev See {Governor-_voteSucceeded}. In this module, the forVotes must be strictly over the againstVotes. - */ -- function _voteSucceeded(uint256 proposalId) internal view virtual override returns (bool) { -+ function _voteSucceeded(uint256 proposalId) public view virtual override returns (bool) { - ProposalVote storage proposalvote = _proposalVotes[proposalId]; - - return proposalvote.forVotes > proposalvote.againstVotes; -diff -ruN governance/extensions/GovernorTimelockControl.sol governance/extensions/GovernorTimelockControl.sol ---- governance/extensions/GovernorTimelockControl.sol 2021-12-03 15:24:56.523654357 -0500 -+++ governance/extensions/GovernorTimelockControl.sol 2021-12-09 14:46:33.923637220 -0500 -@@ -111,7 +111,7 @@ - bytes[] memory calldatas, - bytes32 descriptionHash - ) internal virtual override { -- _timelock.executeBatch{value: msg.value}(targets, values, calldatas, 0, descriptionHash); -+ _timelock.executeBatch{value: msg.value}(targets, values, calldatas, 0, descriptionHash); - } - - /** -diff -ruN governance/Governor.sol governance/Governor.sol ---- governance/Governor.sol 2021-12-03 15:24:56.523654357 -0500 -+++ governance/Governor.sol 2021-12-09 14:46:56.411503587 -0500 -@@ -38,8 +38,8 @@ - - string private _name; - -- mapping(uint256 => ProposalCore) private _proposals; -- -+ mapping(uint256 => ProposalCore) public _proposals; -+ - /** - * @dev Restrict access to governor executing address. Some module might override the _executor function to make - * sure this modifier is consistent with the execution model. -@@ -167,12 +167,12 @@ - /** - * @dev Amount of votes already cast passes the threshold limit. - */ -- function _quorumReached(uint256 proposalId) internal view virtual returns (bool); -+ function _quorumReached(uint256 proposalId) public view virtual returns (bool); // HARNESS: changed to public from internal - - /** - * @dev Is the proposal successful or not. - */ -- function _voteSucceeded(uint256 proposalId) internal view virtual returns (bool); -+ function _voteSucceeded(uint256 proposalId) public view virtual returns (bool); // HARNESS: changed to public from internal - - /** - * @dev Register a vote with a given support and voting weight. -diff -ruN token/ERC20/extensions/ERC20Votes.sol token/ERC20/extensions/ERC20Votes.sol ---- token/ERC20/extensions/ERC20Votes.sol 2021-12-03 15:24:56.527654330 -0500 -+++ token/ERC20/extensions/ERC20Votes.sol 2021-12-09 14:46:33.927637196 -0500 -@@ -84,7 +84,7 @@ - * - * - `blockNumber` must have been already mined - */ -- function getPastVotes(address account, uint256 blockNumber) public view returns (uint256) { -+ function getPastVotes(address account, uint256 blockNumber) public view virtual returns (uint256) { - require(blockNumber < block.number, "ERC20Votes: block not yet mined"); - return _checkpointsLookup(_checkpoints[account], blockNumber); - } diff --git a/certora/harnesses/AccessControlHarness.sol b/certora/harnesses/AccessControlHarness.sol new file mode 100644 index 000000000..0cb1e55d4 --- /dev/null +++ b/certora/harnesses/AccessControlHarness.sol @@ -0,0 +1,7 @@ +// SPDX-License-Identifier: MIT + +pragma solidity ^0.8.0; + +import "../patched/access/AccessControl.sol"; + +contract AccessControlHarness is AccessControl {} diff --git a/certora/harnesses/ERC20FlashMintHarness.sol b/certora/harnesses/ERC20FlashMintHarness.sol new file mode 100644 index 000000000..119eb4768 --- /dev/null +++ b/certora/harnesses/ERC20FlashMintHarness.sol @@ -0,0 +1,36 @@ +// SPDX-License-Identifier: MIT + +pragma solidity ^0.8.0; + +import "../patched/token/ERC20/ERC20.sol"; +import "../patched/token/ERC20/extensions/ERC20Permit.sol"; +import "../patched/token/ERC20/extensions/ERC20FlashMint.sol"; + +contract ERC20FlashMintHarness is ERC20, ERC20Permit, ERC20FlashMint { + uint256 someFee; + address someFeeReceiver; + + constructor(string memory name, string memory symbol) ERC20(name, symbol) ERC20Permit(name) {} + + function mint(address account, uint256 amount) external { + _mint(account, amount); + } + + function burn(address account, uint256 amount) external { + _burn(account, amount); + } + + // public accessor + function flashFeeReceiver() public view returns (address) { + return someFeeReceiver; + } + + // internal hook + function _flashFee(address, uint256) internal view override returns (uint256) { + return someFee; + } + + function _flashFeeReceiver() internal view override returns (address) { + return someFeeReceiver; + } +} diff --git a/certora/harnesses/ERC20PermitHarness.sol b/certora/harnesses/ERC20PermitHarness.sol new file mode 100644 index 000000000..cc66358b2 --- /dev/null +++ b/certora/harnesses/ERC20PermitHarness.sol @@ -0,0 +1,18 @@ +// SPDX-License-Identifier: MIT + +pragma solidity ^0.8.0; + +import "../patched/token/ERC20/ERC20.sol"; +import "../patched/token/ERC20/extensions/ERC20Permit.sol"; + +contract ERC20PermitHarness is ERC20, ERC20Permit { + constructor(string memory name, string memory symbol) ERC20(name, symbol) ERC20Permit(name) {} + + function mint(address account, uint256 amount) external { + _mint(account, amount); + } + + function burn(address account, uint256 amount) external { + _burn(account, amount); + } +} diff --git a/certora/harnesses/ERC20VotesHarness.sol b/certora/harnesses/ERC20VotesHarness.sol deleted file mode 100644 index 5067ecfba..000000000 --- a/certora/harnesses/ERC20VotesHarness.sol +++ /dev/null @@ -1,28 +0,0 @@ -import "../munged/token/ERC20/extensions/ERC20Votes.sol"; - -contract ERC20VotesHarness is ERC20Votes { - constructor(string memory name, string memory symbol) ERC20Permit(name) ERC20(name, symbol) {} - - mapping(address => mapping(uint256 => uint256)) public _getPastVotes; - - function _afterTokenTransfer( - address from, - address to, - uint256 amount - ) internal virtual override { - super._afterTokenTransfer(from, to, amount); - _getPastVotes[from][block.number] -= amount; - _getPastVotes[to][block.number] += amount; - } - - /** - * @dev Change delegation for `delegator` to `delegatee`. - * - * Emits events {DelegateChanged} and {DelegateVotesChanged}. - */ - function _delegate(address delegator, address delegatee) internal virtual override{ - super._delegate(delegator, delegatee); - _getPastVotes[delegator][block.number] -= balanceOf(delegator); - _getPastVotes[delegatee][block.number] += balanceOf(delegator); - } -} diff --git a/certora/harnesses/ERC3156FlashBorrowerHarness.sol b/certora/harnesses/ERC3156FlashBorrowerHarness.sol new file mode 100644 index 000000000..0ad29a16e --- /dev/null +++ b/certora/harnesses/ERC3156FlashBorrowerHarness.sol @@ -0,0 +1,13 @@ +// SPDX-License-Identifier: MIT + +import "../patched/interfaces/IERC3156FlashBorrower.sol"; + +pragma solidity ^0.8.0; + +contract ERC3156FlashBorrowerHarness is IERC3156FlashBorrower { + bytes32 somethingToReturn; + + function onFlashLoan(address, address, uint256, uint256, bytes calldata) external view override returns (bytes32) { + return somethingToReturn; + } +} diff --git a/certora/harnesses/WizardControlFirstPriority.sol b/certora/harnesses/WizardControlFirstPriority.sol deleted file mode 100644 index 5ae7fe066..000000000 --- a/certora/harnesses/WizardControlFirstPriority.sol +++ /dev/null @@ -1,150 +0,0 @@ -// SPDX-License-Identifier: MIT -pragma solidity ^0.8.2; - -import "../munged/governance/Governor.sol"; -import "../munged/governance/extensions/GovernorCountingSimple.sol"; -import "../munged/governance/extensions/GovernorVotes.sol"; -import "../munged/governance/extensions/GovernorVotesQuorumFraction.sol"; -import "../munged/governance/extensions/GovernorTimelockControl.sol"; -import "../munged/governance/extensions/GovernorProposalThreshold.sol"; - -/* -Wizard options: -ProposalThreshhold = 10 -ERC20Votes -TimelockController -*/ - -contract WizardControlFirstPriority is Governor, GovernorProposalThreshold, GovernorCountingSimple, GovernorVotes, GovernorVotesQuorumFraction, GovernorTimelockControl { - constructor(ERC20Votes _token, TimelockController _timelock, string memory name, uint256 quorumFraction) - Governor(name) - GovernorVotes(_token) - GovernorVotesQuorumFraction(quorumFraction) - GovernorTimelockControl(_timelock) - {} - - //HARNESS - - function isExecuted(uint256 proposalId) public view returns (bool) { - return _proposals[proposalId].executed; - } - - function isCanceled(uint256 proposalId) public view returns (bool) { - return _proposals[proposalId].canceled; - } - - uint256 _votingDelay; - - uint256 _votingPeriod; - - uint256 _proposalThreshold; - - mapping(uint256 => uint256) public ghost_sum_vote_power_by_id; - - function _castVote( - uint256 proposalId, - address account, - uint8 support, - string memory reason - ) internal override virtual returns (uint256) { - - uint256 deltaWeight = super._castVote(proposalId, account, support, reason); //HARNESS - ghost_sum_vote_power_by_id[proposalId] += deltaWeight; - - return deltaWeight; - } - - function snapshot(uint256 proposalId) public view returns (uint64) { - return _proposals[proposalId].voteStart._deadline; - } - - - function getExecutor() public view returns (address){ - return _executor(); - } - - // original code, harnessed - - function votingDelay() public view override returns (uint256) { // HARNESS: pure -> view - return _votingDelay; // HARNESS: parametric - } - - function votingPeriod() public view override returns (uint256) { // HARNESS: pure -> view - return _votingPeriod; // HARNESS: parametric - } - - function proposalThreshold() public view override returns (uint256) { // HARNESS: pure -> view - return _proposalThreshold; // HARNESS: parametric - } - - // original code, not harnessed - // The following functions are overrides required by Solidity. - - function quorum(uint256 blockNumber) - public - view - override(IGovernor, GovernorVotesQuorumFraction) - returns (uint256) - { - return super.quorum(blockNumber); - } - - function getVotes(address account, uint256 blockNumber) - public - view - override(IGovernor, GovernorVotes) - returns (uint256) - { - return super.getVotes(account, blockNumber); - } - - function state(uint256 proposalId) - public - view - override(Governor, GovernorTimelockControl) - returns (ProposalState) - { - return super.state(proposalId); - } - - function propose(address[] memory targets, uint256[] memory values, bytes[] memory calldatas, string memory description) - public - override(Governor, GovernorProposalThreshold, IGovernor) - returns (uint256) - { - return super.propose(targets, values, calldatas, description); - } - - function _execute(uint256 proposalId, address[] memory targets, uint256[] memory values, bytes[] memory calldatas, bytes32 descriptionHash) - internal - override(Governor, GovernorTimelockControl) - { - super._execute(proposalId, targets, values, calldatas, descriptionHash); - } - - function _cancel(address[] memory targets, uint256[] memory values, bytes[] memory calldatas, bytes32 descriptionHash) - internal - override(Governor, GovernorTimelockControl) - returns (uint256) - { - return super._cancel(targets, values, calldatas, descriptionHash); - } - - function _executor() - internal - view - override(Governor, GovernorTimelockControl) - returns (address) - { - return super._executor(); - } - - function supportsInterface(bytes4 interfaceId) - public - view - override(Governor, GovernorTimelockControl) - returns (bool) - { - return super.supportsInterface(interfaceId); - } -} diff --git a/certora/harnesses/WizardFirstTry.sol b/certora/harnesses/WizardFirstTry.sol deleted file mode 100644 index 83fece04f..000000000 --- a/certora/harnesses/WizardFirstTry.sol +++ /dev/null @@ -1,141 +0,0 @@ -// SPDX-License-Identifier: MIT -pragma solidity ^0.8.2; - -import "../munged/governance/Governor.sol"; -import "../munged/governance/extensions/GovernorCountingSimple.sol"; -import "../munged/governance/extensions/GovernorVotes.sol"; -import "../munged/governance/extensions/GovernorVotesQuorumFraction.sol"; -import "../munged/governance/extensions/GovernorTimelockCompound.sol"; - -/* -Wizard options: -ERC20Votes -TimelockCompound -*/ - -contract WizardFirstTry is Governor, GovernorCountingSimple, GovernorVotes, GovernorVotesQuorumFraction, GovernorTimelockCompound { - constructor(ERC20Votes _token, ICompoundTimelock _timelock, string memory name, uint256 quorumFraction) - Governor(name) - GovernorVotes(_token) - GovernorVotesQuorumFraction(quorumFraction) - GovernorTimelockCompound(_timelock) - {} - - //HARNESS - - function isExecuted(uint256 proposalId) public view returns (bool) { - return _proposals[proposalId].executed; - } - - function isCanceled(uint256 proposalId) public view returns (bool) { - return _proposals[proposalId].canceled; - } - - function snapshot(uint256 proposalId) public view returns (uint64) { - return _proposals[proposalId].voteStart._deadline; - } - - function getExecutor() public view returns (address){ - return _executor(); - } - - uint256 _votingDelay; - - uint256 _votingPeriod; - - mapping(uint256 => uint256) public ghost_sum_vote_power_by_id; - - function _castVote( - uint256 proposalId, - address account, - uint8 support, - string memory reason - ) internal override virtual returns (uint256) { - - uint256 deltaWeight = super._castVote(proposalId, account, support, reason); //HARNESS - ghost_sum_vote_power_by_id[proposalId] += deltaWeight; - - return deltaWeight; - } - - // original code, harnessed - - function votingDelay() public view override virtual returns (uint256) { // HARNESS: pure -> view - return _votingDelay; // HARNESS: parametric - } - - function votingPeriod() public view override virtual returns (uint256) { // HARNESS: pure -> view - return _votingPeriod; // HARNESS: parametric - } - - // original code, not harnessed - // The following functions are overrides required by Solidity. - - function quorum(uint256 blockNumber) - public - view - override(IGovernor, GovernorVotesQuorumFraction) - returns (uint256) - { - return super.quorum(blockNumber); - } - - function getVotes(address account, uint256 blockNumber) - public - view - override(IGovernor, GovernorVotes) - returns (uint256) - { - return super.getVotes(account, blockNumber); - } - - function state(uint256 proposalId) - public - view - override(Governor, GovernorTimelockCompound) - returns (ProposalState) - { - return super.state(proposalId); - } - - function propose(address[] memory targets, uint256[] memory values, bytes[] memory calldatas, string memory description) - public - override(Governor, IGovernor) - returns (uint256) - { - return super.propose(targets, values, calldatas, description); - } - - function _execute(uint256 proposalId, address[] memory targets, uint256[] memory values, bytes[] memory calldatas, bytes32 descriptionHash) - internal - override(Governor, GovernorTimelockCompound) - { - super._execute(proposalId, targets, values, calldatas, descriptionHash); - } - - function _cancel(address[] memory targets, uint256[] memory values, bytes[] memory calldatas, bytes32 descriptionHash) - internal - override(Governor, GovernorTimelockCompound) - returns (uint256) - { - return super._cancel(targets, values, calldatas, descriptionHash); - } - - function _executor() - internal - view - override(Governor, GovernorTimelockCompound) - returns (address) - { - return super._executor(); - } - - function supportsInterface(bytes4 interfaceId) - public - view - override(Governor, GovernorTimelockCompound) - returns (bool) - { - return super.supportsInterface(interfaceId); - } -} 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/run.js b/certora/run.js new file mode 100644 index 000000000..1da238d4f --- /dev/null +++ b/certora/run.js @@ -0,0 +1,109 @@ +#!/usr/bin/env node + +// USAGE: +// node certora/run.js [[CONTRACT_NAME:]SPEC_NAME] [OPTIONS...] +// EXAMPLES: +// node certora/run.js AccessControl +// node certora/run.js AccessControlHarness:AccessControl + +const MAX_PARALLEL = 4; + +const specs = require(__dirname + '/specs.json'); + +const proc = require('child_process'); +const { PassThrough } = require('stream'); +const events = require('events'); +const limit = require('p-limit')(MAX_PARALLEL); + +let [, , request = '', ...extraOptions] = process.argv; +if (request.startsWith('-')) { + extraOptions.unshift(request); + request = ''; +} +const [reqSpec, reqContract] = request.split(':').reverse(); + +for (const { spec, contract, files, options = [] } of Object.values(specs)) { + if ((!reqSpec || reqSpec === spec) && (!reqContract || reqContract === contract)) { + limit(runCertora, spec, contract, files, [...options, ...extraOptions]); + } +} + +// Run certora, aggregate the output and print it at the end +async function runCertora(spec, contract, files, options = []) { + const args = [...files, '--verify', `${contract}:certora/specs/${spec}.spec`, ...options]; + const child = proc.spawn('certoraRun', args); + + const stream = new PassThrough(); + const output = collect(stream); + + child.stdout.pipe(stream, { end: false }); + child.stderr.pipe(stream, { end: false }); + + // as soon as we have a jobStatus link, print it + stream.on('data', function logStatusUrl(data) { + const urls = data.toString('utf8').match(/https?:\S*/g); + for (const url of urls ?? []) { + if (url.includes('/jobStatus/')) { + console.error(`[${spec}] ${url}`); + stream.off('data', logStatusUrl); + break; + } + } + }); + + // wait for process end + const [code, signal] = await events.once(child, 'exit'); + + // error + if (code || signal) { + console.error(`[${spec}] Exited with code ${code || signal}`); + process.exitCode = 1; + } + + // get all output + stream.end(); + + // write results in markdown format + writeEntry(spec, contract, code || signal, (await output).match(/https:\S*/)[0]); + + // write all details + console.error(`+ certoraRun ${args.join(' ')}\n` + (await output)); +} + +// Collects stream data into a string +async function collect(stream) { + const buffers = []; + for await (const data of stream) { + const buf = Buffer.isBuffer(data) ? data : Buffer.from(data); + buffers.push(buf); + } + return Buffer.concat(buffers).toString('utf8'); +} + +// Formatting +let hasHeader = false; + +function formatRow(...array) { + return ['', ...array, ''].join(' | '); +} + +function writeHeader() { + console.log(formatRow('spec', 'contract', 'result', 'status', 'output')); + console.log(formatRow('-', '-', '-', '-', '-')); +} + +function writeEntry(spec, contract, success, url) { + if (!hasHeader) { + hasHeader = true; + writeHeader(); + } + console.log( + formatRow( + spec, + contract, + success ? ':x:' : ':heavy_check_mark:', + `[link](${url})`, + `[link](${url.replace('/jobStatus/', '/output/')})`, + ), + ); +} diff --git a/certora/scripts/Governor.sh b/certora/scripts/Governor.sh deleted file mode 100755 index 53ade5060..000000000 --- a/certora/scripts/Governor.sh +++ /dev/null @@ -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" diff --git a/certora/scripts/GovernorCountingSimple-counting.sh b/certora/scripts/GovernorCountingSimple-counting.sh deleted file mode 100644 index 9ed8fe34c..000000000 --- a/certora/scripts/GovernorCountingSimple-counting.sh +++ /dev/null @@ -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" diff --git a/certora/scripts/WizardControlFirstPriority.sh b/certora/scripts/WizardControlFirstPriority.sh deleted file mode 100644 index b815986ee..000000000 --- a/certora/scripts/WizardControlFirstPriority.sh +++ /dev/null @@ -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" diff --git a/certora/scripts/WizardFirstTry.sh b/certora/scripts/WizardFirstTry.sh deleted file mode 100644 index fd5a32ab4..000000000 --- a/certora/scripts/WizardFirstTry.sh +++ /dev/null @@ -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" diff --git a/certora/scripts/sanity.sh b/certora/scripts/sanity.sh deleted file mode 100644 index 1c42bf67b..000000000 --- a/certora/scripts/sanity.sh +++ /dev/null @@ -1,14 +0,0 @@ -make -C certora munged - -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 solc8.2 --staging shelly/forSasha \ - --optimistic_loop \ - --msg "checking sanity on ${file%.*}" - --settings -copyLoopUnroll=4 -done diff --git a/certora/scripts/verifyAll.sh b/certora/scripts/verifyAll.sh deleted file mode 100644 index 9b2f11c8c..000000000 --- a/certora/scripts/verifyAll.sh +++ /dev/null @@ -1,39 +0,0 @@ -#!/bin/bash - -make -C certora munged - -for contract in certora/harnesses/Wizard*.sol; -do - for spec in certora/specs/*.spec; - do - contractFile="$(basename $contract)" - specFile="$(basename $spec)" - if [[ "${specFile%.*}" != "RulesInProgress" ]]; - then - 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 solc8.2 \ - --staging shelly/forSasha \ - --disableLocalTypeChecking \ - --optimistic_loop \ - --settings -copyLoopUnroll=4 \ - --send_only \ - --msg "checking $specFile on ${contractFile%.*}" - else - certoraRun certora/harnesses/ERC20VotesHarness.sol certora/harnesses/$contractFile \ - --verify ${contractFile%.*}:certora/specs/$specFile "$@" \ - --solc solc8.2 \ - --staging shelly/forSasha \ - --disableLocalTypeChecking \ - --optimistic_loop \ - --settings -copyLoopUnroll=4 \ - --send_only \ - --msg "checking $specFile on ${contractFile%.*}" - fi - fi - done -done diff --git a/certora/specs.json b/certora/specs.json new file mode 100644 index 000000000..4d3e1fb90 --- /dev/null +++ b/certora/specs.json @@ -0,0 +1,22 @@ +[ + { + "spec": "AccessControl", + "contract": "AccessControlHarness", + "files": ["certora/harnesses/AccessControlHarness.sol"] + }, + { + "spec": "ERC20", + "contract": "ERC20PermitHarness", + "files": ["certora/harnesses/ERC20PermitHarness.sol"], + "options": ["--optimistic_loop"] + }, + { + "spec": "ERC20FlashMint", + "contract": "ERC20FlashMintHarness", + "files": [ + "certora/harnesses/ERC20FlashMintHarness.sol", + "certora/harnesses/ERC3156FlashBorrowerHarness.sol" + ], + "options": ["--optimistic_loop"] + } +] diff --git a/certora/specs/AccessControl.spec b/certora/specs/AccessControl.spec new file mode 100644 index 000000000..170d56fd4 --- /dev/null +++ b/certora/specs/AccessControl.spec @@ -0,0 +1,114 @@ +import "helpers.spec" + +methods { + hasRole(bytes32, address) returns(bool) envfree + getRoleAdmin(bytes32) returns(bytes32) envfree + grantRole(bytes32, address) + revokeRole(bytes32, address) + renounceRole(bytes32, address) +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Identify entrypoints: only grantRole, revokeRole and renounceRole can alter permissions │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule onlyGrantCanGrant(env e, bytes32 role, address account) { + method f; calldataarg args; + + bool hasRoleBefore = hasRole(role, account); + f(e, args); + bool hasRoleAfter = hasRole(role, account); + + assert ( + !hasRoleBefore && + hasRoleAfter + ) => ( + f.selector == grantRole(bytes32, address).selector + ); + + assert ( + hasRoleBefore && + !hasRoleAfter + ) => ( + f.selector == revokeRole(bytes32, address).selector || + f.selector == renounceRole(bytes32, address).selector + ); +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Function correctness: grantRole only affects the specified user/role combo │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule grantRoleEffect(env e) { + require nonpayable(e); + + bytes32 role1; bytes32 role2; + address account1; address account2; + + bool isCallerAdmin = hasRole(getRoleAdmin(role2), e.msg.sender); + bool hasRoleBefore = hasRole(role1, account1); + + grantRole@withrevert(e, role2, account2); + assert !lastReverted <=> isCallerAdmin; + + bool hasRoleAfter = hasRole(role1, account1); + + assert ( + hasRoleBefore != hasRoleAfter + ) => ( + hasRoleAfter == true && role1 == role2 && account1 == account2 + ); +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Function correctness: revokeRole only affects the specified user/role combo │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule revokeRoleEffect(env e) { + require nonpayable(e); + + bytes32 role1; bytes32 role2; + address account1; address account2; + + bool isCallerAdmin = hasRole(getRoleAdmin(role2), e.msg.sender); + bool hasRoleBefore = hasRole(role1, account1); + + revokeRole@withrevert(e, role2, account2); + assert !lastReverted <=> isCallerAdmin; + + bool hasRoleAfter = hasRole(role1, account1); + + assert ( + hasRoleBefore != hasRoleAfter + ) => ( + hasRoleAfter == false && role1 == role2 && account1 == account2 + ); +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Function correctness: renounceRole only affects the specified user/role combo │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule renounceRoleEffect(env e) { + require nonpayable(e); + + bytes32 role1; bytes32 role2; + address account1; address account2; + + bool hasRoleBefore = hasRole(role1, account1); + + renounceRole@withrevert(e, role2, account2); + assert !lastReverted <=> account2 == e.msg.sender; + + bool hasRoleAfter = hasRole(role1, account1); + + assert ( + hasRoleBefore != hasRoleAfter + ) => ( + hasRoleAfter == false && role1 == role2 && account1 == account2 + ); +} diff --git a/certora/specs/ERC20.spec b/certora/specs/ERC20.spec new file mode 100644 index 000000000..85f95e706 --- /dev/null +++ b/certora/specs/ERC20.spec @@ -0,0 +1,414 @@ +import "helpers.spec" +import "methods/IERC20.spec" +import "methods/IERC2612.spec" + +methods { + // non standard ERC20 functions + increaseAllowance(address,uint256) returns (bool) + decreaseAllowance(address,uint256) returns (bool) + + // exposed for FV + mint(address,uint256) + burn(address,uint256) +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Ghost & hooks: sum of all balances │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +ghost sumOfBalances() returns uint256 { + init_state axiom sumOfBalances() == 0; +} + +hook Sstore _balances[KEY address addr] uint256 newValue (uint256 oldValue) STORAGE { + havoc sumOfBalances assuming sumOfBalances@new() == sumOfBalances@old() + newValue - oldValue; +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Invariant: totalSupply is the sum of all balances │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +invariant totalSupplyIsSumOfBalances() + totalSupply() == sumOfBalances() + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Invariant: balance of address(0) is 0 │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +invariant zeroAddressNoBalance() + balanceOf(0) == 0 + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rules: only mint and burn can change total supply │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule noChangeTotalSupply(env e) { + requireInvariant totalSupplyIsSumOfBalances(); + + method f; + calldataarg args; + + uint256 totalSupplyBefore = totalSupply(); + f(e, args); + uint256 totalSupplyAfter = totalSupply(); + + assert totalSupplyAfter > totalSupplyBefore => f.selector == mint(address,uint256).selector; + assert totalSupplyAfter < totalSupplyBefore => f.selector == burn(address,uint256).selector; +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rules: only the token holder or an approved third party can reduce an account's balance │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule onlyAuthorizedCanTransfer(env e) { + requireInvariant totalSupplyIsSumOfBalances(); + + method f; + calldataarg args; + address account; + + uint256 allowanceBefore = allowance(account, e.msg.sender); + uint256 balanceBefore = balanceOf(account); + f(e, args); + uint256 balanceAfter = balanceOf(account); + + assert ( + balanceAfter < balanceBefore + ) => ( + f.selector == burn(address,uint256).selector || + e.msg.sender == account || + balanceBefore - balanceAfter <= allowanceBefore + ); +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rules: only the token holder (or a permit) can increase allowance. The spender can decrease it by using it │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule onlyHolderOfSpenderCanChangeAllowance(env e) { + requireInvariant totalSupplyIsSumOfBalances(); + + method f; + calldataarg args; + address holder; + address spender; + + uint256 allowanceBefore = allowance(holder, spender); + f(e, args); + uint256 allowanceAfter = allowance(holder, spender); + + assert ( + allowanceAfter > allowanceBefore + ) => ( + (f.selector == approve(address,uint256).selector && e.msg.sender == holder) || + (f.selector == increaseAllowance(address,uint256).selector && e.msg.sender == holder) || + (f.selector == permit(address,address,uint256,uint256,uint8,bytes32,bytes32).selector) + ); + + assert ( + allowanceAfter < allowanceBefore + ) => ( + (f.selector == transferFrom(address,address,uint256).selector && e.msg.sender == spender) || + (f.selector == approve(address,uint256).selector && e.msg.sender == holder ) || + (f.selector == decreaseAllowance(address,uint256).selector && e.msg.sender == holder ) || + (f.selector == permit(address,address,uint256,uint256,uint8,bytes32,bytes32).selector) + ); +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rules: mint behavior and side effects │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule mint(env e) { + requireInvariant totalSupplyIsSumOfBalances(); + require nonpayable(e); + + address to; + address other; + uint256 amount; + + // cache state + uint256 toBalanceBefore = balanceOf(to); + uint256 otherBalanceBefore = balanceOf(other); + uint256 totalSupplyBefore = totalSupply(); + + // run transaction + mint@withrevert(e, to, amount); + + // check outcome + if (lastReverted) { + assert to == 0 || totalSupplyBefore + amount > max_uint256; + } else { + // updates balance and totalSupply + assert balanceOf(to) == toBalanceBefore + amount; + assert totalSupply() == totalSupplyBefore + amount; + + // no other balance is modified + assert balanceOf(other) != otherBalanceBefore => other == to; + } +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rules: burn behavior and side effects │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule burn(env e) { + requireInvariant totalSupplyIsSumOfBalances(); + require nonpayable(e); + + address from; + address other; + uint256 amount; + + // cache state + uint256 fromBalanceBefore = balanceOf(from); + uint256 otherBalanceBefore = balanceOf(other); + uint256 totalSupplyBefore = totalSupply(); + + // run transaction + burn@withrevert(e, from, amount); + + // check outcome + if (lastReverted) { + assert from == 0 || fromBalanceBefore < amount; + } else { + // updates balance and totalSupply + assert balanceOf(from) == fromBalanceBefore - amount; + assert totalSupply() == totalSupplyBefore - amount; + + // no other balance is modified + assert balanceOf(other) != otherBalanceBefore => other == from; + } +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rule: transfer behavior and side effects │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule transfer(env e) { + requireInvariant totalSupplyIsSumOfBalances(); + require nonpayable(e); + + address holder = e.msg.sender; + address recipient; + address other; + uint256 amount; + + // cache state + uint256 holderBalanceBefore = balanceOf(holder); + uint256 recipientBalanceBefore = balanceOf(recipient); + uint256 otherBalanceBefore = balanceOf(other); + + // run transaction + transfer@withrevert(e, recipient, amount); + + // check outcome + if (lastReverted) { + assert holder == 0 || recipient == 0 || amount > holderBalanceBefore; + } else { + // balances of holder and recipient are updated + assert balanceOf(holder) == holderBalanceBefore - (holder == recipient ? 0 : amount); + assert balanceOf(recipient) == recipientBalanceBefore + (holder == recipient ? 0 : amount); + + // no other balance is modified + assert balanceOf(other) != otherBalanceBefore => (other == holder || other == recipient); + } +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rule: transferFrom behavior and side effects │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule transferFrom(env e) { + requireInvariant totalSupplyIsSumOfBalances(); + require nonpayable(e); + + address spender = e.msg.sender; + address holder; + address recipient; + address other; + uint256 amount; + + // cache state + uint256 allowanceBefore = allowance(holder, spender); + uint256 holderBalanceBefore = balanceOf(holder); + uint256 recipientBalanceBefore = balanceOf(recipient); + uint256 otherBalanceBefore = balanceOf(other); + + // run transaction + transferFrom@withrevert(e, holder, recipient, amount); + + // check outcome + if (lastReverted) { + assert holder == 0 || recipient == 0 || spender == 0 || amount > holderBalanceBefore || amount > allowanceBefore; + } else { + // allowance is valid & updated + assert allowanceBefore >= amount; + assert allowance(holder, spender) == (allowanceBefore == max_uint256 ? to_uint256(max_uint256) : allowanceBefore - amount); + + // balances of holder and recipient are updated + assert balanceOf(holder) == holderBalanceBefore - (holder == recipient ? 0 : amount); + assert balanceOf(recipient) == recipientBalanceBefore + (holder == recipient ? 0 : amount); + + // no other balance is modified + assert balanceOf(other) != otherBalanceBefore => (other == holder || other == recipient); + } +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rule: approve behavior and side effects │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule approve(env e) { + require nonpayable(e); + + address holder = e.msg.sender; + address spender; + address otherHolder; + address otherSpender; + uint256 amount; + + // cache state + uint256 otherAllowanceBefore = allowance(otherHolder, otherSpender); + + // run transaction + approve@withrevert(e, spender, amount); + + // check outcome + if (lastReverted) { + assert holder == 0 || spender == 0; + } else { + // allowance is updated + assert allowance(holder, spender) == amount; + + // other allowances are untouched + assert allowance(otherHolder, otherSpender) != otherAllowanceBefore => (otherHolder == holder && otherSpender == spender); + } +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rule: increaseAllowance behavior and side effects │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule increaseAllowance(env e) { + require nonpayable(e); + + address holder = e.msg.sender; + address spender; + address otherHolder; + address otherSpender; + uint256 amount; + + // cache state + uint256 allowanceBefore = allowance(holder, spender); + uint256 otherAllowanceBefore = allowance(otherHolder, otherSpender); + + // run transaction + increaseAllowance@withrevert(e, spender, amount); + + // check outcome + if (lastReverted) { + assert holder == 0 || spender == 0 || allowanceBefore + amount > max_uint256; + } else { + // allowance is updated + assert allowance(holder, spender) == allowanceBefore + amount; + + // other allowances are untouched + assert allowance(otherHolder, otherSpender) != otherAllowanceBefore => (otherHolder == holder && otherSpender == spender); + } +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rule: decreaseAllowance behavior and side effects │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule decreaseAllowance(env e) { + require nonpayable(e); + + address holder = e.msg.sender; + address spender; + address otherHolder; + address otherSpender; + uint256 amount; + + // cache state + uint256 allowanceBefore = allowance(holder, spender); + uint256 otherAllowanceBefore = allowance(otherHolder, otherSpender); + + // run transaction + decreaseAllowance@withrevert(e, spender, amount); + + // check outcome + if (lastReverted) { + assert holder == 0 || spender == 0 || allowanceBefore < amount; + } else { + // allowance is updated + assert allowance(holder, spender) == allowanceBefore - amount; + + // other allowances are untouched + assert allowance(otherHolder, otherSpender) != otherAllowanceBefore => (otherHolder == holder && otherSpender == spender); + } +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rule: permit behavior and side effects │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule permit(env e) { + require nonpayable(e); + + address holder; + address spender; + uint256 amount; + uint256 deadline; + uint8 v; + bytes32 r; + bytes32 s; + + address account1; + address account2; + address account3; + + // cache state + uint256 nonceBefore = nonces(holder); + uint256 otherNonceBefore = nonces(account1); + uint256 otherAllowanceBefore = allowance(account2, account3); + + // sanity: nonce overflow, which possible in theory, is assumed to be impossible in practice + require nonceBefore < max_uint256; + require otherNonceBefore < max_uint256; + + // run transaction + permit@withrevert(e, holder, spender, amount, deadline, v, r, s); + + // check outcome + if (lastReverted) { + // Without formally checking the signature, we can't verify exactly the revert causes + assert true; + } else { + // allowance and nonce are updated + assert allowance(holder, spender) == amount; + assert nonces(holder) == nonceBefore + 1; + + // deadline was respected + assert deadline >= e.block.timestamp; + + // no other allowance or nonce is modified + assert nonces(account1) != otherNonceBefore => account1 == holder; + assert allowance(account2, account3) != otherAllowanceBefore => (account2 == holder && account3 == spender); + } +} diff --git a/certora/specs/ERC20FlashMint.spec b/certora/specs/ERC20FlashMint.spec new file mode 100644 index 000000000..64d97342a --- /dev/null +++ b/certora/specs/ERC20FlashMint.spec @@ -0,0 +1,48 @@ +import "helpers.spec" +import "methods/IERC20.spec" +import "methods/IERC3156.spec" + +methods { + // non standard ERC3156 functions + flashFeeReceiver() returns (address) envfree + + // function summaries below + _mint(address account, uint256 amount) => specMint(account, amount) + _burn(address account, uint256 amount) => specBurn(account, amount) + _transfer(address from, address to, uint256 amount) => specTransfer(from, to, amount) +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Ghost: track mint and burns in the CVL │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +ghost mapping(address => uint256) trackedMintAmount; +ghost mapping(address => uint256) trackedBurnAmount; +ghost mapping(address => mapping(address => uint256)) trackedTransferedAmount; + +function specMint(address account, uint256 amount) returns bool { trackedMintAmount[account] = amount; return true; } +function specBurn(address account, uint256 amount) returns bool { trackedBurnAmount[account] = amount; return true; } +function specTransfer(address from, address to, uint256 amount) returns bool { trackedTransferedAmount[from][to] = amount; return true; } + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rule: When doing a flashLoan, "amount" is minted and burnt, additionally, the fee is either burnt │ +│ (if the fee recipient is 0) or transferred (if the fee recipient is not 0) │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule checkMintAndBurn(env e) { + address receiver; + address token; + uint256 amount; + bytes data; + + uint256 fees = flashFee(token, amount); + address recipient = flashFeeReceiver(); + + flashLoan(e, receiver, token, amount, data); + + assert trackedMintAmount[receiver] == amount; + assert trackedBurnAmount[receiver] == amount + (recipient == 0 ? fees : 0); + assert (fees > 0 && recipient != 0) => trackedTransferedAmount[receiver][recipient] == fees; +} diff --git a/certora/specs/GovernorBase.spec b/certora/specs/GovernorBase.spec deleted file mode 100644 index de728ddac..000000000 --- a/certora/specs/GovernorBase.spec +++ /dev/null @@ -1,333 +0,0 @@ -////////////////////////////////////////////////////////////////////////////// -///////////////////// Governor.sol base definitions ////////////////////////// -////////////////////////////////////////////////////////////////////////////// - -using ERC20VotesHarness as erc20votes - -methods { - proposalSnapshot(uint256) returns uint256 envfree // matches proposalVoteStart - proposalDeadline(uint256) returns uint256 envfree // matches proposalVoteEnd - hashProposal(address[],uint256[],bytes[],bytes32) returns uint256 envfree - isExecuted(uint256) returns bool envfree - isCanceled(uint256) returns bool envfree - execute(address[], uint256[], bytes[], bytes32) returns uint256 - hasVoted(uint256, address) returns bool - castVote(uint256, uint8) returns uint256 - updateQuorumNumerator(uint256) - queue(address[], uint256[], bytes[], bytes32) returns uint256 - - // internal functions made public in harness: - _quorumReached(uint256) returns bool - _voteSucceeded(uint256) returns bool envfree - - // function summarization - proposalThreshold() returns uint256 envfree - - getVotes(address, uint256) returns uint256 => DISPATCHER(true) - - getPastTotalSupply(uint256 t) returns uint256 => PER_CALLEE_CONSTANT - getPastVotes(address a, uint256 t) returns uint256 => PER_CALLEE_CONSTANT - - //scheduleBatch(address[],uint256[],bytes[],bytes32,bytes32,uint256) => DISPATCHER(true) - //executeBatch(address[], uint256[], bytes[], bytes32, bytes32) => DISPATCHER(true) -} - -////////////////////////////////////////////////////////////////////////////// -//////////////////////////////// Definitions ///////////////////////////////// -////////////////////////////////////////////////////////////////////////////// - - -// proposal was created - relation proved in noStartBeforeCreation -definition proposalCreated(uint256 pId) returns bool = proposalSnapshot(pId) > 0; - - -////////////////////////////////////////////////////////////////////////////// -///////////////////////////// Helper Functions /////////////////////////////// -////////////////////////////////////////////////////////////////////////////// - -function helperFunctionsWithRevert(uint256 proposalId, method f, env e) { - address[] targets; uint256[] values; bytes[] calldatas; string reason; bytes32 descriptionHash; - uint8 support; uint8 v; bytes32 r; bytes32 s; - if (f.selector == propose(address[], uint256[], bytes[], string).selector) { - uint256 result = propose@withrevert(e, targets, values, calldatas, reason); - require(result == proposalId); - } else if (f.selector == execute(address[], uint256[], bytes[], bytes32).selector) { - uint256 result = execute@withrevert(e, targets, values, calldatas, descriptionHash); - require(result == proposalId); - } else if (f.selector == castVote(uint256, uint8).selector) { - castVote@withrevert(e, proposalId, support); - } else if (f.selector == castVoteWithReason(uint256, uint8, string).selector) { - castVoteWithReason@withrevert(e, proposalId, support, reason); - } else if (f.selector == castVoteBySig(uint256, uint8,uint8, bytes32, bytes32).selector) { - castVoteBySig@withrevert(e, proposalId, support, v, r, s); - } else if (f.selector == queue(address[], uint256[], bytes[], bytes32).selector) { - queue@withrevert(e, targets, values, calldatas, descriptionHash); - } else { - calldataarg args; - f@withrevert(e, args); - } -} - -/* - ////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////// - ///////////////////////////////////////////////////// State Diagram ////////////////////////////////////////////////////////// - ////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////// - // // - // castVote(s)() // - // ------------- propose() ---------------------- time pass --------------- time passes ----------- // - // | No Proposal | --------> | Before Start (Delay) | --------> | Voting Period | ----------------------> | execute() | // - // ------------- ---------------------- --------------- -> Executed/Canceled ----------- // - // ------------------------------------------------------------|---------------|-------------------------|--------------> // - // t start end timelock // - // // - ////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////// -*/ - - -/////////////////////////////////////////////////////////////////////////////////////// -///////////////////////////////// Global Valid States ///////////////////////////////// -/////////////////////////////////////////////////////////////////////////////////////// - - -/* - * Start and end date are either initialized (non zero) or uninitialized (zero) simultaneously - * This invariant assumes that the block number cannot be 0 at any stage of the contract cycle - * This is very safe assumption as usually the 0 block is genesis block which is uploaded with data - * by the developers and will not be valid to raise proposals (at the current way that block chain is functioning) - */ - // To use env with general preserved block disable type checking [--disableLocalTypeChecking] -invariant startAndEndDatesNonZero(uint256 pId) - proposalSnapshot(pId) != 0 <=> proposalDeadline(pId) != 0 - { preserved with (env e){ - require e.block.number > 0; - }} - - -/* - * If a proposal is canceled it must have a start and an end date - */ - // To use env with general preserved block disable type checking [--disableLocalTypeChecking] -invariant canceledImplyStartAndEndDateNonZero(uint pId) - isCanceled(pId) => proposalSnapshot(pId) != 0 - {preserved with (env e){ - require e.block.number > 0; - }} - - -/* - * If a proposal is executed it must have a start and an end date - */ - // To use env with general preserved block disable type checking [--disableLocalTypeChecking] -invariant executedImplyStartAndEndDateNonZero(uint pId) - isExecuted(pId) => proposalSnapshot(pId) != 0 - { preserved with (env e){ - requireInvariant startAndEndDatesNonZero(pId); - require e.block.number > 0; - }} - - -/* - * A proposal starting block number must be less or equal than the proposal end date - */ -invariant voteStartBeforeVoteEnd(uint256 pId) - // from < to <= because snapshot and deadline can be the same block number if delays are set to 0 - // This is possible before the integration of GovernorSettings.sol to the system. - // After integration of GovernorSettings.sol the invariant expression should be changed from <= to < - (proposalSnapshot(pId) > 0 => proposalSnapshot(pId) <= proposalDeadline(pId)) - // (proposalSnapshot(pId) > 0 => proposalSnapshot(pId) <= proposalDeadline(pId)) - { preserved { - requireInvariant startAndEndDatesNonZero(pId); - }} - - -/* - * A proposal cannot be both executed and canceled simultaneously. - */ -invariant noBothExecutedAndCanceled(uint256 pId) - !isExecuted(pId) || !isCanceled(pId) - - -/* - * A proposal could be executed only if quorum was reached and vote succeeded - */ -rule executionOnlyIfQuoromReachedAndVoteSucceeded(uint256 pId, env e, method f){ - bool isExecutedBefore = isExecuted(pId); - bool quorumReachedBefore = _quorumReached(e, pId); - bool voteSucceededBefore = _voteSucceeded(pId); - - calldataarg args; - f(e, args); - - bool isExecutedAfter = isExecuted(pId); - assert (!isExecutedBefore && isExecutedAfter) => (quorumReachedBefore && voteSucceededBefore), "quorum was changed"; -} - -/////////////////////////////////////////////////////////////////////////////////////// -////////////////////////////////// In-State Rules ///////////////////////////////////// -/////////////////////////////////////////////////////////////////////////////////////// - -//========================================== -//------------- Voting Period -------------- -//========================================== - -/* - * A user cannot vote twice - */ - // Checked for castVote only. all 3 castVote functions call _castVote, so the completeness of the verification is counted on - // the fact that the 3 functions themselves makes no changes, but rather call an internal function to execute. - // That means that we do not check those 3 functions directly, however for castVote & castVoteWithReason it is quite trivial - // to understand why this is ok. For castVoteBySig we basically assume that the signature referendum is correct without checking it. - // We could check each function separately and pass the rule, but that would have uglyfied the code with no concrete - // benefit, as it is evident that nothing is happening in the first 2 functions (calling a view function), and we do not desire to check the signature verification. -rule doubleVoting(uint256 pId, uint8 sup, method f) { - env e; - address user = e.msg.sender; - bool votedCheck = hasVoted(e, pId, user); - - castVote@withrevert(e, pId, sup); - - assert votedCheck => lastReverted, "double voting occurred"; -} - - -/////////////////////////////////////////////////////////////////////////////////////// -//////////////////////////// State Transitions Rules ////////////////////////////////// -/////////////////////////////////////////////////////////////////////////////////////// - -//=========================================== -//-------- Propose() --> End of Time -------- -//=========================================== - - -/* - * Once a proposal is created, voteStart and voteEnd are immutable - */ -rule immutableFieldsAfterProposalCreation(uint256 pId, method f) { - uint256 _voteStart = proposalSnapshot(pId); - uint256 _voteEnd = proposalDeadline(pId); - - require proposalCreated(pId); // startDate > 0 - - env e; calldataarg arg; - f(e, arg); - - uint256 voteStart_ = proposalSnapshot(pId); - uint256 voteEnd_ = proposalDeadline(pId); - assert _voteStart == voteStart_, "Start date was changed"; - assert _voteEnd == voteEnd_, "End date was changed"; -} - - -/* - * Voting cannot start at a block number prior to proposal’s creation block number - */ -rule noStartBeforeCreation(uint256 pId) { - uint256 previousStart = proposalSnapshot(pId); - // This line makes sure that we see only cases where start date is changed from 0, i.e. creation of proposal - // We proved in immutableFieldsAfterProposalCreation that once dates set for proposal, it cannot be changed - require !proposalCreated(pId); // previousStart == 0; - - env e; calldataarg args; - propose(e, args); - - uint256 newStart = proposalSnapshot(pId); - // if created, start is after current block number (creation block) - assert(newStart != previousStart => newStart >= e.block.number); -} - - -//============================================ -//--- End of Voting Period --> End of Time --- -//============================================ - - -/* - * A proposal can neither be executed nor canceled before it ends - */ - // By induction it cannot be executed nor canceled before it starts, due to voteStartBeforeVoteEnd -rule noExecuteOrCancelBeforeDeadline(uint256 pId, method f){ - require !isExecuted(pId) && !isCanceled(pId); - - env e; calldataarg args; - f(e, args); - - assert e.block.number < proposalDeadline(pId) => (!isExecuted(pId) && !isCanceled(pId)), "executed/cancelled before deadline"; -} - -//////////////////////////////////////////////////////////////////////////////// -////////////////////// Integrity Of Functions (Unit Tests) ///////////////////// -//////////////////////////////////////////////////////////////////////////////// - - -//////////////////////////////////////////////////////////////////////////////// -////////////////////////////// High Level Rules //////////////////////////////// -//////////////////////////////////////////////////////////////////////////////// - - -//////////////////////////////////////////////////////////////////////////////// -///////////////////////////// Not Categorized Yet ////////////////////////////// -//////////////////////////////////////////////////////////////////////////////// - - -/* - * All proposal specific (non-view) functions should revert if proposal is executed - */ - // In this rule we show that if a function is executed, i.e. execute() was called on the proposal ID, - // non of the proposal specific functions can make changes again. In executedOnlyAfterExecuteFunc - // we connected the executed attribute to the execute() function, showing that only execute() can - // change it, and that it will always change it. -rule allFunctionsRevertIfExecuted(method f) filtered { f -> - !f.isView && !f.isFallback - && f.selector != updateTimelock(address).selector - && f.selector != updateQuorumNumerator(uint256).selector - && f.selector != queue(address[],uint256[],bytes[],bytes32).selector - && f.selector != relay(address,uint256,bytes).selector - && f.selector != 0xb9a61961 // __acceptAdmin() -} { - env e; calldataarg args; - uint256 pId; - require(isExecuted(pId)); - requireInvariant noBothExecutedAndCanceled(pId); - requireInvariant executedImplyStartAndEndDateNonZero(pId); - - helperFunctionsWithRevert(pId, f, e); - - assert(lastReverted, "Function was not reverted"); -} - -/* - * All proposal specific (non-view) functions should revert if proposal is canceled - */ -rule allFunctionsRevertIfCanceled(method f) filtered { - f -> !f.isView && !f.isFallback - && f.selector != updateTimelock(address).selector - && f.selector != updateQuorumNumerator(uint256).selector - && f.selector != queue(address[],uint256[],bytes[],bytes32).selector - && f.selector != relay(address,uint256,bytes).selector - && f.selector != 0xb9a61961 // __acceptAdmin() -} { - env e; calldataarg args; - uint256 pId; - require(isCanceled(pId)); - requireInvariant noBothExecutedAndCanceled(pId); - requireInvariant canceledImplyStartAndEndDateNonZero(pId); - - helperFunctionsWithRevert(pId, f, e); - - assert(lastReverted, "Function was not reverted"); -} - -/* - * Proposal can be switched to executed only via execute() function - */ -rule executedOnlyAfterExecuteFunc(address[] targets, uint256[] values, bytes[] calldatas, bytes32 descriptionHash, method f) { - env e; calldataarg args; - uint256 pId; - bool executedBefore = isExecuted(pId); - require(!executedBefore); - - helperFunctionsWithRevert(pId, f, e); - - bool executedAfter = isExecuted(pId); - assert(executedAfter != executedBefore => f.selector == execute(address[], uint256[], bytes[], bytes32).selector, "isExecuted only changes in the execute method"); -} diff --git a/certora/specs/GovernorCountingSimple.spec b/certora/specs/GovernorCountingSimple.spec deleted file mode 100644 index 7af73beb6..000000000 --- a/certora/specs/GovernorCountingSimple.spec +++ /dev/null @@ -1,221 +0,0 @@ -import "GovernorBase.spec" - -using ERC20VotesHarness as erc20votes - -methods { - ghost_sum_vote_power_by_id(uint256) returns uint256 envfree - - quorum(uint256) returns uint256 - proposalVotes(uint256) returns (uint256, uint256, uint256) envfree - - quorumNumerator() returns uint256 - _executor() returns address - - erc20votes._getPastVotes(address, uint256) returns uint256 - - getExecutor() returns address - - timelock() returns address -} - - -////////////////////////////////////////////////////////////////////////////// -///////////////////////////////// GHOSTS ///////////////////////////////////// -////////////////////////////////////////////////////////////////////////////// - - -//////////// ghosts to keep track of votes counting //////////// - -/* - * the sum of voting power of those who voted - */ -ghost sum_all_votes_power() returns uint256 { - init_state axiom sum_all_votes_power() == 0; -} - -hook Sstore ghost_sum_vote_power_by_id [KEY uint256 pId] uint256 current_power(uint256 old_power) STORAGE { - havoc sum_all_votes_power assuming sum_all_votes_power@new() == sum_all_votes_power@old() - old_power + current_power; -} - -/* - * sum of all votes casted per proposal - */ -ghost tracked_weight(uint256) returns uint256 { - init_state axiom forall uint256 p. tracked_weight(p) == 0; -} - -/* - * sum of all votes casted - */ -ghost sum_tracked_weight() returns uint256 { - init_state axiom sum_tracked_weight() == 0; -} - -/* - * getter for _proposalVotes.againstVotes - */ -ghost votesAgainst() returns uint256 { - init_state axiom votesAgainst() == 0; -} - -/* - * getter for _proposalVotes.forVotes - */ -ghost votesFor() returns uint256 { - init_state axiom votesFor() == 0; -} - -/* - * getter for _proposalVotes.abstainVotes - */ -ghost votesAbstain() returns uint256 { - init_state axiom votesAbstain() == 0; -} - -hook Sstore _proposalVotes [KEY uint256 pId].againstVotes uint256 votes(uint256 old_votes) STORAGE { - havoc tracked_weight assuming forall uint256 p.(p == pId => tracked_weight@new(p) == tracked_weight@old(p) - old_votes + votes) && - (p != pId => tracked_weight@new(p) == tracked_weight@old(p)); - havoc sum_tracked_weight assuming sum_tracked_weight@new() == sum_tracked_weight@old() - old_votes + votes; - havoc votesAgainst assuming votesAgainst@new() == votesAgainst@old() - old_votes + votes; -} - -hook Sstore _proposalVotes [KEY uint256 pId].forVotes uint256 votes(uint256 old_votes) STORAGE { - havoc tracked_weight assuming forall uint256 p.(p == pId => tracked_weight@new(p) == tracked_weight@old(p) - old_votes + votes) && - (p != pId => tracked_weight@new(p) == tracked_weight@old(p)); - havoc sum_tracked_weight assuming sum_tracked_weight@new() == sum_tracked_weight@old() - old_votes + votes; - havoc votesFor assuming votesFor@new() == votesFor@old() - old_votes + votes; -} - -hook Sstore _proposalVotes [KEY uint256 pId].abstainVotes uint256 votes(uint256 old_votes) STORAGE { - havoc tracked_weight assuming forall uint256 p.(p == pId => tracked_weight@new(p) == tracked_weight@old(p) - old_votes + votes) && - (p != pId => tracked_weight@new(p) == tracked_weight@old(p)); - havoc sum_tracked_weight assuming sum_tracked_weight@new() == sum_tracked_weight@old() - old_votes + votes; - havoc votesAbstain assuming votesAbstain@new() == votesAbstain@old() - old_votes + votes; -} - - -////////////////////////////////////////////////////////////////////////////// -////////////////////////////// INVARIANTS //////////////////////////////////// -////////////////////////////////////////////////////////////////////////////// - - -/* - * sum of all votes casted is equal to the sum of voting power of those who voted, per each proposal - */ -invariant SumOfVotesCastEqualSumOfPowerOfVotedPerProposal(uint256 pId) - tracked_weight(pId) == ghost_sum_vote_power_by_id(pId) - - -/* - * sum of all votes casted is equal to the sum of voting power of those who voted - */ -invariant SumOfVotesCastEqualSumOfPowerOfVoted() - sum_tracked_weight() == sum_all_votes_power() - - -/* -* sum of all votes casted is greater or equal to the sum of voting power of those who voted at a specific proposal -*/ -invariant OneIsNotMoreThanAll(uint256 pId) - sum_all_votes_power() >= tracked_weight(pId) - - -////////////////////////////////////////////////////////////////////////////// -///////////////////////////////// RULES ////////////////////////////////////// -////////////////////////////////////////////////////////////////////////////// - - -/* - * Only sender's voting status can be changed by execution of any cast vote function - */ -// Checked for castVote only. all 3 castVote functions call _castVote, so the completeness of the verification is counted on - // the fact that the 3 functions themselves makes no changes, but rather call an internal function to execute. - // That means that we do not check those 3 functions directly, however for castVote & castVoteWithReason it is quite trivial - // to understand why this is ok. For castVoteBySig we basically assume that the signature referendum is correct without checking it. - // We could check each function separately and pass the rule, but that would have uglyfied the code with no concrete - // benefit, as it is evident that nothing is happening in the first 2 functions (calling a view function), and we do not desire to check the signature verification. -rule noVoteForSomeoneElse(uint256 pId, uint8 sup, method f) { - env e; calldataarg args; - - address voter = e.msg.sender; - address user; - - bool hasVotedBefore_User = hasVoted(e, pId, user); - - castVote@withrevert(e, pId, sup); - require(!lastReverted); - - bool hasVotedAfter_User = hasVoted(e, pId, user); - - assert user != voter => hasVotedBefore_User == hasVotedAfter_User; -} - - -/* -* Total voting tally is monotonically non-decreasing in every operation -*/ -rule votingWeightMonotonicity(method f){ - uint256 votingWeightBefore = sum_tracked_weight(); - - env e; - calldataarg args; - f(e, args); - - uint256 votingWeightAfter = sum_tracked_weight(); - - assert votingWeightBefore <= votingWeightAfter, "Voting weight was decreased somehow"; -} - - -/* -* A change in hasVoted must be correlated with an non-decreasing of the vote supports (nondecrease because user can vote with weight 0) -*/ -rule hasVotedCorrelation(uint256 pId, method f, env e, uint256 bn) { - address acc = e.msg.sender; - - uint256 againstBefore = votesAgainst(); - uint256 forBefore = votesFor(); - uint256 abstainBefore = votesAbstain(); - - bool hasVotedBefore = hasVoted(e, pId, acc); - - helperFunctionsWithRevert(pId, f, e); - require(!lastReverted); - - uint256 againstAfter = votesAgainst(); - uint256 forAfter = votesFor(); - uint256 abstainAfter = votesAbstain(); - - bool hasVotedAfter = hasVoted(e, pId, acc); - - assert (!hasVotedBefore && hasVotedAfter) => againstBefore <= againstAfter || forBefore <= forAfter || abstainBefore <= abstainAfter, "no correlation"; -} - - -/* -* Only privileged users can execute privileged operations, e.g. change _quorumNumerator or _timelock -*/ -rule privilegedOnlyNumerator(method f, uint256 newQuorumNumerator){ - env e; - calldataarg arg; - uint256 quorumNumBefore = quorumNumerator(e); - - f(e, arg); - - uint256 quorumNumAfter = quorumNumerator(e); - address executorCheck = getExecutor(e); - - assert quorumNumBefore != quorumNumAfter => e.msg.sender == executorCheck, "non privileged user changed quorum numerator"; -} - -rule privilegedOnlyTimelock(method f, uint256 newQuorumNumerator){ - env e; - calldataarg arg; - uint256 timelockBefore = timelock(e); - - f(e, arg); - - uint256 timelockAfter = timelock(e); - - assert timelockBefore != timelockAfter => e.msg.sender == timelockBefore, "non privileged user changed timelock"; -} diff --git a/certora/specs/RulesInProgress.spec b/certora/specs/RulesInProgress.spec deleted file mode 100644 index cbad3336e..000000000 --- a/certora/specs/RulesInProgress.spec +++ /dev/null @@ -1,139 +0,0 @@ -////////////////////////////////////////////////////////////////////////////// -////////////// THIS SPEC IS A RESERVE FOR NOT IN PROGRESS ////////////// -////////////////////////////////////////////////////////////////////////////// - -import "GovernorBase.spec" - -using ERC20VotesHarness as erc20votes - -methods { - ghost_sum_vote_power_by_id(uint256) returns uint256 envfree - - quorum(uint256) returns uint256 - proposalVotes(uint256) returns (uint256, uint256, uint256) envfree - - quorumNumerator() returns uint256 - _executor() returns address - - erc20votes._getPastVotes(address, uint256) returns uint256 - - getExecutor() returns address - - timelock() returns address -} - - -////////////////////////////////////////////////////////////////////////////// -///////////////////////////////// GHOSTS ///////////////////////////////////// -////////////////////////////////////////////////////////////////////////////// - - -//////////// ghosts to keep track of votes counting //////////// - -/* - * the sum of voting power of those who voted - */ -ghost sum_all_votes_power() returns uint256 { - init_state axiom sum_all_votes_power() == 0; -} - -hook Sstore ghost_sum_vote_power_by_id [KEY uint256 pId] uint256 current_power(uint256 old_power) STORAGE { - havoc sum_all_votes_power assuming sum_all_votes_power@new() == sum_all_votes_power@old() - old_power + current_power; -} - -/* - * sum of all votes casted per proposal - */ -ghost tracked_weight(uint256) returns uint256 { - init_state axiom forall uint256 p. tracked_weight(p) == 0; -} - -/* - * sum of all votes casted - */ -ghost sum_tracked_weight() returns uint256 { - init_state axiom sum_tracked_weight() == 0; -} - -/* - * getter for _proposalVotes.againstVotes - */ -ghost votesAgainst() returns uint256 { - init_state axiom votesAgainst() == 0; -} - -/* - * getter for _proposalVotes.forVotes - */ -ghost votesFor() returns uint256 { - init_state axiom votesFor() == 0; -} - -/* - * getter for _proposalVotes.abstainVotes - */ -ghost votesAbstain() returns uint256 { - init_state axiom votesAbstain() == 0; -} - -hook Sstore _proposalVotes [KEY uint256 pId].againstVotes uint256 votes(uint256 old_votes) STORAGE { - havoc tracked_weight assuming forall uint256 p.(p == pId => tracked_weight@new(p) == tracked_weight@old(p) - old_votes + votes) && - (p != pId => tracked_weight@new(p) == tracked_weight@old(p)); - havoc sum_tracked_weight assuming sum_tracked_weight@new() == sum_tracked_weight@old() - old_votes + votes; - havoc votesAgainst assuming votesAgainst@new() == votesAgainst@old() - old_votes + votes; -} - -hook Sstore _proposalVotes [KEY uint256 pId].forVotes uint256 votes(uint256 old_votes) STORAGE { - havoc tracked_weight assuming forall uint256 p.(p == pId => tracked_weight@new(p) == tracked_weight@old(p) - old_votes + votes) && - (p != pId => tracked_weight@new(p) == tracked_weight@old(p)); - havoc sum_tracked_weight assuming sum_tracked_weight@new() == sum_tracked_weight@old() - old_votes + votes; - havoc votesFor assuming votesFor@new() == votesFor@old() - old_votes + votes; -} - -hook Sstore _proposalVotes [KEY uint256 pId].abstainVotes uint256 votes(uint256 old_votes) STORAGE { - havoc tracked_weight assuming forall uint256 p.(p == pId => tracked_weight@new(p) == tracked_weight@old(p) - old_votes + votes) && - (p != pId => tracked_weight@new(p) == tracked_weight@old(p)); - havoc sum_tracked_weight assuming sum_tracked_weight@new() == sum_tracked_weight@old() - old_votes + votes; - havoc votesAbstain assuming votesAbstain@new() == votesAbstain@old() - old_votes + votes; -} - - -////////////////////////////////////////////////////////////////////////////// -////////////////////////////// INVARIANTS //////////////////////////////////// -////////////////////////////////////////////////////////////////////////////// - - - -////////////////////////////////////////////////////////////////////////////// -///////////////////////////////// RULES ////////////////////////////////////// -////////////////////////////////////////////////////////////////////////////// - - -//NOT FINISHED -/* -* the sum of voting power of those who voted is less or equal to the maximum possible votes, per each proposal -*/ -rule possibleTotalVotes(uint256 pId, uint8 sup, env e, method f) { - - // add requireinvariant for all i, j. i = i - 1 && i < j => checkpointlookup[i] < checkpointlookup[j]; - require tracked_weight(pId) <= erc20votes.getPastTotalSupply(e, proposalSnapshot(pId)); - - uint256 againstB; - uint256 forB; - uint256 absatinB; - againstB, forB, absatinB = proposalVotes(pId); - - calldataarg args; - //f(e, args); - - castVote(e, pId, sup); - - uint256 against; - uint256 for; - uint256 absatin; - against, for, absatin = proposalVotes(pId); - - uint256 ps = proposalSnapshot(pId); - - assert tracked_weight(pId) <= erc20votes.getPastTotalSupply(e, proposalSnapshot(pId)), "bla bla bla"; -} \ No newline at end of file diff --git a/certora/specs/helpers.spec b/certora/specs/helpers.spec new file mode 100644 index 000000000..24842d62f --- /dev/null +++ b/certora/specs/helpers.spec @@ -0,0 +1 @@ +definition nonpayable(env e) returns bool = e.msg.value == 0; diff --git a/certora/specs/methods/IERC20.spec b/certora/specs/methods/IERC20.spec new file mode 100644 index 000000000..cfa454e13 --- /dev/null +++ b/certora/specs/methods/IERC20.spec @@ -0,0 +1,11 @@ +methods { + name() returns (string) envfree => DISPATCHER(true) + symbol() returns (string) envfree => DISPATCHER(true) + decimals() returns (uint8) envfree => DISPATCHER(true) + totalSupply() returns (uint256) envfree => DISPATCHER(true) + balanceOf(address) returns (uint256) envfree => DISPATCHER(true) + allowance(address,address) returns (uint256) envfree => DISPATCHER(true) + approve(address,uint256) returns (bool) => DISPATCHER(true) + transfer(address,uint256) returns (bool) => DISPATCHER(true) + transferFrom(address,address,uint256) returns (bool) => DISPATCHER(true) +} diff --git a/certora/specs/methods/IERC2612.spec b/certora/specs/methods/IERC2612.spec new file mode 100644 index 000000000..0c1689da4 --- /dev/null +++ b/certora/specs/methods/IERC2612.spec @@ -0,0 +1,5 @@ +methods { + permit(address,address,uint256,uint256,uint8,bytes32,bytes32) => DISPATCHER(true) + nonces(address) returns (uint256) envfree => DISPATCHER(true) + DOMAIN_SEPARATOR() returns (bytes32) envfree => DISPATCHER(true) +} diff --git a/certora/specs/methods/IERC3156.spec b/certora/specs/methods/IERC3156.spec new file mode 100644 index 000000000..18c10c515 --- /dev/null +++ b/certora/specs/methods/IERC3156.spec @@ -0,0 +1,5 @@ +methods { + maxFlashLoan(address) returns (uint256) envfree => DISPATCHER(true) + flashFee(address,uint256) returns (uint256) envfree => DISPATCHER(true) + flashLoan(address,address,uint256,bytes) returns (bool) => DISPATCHER(true) +} diff --git a/certora/specs/sanity.spec b/certora/specs/sanity.spec deleted file mode 100644 index e08f68845..000000000 --- a/certora/specs/sanity.spec +++ /dev/null @@ -1,14 +0,0 @@ -/* -This rule looks for a non-reverting execution path to each method, including those overridden in the harness. -A method has such an execution path if it violates this rule. -How it works: - - If there is a non-reverting execution path, we reach the false assertion, and the sanity fails. - - 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; - f(e, arg); - assert false; -} \ No newline at end of file diff --git a/package-lock.json b/package-lock.json index f3081ffa9..b9b491e05 100644 --- a/package-lock.json +++ b/package-lock.json @@ -39,6 +39,7 @@ "lodash.zip": "^4.2.0", "merkletreejs": "^0.2.13", "micromatch": "^4.0.2", + "p-limit": "^3.1.0", "prettier": "^2.8.1", "prettier-plugin-solidity": "^1.1.0", "rimraf": "^3.0.2", @@ -215,6 +216,21 @@ "changeset": "bin.js" } }, + "node_modules/@changesets/cli/node_modules/p-limit": { + "version": "2.3.0", + "resolved": "https://registry.npmjs.org/p-limit/-/p-limit-2.3.0.tgz", + "integrity": "sha512-//88mFWSJx8lxCzwdAABTJL2MyWB12+eIY7MDL2SqLmAkeKU9qxRvWuSyTjm3FUmpBEMuFfckAIqEaVGUDxb6w==", + "dev": true, + "dependencies": { + "p-try": "^2.0.0" + }, + "engines": { + "node": ">=6" + }, + "funding": { + "url": "https://github.com/sponsors/sindresorhus" + } + }, "node_modules/@changesets/cli/node_modules/semver": { "version": "5.7.1", "resolved": "https://registry.npmjs.org/semver/-/semver-5.7.1.tgz", @@ -5375,21 +5391,6 @@ "url": "https://github.com/sponsors/sindresorhus" } }, - "node_modules/eslint/node_modules/p-limit": { - "version": "3.1.0", - "resolved": "https://registry.npmjs.org/p-limit/-/p-limit-3.1.0.tgz", - "integrity": "sha512-TYOanM3wGwNGsZN2cVTYPArw454xnXj5qmWF1bEoAc4+cU/ol7GVh7odevjp1FNHduHc3KZMcFduxU5Xc6uJRQ==", - "dev": true, - "dependencies": { - "yocto-queue": "^0.1.0" - }, - "engines": { - "node": ">=10" - }, - "funding": { - "url": "https://github.com/sponsors/sindresorhus" - } - }, "node_modules/eslint/node_modules/p-locate": { "version": "5.0.0", "resolved": "https://registry.npmjs.org/p-locate/-/p-locate-5.0.0.tgz", @@ -5835,6 +5836,21 @@ "node": ">= 0.4" } }, + "node_modules/eth-gas-reporter/node_modules/p-limit": { + "version": "2.3.0", + "resolved": "https://registry.npmjs.org/p-limit/-/p-limit-2.3.0.tgz", + "integrity": "sha512-//88mFWSJx8lxCzwdAABTJL2MyWB12+eIY7MDL2SqLmAkeKU9qxRvWuSyTjm3FUmpBEMuFfckAIqEaVGUDxb6w==", + "dev": true, + "dependencies": { + "p-try": "^2.0.0" + }, + "engines": { + "node": ">=6" + }, + "funding": { + "url": "https://github.com/sponsors/sindresorhus" + } + }, "node_modules/eth-gas-reporter/node_modules/p-locate": { "version": "3.0.0", "resolved": "https://registry.npmjs.org/p-locate/-/p-locate-3.0.0.tgz", @@ -9516,21 +9532,6 @@ "integrity": "sha512-6FlzubTLZG3J2a/NVCAleEhjzq5oxgHyaCU9yYXvcLsvoVaHJq/s5xXI6/XXP6tz7R9xAOtHnSO/tXtF3WRTlA==", "dev": true }, - "node_modules/mocha/node_modules/p-limit": { - "version": "3.1.0", - "resolved": "https://registry.npmjs.org/p-limit/-/p-limit-3.1.0.tgz", - "integrity": "sha512-TYOanM3wGwNGsZN2cVTYPArw454xnXj5qmWF1bEoAc4+cU/ol7GVh7odevjp1FNHduHc3KZMcFduxU5Xc6uJRQ==", - "dev": true, - "dependencies": { - "yocto-queue": "^0.1.0" - }, - "engines": { - "node": ">=10" - }, - "funding": { - "url": "https://github.com/sponsors/sindresorhus" - } - }, "node_modules/mocha/node_modules/p-locate": { "version": "5.0.0", "resolved": "https://registry.npmjs.org/p-locate/-/p-locate-5.0.0.tgz", @@ -10108,15 +10109,15 @@ } }, "node_modules/p-limit": { - "version": "2.3.0", - "resolved": "https://registry.npmjs.org/p-limit/-/p-limit-2.3.0.tgz", - "integrity": "sha512-//88mFWSJx8lxCzwdAABTJL2MyWB12+eIY7MDL2SqLmAkeKU9qxRvWuSyTjm3FUmpBEMuFfckAIqEaVGUDxb6w==", + "version": "3.1.0", + "resolved": "https://registry.npmjs.org/p-limit/-/p-limit-3.1.0.tgz", + "integrity": "sha512-TYOanM3wGwNGsZN2cVTYPArw454xnXj5qmWF1bEoAc4+cU/ol7GVh7odevjp1FNHduHc3KZMcFduxU5Xc6uJRQ==", "dev": true, "dependencies": { - "p-try": "^2.0.0" + "yocto-queue": "^0.1.0" }, "engines": { - "node": ">=6" + "node": ">=10" }, "funding": { "url": "https://github.com/sponsors/sindresorhus" @@ -10134,6 +10135,21 @@ "node": ">=8" } }, + "node_modules/p-locate/node_modules/p-limit": { + "version": "2.3.0", + "resolved": "https://registry.npmjs.org/p-limit/-/p-limit-2.3.0.tgz", + "integrity": "sha512-//88mFWSJx8lxCzwdAABTJL2MyWB12+eIY7MDL2SqLmAkeKU9qxRvWuSyTjm3FUmpBEMuFfckAIqEaVGUDxb6w==", + "dev": true, + "dependencies": { + "p-try": "^2.0.0" + }, + "engines": { + "node": ">=6" + }, + "funding": { + "url": "https://github.com/sponsors/sindresorhus" + } + }, "node_modules/p-map": { "version": "4.0.0", "resolved": "https://registry.npmjs.org/p-map/-/p-map-4.0.0.tgz", @@ -10456,21 +10472,6 @@ "url": "https://github.com/sponsors/sindresorhus" } }, - "node_modules/preferred-pm/node_modules/p-limit": { - "version": "3.1.0", - "resolved": "https://registry.npmjs.org/p-limit/-/p-limit-3.1.0.tgz", - "integrity": "sha512-TYOanM3wGwNGsZN2cVTYPArw454xnXj5qmWF1bEoAc4+cU/ol7GVh7odevjp1FNHduHc3KZMcFduxU5Xc6uJRQ==", - "dev": true, - "dependencies": { - "yocto-queue": "^0.1.0" - }, - "engines": { - "node": ">=10" - }, - "funding": { - "url": "https://github.com/sponsors/sindresorhus" - } - }, "node_modules/preferred-pm/node_modules/p-locate": { "version": "5.0.0", "resolved": "https://registry.npmjs.org/p-locate/-/p-locate-5.0.0.tgz", @@ -12942,6 +12943,21 @@ "node": ">= 0.4" } }, + "node_modules/solidity-coverage/node_modules/p-limit": { + "version": "2.3.0", + "resolved": "https://registry.npmjs.org/p-limit/-/p-limit-2.3.0.tgz", + "integrity": "sha512-//88mFWSJx8lxCzwdAABTJL2MyWB12+eIY7MDL2SqLmAkeKU9qxRvWuSyTjm3FUmpBEMuFfckAIqEaVGUDxb6w==", + "dev": true, + "dependencies": { + "p-try": "^2.0.0" + }, + "engines": { + "node": ">=6" + }, + "funding": { + "url": "https://github.com/sponsors/sindresorhus" + } + }, "node_modules/solidity-coverage/node_modules/p-locate": { "version": "3.0.0", "resolved": "https://registry.npmjs.org/p-locate/-/p-locate-3.0.0.tgz", @@ -15347,6 +15363,15 @@ "tty-table": "^4.1.5" }, "dependencies": { + "p-limit": { + "version": "2.3.0", + "resolved": "https://registry.npmjs.org/p-limit/-/p-limit-2.3.0.tgz", + "integrity": "sha512-//88mFWSJx8lxCzwdAABTJL2MyWB12+eIY7MDL2SqLmAkeKU9qxRvWuSyTjm3FUmpBEMuFfckAIqEaVGUDxb6w==", + "dev": true, + "requires": { + "p-try": "^2.0.0" + } + }, "semver": { "version": "5.7.1", "resolved": "https://registry.npmjs.org/semver/-/semver-5.7.1.tgz", @@ -19264,15 +19289,6 @@ "p-locate": "^5.0.0" } }, - "p-limit": { - "version": "3.1.0", - "resolved": "https://registry.npmjs.org/p-limit/-/p-limit-3.1.0.tgz", - "integrity": "sha512-TYOanM3wGwNGsZN2cVTYPArw454xnXj5qmWF1bEoAc4+cU/ol7GVh7odevjp1FNHduHc3KZMcFduxU5Xc6uJRQ==", - "dev": true, - "requires": { - "yocto-queue": "^0.1.0" - } - }, "p-locate": { "version": "5.0.0", "resolved": "https://registry.npmjs.org/p-locate/-/p-locate-5.0.0.tgz", @@ -19650,6 +19666,15 @@ "object-keys": "^1.0.11" } }, + "p-limit": { + "version": "2.3.0", + "resolved": "https://registry.npmjs.org/p-limit/-/p-limit-2.3.0.tgz", + "integrity": "sha512-//88mFWSJx8lxCzwdAABTJL2MyWB12+eIY7MDL2SqLmAkeKU9qxRvWuSyTjm3FUmpBEMuFfckAIqEaVGUDxb6w==", + "dev": true, + "requires": { + "p-try": "^2.0.0" + } + }, "p-locate": { "version": "3.0.0", "resolved": "https://registry.npmjs.org/p-locate/-/p-locate-3.0.0.tgz", @@ -22564,15 +22589,6 @@ "integrity": "sha512-6FlzubTLZG3J2a/NVCAleEhjzq5oxgHyaCU9yYXvcLsvoVaHJq/s5xXI6/XXP6tz7R9xAOtHnSO/tXtF3WRTlA==", "dev": true }, - "p-limit": { - "version": "3.1.0", - "resolved": "https://registry.npmjs.org/p-limit/-/p-limit-3.1.0.tgz", - "integrity": "sha512-TYOanM3wGwNGsZN2cVTYPArw454xnXj5qmWF1bEoAc4+cU/ol7GVh7odevjp1FNHduHc3KZMcFduxU5Xc6uJRQ==", - "dev": true, - "requires": { - "yocto-queue": "^0.1.0" - } - }, "p-locate": { "version": "5.0.0", "resolved": "https://registry.npmjs.org/p-locate/-/p-locate-5.0.0.tgz", @@ -23028,12 +23044,12 @@ } }, "p-limit": { - "version": "2.3.0", - "resolved": "https://registry.npmjs.org/p-limit/-/p-limit-2.3.0.tgz", - "integrity": "sha512-//88mFWSJx8lxCzwdAABTJL2MyWB12+eIY7MDL2SqLmAkeKU9qxRvWuSyTjm3FUmpBEMuFfckAIqEaVGUDxb6w==", + "version": "3.1.0", + "resolved": "https://registry.npmjs.org/p-limit/-/p-limit-3.1.0.tgz", + "integrity": "sha512-TYOanM3wGwNGsZN2cVTYPArw454xnXj5qmWF1bEoAc4+cU/ol7GVh7odevjp1FNHduHc3KZMcFduxU5Xc6uJRQ==", "dev": true, "requires": { - "p-try": "^2.0.0" + "yocto-queue": "^0.1.0" } }, "p-locate": { @@ -23043,6 +23059,17 @@ "dev": true, "requires": { "p-limit": "^2.2.0" + }, + "dependencies": { + "p-limit": { + "version": "2.3.0", + "resolved": "https://registry.npmjs.org/p-limit/-/p-limit-2.3.0.tgz", + "integrity": "sha512-//88mFWSJx8lxCzwdAABTJL2MyWB12+eIY7MDL2SqLmAkeKU9qxRvWuSyTjm3FUmpBEMuFfckAIqEaVGUDxb6w==", + "dev": true, + "requires": { + "p-try": "^2.0.0" + } + } } }, "p-map": { @@ -23286,15 +23313,6 @@ "p-locate": "^5.0.0" } }, - "p-limit": { - "version": "3.1.0", - "resolved": "https://registry.npmjs.org/p-limit/-/p-limit-3.1.0.tgz", - "integrity": "sha512-TYOanM3wGwNGsZN2cVTYPArw454xnXj5qmWF1bEoAc4+cU/ol7GVh7odevjp1FNHduHc3KZMcFduxU5Xc6uJRQ==", - "dev": true, - "requires": { - "yocto-queue": "^0.1.0" - } - }, "p-locate": { "version": "5.0.0", "resolved": "https://registry.npmjs.org/p-locate/-/p-locate-5.0.0.tgz", @@ -25146,6 +25164,15 @@ "object-keys": "^1.0.11" } }, + "p-limit": { + "version": "2.3.0", + "resolved": "https://registry.npmjs.org/p-limit/-/p-limit-2.3.0.tgz", + "integrity": "sha512-//88mFWSJx8lxCzwdAABTJL2MyWB12+eIY7MDL2SqLmAkeKU9qxRvWuSyTjm3FUmpBEMuFfckAIqEaVGUDxb6w==", + "dev": true, + "requires": { + "p-try": "^2.0.0" + } + }, "p-locate": { "version": "3.0.0", "resolved": "https://registry.npmjs.org/p-locate/-/p-locate-3.0.0.tgz", diff --git a/package.json b/package.json index 282547535..56798f788 100644 --- a/package.json +++ b/package.json @@ -80,6 +80,7 @@ "lodash.zip": "^4.2.0", "merkletreejs": "^0.2.13", "micromatch": "^4.0.2", + "p-limit": "^3.1.0", "prettier": "^2.8.1", "prettier-plugin-solidity": "^1.1.0", "rimraf": "^3.0.2", diff --git a/requirements.txt b/requirements.txt new file mode 100644 index 000000000..797b3598d --- /dev/null +++ b/requirements.txt @@ -0,0 +1 @@ +certora-cli==3.6.3