mirror of https://github.com/vacp2p/minime.git
feat: add certora specs and audit
This commit is contained in:
parent
6d9d4f5487
commit
1f6820c245
|
@ -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`?
|
||||
|
|
|
@ -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
|
||||
|
|
|
@ -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/*
|
||||
|
|
|
@ -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)
|
|
@ -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;
|
Binary file not shown.
|
@ -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;
|
||||
}
|
||||
}
|
|
@ -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;
|
||||
}
|
||||
}
|
|
@ -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;
|
||||
}
|
||||
}
|
|
@ -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;
|
||||
}
|
||||
}
|
|
@ -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"
|
|
@ -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;
|
||||
}
|
||||
}
|
|
@ -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"
|
||||
|
|
Loading…
Reference in New Issue