feat: add certora specs and audit

.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`?

.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

.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/*

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)

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;

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;
+    }
+}

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;
+    }
+}

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;
+    }
+}

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;
+    }
+}

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"