Add certora rules and workflow verification step (m0-foundation#167)

.github/workflows/certora_verification.yml

@@ -0,0 +1,50 @@
+name: certora-verification
+
+on:
+  push:
+    branches:
+      - main
+  pull_request:
+    branches:
+      - main
+
+  workflow_dispatch:
+
+jobs:
+  verify:
+    runs-on: ubuntu-latest
+
+    steps:
+      - uses: actions/checkout@v2
+        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==7.0.7
+
+      - name: Install solc
+        run: |
+          wget https://github.com/ethereum/solidity/releases/download/v0.8.23/solc-static-linux
+          chmod +x solc-static-linux
+          sudo mv solc-static-linux /usr/local/bin/solc8.23
+      - name: Verify
+        run: |
+          certoraRun certora/confs/${{ matrix.contract }}
+        env:
+          CERTORAKEY: ${{ secrets.CERTORAKEY }}
+
+    strategy:
+      fail-fast: false
+      max-parallel: 16
+      matrix:
+        contract:
+          - MinterGateway.conf
+          - ContinuousIndexingMath.conf

.gitignore

@@ -23,3 +23,7 @@ node_modules/
 
 results.sarif
 yarn-error.log
+
+# Certora verification:
+.certora_internal
+certora/munged/*

certora/confs/ContinuousIndexingMath.conf

@@ -0,0 +1,12 @@
+{
+    "files": [
+        "test/utils/ContinuousIndexingMathHarness.sol"
+    ],
+    "solc": "solc8.23",
+    "msg": "ContinuousIndexingMath Equivalence",
+    "smt_timeout": "1000",
+    "loop_iter":"2",
+    "verify": 
+        "ContinuousIndexingMathHarness:certora/specs/ContinuousMathEquivalence.spec",
+    "server": "production",
+}

certora/confs/MinterGateway-r01-only.conf

@@ -0,0 +1,33 @@
+{
+    "files": [
+        "certora/harness/MinterGatewayHarness.sol",
+        "certora/harness/MTokenHarness.sol",
+        "certora/mocks/MockTTGRegistrar.sol"
+    ],
+    "link" : [
+        "MinterGatewayHarness:mToken=MTokenHarness",
+        "MinterGatewayHarness:ttgRegistrar=MockTTGRegistrar",
+        "MTokenHarness:ttgRegistrar=MockTTGRegistrar",
+        "MTokenHarness:minterGateway=MinterGatewayHarness"
+    ],
+    "parametric_contracts": [ "MinterGatewayHarness"],
+    "assert_autofinder_success": true,
+    "solc": "solc8.23",
+    "smt_timeout": "2000",
+    "optimistic_loop": true,
+    "optimistic_summary_recursion": true,
+    "summary_recursion_limit" : "1",
+    "loop_iter":"2",
+    "optimistic_hashing": true,
+    "rule" : [
+        "r01_totalOwedMExceedsTotalMSupply",
+    ],
+    "prover_args":[
+        "-mediumTimeout 90",
+        "-depth 3",
+    ],
+    "java_args": ['"-ea -Dlevel.setup.helpers=info"'],
+    "verify":"MinterGatewayHarness:certora/specs/MinterGateway-r01-only.spec",
+    "server": "production",
+    "msg": "MinterGateway-r01-only",
+}

certora/confs/MinterGateway.conf

@@ -0,0 +1,30 @@
+{
+    "files": [
+        "certora/harness/MinterGatewayHarness.sol",
+        "certora/harness/MTokenHarness.sol",
+        "certora/mocks/MockTTGRegistrar.sol"
+    ],
+    "link" : [
+        "MinterGatewayHarness:mToken=MTokenHarness",
+        "MinterGatewayHarness:ttgRegistrar=MockTTGRegistrar",
+        "MTokenHarness:ttgRegistrar=MockTTGRegistrar",
+        "MTokenHarness:minterGateway=MinterGatewayHarness"
+    ],
+    "parametric_contracts": [ "MinterGatewayHarness"],
+    "assert_autofinder_success": true,
+    "solc": "solc8.23",
+    "smt_timeout": "2000",
+    "optimistic_loop": true,
+    "optimistic_summary_recursion": true,
+    "summary_recursion_limit" : "1",
+    "loop_iter":"2",
+    "optimistic_hashing": true,
+    "prover_args":[
+        "-mediumTimeout 90",
+        "-depth 3",
+    ],
+    "java_args": ['"-ea -Dlevel.setup.helpers=info"'],
+    "verify":"MinterGatewayHarness:certora/specs/MinterGateway.spec",
+    "server": "production",
+    "msg": "MinterGateway",
+}

certora/harness/MTokenHarness.sol

@@ -0,0 +1,39 @@
+// SPDX-License-Identifier: GPL-3.0
+
+pragma solidity 0.8.23;
+import "../../src/MToken.sol";
+
+
+contract MTokenHarness is MToken {
+
+    constructor(address ttgRegistrar_, address minterGateway_) MToken(ttgRegistrar_, minterGateway_) {}
+
+    /******************************************************************************************************************\
+    |                                                     Getters                                                      |
+    \******************************************************************************************************************/
+
+
+    function getLatestIndexInMToken() public view returns (uint128) {
+        return latestIndex;
+    }
+
+    function getLatestRateInMToken() public view returns (uint32) {
+        return _latestRate;
+    }
+
+    function getLatestUpdateTimestampInMToken() public view returns (uint40) {
+        return latestUpdateTimestamp;
+    }
+
+    function getIsEarning(address account_) public view returns (bool) {
+        return _balances[account_].isEarning;
+    }
+
+    function getInternalBalanceOf(address account_) public view returns (uint240) {
+        return _balances[account_].rawBalance;
+    }
+
+    function getEarnerRate() public view returns (uint32) {
+        return _rate();
+    }
+}

