diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 16c5eda..6f94a69 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -44,15 +44,12 @@ jobs: - "termRepoCollateralManager.conf" - "termRepoLocker.conf" - "termRepoRolloverManager.conf" - - "termRepoServicer.conf" - "termRepoServicer-lockFulfill.conf" - - "termRepoServicer-lockFulfillReverts.conf" - "termRepoServicer-mintCollapse.conf" + - "termRepoServicer-mintIntegrity.conf" - "termRepoServicer-mintCollapseReverts.conf" - "termRepoServicer-repaymentsRedemptions.conf" - - "termRepoServicer-repaymentsRedemptionsReverts.conf" - "termRepoServicer-stateVariables.conf" - - "termRepoServicer.conf" - "termRepoToken.conf" steps: - uses: actions/checkout@master @@ -83,3 +80,44 @@ jobs: env: CERTORAKEY: ${{ secrets.CERTORAKEY }} SOLC_VERSION: 0.8.18 + formal-verfication-beta: + runs-on: ubuntu-latest + needs: test + strategy: + matrix: + ruleset: + - "termRepoServicer-lockFulfillReverts.conf" + - "termRepoServicer-repaymentsReverts.conf" + - "termRepoServicer-redemptionsReverts.conf" + - "termRepoServicer-rolloverReverts.conf" + - "termRepoServicer.conf" + steps: + - uses: actions/checkout@master + with: + fetch-depth: 0 + - uses: actions/setup-node@v4 + with: + node-version: "18.15" + cache: yarn + - uses: actions/setup-python@v4 + with: + python-version: "3.11" + - run: | + yarn install --immutable + yarn build + - run: | + pip3 install certora-cli-beta + - run: | + msg="${2:-"$(hostname) - ${conf_file} - $(date +%s)"}" + + pip3 install solc-select + solc-select install ${SOLC_VERSION} + + certoraRun "./certora/confs/${{ matrix.ruleset }}" \ + --msg "$(hostname) - ${{ matrix.ruleset }} - $(date +%s)" \ + --wait_for_results all \ + --rule_sanity basic + env: + CERTORAKEY: ${{ secrets.CERTORAKEY }} + SOLC_VERSION: 0.8.18 + diff --git a/certora/confs/termAuctionBidLocker-locking.conf b/certora/confs/termAuctionBidLocker-locking.conf index 7568455..7b8ef24 100644 --- a/certora/confs/termAuctionBidLocker-locking.conf +++ b/certora/confs/termAuctionBidLocker-locking.conf @@ -21,6 +21,6 @@ ], "server": "production", "rule_sanity": "basic", - "contract_compiler_skip_severe_warning_as_error": true, + "ignore_solidity_warnings": true, "verify": "TermAuctionBidLockerHarness:certora/specs/termAuctionBidLocker/rulesLocking.spec" } \ No newline at end of file diff --git a/certora/confs/termAuctionBidLocker-lockingReverts.conf b/certora/confs/termAuctionBidLocker-lockingReverts.conf index f0746bc..aefea02 100644 --- a/certora/confs/termAuctionBidLocker-lockingReverts.conf +++ b/certora/confs/termAuctionBidLocker-lockingReverts.conf @@ -21,6 +21,6 @@ ], "server": "production", "rule_sanity": "basic", - "contract_compiler_skip_severe_warning_as_error": true, + "ignore_solidity_warnings": true, "verify": "TermAuctionBidLockerHarness:certora/specs/termAuctionBidLocker/rulesLockingReverts.spec" } \ No newline at end of file diff --git a/certora/confs/termAuctionBidLocker-stateVariables.conf b/certora/confs/termAuctionBidLocker-stateVariables.conf index 8b845ca..aeb791f 100644 --- a/certora/confs/termAuctionBidLocker-stateVariables.conf +++ b/certora/confs/termAuctionBidLocker-stateVariables.conf @@ -21,6 +21,6 @@ ], "server": "production", "rule_sanity": "basic", - "contract_compiler_skip_severe_warning_as_error": true, + "ignore_solidity_warnings": true, "verify": "TermAuctionBidLockerHarness:certora/specs/termAuctionBidLocker/rulesStateVariables.spec" } \ No newline at end of file diff --git a/certora/confs/termAuctionBidLocker.conf b/certora/confs/termAuctionBidLocker.conf index 5e1c480..34519b0 100644 --- a/certora/confs/termAuctionBidLocker.conf +++ b/certora/confs/termAuctionBidLocker.conf @@ -21,6 +21,6 @@ ], "server": "production", "rule_sanity": "basic", - "contract_compiler_skip_severe_warning_as_error": true, + "ignore_solidity_warnings": true, "verify": "TermAuctionBidLockerHarness:certora/specs/termAuctionBidLocker/rules.spec" } \ No newline at end of file diff --git a/certora/confs/termRepoCollateralManager-batchDefault.conf b/certora/confs/termRepoCollateralManager-batchDefault.conf index 7d99c6e..0469307 100644 --- a/certora/confs/termRepoCollateralManager-batchDefault.conf +++ b/certora/confs/termRepoCollateralManager-batchDefault.conf @@ -21,7 +21,7 @@ "solc_optimize": "50", "loop_iter": "2", "optimistic_loop": true, - "contract_compiler_skip_severe_warning_as_error": true, + "ignore_solidity_warnings": true, "prover_args": [ "-smt_initialSplitDepth 3", "-depth 10" diff --git a/certora/confs/termRepoCollateralManager-batchLiquidation.conf b/certora/confs/termRepoCollateralManager-batchLiquidation.conf index 4ccb708..1166d74 100644 --- a/certora/confs/termRepoCollateralManager-batchLiquidation.conf +++ b/certora/confs/termRepoCollateralManager-batchLiquidation.conf @@ -21,7 +21,7 @@ "solc_optimize": "50", "loop_iter": "2", "optimistic_loop": true, - "contract_compiler_skip_severe_warning_as_error": true, + "ignore_solidity_warnings": true, "prover_args": [ "-smt_initialSplitDepth 3", "-depth 10" diff --git a/certora/confs/termRepoCollateralManager-batchLiquidationWithRepoToken.conf b/certora/confs/termRepoCollateralManager-batchLiquidationWithRepoToken.conf index b54fd2f..3120da7 100644 --- a/certora/confs/termRepoCollateralManager-batchLiquidationWithRepoToken.conf +++ b/certora/confs/termRepoCollateralManager-batchLiquidationWithRepoToken.conf @@ -21,7 +21,7 @@ "solc_optimize": "50", "loop_iter": "2", "optimistic_loop": true, - "contract_compiler_skip_severe_warning_as_error": true, + "ignore_solidity_warnings": true, "prover_args": [ "-smt_initialSplitDepth 4", "-depth 20", diff --git a/certora/confs/termRepoCollateralManager-stateVariables.conf b/certora/confs/termRepoCollateralManager-stateVariables.conf index f6fd20d..e3b45e4 100644 --- a/certora/confs/termRepoCollateralManager-stateVariables.conf +++ b/certora/confs/termRepoCollateralManager-stateVariables.conf @@ -21,7 +21,7 @@ "solc_optimize": "50", "loop_iter": "3", "optimistic_loop": true, - "contract_compiler_skip_severe_warning_as_error": true, + "ignore_solidity_warnings": true, "prover_args": [ "-depth 15", "-splitParallel true" diff --git a/certora/confs/termRepoCollateralManager.conf b/certora/confs/termRepoCollateralManager.conf index 413f15a..d0dabb0 100644 --- a/certora/confs/termRepoCollateralManager.conf +++ b/certora/confs/termRepoCollateralManager.conf @@ -21,7 +21,7 @@ "solc_optimize": "50", "loop_iter": "3", "optimistic_loop": true, - "contract_compiler_skip_severe_warning_as_error": true, + "ignore_solidity_warnings": true, "prover_args": [ "-depth 15", "-splitParallel true" diff --git a/certora/confs/termRepoRolloverManager.conf b/certora/confs/termRepoRolloverManager.conf index a5fa870..9c4fb83 100644 --- a/certora/confs/termRepoRolloverManager.conf +++ b/certora/confs/termRepoRolloverManager.conf @@ -15,7 +15,7 @@ "solc_optimize": "50", "loop_iter": "3", "optimistic_loop": true, - "contract_compiler_skip_severe_warning_as_error": true, + "ignore_solidity_warnings": true, "parametric_contracts": [ "TermRepoRolloverManagerHarness" ], diff --git a/certora/confs/termRepoServicer-lockFulfill.conf b/certora/confs/termRepoServicer-lockFulfill.conf index 1b4216d..28dd3b6 100644 --- a/certora/confs/termRepoServicer-lockFulfill.conf +++ b/certora/confs/termRepoServicer-lockFulfill.conf @@ -20,14 +20,14 @@ "-smt_initialSplitDepth 5", "-depth 15", "-mediumTimeout 20", - "-newSplitParallel true", + "-splitParallel true", "-splitParallelTimelimit 7200", "-splitParallelInitialDepth 10" ], "solc_optimize": "50", "loop_iter": "2", "optimistic_loop": true, - "contract_compiler_skip_severe_warning_as_error": true, + "ignore_solidity_warnings": true, "smt_timeout": "7200", "parametric_contracts": [ diff --git a/certora/confs/termRepoServicer-lockFulfillReverts.conf b/certora/confs/termRepoServicer-lockFulfillReverts.conf index 63dc0d6..cecbe0a 100644 --- a/certora/confs/termRepoServicer-lockFulfillReverts.conf +++ b/certora/confs/termRepoServicer-lockFulfillReverts.conf @@ -27,7 +27,7 @@ "solc_optimize": "50", "loop_iter": "2", "optimistic_loop": true, - "contract_compiler_skip_severe_warning_as_error": true, + "ignore_solidity_warnings": true, "smt_timeout": "7200", "parametric_contracts": [ diff --git a/certora/confs/termRepoServicer-mintCollapse.conf b/certora/confs/termRepoServicer-mintCollapse.conf index 17a52f1..9805322 100644 --- a/certora/confs/termRepoServicer-mintCollapse.conf +++ b/certora/confs/termRepoServicer-mintCollapse.conf @@ -20,14 +20,14 @@ "-smt_initialSplitDepth 5", "-depth 15", "-mediumTimeout 2", - "-newSplitParallel true", + "-splitParallel true", "-splitParallelTimelimit 7200", "-splitParallelInitialDepth 5" ], "solc_optimize": "50", "loop_iter": "2", "optimistic_loop": true, - "contract_compiler_skip_severe_warning_as_error": true, + "ignore_solidity_warnings": true, "smt_timeout": "7200", "parametric_contracts": [ "TermRepoServicerHarness" diff --git a/certora/confs/termRepoServicer-mintCollapseReverts.conf b/certora/confs/termRepoServicer-mintCollapseReverts.conf index 0697516..35f6168 100644 --- a/certora/confs/termRepoServicer-mintCollapseReverts.conf +++ b/certora/confs/termRepoServicer-mintCollapseReverts.conf @@ -23,7 +23,7 @@ "solc_optimize": "50", "loop_iter": "2", "optimistic_loop": true, - "contract_compiler_skip_severe_warning_as_error": true, + "ignore_solidity_warnings": true, "smt_timeout": "7200", "parametric_contracts": [ "TermRepoServicerHarness" diff --git a/certora/confs/termRepoServicer-mintIntegrity.conf b/certora/confs/termRepoServicer-mintIntegrity.conf new file mode 100644 index 0000000..78fdf4f --- /dev/null +++ b/certora/confs/termRepoServicer-mintIntegrity.conf @@ -0,0 +1,37 @@ +{ + "files": [ + "certora/harness/TermRepoServicerHarness.sol", + "contracts/TermAuctionBidLocker.sol", + "contracts/TermController.sol", + "contracts/TermRepoLocker.sol", + "contracts/TermRepoToken.sol", + "contracts/TermRepoRolloverManager.sol", + "certora/harness/TermRepoCollateralManagerHarness.sol", + "certora/helpers/DummyERC20A.sol" + ], + "link": [ + "TermRepoServicerHarness:termRepoToken=TermRepoToken", + "TermRepoServicerHarness:termRepoLocker=TermRepoLocker", + "TermRepoServicerHarness:termRepoCollateralManager=TermRepoCollateralManagerHarness", + "TermRepoServicerHarness:termRepoRolloverManager=TermRepoRolloverManager", + "TermRepoCollateralManagerHarness:termRepoLocker=TermRepoLocker" + ], + "prover_args": [ + "-depth 15", + "-splitParallel true" + ], + "solc_optimize": "50", + "loop_iter": "2", + "optimistic_loop": true, + "ignore_solidity_warnings": true, + "smt_timeout": "7200", + "parametric_contracts": [ + "TermRepoServicerHarness" + ], + "rule_sanity": "basic", + "packages": [ + "@chainlink=node_modules/@chainlink", + "@openzeppelin=node_modules/@openzeppelin" + ], + "verify": "TermRepoServicerHarness:certora/specs/termRepoServicer/rulesMintIntegrity.spec" +} \ No newline at end of file diff --git a/certora/confs/termRepoServicer-redemptionsReverts.conf b/certora/confs/termRepoServicer-redemptionsReverts.conf new file mode 100644 index 0000000..86f89b6 --- /dev/null +++ b/certora/confs/termRepoServicer-redemptionsReverts.conf @@ -0,0 +1,37 @@ +{ + "files": [ + "certora/harness/TermRepoServicerHarness.sol", + "contracts/TermAuctionBidLocker.sol", + "contracts/TermController.sol", + "contracts/TermRepoLocker.sol", + "contracts/TermRepoToken.sol", + "contracts/TermRepoRolloverManager.sol", + "certora/harness/TermRepoCollateralManagerHarness.sol", + "certora/helpers/DummyERC20A.sol" + ], + "link": [ + "TermRepoServicerHarness:termRepoToken=TermRepoToken", + "TermRepoServicerHarness:termRepoLocker=TermRepoLocker", + "TermRepoServicerHarness:termRepoCollateralManager=TermRepoCollateralManagerHarness", + "TermRepoServicerHarness:termRepoRolloverManager=TermRepoRolloverManager", + "TermRepoCollateralManagerHarness:termRepoLocker=TermRepoLocker" + ], + "prover_args": [ + "-depth 15", + "-splitParallel true" + ], + "solc_optimize": "50", + "ignore_solidity_warnings": true, + "loop_iter": "2", + "optimistic_loop": true, + "smt_timeout": "7200", + "parametric_contracts": [ + "TermRepoServicerHarness" + ], + "rule_sanity": "basic", + "packages": [ + "@chainlink=node_modules/@chainlink", + "@openzeppelin=node_modules/@openzeppelin" + ], + "verify": "TermRepoServicerHarness:certora/specs/termRepoServicer/rulesRedemptionsReverts.spec" +} \ No newline at end of file diff --git a/certora/confs/termRepoServicer-repaymentsRedemptions.conf b/certora/confs/termRepoServicer-repaymentsRedemptions.conf index 391f87d..920c5cc 100644 --- a/certora/confs/termRepoServicer-repaymentsRedemptions.conf +++ b/certora/confs/termRepoServicer-repaymentsRedemptions.conf @@ -20,12 +20,12 @@ "-smt_initialSplitDepth 5", "-depth 15", "-mediumTimeout 20", - "-newSplitParallel true", + "-splitParallel true", "-splitParallelTimelimit 7200", "-splitParallelInitialDepth 5" ], "solc_optimize": "50", - "contract_compiler_skip_severe_warning_as_error": true, + "ignore_solidity_warnings": true, "loop_iter": "2", "optimistic_loop": true, "smt_timeout": "7200", @@ -37,6 +37,5 @@ "@chainlink=node_modules/@chainlink", "@openzeppelin=node_modules/@openzeppelin" ], - "prover_version": "jtoman/finder-fixes-will-it-ever-end", "verify": "TermRepoServicerHarness:certora/specs/termRepoServicer/rulesRepaymentsRedemptions.spec" } \ No newline at end of file diff --git a/certora/confs/termRepoServicer-repaymentsRedemptionsReverts.conf b/certora/confs/termRepoServicer-repaymentsReverts.conf similarity index 89% rename from certora/confs/termRepoServicer-repaymentsRedemptionsReverts.conf rename to certora/confs/termRepoServicer-repaymentsReverts.conf index f668ece..7772a56 100644 --- a/certora/confs/termRepoServicer-repaymentsRedemptionsReverts.conf +++ b/certora/confs/termRepoServicer-repaymentsReverts.conf @@ -25,7 +25,7 @@ "-splitParallelInitialDepth 5" ], "solc_optimize": "50", - "contract_compiler_skip_severe_warning_as_error": true, + "ignore_solidity_warnings": true, "loop_iter": "2", "optimistic_loop": true, "smt_timeout": "7200", @@ -37,6 +37,5 @@ "@chainlink=node_modules/@chainlink", "@openzeppelin=node_modules/@openzeppelin" ], - "prover_version": "jtoman/finder-fixes-will-it-ever-end", - "verify": "TermRepoServicerHarness:certora/specs/termRepoServicer/rulesRepaymentsRedemptionsReverts.spec" + "verify": "TermRepoServicerHarness:certora/specs/termRepoServicer/rulesRepaymentsReverts.spec" } \ No newline at end of file diff --git a/certora/confs/termRepoServicer-rolloverReverts.conf b/certora/confs/termRepoServicer-rolloverReverts.conf new file mode 100644 index 0000000..bfa3666 --- /dev/null +++ b/certora/confs/termRepoServicer-rolloverReverts.conf @@ -0,0 +1,42 @@ +{ + "files": [ + "certora/harness/TermRepoServicerHarness.sol", + "contracts/TermAuctionBidLocker.sol", + "contracts/TermController.sol", + "contracts/TermRepoLocker.sol", + "contracts/TermRepoToken.sol", + "contracts/TermRepoRolloverManager.sol", + "certora/harness/TermRepoCollateralManagerHarness.sol", + "certora/helpers/DummyERC20A.sol" + ], + "link": [ + "TermRepoServicerHarness:termRepoToken=TermRepoToken", + "TermRepoServicerHarness:termRepoLocker=TermRepoLocker", + "TermRepoServicerHarness:termRepoCollateralManager=TermRepoCollateralManagerHarness", + "TermRepoServicerHarness:termController=TermController", + "TermRepoServicerHarness:termRepoRolloverManager=TermRepoRolloverManager", + "TermRepoCollateralManagerHarness:termRepoLocker=TermRepoLocker" + ], + "prover_args": [ + "-smt_initialSplitDepth 10", + "-depth 20", + "-mediumTimeout 2", + "-splitParallel true", + "-splitParallelTimelimit 7200", + "-splitParallelInitialDepth 10" + ], + "solc_optimize": "50", + "loop_iter": "2", + "optimistic_loop": true, + "ignore_solidity_warnings": true, + "smt_timeout": "7200", + "parametric_contracts": [ + "TermRepoServicerHarness" + ], + "rule_sanity": "basic", + "packages": [ + "@chainlink=node_modules/@chainlink", + "@openzeppelin=node_modules/@openzeppelin" + ], + "verify": "TermRepoServicerHarness:certora/specs/termRepoServicer/rulesRolloverReverts.spec" +} \ No newline at end of file diff --git a/certora/confs/termRepoServicer-stateVariables.conf b/certora/confs/termRepoServicer-stateVariables.conf index 033e07b..eb5cc67 100644 --- a/certora/confs/termRepoServicer-stateVariables.conf +++ b/certora/confs/termRepoServicer-stateVariables.conf @@ -20,12 +20,12 @@ "-smt_initialSplitDepth 10", "-depth 20", "-mediumTimeout 2", - "-newSplitParallel true", + "-splitParallel true", "-splitParallelTimelimit 7200", "-splitParallelInitialDepth 10" ], "solc_optimize": "50", - "contract_compiler_skip_severe_warning_as_error": true, + "ignore_solidity_warnings": true, "loop_iter": "2", "optimistic_loop": true, "smt_timeout": "7200", diff --git a/certora/confs/termRepoServicer.conf b/certora/confs/termRepoServicer.conf index c26e4b0..de603df 100644 --- a/certora/confs/termRepoServicer.conf +++ b/certora/confs/termRepoServicer.conf @@ -13,21 +13,18 @@ "TermRepoServicerHarness:termRepoToken=TermRepoToken", "TermRepoServicerHarness:termRepoLocker=TermRepoLocker", "TermRepoServicerHarness:termRepoCollateralManager=TermRepoCollateralManagerHarness", + "TermRepoServicerHarness:termController=TermController", "TermRepoServicerHarness:termRepoRolloverManager=TermRepoRolloverManager", "TermRepoCollateralManagerHarness:termRepoLocker=TermRepoLocker" ], "prover_args": [ - "-smt_initialSplitDepth 10", - "-depth 20", - "-mediumTimeout 2", - "-newSplitParallel true", - "-splitParallelTimelimit 7200", - "-splitParallelInitialDepth 10" + "-depth 15", + "-splitParallel true" ], "solc_optimize": "50", "loop_iter": "2", "optimistic_loop": true, - "contract_compiler_skip_severe_warning_as_error": true, + "ignore_solidity_warnings": true, "smt_timeout": "7200", "parametric_contracts": [ "TermRepoServicerHarness" diff --git a/certora/specs/termRepoServicer/accessRoles.spec b/certora/specs/termRepoServicer/accessRoles.spec index 89c4f28..d467a72 100644 --- a/certora/specs/termRepoServicer/accessRoles.spec +++ b/certora/specs/termRepoServicer/accessRoles.spec @@ -1,6 +1,9 @@ import "../methods/erc20Methods.spec"; import "../methods/emitMethods.spec"; +using TermController as servicerAccessController; + + methods { function hasRole(bytes32, address) external returns (bool) envfree; function ADMIN_ROLE() external returns (bytes32) envfree; @@ -9,10 +12,11 @@ methods { function COLLATERAL_MANAGER() external returns (bytes32) envfree; function DEVOPS_ROLE() external returns (bytes32) envfree; function INITIALIZER_ROLE() external returns (bytes32) envfree; - function SPECIALIST_ROLE() external returns (bytes32) envfree; function ROLLOVER_MANAGER() external returns (bytes32) envfree; function ROLLOVER_TARGET_AUCTIONEER_ROLE() external returns (bytes32) envfree; -} + + function _.verifyMintExposureAccess(address) external => DISPATCHER(true); + } rule onlyRoleCanCallRevert(method f, calldataarg args, env e) filtered { @@ -36,10 +40,10 @@ rule onlyRoleCanCallRevert(method f, calldataarg args, env e) filtered { || hasRole(AUCTIONEER(),e.msg.sender) || hasRole(COLLATERAL_MANAGER(),e.msg.sender) || hasRole(DEVOPS_ROLE(),e.msg.sender) - || hasRole(SPECIALIST_ROLE(),e.msg.sender) || hasRole(ROLLOVER_MANAGER(),e.msg.sender) || hasRole(ROLLOVER_TARGET_AUCTIONEER_ROLE(),e.msg.sender) - || hasRole(INITIALIZER_ROLE(),e.msg.sender); + || hasRole(INITIALIZER_ROLE(),e.msg.sender) + || servicerAccessController.verifyMintExposureAccess(e, e.msg.sender); } rule onlyRoleCanCallStorage(method f, calldataarg args, env e) filtered { @@ -64,8 +68,8 @@ rule onlyRoleCanCallStorage(method f, calldataarg args, env e) filtered { || hasRole(AUCTIONEER(),e.msg.sender) || hasRole(COLLATERAL_MANAGER(),e.msg.sender) || hasRole(DEVOPS_ROLE(),e.msg.sender) - || hasRole(SPECIALIST_ROLE(),e.msg.sender) || hasRole(ROLLOVER_MANAGER(),e.msg.sender) || hasRole(ROLLOVER_TARGET_AUCTIONEER_ROLE(),e.msg.sender) - || hasRole(INITIALIZER_ROLE(),e.msg.sender); + || hasRole(INITIALIZER_ROLE(),e.msg.sender) + || servicerAccessController.verifyMintExposureAccess(e, e.msg.sender); } \ No newline at end of file diff --git a/certora/specs/termRepoServicer/collapses.spec b/certora/specs/termRepoServicer/collapses.spec index 98e0b99..73164e3 100644 --- a/certora/specs/termRepoServicer/collapses.spec +++ b/certora/specs/termRepoServicer/collapses.spec @@ -47,6 +47,9 @@ methods { function DummyERC20A.balanceOf(address) external returns(uint256) envfree; function DummyERC20A.decimals() external returns(uint256) envfree; function DummyERC20A.totalSupply() external returns(uint256) envfree; + + function _.verifyMintExposureAccess(address) external => DISPATCHER(true); + } rule burnCollapseExposureMonotonicBehavior(env e) { diff --git a/certora/specs/termRepoServicer/minting.spec b/certora/specs/termRepoServicer/minting.spec index 94557f0..b03b111 100644 --- a/certora/specs/termRepoServicer/minting.spec +++ b/certora/specs/termRepoServicer/minting.spec @@ -6,7 +6,6 @@ using TermRepoToken as mintingRepoToken; using DummyERC20A as mintingToken; methods { - function SPECIALIST_ROLE() external returns (bytes32) envfree; function collateralBalance(address,uint256) external returns (uint256) envfree; function endOfRepurchaseWindow() external returns (uint256) envfree; function getBorrowerRepurchaseObligation(address) external returns (uint256) envfree; @@ -46,6 +45,8 @@ methods { function DummyERC20A.allowance(address,address) external returns(uint256) envfree; function DummyERC20A.balanceOf(address) external returns(uint256) envfree; function DummyERC20A.totalSupply() external returns(uint256) envfree; + + function TermController.verifyMintExposureAccess(address) external returns (bool) envfree; } @@ -188,7 +189,7 @@ rule mintOpenExposureRevertConditions(env e) { require(mintingCollateralManager.encumberedCollateralBalance(mintingToken) + collateralAmounts[0] <= max_uint256 ); require(mintingCollateralManager.getCollateralBalance(e.msg.sender, mintingToken) + collateralAmounts[0] <= max_uint256); bool payable = e.msg.value > 0; - bool callerNotSpecialist = !hasRole(SPECIALIST_ROLE(), e.msg.sender); + bool callerNotSpecialist = !mintingController.verifyMintExposureAccess(e.msg.sender); bool noMinterRole = !mintingRepoToken.hasRole(mintingRepoToken.MINTER_ROLE(), currentContract); bool noServicerRoleToCollatManager = !mintingCollateralManager.hasRole(mintingCollateralManager.SERVICER_ROLE(), currentContract); bool borrowerNotEnoughCollateralBalance = mintingToken.balanceOf(e.msg.sender) < collateralAmounts[0]; diff --git a/certora/specs/termRepoServicer/redemptions.spec b/certora/specs/termRepoServicer/redemptions.spec index f792a0c..9b42769 100644 --- a/certora/specs/termRepoServicer/redemptions.spec +++ b/certora/specs/termRepoServicer/redemptions.spec @@ -29,6 +29,7 @@ methods { function TermRepoToken.BURNER_ROLE() external returns (bytes32) envfree; function TermRepoToken.burningPaused() external returns (bool) envfree; function TermRepoToken.mintExposureCap() external returns (uint256) envfree; + function TermRepoToken.totalSupply() external returns (uint256) envfree; function TermRepoToken.hasRole(bytes32,address) external returns (bool) envfree; function tokenRedempt.allowance(address,address) external returns(uint256) envfree; function tokenRedempt.balanceOf(address) external returns(uint256) envfree; diff --git a/certora/specs/termRepoServicer/repayments.spec b/certora/specs/termRepoServicer/repayments.spec index 4762d06..2d6313e 100644 --- a/certora/specs/termRepoServicer/repayments.spec +++ b/certora/specs/termRepoServicer/repayments.spec @@ -170,6 +170,8 @@ rule repaymentsRevertingConditions(env e){ } bool payable = e.msg.value > 0; + bool zeroRepayment = repayment == 0; + bool maxRepaymentZero = maxRepayment == 0; bool lockerTransfersPaused = locker.transfersPaused(); bool noLockerServicerAccess = !locker.hasRole(locker.SERVICER_ROLE(), currentContract); bool allowanceTooLow = token.allowance( borrower, termRepoLocker()) < repayment; @@ -180,7 +182,7 @@ rule repaymentsRevertingConditions(env e){ bool repaymentGreaterThanMax = repaymentAmount > maxRepayment; bool noServicerRoleOnCollateralManager = !repaymentCollateralManager.hasRole(repaymentCollateralManager.SERVICER_ROLE(), currentContract); - bool isExpectedToRevert = payable || lockerTransfersPaused || noLockerServicerAccess || borrowTokenBalanceTooLow || allowanceTooLow || afterRepurchaseWindow || borrowerZeroObligation || uintMaxRepayment || repaymentGreaterThanMax || noServicerRoleOnCollateralManager; + bool isExpectedToRevert = payable || zeroRepayment || maxRepaymentZero || lockerTransfersPaused || noLockerServicerAccess || borrowTokenBalanceTooLow || allowanceTooLow || afterRepurchaseWindow || borrowerZeroObligation || uintMaxRepayment || repaymentGreaterThanMax || noServicerRoleOnCollateralManager; submitRepurchasePayment@withrevert(e, repayment); diff --git a/certora/specs/termRepoServicer/rolloverExposure.spec b/certora/specs/termRepoServicer/rolloverExposure.spec index 87aa923..d55103c 100644 --- a/certora/specs/termRepoServicer/rolloverExposure.spec +++ b/certora/specs/termRepoServicer/rolloverExposure.spec @@ -1,3 +1,4 @@ +using TermController as rolloverExposureController; using TermRepoLocker as rolloverExposureLocker; using TermRepoRolloverManager as rolloverExposureRolloverManager; using TermRepoCollateralManagerHarness as rolloverExposureRepaymentCollateralManager; @@ -34,6 +35,7 @@ methods { function DummyERC20A.allowance(address,address) external returns(uint256) envfree; function DummyERC20A.balanceOf(address) external returns(uint256) envfree; function DummyERC20A.totalSupply() external returns(uint256) envfree; + } rule openExposureOnRolloverNewIntegrity(env e) { @@ -50,6 +52,7 @@ rule openExposureOnRolloverNewIntegrity(env e) { require(rolloverExposureLocker != previousTermRepoLocker); require(rolloverExposureLocker != 100); // Protecting locker from using treasury address; require(previousTermRepoLocker != 100); // Protecting previous locker from using treasury address; + require(e.msg.sender != 0); // Protecting from zero address mathint balanceBefore = getBorrowerRepurchaseObligation(borrower); mathint tokenBalanceTermRepoLockerBefore = rolloverExposureToken.balanceOf(rolloverExposureLocker); diff --git a/certora/specs/termRepoServicer/rules.spec b/certora/specs/termRepoServicer/rules.spec index 8afce09..212c077 100644 --- a/certora/specs/termRepoServicer/rules.spec +++ b/certora/specs/termRepoServicer/rules.spec @@ -26,8 +26,8 @@ methods { // function _.transferTokenToWallet(address,address,uint256) external => DISPATCHER(true); // TermController - function _.getTreasuryAddress() external => ALWAYS(100); - function _.getProtocolReserveAddress() external => ALWAYS(100); + function TermController.getTreasuryAddress() external returns (address) => ALWAYS(100); + function TermController.getProtocolReserveAddress() external returns (address) => ALWAYS(100); // // TermRepoRolloverManager @@ -80,7 +80,5 @@ use rule onlyRoleCanCallStorage; use rule openExposureOnRolloverNewIntegrity; use rule openExposureOnRolloverNewDoesNotAffectThirdParty; -use rule openExposureOnRolloverNewRevertConditions; use rule closeExposureOnRolloverExistingIntegrity; use rule closeExposureOnRolloverExistingDoesNotAffectThirdParty; -use rule closeExposureOnRolloverExistingRevertConditions; diff --git a/certora/specs/termRepoServicer/rulesMintCollapse.spec b/certora/specs/termRepoServicer/rulesMintCollapse.spec index abe08c8..8e766f7 100644 --- a/certora/specs/termRepoServicer/rulesMintCollapse.spec +++ b/certora/specs/termRepoServicer/rulesMintCollapse.spec @@ -60,5 +60,4 @@ use rule burnCollapseExposureIntegrity; use rule burnCollapseExposureDoesNotAffectThirdParty; use rule mintOpenExposureMonotonicBehavior; -use rule mintOpenExposureIntegrity; use rule mintOpenExposureDoesNotAffectThirdParty; diff --git a/certora/specs/termRepoServicer/rulesMintIntegrity.spec b/certora/specs/termRepoServicer/rulesMintIntegrity.spec new file mode 100644 index 0000000..11d4d8e --- /dev/null +++ b/certora/specs/termRepoServicer/rulesMintIntegrity.spec @@ -0,0 +1,58 @@ +import "../methods/erc20Methods.spec"; +import "../methods/emitMethods.spec"; +import "./collapses.spec"; +import "./minting.spec"; +import "./stateVariables.spec"; + + +methods { + function upgradeToAndCall(address,bytes) external => NONDET DELETE; + function _.usdValueOfTokens(address,uint256) external => NONDET DELETE; + function _.div_(uint256 x, uint256 y) internal => divCVL(x,y) expect uint256; + function _.mul_(uint256 x, uint256 y) internal => mulCVL(x,y) expect uint256; + + // // TermRepoToken + // function _.totalRedemptionValue() external => DISPATCHER(true); + // function _.redemptionValue() external => DISPATCHER(true); + // function _.burnAndReturnValue(address,uint256) external => DISPATCHER(true); + // function _.mintRedemptionValue(address,uint256) external => DISPATCHER(true); + // function _.mintTokens(address,uint256) external => DISPATCHER(true); + // function _.decrementMintExposureCap(uint256) external => DISPATCHER(true); + // function _.burn(address,uint256) external => DISPATCHER(true); + + // TermRepoLocker + // function _.transferTokenFromWallet(address,address,uint256) external => DISPATCHER(true); + // function _.transferTokenToWallet(address,address,uint256) external => DISPATCHER(true); + + // TermController + function _.getTreasuryAddress() external => ALWAYS(100); + function _.getProtocolReserveAddress() external => ALWAYS(100); + + + // // TermRepoRolloverManager + // function _.getRolloverInstructions(address) external => DISPATCHER(true); + // function _.fulfillRollover(address) external => DISPATCHER(true); + + // // TermRepoCollateralManager + // function _.numOfAcceptedCollateralTokens() external => DISPATCHER(true); + // function _.collateralTokens() external => DISPATCHER(true); + // function _.collateralTokens(uint256) external => DISPATCHER(true); + // function _.calculateMintableExposure(address,uint256) external => DISPATCHER(true); + // function _.encumberedCollateralRemaining() external => DISPATCHER(true); + // function _.unlockCollateralOnRepurchase(address) external => DISPATCHER(true); + // function _.journalBidCollateralToCollateralManager(address,address[],uint256[]) external => DISPATCHER(true); + // function _.mintOpenExposureLockCollateral(address,address,uint256) external => DISPATCHER(true); +} + +function mulCVL(uint256 x, uint256 y) returns uint256 { + return require_uint256(x * y); +} + +function divCVL(uint256 x, uint256 y) returns uint256 { + require y != 0; + return require_uint256(x / y); +} + + +use invariant totalOutstandingRepurchaseExposureIsSumOfRepurchases; +use rule mintOpenExposureIntegrity; diff --git a/certora/specs/termRepoServicer/rulesRedemptionsReverts.spec b/certora/specs/termRepoServicer/rulesRedemptionsReverts.spec new file mode 100644 index 0000000..8e64c4f --- /dev/null +++ b/certora/specs/termRepoServicer/rulesRedemptionsReverts.spec @@ -0,0 +1,57 @@ +import "../methods/erc20Methods.spec"; +import "../methods/emitMethods.spec"; +import "./redemptions.spec"; +import "./stateVariables.spec"; + + +methods { + function upgradeToAndCall(address,bytes) external => NONDET DELETE; + function _.usdValueOfTokens(address,uint256) external => NONDET DELETE; + function _.div_(uint256 x, uint256 y) internal => divCVL(x,y) expect uint256; + function _.mul_(uint256 x, uint256 y) internal => mulCVL(x,y) expect uint256; + + // // TermRepoToken + // function _.totalRedemptionValue() external => DISPATCHER(true); + // function _.redemptionValue() external => DISPATCHER(true); + // function _.burnAndReturnValue(address,uint256) external => DISPATCHER(true); + // function _.mintRedemptionValue(address,uint256) external => DISPATCHER(true); + // function _.mintTokens(address,uint256) external => DISPATCHER(true); + // function _.decrementMintExposureCap(uint256) external => DISPATCHER(true); + // function _.burn(address,uint256) external => DISPATCHER(true); + + // TermRepoLocker + // function _.transferTokenFromWallet(address,address,uint256) external => DISPATCHER(true); + // function _.transferTokenToWallet(address,address,uint256) external => DISPATCHER(true); + + // TermController + function _.getTreasuryAddress() external => ALWAYS(100); + function _.getProtocolReserveAddress() external => ALWAYS(100); + + + // // TermRepoRolloverManager + // function _.getRolloverInstructions(address) external => DISPATCHER(true); + // function _.fulfillRollover(address) external => DISPATCHER(true); + + // // TermRepoCollateralManager + // function _.numOfAcceptedCollateralTokens() external => DISPATCHER(true); + // function _.collateralTokens() external => DISPATCHER(true); + // function _.collateralTokens(uint256) external => DISPATCHER(true); + // function _.calculateMintableExposure(address,uint256) external => DISPATCHER(true); + // function _.encumberedCollateralRemaining() external => DISPATCHER(true); + // function _.unlockCollateralOnRepurchase(address) external => DISPATCHER(true); + // function _.journalBidCollateralToCollateralManager(address,address[],uint256[]) external => DISPATCHER(true); + // function _.mintOpenExposureLockCollateral(address,address,uint256) external => DISPATCHER(true); +} + +function mulCVL(uint256 x, uint256 y) returns uint256 { + return require_uint256(x * y); +} + +function divCVL(uint256 x, uint256 y) returns uint256 { + require y != 0; + return require_uint256(x / y); +} + +use invariant totalOutstandingRepurchaseExposureIsSumOfRepurchases; + +use rule redemptionsRevertConditions; diff --git a/certora/specs/termRepoServicer/rulesRepaymentsRedemptionsReverts.spec b/certora/specs/termRepoServicer/rulesRepaymentsReverts.spec similarity index 97% rename from certora/specs/termRepoServicer/rulesRepaymentsRedemptionsReverts.spec rename to certora/specs/termRepoServicer/rulesRepaymentsReverts.spec index 0cfea59..b40c0e3 100644 --- a/certora/specs/termRepoServicer/rulesRepaymentsRedemptionsReverts.spec +++ b/certora/specs/termRepoServicer/rulesRepaymentsReverts.spec @@ -1,7 +1,6 @@ import "../methods/erc20Methods.spec"; import "../methods/emitMethods.spec"; import "./liquidationRepayment.spec"; -import "./redemptions.spec"; import "./repayments.spec"; import "./stateVariables.spec"; @@ -56,6 +55,4 @@ function divCVL(uint256 x, uint256 y) returns uint256 { use invariant totalOutstandingRepurchaseExposureIsSumOfRepurchases; -use rule redemptionsRevertConditions; - use rule repaymentsRevertingConditions; diff --git a/certora/specs/termRepoServicer/rulesRolloverReverts.spec b/certora/specs/termRepoServicer/rulesRolloverReverts.spec new file mode 100644 index 0000000..5aea4e5 --- /dev/null +++ b/certora/specs/termRepoServicer/rulesRolloverReverts.spec @@ -0,0 +1,60 @@ +import "../methods/erc20Methods.spec"; +import "../methods/emitMethods.spec"; +import "../common/isTermContractPaired.spec"; +import "../complexity.spec"; +import "./accessRoles.spec"; +import "./rolloverExposure.spec"; +import "./stateVariables.spec"; + +methods { + function upgradeToAndCall(address,bytes) external => NONDET DELETE; + function _.usdValueOfTokens(address,uint256) external => NONDET DELETE; + function _.div_(uint256 x, uint256 y) internal => divCVL(x,y) expect uint256; + function _.mul_(uint256 x, uint256 y) internal => mulCVL(x,y) expect uint256; + + // // TermRepoToken + // function _.totalRedemptionValue() external => DISPATCHER(true); + // function _.redemptionValue() external => DISPATCHER(true); + // function _.burnAndReturnValue(address,uint256) external => DISPATCHER(true); + // function _.mintRedemptionValue(address,uint256) external => DISPATCHER(true); + // function _.mintTokens(address,uint256) external => DISPATCHER(true); + // function _.decrementMintExposureCap(uint256) external => DISPATCHER(true); + // function _.burn(address,uint256) external => DISPATCHER(true); + + // TermRepoLocker + // function _.transferTokenFromWallet(address,address,uint256) external => DISPATCHER(true); + // function _.transferTokenToWallet(address,address,uint256) external => DISPATCHER(true); + + // TermController + function TermController.getTreasuryAddress() external returns (address) => ALWAYS(100); + function TermController.getProtocolReserveAddress() external returns (address) => ALWAYS(100); + + + // // TermRepoRolloverManager + // function _.getRolloverInstructions(address) external => DISPATCHER(true); + // function _.fulfillRollover(address) external => DISPATCHER(true); + + // // TermRepoCollateralManager + // function _.numOfAcceptedCollateralTokens() external => DISPATCHER(true); + // function _.collateralTokens() external => DISPATCHER(true); + // function _.collateralTokens(uint256) external => DISPATCHER(true); + // function _.calculateMintableExposure(address,uint256) external => DISPATCHER(true); + // function _.encumberedCollateralRemaining() external => DISPATCHER(true); + // function _.unlockCollateralOnRepurchase(address) external => DISPATCHER(true); + // function _.journalBidCollateralToCollateralManager(address,address[],uint256[]) external => DISPATCHER(true); + // function _.mintOpenExposureLockCollateral(address,address,uint256) external => DISPATCHER(true); +} + +function mulCVL(uint256 x, uint256 y) returns uint256 { + return require_uint256(x * y); +} + +function divCVL(uint256 x, uint256 y) returns uint256 { + require y != 0; + return require_uint256(x / y); +} + +use invariant totalOutstandingRepurchaseExposureIsSumOfRepurchases; + +use rule openExposureOnRolloverNewRevertConditions; +use rule closeExposureOnRolloverExistingRevertConditions; diff --git a/contracts/TermRepoServicer.sol b/contracts/TermRepoServicer.sol index 673a5d9..5a02065 100644 --- a/contracts/TermRepoServicer.sol +++ b/contracts/TermRepoServicer.sol @@ -46,7 +46,6 @@ contract TermRepoServicer is bytes32 public constant COLLATERAL_MANAGER = keccak256("COLLATERAL_MANAGER"); bytes32 public constant DEVOPS_ROLE = keccak256("DEVOPS_ROLE"); - bytes32 public constant SPECIALIST_ROLE = keccak256("SPECIALIST_ROLE"); bytes32 public constant ROLLOVER_MANAGER = keccak256("ROLLOVER_MANAGER"); bytes32 public constant ROLLOVER_TARGET_AUCTIONEER_ROLE = keccak256("ROLLOVER_TARGET_AUCTIONEER_ROLE");