diff --git a/.github/PULL_REQUEST_TEMPLATE.md b/.github/PULL_REQUEST_TEMPLATE.md index 4151484..0b191ff 100644 --- a/.github/PULL_REQUEST_TEMPLATE.md +++ b/.github/PULL_REQUEST_TEMPLATE.md @@ -10,3 +10,4 @@ Ensure you completed **all of the steps** below before submitting your pull requ - [ ] Ran `forge snapshot`? - [ ] Ran `pnpm lint`? - [ ] Ran `pnpm gas-report`? +- [ ] Ran `pnpm verify`? diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index e2d09a3..f3a0d21 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -10,6 +10,7 @@ on: push: branches: - "main" + - "master" jobs: lint: @@ -117,3 +118,51 @@ jobs: run: | echo "## Coverage result" >> $GITHUB_STEP_SUMMARY echo "✅ Uploaded to Codecov" >> $GITHUB_STEP_SUMMARY + verify: + needs: ["lint", "build"] + runs-on: ubuntu-latest + + steps: + - uses: actions/checkout@v3 + with: + submodules: recursive + + - name: Install Python + uses: actions/setup-python@v2 + with: { python-version: 3.9 } + + - name: Install Java + uses: actions/setup-java@v1 + with: { java-version: "11", java-package: jre } + + - name: Install Certora CLI + run: pip3 install certora-cli==5.0.5 + + - name: Install Solidity + run: | + wget https://github.com/ethereum/solidity/releases/download/v0.8.18/solc-static-linux + chmod +x solc-static-linux + sudo mv solc-static-linux /usr/local/bin/solc + + - name: "Install Pnpm" + uses: "pnpm/action-setup@v2" + with: + version: "8" + + - name: "Install Node.js" + uses: "actions/setup-node@v3" + with: + cache: "pnpm" + node-version: "lts/*" + + - name: "Install the Node.js dependencies" + run: "pnpm install" + + - name: Verify rules + run: "pnpm verify" + env: + CERTORAKEY: ${{ secrets.CERTORAKEY }} + + strategy: + fail-fast: false + max-parallel: 16 diff --git a/.gitignore b/.gitignore index 27c05e8..d8dc741 100644 --- a/.gitignore +++ b/.gitignore @@ -15,3 +15,11 @@ yarn.lock !broadcast broadcast/* broadcast/*/31337/ + +# Certora +.certora* +resource_errors.json +last_conf* +certora*.txt +.zip-output-url.txt +certora/munged/* diff --git a/certora/Makefile b/certora/Makefile new file mode 100644 index 0000000..9471bcb --- /dev/null +++ b/certora/Makefile @@ -0,0 +1,23 @@ +default: help + +PATCH = MiniMeBase.patch +CONTRACTS_DIR = ../contracts +MUNGED_DIR = ./munged +MiniMeBase_origin = ../contracts/ +MiniMeBase_munged = ./munged/ +help: + @echo "usage:" + @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: + cp -R $(MiniMeBase_origin) $(MUNGED_DIR) + patch -d $(MUNGED_DIR) < $(PATCH) + +record: + diff -burN $(MiniMeBase_origin) $(MiniMeBase_munged) | sed 's+\$(MiniMeBase_origin)/++g' | sed 's+$(MiniMeBase_munged)++g' > $(PATCH) + +clean: + git clean -fdX + touch $(PATCH) \ No newline at end of file diff --git a/certora/MiniMeBase.patch b/certora/MiniMeBase.patch new file mode 100644 index 0000000..f58ffd6 --- /dev/null +++ b/certora/MiniMeBase.patch @@ -0,0 +1,21 @@ +diff --git a/contracts/MiniMeBase.sol b/contracts/MiniMeBase.sol +index c518f8f..2ed2604 100644 +--- a/contracts/MiniMeBase.sol ++++ b/contracts/MiniMeBase.sol +@@ -76,13 +76,13 @@ abstract contract MiniMeBase is Controlled, IERC20, IERC20Permit, EIP712, Nonces + // `balances` is the map that tracks the balance of each address, in this + // contract when the balance changes the block number that the change + // occurred is also included in the map +- mapping(address account => Checkpoint[] history) private balances; ++ mapping(address account => Checkpoint[] history) public balances; + + // `allowed` tracks any extra transfer rights as in all ERC20 tokens +- mapping(address account => mapping(address authorized => uint256 amount) allowance) private allowed; ++ mapping(address account => mapping(address authorized => uint256 amount) allowance) public allowed; + + // Tracks the history of the `totalSupply` of the token +- Checkpoint[] private totalSupplyHistory; ++ Checkpoint[] public totalSupplyHistory; + + // Flag that determines if the token is transferable or not. + bool public transfersEnabled; diff --git a/certora/Status Final Report by Certora.pdf b/certora/Status Final Report by Certora.pdf new file mode 100644 index 0000000..25fb73e Binary files /dev/null and b/certora/Status Final Report by Certora.pdf differ diff --git a/certora/harness/MiniMeTokenHarness.sol b/certora/harness/MiniMeTokenHarness.sol new file mode 100644 index 0000000..b90c61d --- /dev/null +++ b/certora/harness/MiniMeTokenHarness.sol @@ -0,0 +1,48 @@ +// SPDX-License-Identifier: GPL-3.0 +pragma solidity 0.8.18; + +import { MiniMeToken } from "../munged/MiniMeToken.sol"; + +contract MiniMeTokenHarness is MiniMeToken { + + error MinimeTokenHarness_InvalidCheckpointLength(); + + constructor( + MiniMeToken _parentToken, + uint256 _parentSnapShotBlock, + string memory _tokenName, + uint8 _decimalUnits, + string memory _tokenSymbol, + bool _transfersEnabled + ) public MiniMeToken( + _parentToken, + _parentSnapShotBlock, + _tokenName, + _decimalUnits, + _tokenSymbol, + _transfersEnabled + ) {} + + function getCheckpointsLengthByAddress(address user) public view returns (uint256) { + return balances[user].length; + } + + function getLatestBlockNumberByAddress(address user) public view returns (uint256) { + uint256 checkpointsLength = getCheckpointsLengthByAddress(user); + if (checkpointsLength == 0) revert MinimeTokenHarness_InvalidCheckpointLength(); + Checkpoint memory latestCheckPoint = getCheckpointByAddressAndIndex(user, checkpointsLength - 1); + return latestCheckPoint.fromBlock; + } + + function getCheckpointByAddressAndIndex(address user, uint256 index) public view returns (Checkpoint memory) { + uint256 checkpointsLength = getCheckpointsLengthByAddress(user); + if (checkpointsLength == 0 || index >= checkpointsLength) revert MinimeTokenHarness_InvalidCheckpointLength(); + return balances[user][index]; + } + + function getFromBlockByAddressAndIndex(address user, uint256 index) public view returns (uint256) { + uint256 checkpointsLength = getCheckpointsLengthByAddress(user); + if (checkpointsLength == 0 || index >= checkpointsLength) revert MinimeTokenHarness_InvalidCheckpointLength(); + return balances[user][index].fromBlock; + } +} diff --git a/certora/mocks/DummyController.sol b/certora/mocks/DummyController.sol new file mode 100644 index 0000000..8956477 --- /dev/null +++ b/certora/mocks/DummyController.sol @@ -0,0 +1,9 @@ +// SPDX-License-Identifier: agpl-3.0 +pragma solidity ^0.8.0; + +contract DummyController { + // solhint-disable-next-line no-unused-vars + function transfer(address recipient, uint256 amount) external returns (bool) { + return true; + } +} diff --git a/certora/mocks/DummyERC20Impl.sol b/certora/mocks/DummyERC20Impl.sol new file mode 100644 index 0000000..c9d2e65 --- /dev/null +++ b/certora/mocks/DummyERC20Impl.sol @@ -0,0 +1,27 @@ +// SPDX-License-Identifier: agpl-3.0 +pragma solidity ^0.8.0; + +contract DummyERC20Impl { + uint256 public t; + mapping (address owner => uint256 balance) public balances; + mapping (address holder => mapping (address spender => uint256 amount)) public allowances; + + string public name; + string public symbol; + uint256 public decimals; + + // solhint-disable-next-line no-unused-vars + function balanceOfAt(address _owner, uint _blockNumber) public view returns (uint) { + return balances[_owner]; + } + + /** + * @notice Total amount of tokens at a specific `_blockNumber`. + * @param _blockNumber The block number when the totalSupply is queried + * @return The total amount of tokens at `_blockNumber` + */ + // solhint-disable-next-line no-unused-vars + function totalSupplyAt(uint _blockNumber) public view returns(uint) { + return t; + } +} diff --git a/certora/mocks/DummyERC20ImplA.sol b/certora/mocks/DummyERC20ImplA.sol new file mode 100644 index 0000000..27216eb --- /dev/null +++ b/certora/mocks/DummyERC20ImplA.sol @@ -0,0 +1,71 @@ +// SPDX-License-Identifier: agpl-3.0 +pragma solidity ^0.8.0; + +contract DummyERC20ImplA { + uint256 public t; + mapping (address owner => uint256 amount) public balances; + mapping (address holder => mapping (address spender => uint256 amount)) public allowances; + + string public name; + string public symbol; + uint256 public decimals; + + function myAddress() public returns (address) { + return address(this); + } + + function add(uint a, uint b) internal pure returns (uint256) { + uint c = a + b; + require (c >= a, "c is less than a"); + return c; + } + function sub(uint a, uint b) internal pure returns (uint256) { + require (a >= b, "a is less than b"); + return a - b; + } + + function totalSupply() external view returns (uint256) { + return t; + } + function balanceOf(address account) external view returns (uint256) { + return balances[account]; + } + function transfer(address recipient, uint256 amount) external returns (bool) { + balances[msg.sender] = sub(balances[msg.sender], amount); + balances[recipient] = add(balances[recipient], amount); + return true; + } + function allowance(address owner, address spender) external view returns (uint256) { + return allowances[owner][spender]; + } + function approve(address spender, uint256 amount) external returns (bool) { + allowances[msg.sender][spender] = amount; + return true; + } + + function transferFrom( + address sender, + address recipient, + uint256 amount + ) external returns (bool) { + balances[sender] = sub(balances[sender], amount); + balances[recipient] = add(balances[recipient], amount); + allowances[sender][msg.sender] = sub(allowances[sender][msg.sender], amount); + return true; + } + + // solhint-disable-next-line no-unused-vars + function balanceOfAt(address _owner, uint _blockNumber) public view returns (uint) { + return balances[_owner]; + } + + /** + * @notice Total amount of tokens at a specific `_blockNumber`. + * @param _blockNumber The block number when the totalSupply is queried + * @return The total amount of tokens at `_blockNumber` + */ + // solhint-disable-next-line no-unused-vars + function totalSupplyAt(uint _blockNumber) public view returns(uint) { + return t; + } +} diff --git a/certora/scripts/MiniMeToken.sh b/certora/scripts/MiniMeToken.sh new file mode 100755 index 0000000..805e80e --- /dev/null +++ b/certora/scripts/MiniMeToken.sh @@ -0,0 +1,9 @@ +certoraRun certora/harness/MiniMeTokenHarness.sol certora/mocks/DummyERC20Impl.sol certora/mocks/DummyERC20ImplA.sol certora/mocks/DummyController.sol \ +--verify MiniMeTokenHarness:certora/specs/MiniMeToken.spec \ +--link MiniMeTokenHarness:parentToken=DummyERC20Impl \ +--link MiniMeTokenHarness:controller=DummyController \ +--address DummyERC20Impl:0 \ +--loop_iter 3 \ +--optimistic_loop \ +--packages @openzeppelin=lib/openzeppelin-contracts \ +--msg "MiniMe Token" diff --git a/certora/specs/MiniMeToken.spec b/certora/specs/MiniMeToken.spec new file mode 100644 index 0000000..4c35b54 --- /dev/null +++ b/certora/specs/MiniMeToken.spec @@ -0,0 +1,489 @@ +using DummyERC20ImplA as DummyERC20; +using DummyController as DummyController; +using DummyERC20Impl as DummyERC20Impl; + +methods { + function _.transfer(address _to, uint256 _amount) external => DISPATCHER(true); + function transferFrom(address _from, address _to, uint256 _amount) external returns (bool); + function doTransfer(address _from, address _to, uint _amount) internal returns (bool); + function doApprove(address _from, address _spender, uint256 _amount) internal returns (bool); + function _mint(address, uint) internal returns (bool); + function _burn(address _owner, uint _amount) internal returns (bool); + function _.balanceOf(address _owner) external => DISPATCHER(true); + function approve(address _spender, uint256 _amount) external returns (bool); + function allowance(address _owner, address _spender) external returns (uint256) envfree; + function approveAndCall(address _spender, uint256 _amount, bytes memory _extraData) external returns (bool); + function totalSupply() external returns (uint); + function balanceOfAt(address _owner, uint _blockNumber) external returns (uint) envfree; + function totalSupplyAt(uint _blockNumber) external returns (uint) envfree; + function generateTokens(address _owner, uint _amount) external returns (bool); // onlyController + function destroyTokens(address _owner, uint _amount) external returns (bool); // onlyController + function enableTransfers(bool _transfersEnabled) external; // onlyController + function isContract(address _addr) internal returns(bool); + function min(uint a, uint b) internal returns (uint); + function claimTokens(address _token) external; // onlyController + function permit( address owner, address spender, uint256 value, uint256 deadline, uint8 v, bytes32 r, bytes32 s) external; + function nonces(address owner) external returns (uint256); + function DOMAIN_SEPARATOR() external returns (bytes32); + + // Getters: + function creationBlock() external returns (uint) envfree; + function transfersEnabled() external returns (bool) envfree; + function parentSnapShotBlock() external returns (uint) envfree; + function controller() external returns (address) envfree; + + // Harness: + function getCheckpointsLengthByAddress(address user) external returns (uint256) envfree; + function getLatestBlockNumberByAddress(address user) external returns (uint256) envfree; + function getCheckpointByAddressAndIndex(address user, uint256 index) external returns (MiniMeBase.Checkpoint) envfree; + function getFromBlockByAddressAndIndex(address user, uint256 index) external returns (uint256) envfree; + + // Summarizations: + function _.onTransfer(address _from, address _to, uint _amount) external => ALWAYS(true); + function _.onApprove(address _from, address _spender, uint _amount) external => NONDET; + function _.receiveApproval(address from, uint256 _amount, address _token, bytes _data) external => NONDET; + function _.proxyPayment(address) external => NONDET; + function DummyController.transfer(address, uint256) external returns (bool) => NONDET; + +} + +definition MaxHistoryRecords() returns uint256 = 1000000; + +ghost mapping(address => mapping(uint256 => uint128)) fromBlocks { + axiom forall address user . forall uint256 index1 . fromBlocks[user][index1] == 0; +} +ghost mapping(uint256 => uint128) totalSupplyFromBlocks { + axiom forall uint256 index1 . totalSupplyFromBlocks[index1] == 0; +} +ghost mapping(address => mapping(uint256 => uint128)) values; +ghost mapping(uint256 => uint128) totalSupplyvalues; + +// Mirror total supply history checkpoits values +hook Sload uint128 _value totalSupplyHistory[INDEX uint256 indx].value STORAGE { + require totalSupplyvalues[indx] == _value; +} + +hook Sstore totalSupplyHistory[INDEX uint256 indx].value uint128 _value (uint128 old_value) STORAGE { + totalSupplyvalues[indx] = _value; +} + +// Mirror total supply history checkpoits fromBlocks +hook Sload uint128 _fromBlock totalSupplyHistory[INDEX uint256 indx].fromBlock STORAGE { + require totalSupplyFromBlocks[indx] == _fromBlock; +} + +hook Sstore totalSupplyHistory[INDEX uint256 indx].fromBlock uint128 _fromBlock (uint128 old_fromBlock) STORAGE { + totalSupplyFromBlocks[indx] = _fromBlock; +} + +// Mirror balances history checkpoits values +hook Sload uint128 _value balances[KEY address user][INDEX uint256 indx].value STORAGE { + require values[user][indx] == _value; +} + +hook Sstore balances[KEY address user][INDEX uint256 indx].value uint128 _value (uint128 old_value) STORAGE { + values[user][indx] = _value; +} + +// Mirror balances history checkpoits fromBlocks +hook Sload uint128 _fromBlock balances[KEY address user][INDEX uint256 indx].fromBlock STORAGE { + require fromBlocks[user][indx] == _fromBlock; +} + +hook Sstore balances[KEY address user][INDEX uint256 indx].fromBlock uint128 _fromBlock (uint128 old_fromBlock) STORAGE { + fromBlocks[user][indx] = _fromBlock; +} + +// Limit history records to avoid overflows. +hook Sload uint256 _length balances[KEY address user].(offset 0) STORAGE { + require _length < MaxHistoryRecords(); +} + +hook Sload uint256 _length totalSupplyHistory.(offset 0) STORAGE { + require _length < MaxHistoryRecords(); +} + +// function that filtered out do not change the total supply +function doesntChangeBalance(method f) returns bool { + return (f.selector != sig:generateTokens(address, uint).selector && + f.selector != sig:claimTokens(address).selector && + f.selector != sig:destroyTokens(address, uint).selector); +} + +/* + @Description: + Each checkpoint.fromBlock must be less than the current blocknumber (no checkpoints from the future). +*/ +invariant checkPointBlockNumberValidity(env e1) + e1.block.number > 0 => (forall uint256 i . forall address user . to_mathint(fromBlocks[user][i]) <= to_mathint(e1.block.number)) + { + preserved with (env e) { + require e1.block.number < max_uint128 && e.block.number == e1.block.number; + } + } + +/* + @Description: + checkpoint.fromBlock is monotonicly increasing for each user. This rule was proven inorder to assume this property on the mirrored structs and thats why it is vaccuous now. +*/ +invariant blockNumberMonotonicInc(env e1) + getFromBlockByAddressAndIndex(e1.msg.sender, e1.block.number) < getFromBlockByAddressAndIndex(e1.msg.sender, assert_uint256(e1.block.number + 1)) + { + preserved with (env e) { + requireInvariant checkPointBlockNumberValidity(e); + } + } + +/* + @Description: + All Block Numbers Are Greater OrEqual To the Creation Block. +*/ +invariant allBlockNumbersAreGreaterOrEqualToCreationBlock(address user, uint256 index) + getFromBlockByAddressAndIndex(user, index) >= creationBlock() + { preserved with (env e) { require e.block.number > creationBlock();} } + +/* + @Description: + All Block Numbers Are Greater OrEqual To the Parent Snapshot Block. +*/ +invariant allFromBlockAreGreaterThanParentSnapShotBlock(address user, uint256 index) + getFromBlockByAddressAndIndex(user, index) >= parentSnapShotBlock(); + +/* + @Description: + The balance of each user must be less or equal to the total supply. +*/ +invariant balanceOfLessOrEqToTotalSpply(env e, address owner, uint blocknumber) + balanceOfAt(e, owner, blocknumber) <= totalSupplyAt(e, blocknumber); + +/* + @Description: + Balance of address 0 is always 0 +*/ +invariant ZeroAddressNoBalance(env e) + currentContract.balanceOf(e, 0) == 0 + { + preserved claimTokens(address _token) with (env e1) { + require _token == DummyERC20; + } + } + +/* + @Description: + Cant change balances and totalSupply history. +*/ +rule historyMutability(method f, address user) { + env e1; + env e; + calldataarg args; + + require e1.block.number > e.block.number; + + uint256 balanceOfBefore = balanceOfAt(e, user, e.block.number); + uint256 totalSupplyBefore = totalSupplyAt(e, e.block.number); + + f(e1, args); + + uint256 balanceOfAfter = balanceOfAt(e, user, e.block.number); + uint256 totalSupplyAfter = totalSupplyAt(e, e.block.number); + + assert balanceOfBefore == balanceOfAfter; + assert totalSupplyBefore == totalSupplyAfter; +} + +/* + @Description: + Verify that there is no fee on transferFrom() (like potentially on USDT) +*/ +rule noFeeOnTransferFrom(address alice, address bob, uint256 amount) { + env e; + require alice != bob; + require allowance(alice, e.msg.sender) >= amount; + requireInvariant checkPointBlockNumberValidity(e); + requireInvariant allFromBlockAreGreaterThanParentSnapShotBlock(e.msg.sender, 0); + requireInvariant allFromBlockAreGreaterThanParentSnapShotBlock(bob, 0); + requireInvariant allFromBlockAreGreaterThanParentSnapShotBlock(alice, 0); + mathint balanceBefore = currentContract.balanceOf(e, bob); + mathint balanceAliceBefore = currentContract.balanceOf(e, alice); + // avoid overflows + require balanceBefore + balanceAliceBefore < max_uint128; + + bool success = transferFrom(e, alice, bob, amount); + + mathint balanceAfter = currentContract.balanceOf(e, bob); + mathint balanceAliceAfter = currentContract.balanceOf(e, alice); + + assert success => balanceAfter == balanceBefore + amount; + assert success => balanceAliceAfter == balanceAliceBefore - amount; + assert !success => balanceAfter == balanceBefore; + assert !success => balanceAliceAfter == balanceAliceBefore; +} + +/* + @Description: + Verify that there is no fee on transfer() (like potentially on USDT) +*/ +rule noFeeOnTransfer(address bob, uint256 amount) { + env e; + require bob != e.msg.sender; + requireInvariant checkPointBlockNumberValidity(e); + requireInvariant allFromBlockAreGreaterThanParentSnapShotBlock(e.msg.sender, 0); + requireInvariant allFromBlockAreGreaterThanParentSnapShotBlock(bob, 0); + mathint balanceSenderBefore = currentContract.balanceOf(e, e.msg.sender); + mathint balanceBefore = currentContract.balanceOf(e, bob); + // avoid overflows + require balanceBefore + balanceSenderBefore < max_uint128; + + bool success = transfer(e, bob, amount); + + mathint balanceAfter = currentContract.balanceOf(e, bob); + mathint balanceSenderAfter = currentContract.balanceOf(e, e.msg.sender); + + assert success => balanceAfter == balanceBefore + amount; + assert success => balanceSenderAfter == balanceSenderBefore - amount; + assert !success => balanceAfter == balanceBefore; + assert !success => balanceSenderAfter == balanceSenderBefore; +} + +/* + @Description: + Token transfer works correctly. Balances are updated if not reverted. + If reverted then the transfer amount was too high, or the recipient is 0. + + + @Notes: + This rule fails on tokens with a blacklist function, like USDC and USDT. + The prover finds a counterexample of a reverted transfer to a blacklisted address or a transfer in a paused state. +*/ +rule transferCorrect(address to, uint256 amount) { + env e; + requireInvariant checkPointBlockNumberValidity(e); + + uint256 fromBalanceBefore = currentContract.balanceOf(e, e.msg.sender); + uint256 toBalanceBefore = currentContract.balanceOf(e, to); + // avoid overflows + require fromBalanceBefore + toBalanceBefore <= max_uint128; + + bool success = transfer(e, to, amount); + if (success) { + if (e.msg.sender == to) { + assert currentContract.balanceOf(e, e.msg.sender) == fromBalanceBefore; + } else { + assert currentContract.balanceOf(e, e.msg.sender) == assert_uint256(fromBalanceBefore - amount); + assert currentContract.balanceOf(e, to) == assert_uint256(toBalanceBefore + amount); + } + } else { + assert amount > fromBalanceBefore || to == 0; + } +} + +/* + @Description: + Test that transferFrom works correctly. Balances are updated if not reverted. + If reverted, it means the transfer amount was too high, or the recipient is 0 + + @Notes: + This rule fails on tokens with a blacklist and or pause function, like USDC and USDT. + The prover finds a counterexample of a reverted transfer to a blacklisted address or a transfer in a paused state. +*/ +rule transferFromCorrect(address from, address to, uint256 amount) { + env e; + uint256 fromBalanceBefore = currentContract.balanceOf(e, from); + uint256 toBalanceBefore = currentContract.balanceOf(e, to); + uint256 allowanceBefore = allowance(from, e.msg.sender); + // avoid overflows + require fromBalanceBefore + toBalanceBefore <= max_uint128; + + bool success = transferFrom(e, from, to, amount); + + assert (success && from != to) => + currentContract.balanceOf(e, from) == assert_uint256(fromBalanceBefore - amount) && + currentContract.balanceOf(e, to) == assert_uint256(toBalanceBefore + amount) && + allowance(from, e.msg.sender) == assert_uint256(allowanceBefore - amount); +} + +/* + @Description: + transferFrom should revert if and only if the amount is too high or the recipient is 0 or transfer is not enabled (if the was not made by the controller) or if the blocknumber is not valid. + + @Notes: + Fails on tokens with pause/blacklist functions, like USDC. +*/ +rule transferFromReverts(address from, address to, uint256 amount) { + env e; + uint256 allowanceBefore = allowance(from, e.msg.sender); + uint256 fromBalanceBefore = currentContract.balanceOf(e, from); + address controllerAddress = controller(); + requireInvariant allFromBlockAreGreaterThanParentSnapShotBlock(e.msg.sender, 0); + require from != 0 && e.msg.sender != 0; + require e.msg.value == 0; + // avoid overflows + require fromBalanceBefore + currentContract.balanceOf(e, to) <= max_uint128; + bool transfersEnabled = transfersEnabled(); + + transferFrom@withrevert(e, from, to, amount); + + bool didRevert = lastReverted; + + assert didRevert <=> + (allowanceBefore < amount && e.msg.sender != controllerAddress || amount > fromBalanceBefore || to == 0 && amount != 0 || to == currentContract && amount != 0 || !transfersEnabled && e.msg.sender != controllerAddress || parentSnapShotBlock() >= e.block.number && amount != 0); // && e.msg.sender != controllerAdress; +} + +/* + @Description: + Contract calls don't change token total supply. + + @Notes: + This rule should fail for any token that has functions that change totalSupply(), like mint() and burn(). + It's still important to run the rule and see if it fails in functions that _aren't_ supposed to modify totalSupply() +*/ +rule NoChangeTotalSupply(method f) { + env eTotalSupply; + env e; + calldataarg args; + require doesntChangeBalance(f); + uint256 totalSupplyBefore = currentContract.totalSupply(eTotalSupply); + f(e, args); + assert currentContract.totalSupply(eTotalSupply) == totalSupplyBefore; +} + +/* + @Description: + Test that generateTokens works correctly. Balances and totalSupply are updated corrct according to the paramenters. +*/ +rule integrityOfGenerateTokens(address owner, uint amount) { + env e; + requireInvariant checkPointBlockNumberValidity(e); + mathint totalSupplyBefore = currentContract.totalSupply(e); + mathint ownerBalanceBefore = currentContract.balanceOf(e, owner); + + // avoid overflows + require totalSupplyBefore + amount < max_uint128; + require ownerBalanceBefore + amount < max_uint128; + + bool success = generateTokens(e, owner, amount); + + mathint totalSupplyAfter = currentContract.totalSupply(e); + mathint ownerBalanceAfter = currentContract.balanceOf(e, owner); + + assert success => (totalSupplyAfter == totalSupplyBefore + amount && ownerBalanceAfter == ownerBalanceBefore + amount); + assert !success => (totalSupplyAfter == totalSupplyBefore && ownerBalanceAfter == ownerBalanceBefore); +} + +/* + @Description: + Test that destroyTokens works correctly. Balances and totalSupply are updated corrct according to the paramenters. +*/ +rule integrityOfDestroyTokens(address owner, uint amount) { + env e; + requireInvariant checkPointBlockNumberValidity(e); + mathint totalSupplyBefore = currentContract.totalSupply(e); + mathint ownerBalanceBefore = currentContract.balanceOf(e, owner); + + bool success = destroyTokens(e, owner, amount); + + mathint totalSupplyAfter = currentContract.totalSupply(e); + mathint ownerBalanceAfter = currentContract.balanceOf(e, owner); + + assert success => (totalSupplyAfter == totalSupplyBefore - amount && ownerBalanceAfter == ownerBalanceBefore - amount); + assert !success => (totalSupplyAfter == totalSupplyBefore && ownerBalanceAfter == ownerBalanceBefore); +} + +/* + @Description: + Transfer from a to b using transfer doesn't change the balance of other addresses +*/ +rule TransferDoesntChangeOtherBalances(address other, address bob, uint256 amount) { + env e; + require bob != e.msg.sender; + require bob != other && e.msg.sender != other; + requireInvariant checkPointBlockNumberValidity(e); + + mathint balanceBeforeOther = currentContract.balanceOf(e, other); + + bool success = transfer(e, bob, amount); + + assert balanceBeforeOther == to_mathint(currentContract.balanceOf(e, other)); +} + +/* + @Description: + Transfer from a to b using transferFrom doesn't change the balance of other addresses +*/ +rule TransferFromDoesntChangeOtherBalances(address other, address alice, address bob, uint256 amount) { + env e; + require bob != alice; + require bob != other && e.msg.sender != other && other != alice; + requireInvariant checkPointBlockNumberValidity(e); + + mathint balanceBeforeOther = currentContract.balanceOf(e, other); + + bool success = transferFrom(e, alice, bob, amount); + + assert balanceBeforeOther == to_mathint(currentContract.balanceOf(e, other)); +} + + +/* + @Description: + Allowance changes correctly as a result of calls to approve, transfer, increaseAllowance, decreaseAllowance + + + @Notes: + Some ERC20 tokens have functions like permit() that change allowance via a signature. + The rule will fail on such functions. +*/ +rule ChangingAllowance(method f, address from, address spender) { + uint256 allowanceBefore = allowance(from, spender); + env e; + if (f.selector == sig:approve(address, uint256).selector) { + address spender_; + uint256 amount; + approve(e, spender_, amount); + if (from == e.msg.sender && spender == spender_) { + assert allowance(from, spender) == amount; + } else { + assert allowance(from, spender) == allowanceBefore; + } + } else if (f.selector == sig:transferFrom(address,address,uint256).selector) { + address from_; + address to; + uint256 amount; + transferFrom(e, from_, to, amount); + mathint allowanceAfter = allowance(from, spender); + if (from == from_ && spender == e.msg.sender) { + assert from == to || allowanceBefore == max_uint256 || allowanceAfter == allowanceBefore - amount; + } else { + assert allowance(from, spender) == allowanceBefore; + } + } else if (f.selector == sig:permit(address, address, uint256, uint256, uint8, bytes32, bytes32).selector) { + address owner; + address spender_; + uint256 value; + uint256 deadline; + uint8 v; + bytes32 r; + bytes32 s; + permit(e, owner, spender_, value, deadline, v, r, s); + if (from == owner && spender == spender_) { + assert allowance(from, spender) == value; + } else { + assert allowance(from, spender) == allowanceBefore; + } + } else if (f.selector == sig:approveAndCall(address, uint256, bytes).selector) { + address spender_; + uint256 amount_; + bytes extraData_; + approveAndCall(e, spender_, amount_, extraData_); + if (from == e.msg.sender && spender == spender_) { + assert allowance(from, spender) == amount_; + } else { + assert allowance(from, spender) == allowanceBefore; + } + } else + { + calldataarg args; + f(e, args); + assert allowance(from, spender) == allowanceBefore; + } +} diff --git a/package.json b/package.json index 1ec4894..4f9404d 100644 --- a/package.json +++ b/package.json @@ -24,6 +24,7 @@ "gas-report": "forge test --gas-report 2>&1 | (tee /dev/tty | awk '/Test result:/ {found=1; buffer=\"\"; next} found && !/Ran/ {buffer=buffer $0 ORS} /Ran/ {found=0} END {printf \"%s\", buffer}' > .gas-report)", "clean": "rm -rf cache out", "lint": "pnpm lint:sol && pnpm prettier:check", + "verify": "touch certora/MiniMeBase.patch && cd certora && make munged && cd ../ && sh certora/scripts/MiniMeToken.sh", "lint:sol": "forge fmt --check && pnpm solhint {script,src,test}/**/*.sol", "prettier:check": "prettier --check **/*.{json,md,yml} --ignore-path=.prettierignore", "prettier:write": "prettier --write **/*.{json,md,yml} --ignore-path=.prettierignore"