certora/harness/MinterGatewayHarness.sol

@@ -0,0 +1,46 @@
+// SPDX-License-Identifier: GPL-3.0
+
+pragma solidity 0.8.23;
+import "../../src/MinterGateway.sol";
+
+contract MinterGatewayHarness is MinterGateway {
+    constructor(address ttgRegistrar_, address mToken_) MinterGateway(ttgRegistrar_, mToken_) {}
+
+    function totalMSupply() public view returns (uint240) {
+        // Note this is also used to determine the total M supply in
+        // functions implemented in MinterGatway
+        return uint240(IMToken(mToken).totalSupply()); 
+    }
+
+    /******************************************************************************************************************\
+    |                                                     Getters                                                      |
+    \******************************************************************************************************************/
+
+    function getLatestIndexInMinterGateway() public view returns (uint128) {
+        return latestIndex;
+    }
+
+    function getLatestRateInMinterGateway() public view returns (uint32) {
+        return _latestRate;
+    }
+
+    function getLatestUpdateTimestampInMinterGateway() public view returns (uint40) {
+        return latestUpdateTimestamp;
+    }
+
+    function getPrincipalAmountRoundedDown(uint240 amount_) public view returns (uint112 principalAmount_) {
+        return _getPrincipalAmountRoundedDown(amount_);
+    }
+
+    function getPrincipalAmountRoundedUp(uint240 amount_) public view returns (uint112 principalAmount_) {
+        return _getPrincipalAmountRoundedUp(amount_);
+    }
+
+    function getMinterRate() public view returns (uint32) {
+        return _rate();
+    }
+
+    function getPresentAmount(uint112 principalAmount_) public view returns (uint240) {
+        return _getPresentAmount(principalAmount_);
+    }
+}

certora/mocks/MockTTGRegistrar.sol

