From 9f2b32002c3367164a4fd634a274e1771e366de4 Mon Sep 17 00:00:00 2001 From: toninorair Date: Mon, 15 Apr 2024 15:58:57 -0400 Subject: [PATCH] Add certora rules and workflow verification step (#167) --- .github/workflows/certora_verification.yml | 50 +++ .gitignore | 4 + certora/confs/ContinuousIndexingMath.conf | 12 + certora/confs/MinterGateway-r01-only.conf | 33 ++ certora/confs/MinterGateway.conf | 30 ++ certora/harness/MTokenHarness.sol | 39 +++ certora/harness/MinterGatewayHarness.sol | 46 +++ certora/mocks/MockTTGRegistrar.sol | 48 +++ certora/specs/ContinuousMathCVL.spec | 39 +++ certora/specs/ContinuousMathEquivalence.spec | 26 ++ certora/specs/MToken_hooks.spec | 103 +++++++ certora/specs/MinterGateway-r01-only.spec | 127 ++++++++ certora/specs/MinterGateway.spec | 307 +++++++++++++++++++ certora/specs/MinterGateway_hooks.spec | 76 +++++ certora/specs/setup.spec | 79 +++++ 15 files changed, 1019 insertions(+) create mode 100644 .github/workflows/certora_verification.yml create mode 100644 certora/confs/ContinuousIndexingMath.conf create mode 100644 certora/confs/MinterGateway-r01-only.conf create mode 100644 certora/confs/MinterGateway.conf create mode 100644 certora/harness/MTokenHarness.sol create mode 100644 certora/harness/MinterGatewayHarness.sol create mode 100644 certora/mocks/MockTTGRegistrar.sol create mode 100644 certora/specs/ContinuousMathCVL.spec create mode 100644 certora/specs/ContinuousMathEquivalence.spec create mode 100644 certora/specs/MToken_hooks.spec create mode 100644 certora/specs/MinterGateway-r01-only.spec create mode 100644 certora/specs/MinterGateway.spec create mode 100644 certora/specs/MinterGateway_hooks.spec create mode 100644 certora/specs/setup.spec diff --git a/.github/workflows/certora_verification.yml b/.github/workflows/certora_verification.yml new file mode 100644 index 00000000..223738c4 --- /dev/null +++ b/.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 diff --git a/.gitignore b/.gitignore index f8ac9105..8ac5bb9d 100644 --- a/.gitignore +++ b/.gitignore @@ -23,3 +23,7 @@ node_modules/ results.sarif yarn-error.log + +# Certora verification: +.certora_internal +certora/munged/* diff --git a/certora/confs/ContinuousIndexingMath.conf b/certora/confs/ContinuousIndexingMath.conf new file mode 100644 index 00000000..d023a342 --- /dev/null +++ b/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", +} diff --git a/certora/confs/MinterGateway-r01-only.conf b/certora/confs/MinterGateway-r01-only.conf new file mode 100644 index 00000000..99d321ac --- /dev/null +++ b/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", +} diff --git a/certora/confs/MinterGateway.conf b/certora/confs/MinterGateway.conf new file mode 100644 index 00000000..2a7a3032 --- /dev/null +++ b/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", +} diff --git a/certora/harness/MTokenHarness.sol b/certora/harness/MTokenHarness.sol new file mode 100644 index 00000000..1c2bd535 --- /dev/null +++ b/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(); + } +} diff --git a/certora/harness/MinterGatewayHarness.sol b/certora/harness/MinterGatewayHarness.sol new file mode 100644 index 00000000..ebe0d072 --- /dev/null +++ b/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_); + } +} diff --git a/certora/mocks/MockTTGRegistrar.sol b/certora/mocks/MockTTGRegistrar.sol new file mode 100644 index 00000000..dc4bcd2f --- /dev/null +++ b/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; + } +} diff --git a/certora/specs/ContinuousMathCVL.spec b/certora/specs/ContinuousMathCVL.spec new file mode 100644 index 00000000..815c775f --- /dev/null +++ b/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())) + ); +} diff --git a/certora/specs/ContinuousMathEquivalence.spec b/certora/specs/ContinuousMathEquivalence.spec new file mode 100644 index 00000000..b26dd24a --- /dev/null +++ b/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); +} diff --git a/certora/specs/MToken_hooks.spec b/certora/specs/MToken_hooks.spec new file mode 100644 index 00000000..2285ee9e --- /dev/null +++ b/certora/specs/MToken_hooks.spec @@ -0,0 +1,103 @@ +import "setup.spec"; + +using MTokenHarness as MToken; + +/// True sum of balances. +ghost mathint sumOfBalancesMToken { init_state axiom sumOfBalancesMToken == 0; } +ghost mathint sumOfActiveBalancesMToken { init_state axiom sumOfActiveBalancesMToken == 0; } +ghost mathint sumOfInactiveBalancesMToken { init_state axiom sumOfInactiveBalancesMToken == 0; } + +/// The initial value is being updated as we access the acounts balances one-by-one. +/// Should only be used as an initial value, never post-action! +ghost mathint sumOfBalancesMToken_init { init_state axiom sumOfBalancesMToken_init == 0; } +ghost mathint sumOfActiveBalancesMToken_init { init_state axiom sumOfActiveBalancesMToken_init == 0; } +ghost mathint sumOfInactiveBalancesMToken_init { init_state axiom sumOfInactiveBalancesMToken_init == 0; } + +ghost mapping(address => bool) g_rawBalanceAccessed; // for each address checks if the rawBalance was ever read +ghost mapping(address => bool) g_isEarning; // for each address account - offset 0 +ghost mapping(address => uint240) g_rawBalance; // for each address account - offset 8 + +hook Sstore MToken._balances[KEY address k].isEarning bool isEarning (bool wasEarning) { + g_isEarning[k] = isEarning; + uint240 balance = MToken._balances[k].rawBalance; + if(isEarning && !wasEarning) { + sumOfActiveBalancesMToken = sumOfActiveBalancesMToken + balance; + sumOfInactiveBalancesMToken = sumOfInactiveBalancesMToken - balance; + } + else if(!isEarning && wasEarning) { + sumOfActiveBalancesMToken = sumOfActiveBalancesMToken - balance; + sumOfInactiveBalancesMToken = sumOfInactiveBalancesMToken + balance; + } +} + +hook Sload bool isEarning MToken._balances[KEY address k].isEarning { + require g_isEarning[k] == isEarning; +} + +hook Sstore MToken._balances[KEY address k].rawBalance uint240 rawBalance (uint240 rawBalance_old) { + g_rawBalance[k] = rawBalance; + // require rawBalance <= UINT112_MAX(); // ensure we don't overflow + if (!g_rawBalanceAccessed[k] && g_isEarning[k]) { + require rawBalance <= UINT112_MAX(); // earning + g_rawBalanceAccessed[k] = true; + + sumOfBalancesMToken_init = sumOfBalancesMToken_init - rawBalance_old; + require sumOfBalancesMToken_init >= 0; + + sumOfActiveBalancesMToken_init = sumOfActiveBalancesMToken_init - rawBalance_old; + require sumOfActiveBalancesMToken_init >= 0; + } else if (!g_rawBalanceAccessed[k] && !g_isEarning[k]) { + require rawBalance <= UINT112x128_MAX(); // non earning + g_rawBalanceAccessed[k] = true; + + sumOfBalancesMToken_init = sumOfBalancesMToken_init - rawBalance_old; + require sumOfBalancesMToken_init >= 0; + + sumOfInactiveBalancesMToken_init = sumOfInactiveBalancesMToken_init - rawBalance_old; + require sumOfInactiveBalancesMToken_init >= 0; + } + sumOfBalancesMToken = sumOfBalancesMToken + rawBalance - rawBalance_old; + + if (g_isEarning[k]) { + sumOfActiveBalancesMToken = sumOfActiveBalancesMToken + rawBalance - rawBalance_old; + } else { + sumOfInactiveBalancesMToken = sumOfInactiveBalancesMToken + rawBalance - rawBalance_old; + } +} + +hook Sload uint240 rawBalance MToken._balances[KEY address k].rawBalance { + require g_rawBalance[k] == rawBalance; + if (!g_rawBalanceAccessed[k] && g_isEarning[k]) { + require rawBalance <= UINT112_MAX(); // earning + g_rawBalanceAccessed[k] = true; + + sumOfBalancesMToken_init = sumOfBalancesMToken_init - rawBalance; + require sumOfBalancesMToken_init >= 0; + + sumOfActiveBalancesMToken_init = sumOfActiveBalancesMToken_init - rawBalance; + require sumOfActiveBalancesMToken_init >= 0; + } else if (!g_rawBalanceAccessed[k] && !g_isEarning[k]) { + require rawBalance <= UINT112x128_MAX(); // non earning + g_rawBalanceAccessed[k] = true; + + sumOfBalancesMToken_init = sumOfBalancesMToken_init - rawBalance; + require sumOfBalancesMToken_init >= 0; + + sumOfInactiveBalancesMToken_init = sumOfInactiveBalancesMToken_init - rawBalance; + require sumOfInactiveBalancesMToken_init >= 0; + } + // require rawBalance <= UINT112_MAX(); // ensure we don't overflow +} + +function SumTrackingSetup_MToken(env e) { + require sumOfBalancesMToken == sumOfBalancesMToken_init; + require sumOfActiveBalancesMToken == sumOfActiveBalancesMToken_init; + require sumOfInactiveBalancesMToken == sumOfInactiveBalancesMToken_init; + setAllRawBalanceAccessedToFalse(); +} + +function setAllRawBalanceAccessedToFalse() { + require forall address a. !g_rawBalanceAccessed[a]; + //havoc g_rawBalanceAccessed assuming + // forall address a. !g_rawBalanceAccessed@new[a]; +} diff --git a/certora/specs/MinterGateway-r01-only.spec b/certora/specs/MinterGateway-r01-only.spec new file mode 100644 index 00000000..6842a3d5 --- /dev/null +++ b/certora/specs/MinterGateway-r01-only.spec @@ -0,0 +1,127 @@ +import "./ContinuousMathCVL.spec"; +import "./MinterGateway_hooks.spec"; +import "./MToken_hooks.spec"; + +using MockTTGRegistrar as MockTTGRegistrarContract; + +function SumTrackingSetup(env e) { + SumTrackingSetup_MToken(e); + SumTrackingSetup_Minter(e); +} + +/// @title The sum of active/inactive balances equals to the respective total (in minterGateway) +invariant SumOfBalancesEqualsTotalSupply() + sumOfInactiveBalances == to_mathint(minterGateway.totalInactiveOwedM) + && + sumOfActiveBalances == to_mathint(minterGateway.principalOfTotalActiveOwedM) + && + sumOfActiveBalances <= to_mathint(UINT112_MAX()) + { + preserved with(env e) { + setLegalInitialState(e); + SumTrackingSetup(e); + requireInvariant SumOfBalancesEqualsTotalSupplyMToken(); + } + preserved deactivateMinter(address minter) with (env e) { + setLegalInitialState(e); + SumTrackingSetup(e); + require minterGateway.getPresentAmount(e, max_uint112) + minterGateway.totalInactiveOwedM(e) < max_uint240; + requireInvariant SumOfBalancesEqualsTotalSupplyMToken(); + } + preserved activateMinter(address minter) with (env e) { + /// Need to be proven: + require minterGateway._rawOwedM[minter] == 0; // passes + setLegalInitialState(e); + SumTrackingSetup(e); + requireInvariant SumOfBalancesEqualsTotalSupplyMToken(); + } + } + +/// @title The sum of active/inactive balances equals to the respective total (in MToken) +invariant SumOfBalancesEqualsTotalSupplyMToken() + sumOfInactiveBalancesMToken == to_mathint(MToken.totalNonEarningSupply) + && + sumOfActiveBalancesMToken == to_mathint(MToken.principalOfTotalEarningSupply) + { + preserved with(env e) { + setLegalInitialState(e); + SumTrackingSetup(e); + requireInvariant SumOfBalancesEqualsTotalSupply(); + } + } + +function LatestTimesAreSynched(env e) returns bool { + return + MToken.getLatestUpdateTimestampInMToken(e) == + minterGateway.getLatestUpdateTimestampInMinterGateway(e); +} + +function LatestIndexAndRatesAreSynched(env e) returns bool { + uint128 currentIndex_token = MToken.currentIndex(e); + uint128 latestIndex_token = MToken.getLatestIndexInMToken(e); + uint32 currentRate_token = MToken.getEarnerRate(e); + uint32 latestRate_token = MToken.getLatestRateInMToken(e); + uint256 latestTimestamp_token = assert_uint256(MToken.getLatestUpdateTimestampInMToken(e)); + + uint128 currentIndex_minter = minterGateway.currentIndex(e); + uint128 latestIndex_minter= minterGateway.getLatestIndexInMinterGateway(e); + uint32 currentRate_minter = minterGateway.getMinterRate(e); + uint32 latestRate_minter = minterGateway.getLatestRateInMinterGateway(e); + uint256 latestTimestamp_minter = minterGateway.getLatestUpdateTimestampInMinterGateway(e); + + return ( + latestTimestamp_token == e.block.timestamp => + (currentIndex_token == latestIndex_token && currentRate_token == latestRate_token) + ) + && + ( + latestTimestamp_minter == e.block.timestamp => + (currentIndex_minter == latestIndex_minter && currentRate_minter == latestRate_minter) + ); +} + +function setLegalInitialState(env e) { + require ValidTimestamp(e); + require LatestTimesAreSynched(e); + require LatestIndexAndRatesAreSynched(e); + require MToken.getLatestRateInMToken(e) < 40000; // up to 400% + require minterGateway.getLatestRateInMinterGateway(e) < 40000; // up to 400% + require MToken.getLatestIndexInMToken(e) >= assert_uint128(EXP_SCALED_ONE()); + require minterGateway.getLatestIndexInMinterGateway(e) >= assert_uint128(EXP_SCALED_ONE()); + + address vault; + require minterGateway.ttgVault(e) == vault; + require vault != 0 && vault != minterGateway && vault != MToken && vault != MockTTGRegistrarContract; + + bool vaultIsEarning = MToken.getIsEarning(e,vault); + require !vaultIsEarning; // vault cannot be earning +} + +/// @title MZero Protocol Property 1: totalOwedM >= totalMSupply +/// This property is mentioned in the MZero protocol engineering spec doc +rule r01_totalOwedMExceedsTotalMSupply(method f) filtered { + f -> !f.isView // view functions are not interesting to verify since they obviously cannot violate this property +}{ + env e; calldataarg args; + setLegalInitialState(e); + SumTrackingSetup(e); + + requireInvariant SumOfBalancesEqualsTotalSupplyMToken(); + requireInvariant SumOfBalancesEqualsTotalSupply(); + require minterGateway.getPresentAmount(e, max_uint112) + minterGateway.totalInactiveOwedM(e) < max_uint240; // assume no overflow of totalOwedM + + require minterGateway.totalOwedM(e) >= minterGateway.totalActiveOwedM(e); // assume no overflow + require minterGateway.totalOwedM(e) >= minterGateway.totalInactiveOwedM; // assume no overflow + + require MToken.totalSupply(e) >= assert_uint256(MToken.totalEarningSupply(e)); // assume no overflow + require MToken.totalSupply(e) >= assert_uint256(MToken.totalNonEarningSupply(e)); // assume no overflow + + require minterGateway.excessOwedM(e) + MToken.totalSupply(e) < max_uint240; // assume no overflow + + uint240 totalOwedMBefore = minterGateway.totalOwedM(e); + uint240 totalMSupplyBefore = minterGateway.totalMSupply(e); + f(e, args); + uint240 totalOwedMAfter = minterGateway.totalOwedM(e); + uint240 totalMSupplyAfter = minterGateway.totalMSupply(e); + assert totalOwedMBefore >= totalMSupplyBefore => totalOwedMAfter >= totalMSupplyAfter; +} diff --git a/certora/specs/MinterGateway.spec b/certora/specs/MinterGateway.spec new file mode 100644 index 00000000..e62c5f94 --- /dev/null +++ b/certora/specs/MinterGateway.spec @@ -0,0 +1,307 @@ +import "./ContinuousMathCVL.spec"; +import "./MinterGateway_hooks.spec"; +import "./MToken_hooks.spec"; + +using MockTTGRegistrar as MockTTGRegistrarContract; + +function SumTrackingSetup(env e) { + SumTrackingSetup_MToken(e); + SumTrackingSetup_Minter(e); +} + +/// @title The sum of active/inactive balances equals to the respective total (in minterGateway) +invariant SumOfBalancesEqualsTotalSupply() + sumOfInactiveBalances == to_mathint(minterGateway.totalInactiveOwedM) + && + sumOfActiveBalances == to_mathint(minterGateway.principalOfTotalActiveOwedM) + && + sumOfActiveBalances <= to_mathint(UINT112_MAX()) + { + preserved with(env e) { + SumTrackingSetup(e); + setLegalInitialState(e); + requireInvariant SumOfBalancesEqualsTotalSupplyMToken(); + } + preserved deactivateMinter(address minter) with (env e) { + SumTrackingSetup(e); + setLegalInitialState(e); + require minterGateway.getPresentAmount(e, max_uint112) + minterGateway.totalInactiveOwedM(e) < max_uint240; + requireInvariant SumOfBalancesEqualsTotalSupplyMToken(); + } + preserved activateMinter(address minter) with (env e) { + /// Need to be proven: + require minterGateway._rawOwedM[minter] == 0; // passes + SumTrackingSetup(e); + setLegalInitialState(e); + requireInvariant SumOfBalancesEqualsTotalSupplyMToken(); + } + } + +/// @title The sum of active/inactive balances equals to the respective total (in MToken) +invariant SumOfBalancesEqualsTotalSupplyMToken() + sumOfInactiveBalancesMToken == to_mathint(MToken.totalNonEarningSupply) + && + sumOfActiveBalancesMToken == to_mathint(MToken.principalOfTotalEarningSupply) + { + preserved with(env e) { + SumTrackingSetup(e); + setLegalInitialState(e); + requireInvariant SumOfBalancesEqualsTotalSupply(); + } + } + +function LatestTimesAreSynched(env e) returns bool { + return + MToken.getLatestUpdateTimestampInMToken(e) == + minterGateway.getLatestUpdateTimestampInMinterGateway(e); +} + +function LatestIndexAndRatesAreSynched(env e) returns bool { + uint128 currentIndex_token = MToken.currentIndex(e); + uint128 latestIndex_token = MToken.getLatestIndexInMToken(e); + uint32 currentRate_token = MToken.getEarnerRate(e); + uint32 latestRate_token = MToken.getLatestRateInMToken(e); + uint256 latestTimestamp_token = assert_uint256(MToken.getLatestUpdateTimestampInMToken(e)); + + uint128 currentIndex_minter = minterGateway.currentIndex(e); + uint128 latestIndex_minter= minterGateway.getLatestIndexInMinterGateway(e); + uint32 currentRate_minter = minterGateway.getMinterRate(e); + uint32 latestRate_minter = minterGateway.getLatestRateInMinterGateway(e); + uint256 latestTimestamp_minter = minterGateway.getLatestUpdateTimestampInMinterGateway(e); + + return ( + latestTimestamp_token == e.block.timestamp => + (currentIndex_token == latestIndex_token && currentRate_token == latestRate_token) + ) + && + ( + latestTimestamp_minter == e.block.timestamp => + (currentIndex_minter == latestIndex_minter && currentRate_minter == latestRate_minter) + ); +} + +/// @title Latest times and indexes remain synced after executing any method of minterGateway +rule LatestTimesRemainSynched(method f, env e) filtered{f -> !f.isView && !f.isPure} { + setLegalInitialState(e); + require LatestTimesAreSynched(e); + require LatestIndexAndRatesAreSynched(e); + require MToken.getLatestUpdateTimestampInMToken(e) <= assert_uint40(e.block.timestamp); + env eP; + require eP.block.timestamp >= e.block.timestamp; + require ValidTimestamp(eP); + calldataarg args; + f(eP,args); + assert LatestTimesAreSynched(eP); + assert LatestIndexAndRatesAreSynched(eP); + assert MToken.getLatestUpdateTimestampInMToken(eP) <= assert_uint40(eP.block.timestamp); +} + +function setLegalInitialState(env e) { + require ValidTimestamp(e); + require LatestTimesAreSynched(e); + require LatestIndexAndRatesAreSynched(e); + require MToken.getLatestRateInMToken(e) < 40000; // up to 400% + require minterGateway.getLatestRateInMinterGateway(e) < 40000; // up to 400% + require MToken.getLatestIndexInMToken(e) >= assert_uint128(EXP_SCALED_ONE()); + require minterGateway.getLatestIndexInMinterGateway(e) >= assert_uint128(EXP_SCALED_ONE()); + + address vault; + require minterGateway.ttgVault(e) == vault; + require vault != 0 && vault != minterGateway && vault != MToken && vault != MockTTGRegistrarContract; + + bool vaultIsEarning = MToken.getIsEarning(e,vault); + require !vaultIsEarning; // vault cannot be earning +} + +/* we exported the next rule into a separate spec since it requires excessive computation +/// @title MZero Protocol Property 1: totalOwedM >= totalMSupply +/// This property is mentioned in the MZero protocol engineering spec doc +rule r01_totalOwedMExceedsTotalMSupply(method f) filtered { + f -> !f.isView // view functions are not interesting to verify since they obviously cannot violate this property +}{ + env e; calldataarg args; + SumTrackingSetup(e); + setLegalInitialState(e); + + requireInvariant SumOfBalancesEqualsTotalSupplyMToken(); + requireInvariant SumOfBalancesEqualsTotalSupply(); + require minterGateway.getPresentAmount(e, max_uint112) + minterGateway.totalInactiveOwedM(e) < max_uint240; // assume no overflow of totalOwedM + + require minterGateway.totalOwedM(e) >= minterGateway.totalActiveOwedM(e); // assume no overflow + require minterGateway.totalOwedM(e) >= minterGateway.totalInactiveOwedM; // assume no overflow + + require MToken.totalSupply(e) >= assert_uint256(MToken.totalEarningSupply(e)); // assume no overflow + require MToken.totalSupply(e) >= assert_uint256(MToken.totalNonEarningSupply(e)); // assume no overflow + + require minterGateway.excessOwedM(e) + MToken.totalSupply(e) < max_uint240; // assume no overflow + + uint240 totalOwedMBefore = minterGateway.totalOwedM(e); + uint240 totalMSupplyBefore = minterGateway.totalMSupply(e); + f(e, args); + uint240 totalOwedMAfter = minterGateway.totalOwedM(e); + uint240 totalMSupplyAfter = minterGateway.totalMSupply(e); + assert totalOwedMBefore >= totalMSupplyBefore => totalOwedMAfter >= totalMSupplyAfter; +} */ + +/// @title MZero Protocol Property 2: totalOwedM = totalActiveOwedM + totalInactiveOwedM +/// This property is mentioned in the MZero protocol engineering spec doc +rule r02_totalOwedMCorrectness { + env e; + // There is an assumption in the solidity code about why + // a potential unchecked overflow is not possible. This should + // be verified separately. + assert minterGateway.totalOwedM(e) == require_uint240(minterGateway.totalActiveOwedM(e) + minterGateway.totalInactiveOwedM); +} + +/// @title MZero Protocol Property 3: totalMSupply = totalNonEarningMSupply + totalEarningMSupply +/// This property is mentioned in the MZero protocol engineering spec doc +rule r03_totalMSupplyCorrectness { + env e; + // There is an assumption in the solidity code about why + // a potential unchecked overflow is not possible. This should + // be verified separately. + assert minterGateway.totalMSupply(e) == require_uint240(MToken.totalNonEarningSupply + MToken.totalEarningSupply(e)); +} + +/// @title MZero Protocol Property 9: +/// Minters cannot generate M unless their Eligible Collateral +/// (tracked by Collateral Value) is sufficiently high (they are overcollateralized) +rule r09_mintersCannotMintMUnlessAreOvercollateralized { + env e; address minter; uint256 mintId; + + uint256 maxAllowedActiveOwedMOfMinter = maxAllowedActiveOwedMOf(e, minter); + uint256 activeOwedMOfMinter = assert_uint256(activeOwedMOf(e, minter)); // this is uint240 so this cast always succeeds + + mintM(e, mintId); + // if mint was called without reverting the caller must + // be overcollateralized + assert e.msg.sender == minter => activeOwedMOfMinter <= maxAllowedActiveOwedMOfMinter; +} + +/// @title MZero Protocol Property 10: If a minter does not call update during the +/// required interval, their eligible collateral is assumed 0. +rule r10_collateralOfMinterIsZeroIfMinterDoesNotCallUpdate { + env e; + address minter; + // the following returns uint40 so it can always be cast to uint256 + uint256 expiry_time = assert_uint256(collateralExpiryTimestampOf(e, minter)); + uint240 collateralOfMinter = collateralOf(e, minter); + + assert e.block.timestamp > expiry_time => collateralOfMinter == 0; +} + +/// @title MZero Protocol Property 13: A Propose Mint call cannot succeed +/// before MintDelay time has elapsed. +rule r13_minterMustWaitMintDelayTimeToMintM { + env e; + require e.block.timestamp > 1704060000; // 01.01.2024 00:00:00 + uint256 mintId; + uint40 createdAt = minterGateway._mintProposals[e.msg.sender].createdAt; + uint32 mintDelay = mintDelay(e); + + mintM(e, mintId); + + // if mintM did not revert, it must be that the proposal + // was created at least mintDelay seconds ago + + assert assert_uint256(createdAt) <= e.block.timestamp => + assert_uint256(createdAt + mintDelay) <= e.block.timestamp; +} + +/// @title Sanity rule to check all methods are reachable and do not always revert. +rule sanity(method f) +{ + env e; + calldataarg args; + f(e,args); + satisfy true; +} + +/// @title It is not possible that minter can be both deactivated and active +invariant minterStatesCannotBeContradicting(address minter) + !(minterGateway._minterStates[minter].isDeactivated && + minterGateway._minterStates[minter].isActive); + +/// @title In two consecutive calls at the same timestamp of updateIndex(), +/// the second call should not increase the MToken balance of the ttgVault +rule consecutiveCallOfUpdateIndexCannotIncreaseMToken() { + env e; + setLegalInitialState(e); + minterGateway.updateIndex(e); // first call + + uint240 totalMSupplyBefore = minterGateway.totalMSupply(e); + minterGateway.updateIndex(e); // second call should not change the state + uint240 totalMSupplyAfter = minterGateway.totalMSupply(e); + + assert totalMSupplyBefore == totalMSupplyAfter; +} + + +/// @title Only the balance of msg.sender can be reduced when calling burnM() +rule r08_burnReducesOnlyTheBalanceOfMsgSender() { + env e; + SumTrackingSetup(e); + setLegalInitialState(e); + + requireInvariant SumOfBalancesEqualsTotalSupply(); + requireInvariant SumOfBalancesEqualsTotalSupplyMToken(); + + require minterGateway.totalOwedM(e) >= minterGateway.totalActiveOwedM(e); // assume no overflow + require minterGateway.totalOwedM(e) >= minterGateway.totalInactiveOwedM; // assume no overflow + + require MToken.totalSupply(e) >= assert_uint256(MToken.totalEarningSupply(e)); // assume no overflow + require MToken.totalSupply(e) >= assert_uint256(MToken.totalNonEarningSupply(e)); // assume no overflow + + require minterGateway.excessOwedM(e) + MToken.totalSupply(e) < max_uint240; // assume no overflow + + address account; + address minter; uint256 maxPrincipalAmount; uint256 maxAmount; + address vault = minterGateway.ttgVault(e); + + uint256 balanceBefore = MToken.balanceOf(e, account); + burnM(e, minter, maxPrincipalAmount, maxAmount); + uint256 balanceAfter = MToken.balanceOf(e, account); + + assert (e.msg.sender != account) => balanceBefore <= balanceAfter; + assert (e.msg.sender == account) && account != vault => balanceBefore >= balanceAfter; +} + +/// @title Any validator can always freeze any minter +rule r16_validatorCanAlwaysFreezeAnyMinter() { + env e1; env e2; address minter; address validator; + require e2.block.timestamp < 4102444800; // 01.01.2100 00:00:00 + require e2.block.timestamp > 1704067200; // 01.01.2024 00:00:00 + + bool isValidator = isValidatorApproved(e1, validator); + minterGateway.freezeMinter(e2, minter); + + assert e2.msg.sender == validator => isValidator && minterGateway._minterStates[minter].frozenUntilTimestamp >= assert_uint40(e2.block.timestamp); +} + +/// @title Any validator can cancel any existing mintId +rule r16_validatorCanAlwaysCancelAnyExistingMintId() { + env e1; env e2; address minter; uint256 mintId; address validator; + + bool isValidator = isValidatorApproved(e1, validator); + + uint48 idBefore = minterGateway._mintProposals[minter].id; + minterGateway.cancelMint(e2, minter, mintId); + uint48 idAfter = minterGateway._mintProposals[minter].id; + + assert e2.msg.sender == validator => isValidator && idBefore == assert_uint48(mintId) && idAfter == 0; +} + +/// @title After calling minterGateway.updateIndex() the excessOwedM() should be zero +rule mgUpdateIndexZeroesExcessOwedM() { + env e; + setLegalInitialState(e); + + uint240 excessOwedMBefore = minterGateway.excessOwedM(e); + minterGateway.updateIndex(e); + uint240 excessOwedMAfter = minterGateway.excessOwedM(e); + + address vault = minterGateway.ttgVault(e); + bool vaultIsEarning = MToken.getIsEarning(e,vault); + + assert !vaultIsEarning => excessOwedMAfter == 0; +} diff --git a/certora/specs/MinterGateway_hooks.spec b/certora/specs/MinterGateway_hooks.spec new file mode 100644 index 00000000..387cfb20 --- /dev/null +++ b/certora/specs/MinterGateway_hooks.spec @@ -0,0 +1,76 @@ +import "setup.spec"; + +using MinterGatewayHarness as minterGateway; + +/// True sum of balances. +ghost mathint sumOfBalances { init_state axiom sumOfBalances == 0; } +ghost mathint sumOfActiveBalances { init_state axiom sumOfActiveBalances == 0; } +ghost mathint sumOfInactiveBalances { init_state axiom sumOfInactiveBalances == 0; } + +/// The initial value is being updated as we access the acounts balances one-by-one. +/// Should only be used as an initial value, never post-action! +ghost mathint sumOfBalances_init { init_state axiom sumOfBalances_init == 0; } +ghost mathint sumOfActiveBalances_init { init_state axiom sumOfActiveBalances_init == 0; } +ghost mathint sumOfInactiveBalances_init { init_state axiom sumOfInactiveBalances_init == 0; } + +ghost mapping(address => bool) didAccessAccount; + +function SumTrackingSetup_Minter(env e) { + require sumOfBalances == sumOfBalances_init; + require sumOfActiveBalances == sumOfActiveBalances_init; + require sumOfInactiveBalances == sumOfInactiveBalances_init; + //havoc didAccessAccount assuming + require forall address minter. !didAccessAccount[minter]; +} + +hook Sstore minterGateway._minterStates[KEY address minter].isActive bool isActive (bool wasActive) { + uint240 _balance = minterGateway._rawOwedM[minter]; + //require to_mathint(_balance) <= to_mathint(UINT112_MAX()); + if(isActive && !wasActive) { + sumOfActiveBalances = sumOfActiveBalances + _balance; + sumOfInactiveBalances = sumOfInactiveBalances - _balance; + } + else if(!isActive && wasActive) { + sumOfActiveBalances = sumOfActiveBalances - _balance; + sumOfInactiveBalances = sumOfInactiveBalances + _balance; + } +} + +hook Sload uint240 _balance minterGateway._rawOwedM[KEY address minter] { + if(!didAccessAccount[minter]) { + didAccessAccount[minter] = true; + sumOfBalances_init = sumOfBalances_init - _balance; + require sumOfBalances_init >= 0; + if (minterGateway._minterStates[minter].isActive) { + sumOfActiveBalances_init = sumOfActiveBalances_init - _balance; + require sumOfActiveBalances_init >= 0; + } else { + sumOfInactiveBalances_init = sumOfInactiveBalances_init - _balance; + require sumOfInactiveBalances_init >= 0; + } + } +} + +hook Sstore minterGateway._rawOwedM[KEY address minter] uint240 _balance (uint240 _balance_old) { + if(!didAccessAccount[minter]) { + didAccessAccount[minter] = true; + sumOfBalances_init = sumOfBalances_init - _balance_old; + require sumOfBalances_init >= 0; + + if (minterGateway._minterStates[minter].isActive) { + sumOfActiveBalances_init = sumOfActiveBalances_init - _balance_old; + require sumOfActiveBalances_init >= 0; + } else { + sumOfInactiveBalances_init = sumOfInactiveBalances_init - _balance_old; + require sumOfInactiveBalances_init >= 0; + } + } + sumOfBalances = sumOfBalances + _balance - _balance_old; + + if (minterGateway._minterStates[minter].isActive) { + sumOfActiveBalances = sumOfActiveBalances + _balance - _balance_old; + } + else { + sumOfInactiveBalances = sumOfInactiveBalances + _balance - _balance_old; + } +} diff --git a/certora/specs/setup.spec b/certora/specs/setup.spec new file mode 100644 index 00000000..7868ff9f --- /dev/null +++ b/certora/specs/setup.spec @@ -0,0 +1,79 @@ +methods { + function ContinuousIndexingMath.getContinuousIndex(uint64 yearlyRate, uint32 time) internal returns (uint48) => ghostContinuousIndex(yearlyRate, time); + function ContinuousIndexingMath.multiplyIndicesUp(uint128 index, uint48 deltaIndex) internal returns (uint144) => ghostMultiplyIndices(index, deltaIndex); + function ContinuousIndexingMath.multiplyIndicesDown(uint128 index, uint48 deltaIndex) internal returns (uint144) => ghostMultiplyIndices(index, deltaIndex); + + function MinterGatewayHarness.getMinterRate() external returns (uint32); + function MTokenHarness.getEarnerRate() external returns (uint32); + function MinterGateway._rate() internal returns (uint32) => ghostMinterRate; + function MToken._rate() internal returns (uint32) => ghostEarnerRate; + + function MinterGatewayHarness.latestUpdateTimestamp() external returns (uint40) envfree; + function MTokenHarness.latestUpdateTimestamp() external returns (uint40) envfree; + function MTokenHarness.getInternalBalanceOf(address) external returns (uint240) envfree; + + function _._verifyValidatorSignatures( + address minter_, + uint256 collateral_, + uint256[] calldata retrievalIds_, + bytes32 metadataHash_, + address[] calldata validators_, + uint256[] calldata timestamps_, + bytes[] calldata signatures_ + ) internal => NONDET; // assumption that the ERC-712 verification is passing + + function _._getDigest(bytes32 internalDigest_) internal => NONDET; // ERC-712 verification + function _._getDomainSeparator() internal => NONDET; // ERC-712 + + function ContinuousIndexingMath.divideDown(uint240 x, uint128 index) internal returns (uint112) => divideDownCVL(x,index); + function ContinuousIndexingMath.divideUp(uint240 x, uint128 index) internal returns (uint112) => divideUpCVL(x,index); + function ContinuousIndexingMath.multiplyDown(uint112 x, uint128 index) internal returns (uint240) => multiplyDownCVL(x,index); + function ContinuousIndexingMath.multiplyUp(uint112 x, uint128 index) internal returns (uint240) => multiplyUpCVL(x,index); +} + +definition UINT256_MAX() returns uint256 = max_uint256; +definition UINT112_MAX() returns uint240 = max_uint112; +definition UINT128_MAX() returns uint240 = max_uint128; +definition UINT112x128_MAX() returns uint240 = 1766847064778384329583297500742918175539924679078620667118468273195188225; // UINT112_MAX * UINT128_MAX +definition ValidTimestamp(env e) returns bool = + e.block.timestamp < 4102444800 && e.block.timestamp > 1704067200; + // [01.01.2024 00:00:00, 01.01.2100 00:00:00] + +ghost uint32 ghostMinterRate; +ghost uint32 ghostEarnerRate; + +ghost ghostContinuousIndex(uint64, uint32) returns uint48 { + axiom forall uint32 time. + ghostContinuousIndex(0, time) == EXP_SCALED_ONE_48(); // EXP_SCALED_ONE = 1e12 + axiom forall uint64 yearlyRate. + ghostContinuousIndex(yearlyRate, 0) == EXP_SCALED_ONE_48(); // EXP_SCALED_ONE = 1e12 + axiom forall uint64 yearlyRate1. + forall uint64 yearlyRate2. + forall uint32 time. + yearlyRate1 >= yearlyRate2 && yearlyRate2 > 0 => + ghostContinuousIndex(yearlyRate1, time) >= ghostContinuousIndex(yearlyRate2, time); + axiom forall uint64 yearlyRate. + forall uint32 time1. + forall uint32 time2. + time1 >= time2 && time2 > 0 => + ghostContinuousIndex(yearlyRate, time1) >= ghostContinuousIndex(yearlyRate, time2); +} + +ghost ghostMultiplyIndices(uint128, uint48) returns uint144 { + axiom forall uint128 index1. + forall uint128 index2. + forall uint48 deltaIndex. + index1 >= index2 && index2 > 0 => + ghostMultiplyIndices(index1, deltaIndex) >= ghostMultiplyIndices(index2, deltaIndex); + axiom forall uint128 index. + forall uint48 deltaIndex1. + forall uint48 deltaIndex2. + deltaIndex1 >= deltaIndex2 && deltaIndex2 > 0 => + ghostMultiplyIndices(index, deltaIndex1) >= ghostMultiplyIndices(index, deltaIndex2); + axiom forall uint128 index. + forall uint48 deltaIndex. + index == 0 || deltaIndex == 0 => + ghostMultiplyIndices(index, deltaIndex) == 0; + axiom forall uint128 index. + to_mathint(ghostMultiplyIndices(index, EXP_SCALED_ONE_48())) == to_mathint(index); +}