mirror of https://github.com/vacp2p/minime.git
feat: add certora specs and audit
This commit is contained in:
parent
6d9d4f5487
commit
7c12587c67
|
@ -10,3 +10,4 @@ Ensure you completed **all of the steps** below before submitting your pull requ
|
||||||
- [ ] Ran `forge snapshot`?
|
- [ ] Ran `forge snapshot`?
|
||||||
- [ ] Ran `pnpm lint`?
|
- [ ] Ran `pnpm lint`?
|
||||||
- [ ] Ran `pnpm gas-report`?
|
- [ ] Ran `pnpm gas-report`?
|
||||||
|
- [ ] Ran `pnpm verify`?
|
||||||
|
|
|
@ -10,6 +10,7 @@ on:
|
||||||
push:
|
push:
|
||||||
branches:
|
branches:
|
||||||
- "main"
|
- "main"
|
||||||
|
- "master"
|
||||||
|
|
||||||
jobs:
|
jobs:
|
||||||
lint:
|
lint:
|
||||||
|
@ -117,3 +118,51 @@ jobs:
|
||||||
run: |
|
run: |
|
||||||
echo "## Coverage result" >> $GITHUB_STEP_SUMMARY
|
echo "## Coverage result" >> $GITHUB_STEP_SUMMARY
|
||||||
echo "✅ Uploaded to Codecov" >> $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/*
|
broadcast/*
|
||||||
broadcast/*/31337/
|
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)",
|
"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",
|
"clean": "rm -rf cache out",
|
||||||
"lint": "pnpm lint:sol && pnpm prettier:check",
|
"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",
|
"lint:sol": "forge fmt --check && pnpm solhint {script,src,test}/**/*.sol",
|
||||||
"prettier:check": "prettier --check **/*.{json,md,yml} --ignore-path=.prettierignore",
|
"prettier:check": "prettier --check **/*.{json,md,yml} --ignore-path=.prettierignore",
|
||||||
"prettier:write": "prettier --write **/*.{json,md,yml} --ignore-path=.prettierignore"
|
"prettier:write": "prettier --write **/*.{json,md,yml} --ignore-path=.prettierignore"
|
||||||
|
|
Loading…
Reference in New Issue