@@ -0,0 +1,48 @@
+// SPDX-License-Identifier: UNLICENSED
+
+pragma solidity 0.8.23;
+
+import { ITTGRegistrar } from "../../src/interfaces/ITTGRegistrar.sol";
+
+contract MockTTGRegistrar is ITTGRegistrar {
+    address internal _vault;
+
+    mapping(bytes32 list => mapping(address account => bool isInList)) internal _isInList;
+    mapping(bytes32 key => bytes32 value) internal _values;
+
+    function addToList(bytes32 list_, address account_) external {
+        _isInList[list_][account_] = true;
+    }
+
+    function removeFromList(bytes32 list_, address account_) external {
+        _isInList[list_][account_] = false;
+    }
+
+    function get(bytes32 key_) external view returns (bytes32) {
+        return _values[key_];
+    }
+
+    function listContains(bytes32 list_, address account_) external view returns (bool) {
+        return _isInList[list_][account_];
+    }
+
+    function setVault(address vault_) external {
+        _vault = vault_;
+    }
+
+    function updateConfig(bytes32 key_, address value_) external {
+        _values[key_] = bytes32(uint256(uint160(value_)));
+    }
+
+    function updateConfig(bytes32 key_, uint256 value_) external {
+        _values[key_] = bytes32(value_);
+    }
+
+    function updateConfig(bytes32 key_, bytes32 value_) external {
+        _values[key_] = value_;
+    }
+
+    function vault() external view returns (address) {
+        return _vault;
+    }
+}

certora/specs/ContinuousMathCVL.spec

@@ -0,0 +1,39 @@
+definition EXP_SCALED_ONE() returns uint56 = 10^12;
+definition EXP_SCALED_ONE_48() returns uint48 = 10^12;
+
+function mulDivDownCVL(uint256 x, uint256 y, uint256 z) returns uint256 {
+    uint256 res;
+    require z != 0;
+    mathint xy = x * y;
+    mathint fz = res * z;
+
+    require xy >= fz;
+    require fz + z > xy;
+    return res; 
+}
+
+function divideDownCVL(uint240 x, uint128 index) returns uint112 {
+	return require_uint112(
+		mulDivDownCVL(assert_uint256(x) , assert_uint256(EXP_SCALED_ONE()), assert_uint256(index))
+	);
+}
+
+function divideUpCVL(uint240 x, uint128 index) returns uint112 {
+	uint256 temp = require_uint256(EXP_SCALED_ONE() * x + index - 1);
+	return require_uint112(
+		mulDivDownCVL(temp , 1, assert_uint256(index))
+	);
+}
+
+function multiplyDownCVL(uint112 x, uint128 index) returns uint240 {
+	return assert_uint240(
+		mulDivDownCVL(assert_uint256(x), assert_uint256(index), assert_uint256(EXP_SCALED_ONE()))
+	);
+}
+
+function multiplyUpCVL(uint112 x, uint128 index) returns uint240 {
+	uint256 temp = require_uint256(index * x + EXP_SCALED_ONE() - 1);
+	return assert_uint240(
+		mulDivDownCVL(temp, 1, assert_uint256(EXP_SCALED_ONE()))
+	);
+}

certora/specs/ContinuousMathEquivalence.spec

@@ -0,0 +1,26 @@
+import "ContinuousMathCVL.spec";
+
+using ContinuousIndexingMathHarness as harness;
+
+methods {
+    function harness.divideDown(uint240 x, uint128 index) external returns (uint112) envfree;
+	function harness.divideUp(uint240 x, uint128 index) external returns (uint112) envfree;
+	function harness.multiplyDown(uint112 x, uint128 index) external returns (uint240) envfree;
+	function harness.multiplyUp(uint112 x, uint128 index) external returns (uint240) envfree;
+}
+
+rule divideDown_equivalence(uint240 x, uint128 index) {
+    assert harness.divideDown(x, index) == divideDownCVL(x, index);
+}
+
+rule divideUp_equivalence(uint240 x, uint128 index) {
+    assert harness.divideUp(x, index) == divideUpCVL(x, index);
+}
+
+rule multiplyDown_equivalence(uint112 x, uint128 index) {
+    assert harness.multiplyDown(x, index) == multiplyDownCVL(x, index);
+}
+
+rule multiplyUp_equivalence(uint112 x, uint128 index) {
+    assert harness.multiplyUp(x, index) == multiplyUpCVL(x, index);
+}