From 719007cdd556e371f1d710c16a156da32999d878 Mon Sep 17 00:00:00 2001 From: Andrew Zhou Date: Thu, 20 Jun 2024 14:08:38 -0700 Subject: [PATCH 01/47] certora updates --- certora/confs/termAuctionBidLocker-locking.conf | 2 +- certora/confs/termAuctionBidLocker-lockingReverts.conf | 2 +- certora/confs/termAuctionBidLocker-stateVariables.conf | 2 +- certora/confs/termAuctionBidLocker.conf | 2 +- certora/confs/termRepoCollateralManager-batchDefault.conf | 2 +- certora/confs/termRepoCollateralManager-batchLiquidation.conf | 2 +- ...termRepoCollateralManager-batchLiquidationWithRepoToken.conf | 2 +- certora/confs/termRepoCollateralManager-stateVariables.conf | 2 +- certora/confs/termRepoCollateralManager.conf | 2 +- certora/confs/termRepoServicer-lockFulfill.conf | 2 +- certora/confs/termRepoServicer-lockFulfillReverts.conf | 2 +- certora/confs/termRepoServicer-mintCollapse.conf | 2 +- certora/confs/termRepoServicer-mintCollapseReverts.conf | 2 +- certora/confs/termRepoServicer-repaymentsRedemptions.conf | 2 +- .../confs/termRepoServicer-repaymentsRedemptionsReverts.conf | 2 +- certora/confs/termRepoServicer.conf | 2 +- 16 files changed, 16 insertions(+), 16 deletions(-) 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/termRepoServicer-lockFulfill.conf b/certora/confs/termRepoServicer-lockFulfill.conf index 1b4216d..b95ba0f 100644 --- a/certora/confs/termRepoServicer-lockFulfill.conf +++ b/certora/confs/termRepoServicer-lockFulfill.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-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..6d3503d 100644 --- a/certora/confs/termRepoServicer-mintCollapse.conf +++ b/certora/confs/termRepoServicer-mintCollapse.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": [ "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-repaymentsRedemptions.conf b/certora/confs/termRepoServicer-repaymentsRedemptions.conf index 391f87d..7d9dbf8 100644 --- a/certora/confs/termRepoServicer-repaymentsRedemptions.conf +++ b/certora/confs/termRepoServicer-repaymentsRedemptions.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", diff --git a/certora/confs/termRepoServicer-repaymentsRedemptionsReverts.conf b/certora/confs/termRepoServicer-repaymentsRedemptionsReverts.conf index f668ece..a989287 100644 --- a/certora/confs/termRepoServicer-repaymentsRedemptionsReverts.conf +++ b/certora/confs/termRepoServicer-repaymentsRedemptionsReverts.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", diff --git a/certora/confs/termRepoServicer.conf b/certora/confs/termRepoServicer.conf index c26e4b0..4f057fe 100644 --- a/certora/confs/termRepoServicer.conf +++ b/certora/confs/termRepoServicer.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": [ "TermRepoServicerHarness" From 8acea2924920efc8937407d4fbb4fc9ac87a1a76 Mon Sep 17 00:00:00 2001 From: Andrew Zhou Date: Thu, 20 Jun 2024 14:20:20 -0700 Subject: [PATCH 02/47] ignore solidity warnings in servicer --- certora/confs/termRepoServicer-stateVariables.conf | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/certora/confs/termRepoServicer-stateVariables.conf b/certora/confs/termRepoServicer-stateVariables.conf index 033e07b..b1cbd77 100644 --- a/certora/confs/termRepoServicer-stateVariables.conf +++ b/certora/confs/termRepoServicer-stateVariables.conf @@ -25,7 +25,7 @@ "-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", From 23c8feab8cf311c1441957dad7fb62e1f64e641e Mon Sep 17 00:00:00 2001 From: Andrew Zhou Date: Thu, 20 Jun 2024 14:30:21 -0700 Subject: [PATCH 03/47] ignore solidity warnings rollover manager --- certora/confs/termRepoRolloverManager.conf | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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" ], From d1832fda780f285d2a9ddffab0feecaec5f91656 Mon Sep 17 00:00:00 2001 From: Andrew Zhou Date: Thu, 20 Jun 2024 22:59:02 -0700 Subject: [PATCH 04/47] replace newSplitParallel certora config proverarg --- certora/confs/termRepoServicer-lockFulfill.conf | 2 +- certora/confs/termRepoServicer-mintCollapse.conf | 2 +- certora/confs/termRepoServicer-repaymentsRedemptions.conf | 2 +- certora/confs/termRepoServicer.conf | 2 +- 4 files changed, 4 insertions(+), 4 deletions(-) diff --git a/certora/confs/termRepoServicer-lockFulfill.conf b/certora/confs/termRepoServicer-lockFulfill.conf index b95ba0f..28dd3b6 100644 --- a/certora/confs/termRepoServicer-lockFulfill.conf +++ b/certora/confs/termRepoServicer-lockFulfill.conf @@ -20,7 +20,7 @@ "-smt_initialSplitDepth 5", "-depth 15", "-mediumTimeout 20", - "-newSplitParallel true", + "-splitParallel true", "-splitParallelTimelimit 7200", "-splitParallelInitialDepth 10" ], diff --git a/certora/confs/termRepoServicer-mintCollapse.conf b/certora/confs/termRepoServicer-mintCollapse.conf index 6d3503d..9805322 100644 --- a/certora/confs/termRepoServicer-mintCollapse.conf +++ b/certora/confs/termRepoServicer-mintCollapse.conf @@ -20,7 +20,7 @@ "-smt_initialSplitDepth 5", "-depth 15", "-mediumTimeout 2", - "-newSplitParallel true", + "-splitParallel true", "-splitParallelTimelimit 7200", "-splitParallelInitialDepth 5" ], diff --git a/certora/confs/termRepoServicer-repaymentsRedemptions.conf b/certora/confs/termRepoServicer-repaymentsRedemptions.conf index 7d9dbf8..2182638 100644 --- a/certora/confs/termRepoServicer-repaymentsRedemptions.conf +++ b/certora/confs/termRepoServicer-repaymentsRedemptions.conf @@ -20,7 +20,7 @@ "-smt_initialSplitDepth 5", "-depth 15", "-mediumTimeout 20", - "-newSplitParallel true", + "-splitParallel true", "-splitParallelTimelimit 7200", "-splitParallelInitialDepth 5" ], diff --git a/certora/confs/termRepoServicer.conf b/certora/confs/termRepoServicer.conf index 4f057fe..fe9bf90 100644 --- a/certora/confs/termRepoServicer.conf +++ b/certora/confs/termRepoServicer.conf @@ -20,7 +20,7 @@ "-smt_initialSplitDepth 10", "-depth 20", "-mediumTimeout 2", - "-newSplitParallel true", + "-splitParallel true", "-splitParallelTimelimit 7200", "-splitParallelInitialDepth 10" ], From 0bdb54d8b7c4cd39bd518c135e16578d9499fbef Mon Sep 17 00:00:00 2001 From: Andrew Zhou Date: Thu, 20 Jun 2024 23:35:08 -0700 Subject: [PATCH 05/47] get rid of branch versions of certora --- certora/confs/termRepoServicer-repaymentsRedemptions.conf | 1 - certora/confs/termRepoServicer-repaymentsRedemptionsReverts.conf | 1 - 2 files changed, 2 deletions(-) diff --git a/certora/confs/termRepoServicer-repaymentsRedemptions.conf b/certora/confs/termRepoServicer-repaymentsRedemptions.conf index 2182638..920c5cc 100644 --- a/certora/confs/termRepoServicer-repaymentsRedemptions.conf +++ b/certora/confs/termRepoServicer-repaymentsRedemptions.conf @@ -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-repaymentsRedemptionsReverts.conf index a989287..bc9a75c 100644 --- a/certora/confs/termRepoServicer-repaymentsRedemptionsReverts.conf +++ b/certora/confs/termRepoServicer-repaymentsRedemptionsReverts.conf @@ -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" } \ No newline at end of file From 15871d741177c359e90bd3018843370af78f6350 Mon Sep 17 00:00:00 2001 From: Andrew Zhou Date: Fri, 21 Jun 2024 00:06:19 -0700 Subject: [PATCH 06/47] replace newSplitParallel certora config proverarg --- certora/confs/termRepoServicer-stateVariables.conf | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/certora/confs/termRepoServicer-stateVariables.conf b/certora/confs/termRepoServicer-stateVariables.conf index b1cbd77..eb5cc67 100644 --- a/certora/confs/termRepoServicer-stateVariables.conf +++ b/certora/confs/termRepoServicer-stateVariables.conf @@ -20,7 +20,7 @@ "-smt_initialSplitDepth 10", "-depth 20", "-mediumTimeout 2", - "-newSplitParallel true", + "-splitParallel true", "-splitParallelTimelimit 7200", "-splitParallelInitialDepth 10" ], From 3e15dce966f335c19745216e87f5f6a22e7fbe72 Mon Sep 17 00:00:00 2001 From: Andrew Zhou Date: Fri, 21 Jun 2024 10:49:49 -0700 Subject: [PATCH 07/47] update access roles test for servicer with new controller function for mint access --- certora/specs/termRepoServicer/accessRoles.spec | 13 +++++++++---- 1 file changed, 9 insertions(+), 4 deletions(-) diff --git a/certora/specs/termRepoServicer/accessRoles.spec b/certora/specs/termRepoServicer/accessRoles.spec index 89c4f28..40be95b 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,9 +12,10 @@ 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 TermController.verifyMintExposureAccess(address) external returns(bool) envfree; } @@ -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.msg.sender); } rule onlyRoleCanCallStorage(method f, calldataarg args, env e) filtered { @@ -67,5 +71,6 @@ rule onlyRoleCanCallStorage(method f, calldataarg args, env e) filtered { || 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.msg.sender);; } \ No newline at end of file From 793cd2b07b0144a98a6de283366d6d98186ae626 Mon Sep 17 00:00:00 2001 From: Andrew Zhou Date: Fri, 21 Jun 2024 11:02:39 -0700 Subject: [PATCH 08/47] remove extra semicolon --- certora/specs/termRepoServicer/accessRoles.spec | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/certora/specs/termRepoServicer/accessRoles.spec b/certora/specs/termRepoServicer/accessRoles.spec index 40be95b..e9c206f 100644 --- a/certora/specs/termRepoServicer/accessRoles.spec +++ b/certora/specs/termRepoServicer/accessRoles.spec @@ -72,5 +72,5 @@ rule onlyRoleCanCallStorage(method f, calldataarg args, env e) filtered { || hasRole(ROLLOVER_MANAGER(),e.msg.sender) || hasRole(ROLLOVER_TARGET_AUCTIONEER_ROLE(),e.msg.sender) || hasRole(INITIALIZER_ROLE(),e.msg.sender) - || servicerAccessController.verifyMintExposureAccess(e.msg.sender);; + || servicerAccessController.verifyMintExposureAccess(e.msg.sender); } \ No newline at end of file From cd55e0fe60633c15776e496cb11c00bd2bc2d710 Mon Sep 17 00:00:00 2001 From: Andrew Zhou Date: Fri, 21 Jun 2024 11:22:58 -0700 Subject: [PATCH 09/47] remove specialist role from servicer specs certora --- certora/specs/termRepoServicer/accessRoles.spec | 1 - 1 file changed, 1 deletion(-) diff --git a/certora/specs/termRepoServicer/accessRoles.spec b/certora/specs/termRepoServicer/accessRoles.spec index e9c206f..21e664d 100644 --- a/certora/specs/termRepoServicer/accessRoles.spec +++ b/certora/specs/termRepoServicer/accessRoles.spec @@ -68,7 +68,6 @@ 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) From d148d865fb423ff0cf6e184ed82dd1ee71681a69 Mon Sep 17 00:00:00 2001 From: Andrew Zhou Date: Fri, 21 Jun 2024 14:06:35 -0700 Subject: [PATCH 10/47] link controller to servicer in servicer spec for certora --- certora/confs/termRepoServicer.conf | 1 + 1 file changed, 1 insertion(+) diff --git a/certora/confs/termRepoServicer.conf b/certora/confs/termRepoServicer.conf index fe9bf90..bb7fa3b 100644 --- a/certora/confs/termRepoServicer.conf +++ b/certora/confs/termRepoServicer.conf @@ -13,6 +13,7 @@ "TermRepoServicerHarness:termRepoToken=TermRepoToken", "TermRepoServicerHarness:termRepoLocker=TermRepoLocker", "TermRepoServicerHarness:termRepoCollateralManager=TermRepoCollateralManagerHarness", + "TermRepoServicerHarness:termController=TermController", "TermRepoServicerHarness:termRepoRolloverManager=TermRepoRolloverManager", "TermRepoCollateralManagerHarness:termRepoLocker=TermRepoLocker" ], From fa90c26339ea4752effc39a367e69fa32753d28b Mon Sep 17 00:00:00 2001 From: Andrew Zhou Date: Fri, 21 Jun 2024 14:55:22 -0700 Subject: [PATCH 11/47] prevent previous term locker from conflicting with controller treasury address --- certora/specs/termRepoServicer/rolloverExposure.spec | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/certora/specs/termRepoServicer/rolloverExposure.spec b/certora/specs/termRepoServicer/rolloverExposure.spec index 87aa923..dd8f706 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; @@ -50,6 +51,9 @@ 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(rolloverExposureController.getTreasuryAddress() != e.msg.sender); // Protecting treasury from calling this function + require(rolloverExposureController.getTreasuryAddress() != rolloverExposureLocker); // Protecting locker from using treasury address; + require(rolloverExposureController.getTreasuryAddress() != previousTermRepoLocker); // Protecting previous locker from using treasury address; mathint balanceBefore = getBorrowerRepurchaseObligation(borrower); mathint tokenBalanceTermRepoLockerBefore = rolloverExposureToken.balanceOf(rolloverExposureLocker); From 46214740c0e9aa855b1184c2d967a485fa91876e Mon Sep 17 00:00:00 2001 From: Andrew Zhou Date: Fri, 21 Jun 2024 15:26:45 -0700 Subject: [PATCH 12/47] add envfree declaration of get treasury address to rollover exposure certora spec --- certora/specs/termRepoServicer/rolloverExposure.spec | 2 ++ 1 file changed, 2 insertions(+) diff --git a/certora/specs/termRepoServicer/rolloverExposure.spec b/certora/specs/termRepoServicer/rolloverExposure.spec index dd8f706..6c6bc90 100644 --- a/certora/specs/termRepoServicer/rolloverExposure.spec +++ b/certora/specs/termRepoServicer/rolloverExposure.spec @@ -35,6 +35,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.getTreasuryAddress() external returns (address) envfree; } rule openExposureOnRolloverNewIntegrity(env e) { From 42a611ee1fa22f4d3770d6aefd8d7909e510c5cf Mon Sep 17 00:00:00 2001 From: Andrew Zhou Date: Fri, 21 Jun 2024 16:01:39 -0700 Subject: [PATCH 13/47] no zero address msg sender in exposure opening on new rollover certora --- certora/specs/termRepoServicer/rolloverExposure.spec | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/certora/specs/termRepoServicer/rolloverExposure.spec b/certora/specs/termRepoServicer/rolloverExposure.spec index 6c6bc90..a9d699a 100644 --- a/certora/specs/termRepoServicer/rolloverExposure.spec +++ b/certora/specs/termRepoServicer/rolloverExposure.spec @@ -56,7 +56,8 @@ rule openExposureOnRolloverNewIntegrity(env e) { require(rolloverExposureController.getTreasuryAddress() != e.msg.sender); // Protecting treasury from calling this function require(rolloverExposureController.getTreasuryAddress() != rolloverExposureLocker); // Protecting locker from using treasury address; require(rolloverExposureController.getTreasuryAddress() != previousTermRepoLocker); // 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); mathint tokenBalancePreviousTermRepoLockerBefore = rolloverExposureToken.balanceOf(previousTermRepoLocker); From 4faeef2aee3be840e1d198641790afbbe1be0d98 Mon Sep 17 00:00:00 2001 From: Andrew Zhou Date: Fri, 21 Jun 2024 16:25:30 -0700 Subject: [PATCH 14/47] treasuery cannot be borrow address --- certora/specs/termRepoServicer/rolloverExposure.spec | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/certora/specs/termRepoServicer/rolloverExposure.spec b/certora/specs/termRepoServicer/rolloverExposure.spec index a9d699a..9c1cb39 100644 --- a/certora/specs/termRepoServicer/rolloverExposure.spec +++ b/certora/specs/termRepoServicer/rolloverExposure.spec @@ -57,7 +57,8 @@ rule openExposureOnRolloverNewIntegrity(env e) { require(rolloverExposureController.getTreasuryAddress() != rolloverExposureLocker); // Protecting locker from using treasury address; require(rolloverExposureController.getTreasuryAddress() != previousTermRepoLocker); // Protecting previous locker from using treasury address; require(e.msg.sender != 0); // Protecting from zero address - + require(e.msg.sender != borrower); // Protecting from borrower address + mathint balanceBefore = getBorrowerRepurchaseObligation(borrower); mathint tokenBalanceTermRepoLockerBefore = rolloverExposureToken.balanceOf(rolloverExposureLocker); mathint tokenBalancePreviousTermRepoLockerBefore = rolloverExposureToken.balanceOf(previousTermRepoLocker); From 9bb35943d0d2f6caa02cdeffebea23de4656cc9f Mon Sep 17 00:00:00 2001 From: Andrew Zhou Date: Fri, 21 Jun 2024 16:44:47 -0700 Subject: [PATCH 15/47] treasuery cannot be borrow address --- certora/specs/termRepoServicer/rolloverExposure.spec | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/certora/specs/termRepoServicer/rolloverExposure.spec b/certora/specs/termRepoServicer/rolloverExposure.spec index 9c1cb39..2ddc244 100644 --- a/certora/specs/termRepoServicer/rolloverExposure.spec +++ b/certora/specs/termRepoServicer/rolloverExposure.spec @@ -57,7 +57,7 @@ rule openExposureOnRolloverNewIntegrity(env e) { require(rolloverExposureController.getTreasuryAddress() != rolloverExposureLocker); // Protecting locker from using treasury address; require(rolloverExposureController.getTreasuryAddress() != previousTermRepoLocker); // Protecting previous locker from using treasury address; require(e.msg.sender != 0); // Protecting from zero address - require(e.msg.sender != borrower); // Protecting from borrower address + require(rolloverExposureController.getTreasuryAddress() != borrower); // Protecting from borrower address mathint balanceBefore = getBorrowerRepurchaseObligation(borrower); mathint tokenBalanceTermRepoLockerBefore = rolloverExposureToken.balanceOf(rolloverExposureLocker); From 4838471230f6b8d225bdcac0e19a746d4d18076d Mon Sep 17 00:00:00 2001 From: Andrew Zhou Date: Fri, 21 Jun 2024 17:42:35 -0700 Subject: [PATCH 16/47] treasuery address always 100 --- certora/specs/termRepoServicer/rolloverExposure.spec | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/certora/specs/termRepoServicer/rolloverExposure.spec b/certora/specs/termRepoServicer/rolloverExposure.spec index 2ddc244..78bf36a 100644 --- a/certora/specs/termRepoServicer/rolloverExposure.spec +++ b/certora/specs/termRepoServicer/rolloverExposure.spec @@ -36,7 +36,8 @@ methods { function DummyERC20A.balanceOf(address) external returns(uint256) envfree; function DummyERC20A.totalSupply() external returns(uint256) envfree; - function TermController.getTreasuryAddress() external returns (address) envfree; + function _.getTreasuryAddress() external => ALWAYS(100); + } rule openExposureOnRolloverNewIntegrity(env e) { From 84687553a70aa1ed48f6cde7137abbeeb76c6651 Mon Sep 17 00:00:00 2001 From: Andrew Zhou Date: Fri, 21 Jun 2024 17:52:29 -0700 Subject: [PATCH 17/47] treasuery address always 100 --- certora/specs/termRepoServicer/rolloverExposure.spec | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/certora/specs/termRepoServicer/rolloverExposure.spec b/certora/specs/termRepoServicer/rolloverExposure.spec index 78bf36a..62b922a 100644 --- a/certora/specs/termRepoServicer/rolloverExposure.spec +++ b/certora/specs/termRepoServicer/rolloverExposure.spec @@ -36,7 +36,7 @@ methods { function DummyERC20A.balanceOf(address) external returns(uint256) envfree; function DummyERC20A.totalSupply() external returns(uint256) envfree; - function _.getTreasuryAddress() external => ALWAYS(100); + function TermController.getTreasuryAddress() external => ALWAYS(100); } From 7da828e479c1812994e8af17d57ce712e8c83c4a Mon Sep 17 00:00:00 2001 From: Andrew Zhou Date: Fri, 21 Jun 2024 18:06:52 -0700 Subject: [PATCH 18/47] 100 address for treasury imported from rules for servicer --- certora/specs/termRepoServicer/rolloverExposure.spec | 6 ------ 1 file changed, 6 deletions(-) diff --git a/certora/specs/termRepoServicer/rolloverExposure.spec b/certora/specs/termRepoServicer/rolloverExposure.spec index 62b922a..d55103c 100644 --- a/certora/specs/termRepoServicer/rolloverExposure.spec +++ b/certora/specs/termRepoServicer/rolloverExposure.spec @@ -36,8 +36,6 @@ methods { function DummyERC20A.balanceOf(address) external returns(uint256) envfree; function DummyERC20A.totalSupply() external returns(uint256) envfree; - function TermController.getTreasuryAddress() external => ALWAYS(100); - } rule openExposureOnRolloverNewIntegrity(env e) { @@ -54,11 +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(rolloverExposureController.getTreasuryAddress() != e.msg.sender); // Protecting treasury from calling this function - require(rolloverExposureController.getTreasuryAddress() != rolloverExposureLocker); // Protecting locker from using treasury address; - require(rolloverExposureController.getTreasuryAddress() != previousTermRepoLocker); // Protecting previous locker from using treasury address; require(e.msg.sender != 0); // Protecting from zero address - require(rolloverExposureController.getTreasuryAddress() != borrower); // Protecting from borrower address mathint balanceBefore = getBorrowerRepurchaseObligation(borrower); mathint tokenBalanceTermRepoLockerBefore = rolloverExposureToken.balanceOf(rolloverExposureLocker); From 3a42c44764292cfcf460a0d0435636983a80847c Mon Sep 17 00:00:00 2001 From: Andrew Zhou Date: Sat, 22 Jun 2024 11:21:06 -0700 Subject: [PATCH 19/47] 100 address for treasury imported from rules for servicer --- certora/specs/termRepoServicer/rules.spec | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/certora/specs/termRepoServicer/rules.spec b/certora/specs/termRepoServicer/rules.spec index 8afce09..dbaaaea 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 => ALWAYS(100); + function TermController.getProtocolReserveAddress() external => ALWAYS(100); // // TermRepoRolloverManager From a7943dd9109270d19df374d75114796f3bc13ace Mon Sep 17 00:00:00 2001 From: Andrew Zhou Date: Sat, 22 Jun 2024 15:09:58 -0700 Subject: [PATCH 20/47] 100 address for treasury imported from rules for servicer --- certora/specs/termRepoServicer/rules.spec | 4 ---- 1 file changed, 4 deletions(-) diff --git a/certora/specs/termRepoServicer/rules.spec b/certora/specs/termRepoServicer/rules.spec index dbaaaea..1ab9e0f 100644 --- a/certora/specs/termRepoServicer/rules.spec +++ b/certora/specs/termRepoServicer/rules.spec @@ -25,10 +25,6 @@ methods { // function _.transferTokenFromWallet(address,address,uint256) external => DISPATCHER(true); // function _.transferTokenToWallet(address,address,uint256) external => DISPATCHER(true); - // TermController - function TermController.getTreasuryAddress() external => ALWAYS(100); - function TermController.getProtocolReserveAddress() external => ALWAYS(100); - // // TermRepoRolloverManager // function _.getRolloverInstructions(address) external => DISPATCHER(true); From d1e24e14f77667c0cf2a12ce786246d305549e8f Mon Sep 17 00:00:00 2001 From: Andrew Zhou Date: Sat, 22 Jun 2024 21:48:36 -0700 Subject: [PATCH 21/47] controller harness for certora --- certora/confs/termRepoServicer.conf | 2 +- certora/harness/TermControllerHarness.sol | 11 +++++++++++ certora/specs/termRepoServicer/accessRoles.spec | 5 +++-- certora/specs/termRepoServicer/rolloverExposure.spec | 4 +++- 4 files changed, 18 insertions(+), 4 deletions(-) create mode 100644 certora/harness/TermControllerHarness.sol diff --git a/certora/confs/termRepoServicer.conf b/certora/confs/termRepoServicer.conf index bb7fa3b..eafeb55 100644 --- a/certora/confs/termRepoServicer.conf +++ b/certora/confs/termRepoServicer.conf @@ -13,7 +13,7 @@ "TermRepoServicerHarness:termRepoToken=TermRepoToken", "TermRepoServicerHarness:termRepoLocker=TermRepoLocker", "TermRepoServicerHarness:termRepoCollateralManager=TermRepoCollateralManagerHarness", - "TermRepoServicerHarness:termController=TermController", + "TermRepoServicerHarness:termController=TermControllerHarness", "TermRepoServicerHarness:termRepoRolloverManager=TermRepoRolloverManager", "TermRepoCollateralManagerHarness:termRepoLocker=TermRepoLocker" ], diff --git a/certora/harness/TermControllerHarness.sol b/certora/harness/TermControllerHarness.sol new file mode 100644 index 0000000..61c54c6 --- /dev/null +++ b/certora/harness/TermControllerHarness.sol @@ -0,0 +1,11 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.0; + +import "../../contracts/TermController.sol"; + +contract TermControllerHarness is TermController { + function requireTreasuryWallet() external returns (uint256){ + require(treasuryWallet == 100, "treasuryWallet is not 100"); + return 100; + } +} \ No newline at end of file diff --git a/certora/specs/termRepoServicer/accessRoles.spec b/certora/specs/termRepoServicer/accessRoles.spec index 21e664d..ccbee67 100644 --- a/certora/specs/termRepoServicer/accessRoles.spec +++ b/certora/specs/termRepoServicer/accessRoles.spec @@ -1,7 +1,7 @@ import "../methods/erc20Methods.spec"; import "../methods/emitMethods.spec"; -using TermController as servicerAccessController; +using TermControllerHarness as servicerAccessController; methods { @@ -15,7 +15,7 @@ methods { function ROLLOVER_MANAGER() external returns (bytes32) envfree; function ROLLOVER_TARGET_AUCTIONEER_ROLE() external returns (bytes32) envfree; - function TermController.verifyMintExposureAccess(address) external returns(bool) envfree; + function TermControllerHarness.verifyMintExposureAccess(address) external returns(bool) envfree; } @@ -32,6 +32,7 @@ rule onlyRoleCanCallRevert(method f, calldataarg args, env e) filtered { && f.selector != sig:redeemTermRepoTokens(address,uint256).selector && f.selector != sig:redeemTermRepoTokens(address,uint256).selector } { + currentContract.termC currentContract.f@withrevert(e,args); assert !lastReverted => diff --git a/certora/specs/termRepoServicer/rolloverExposure.spec b/certora/specs/termRepoServicer/rolloverExposure.spec index d55103c..32afd72 100644 --- a/certora/specs/termRepoServicer/rolloverExposure.spec +++ b/certora/specs/termRepoServicer/rolloverExposure.spec @@ -1,4 +1,4 @@ -using TermController as rolloverExposureController; +using TermControllerHarness as rolloverExposureController; using TermRepoLocker as rolloverExposureLocker; using TermRepoRolloverManager as rolloverExposureRolloverManager; using TermRepoCollateralManagerHarness as rolloverExposureRepaymentCollateralManager; @@ -47,6 +47,8 @@ rule openExposureOnRolloverNewIntegrity(env e) { uint256 expScale = 10 ^ 18; + require(rolloverExposureController.requireTreasuryWallet() == 100); + require(purchaseToken() == rolloverExposureToken); // bounds for test require(termRepoLocker() == rolloverExposureLocker); // bounds for test require(rolloverExposureLocker != previousTermRepoLocker); From 38073be8d6a9d0394afb232f25160be2acf610e6 Mon Sep 17 00:00:00 2001 From: Andrew Zhou Date: Sat, 22 Jun 2024 21:57:49 -0700 Subject: [PATCH 22/47] controller harness for certora --- certora/confs/termRepoServicer.conf | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/certora/confs/termRepoServicer.conf b/certora/confs/termRepoServicer.conf index eafeb55..759cdc4 100644 --- a/certora/confs/termRepoServicer.conf +++ b/certora/confs/termRepoServicer.conf @@ -2,7 +2,7 @@ "files": [ "certora/harness/TermRepoServicerHarness.sol", "contracts/TermAuctionBidLocker.sol", - "contracts/TermController.sol", + "certora/harness/TermControllerHarness.sol", "contracts/TermRepoLocker.sol", "contracts/TermRepoToken.sol", "contracts/TermRepoRolloverManager.sol", From 893718866032740fa4bdb5d1fba9266d587d2e40 Mon Sep 17 00:00:00 2001 From: Andrew Zhou Date: Sat, 22 Jun 2024 22:09:13 -0700 Subject: [PATCH 23/47] fix acccess roles for servicer certora spec --- certora/specs/termRepoServicer/accessRoles.spec | 1 - 1 file changed, 1 deletion(-) diff --git a/certora/specs/termRepoServicer/accessRoles.spec b/certora/specs/termRepoServicer/accessRoles.spec index ccbee67..0d0e2ee 100644 --- a/certora/specs/termRepoServicer/accessRoles.spec +++ b/certora/specs/termRepoServicer/accessRoles.spec @@ -32,7 +32,6 @@ rule onlyRoleCanCallRevert(method f, calldataarg args, env e) filtered { && f.selector != sig:redeemTermRepoTokens(address,uint256).selector && f.selector != sig:redeemTermRepoTokens(address,uint256).selector } { - currentContract.termC currentContract.f@withrevert(e,args); assert !lastReverted => From 36af4cb2ed5d0ceed073009330f209d2e3b9e44f Mon Sep 17 00:00:00 2001 From: Andrew Zhou Date: Sat, 22 Jun 2024 22:22:59 -0700 Subject: [PATCH 24/47] 100 address for treasury imported from rules for servicer --- certora/confs/termRepoServicer.conf | 4 ++-- certora/harness/TermControllerHarness.sol | 11 ----------- certora/specs/termRepoServicer/accessRoles.spec | 4 ++-- certora/specs/termRepoServicer/rolloverExposure.spec | 4 +--- certora/specs/termRepoServicer/rules.spec | 4 ++++ 5 files changed, 9 insertions(+), 18 deletions(-) delete mode 100644 certora/harness/TermControllerHarness.sol diff --git a/certora/confs/termRepoServicer.conf b/certora/confs/termRepoServicer.conf index 759cdc4..bb7fa3b 100644 --- a/certora/confs/termRepoServicer.conf +++ b/certora/confs/termRepoServicer.conf @@ -2,7 +2,7 @@ "files": [ "certora/harness/TermRepoServicerHarness.sol", "contracts/TermAuctionBidLocker.sol", - "certora/harness/TermControllerHarness.sol", + "contracts/TermController.sol", "contracts/TermRepoLocker.sol", "contracts/TermRepoToken.sol", "contracts/TermRepoRolloverManager.sol", @@ -13,7 +13,7 @@ "TermRepoServicerHarness:termRepoToken=TermRepoToken", "TermRepoServicerHarness:termRepoLocker=TermRepoLocker", "TermRepoServicerHarness:termRepoCollateralManager=TermRepoCollateralManagerHarness", - "TermRepoServicerHarness:termController=TermControllerHarness", + "TermRepoServicerHarness:termController=TermController", "TermRepoServicerHarness:termRepoRolloverManager=TermRepoRolloverManager", "TermRepoCollateralManagerHarness:termRepoLocker=TermRepoLocker" ], diff --git a/certora/harness/TermControllerHarness.sol b/certora/harness/TermControllerHarness.sol deleted file mode 100644 index 61c54c6..0000000 --- a/certora/harness/TermControllerHarness.sol +++ /dev/null @@ -1,11 +0,0 @@ -// SPDX-License-Identifier: MIT -pragma solidity ^0.8.0; - -import "../../contracts/TermController.sol"; - -contract TermControllerHarness is TermController { - function requireTreasuryWallet() external returns (uint256){ - require(treasuryWallet == 100, "treasuryWallet is not 100"); - return 100; - } -} \ No newline at end of file diff --git a/certora/specs/termRepoServicer/accessRoles.spec b/certora/specs/termRepoServicer/accessRoles.spec index 0d0e2ee..21e664d 100644 --- a/certora/specs/termRepoServicer/accessRoles.spec +++ b/certora/specs/termRepoServicer/accessRoles.spec @@ -1,7 +1,7 @@ import "../methods/erc20Methods.spec"; import "../methods/emitMethods.spec"; -using TermControllerHarness as servicerAccessController; +using TermController as servicerAccessController; methods { @@ -15,7 +15,7 @@ methods { function ROLLOVER_MANAGER() external returns (bytes32) envfree; function ROLLOVER_TARGET_AUCTIONEER_ROLE() external returns (bytes32) envfree; - function TermControllerHarness.verifyMintExposureAccess(address) external returns(bool) envfree; + function TermController.verifyMintExposureAccess(address) external returns(bool) envfree; } diff --git a/certora/specs/termRepoServicer/rolloverExposure.spec b/certora/specs/termRepoServicer/rolloverExposure.spec index 32afd72..d55103c 100644 --- a/certora/specs/termRepoServicer/rolloverExposure.spec +++ b/certora/specs/termRepoServicer/rolloverExposure.spec @@ -1,4 +1,4 @@ -using TermControllerHarness as rolloverExposureController; +using TermController as rolloverExposureController; using TermRepoLocker as rolloverExposureLocker; using TermRepoRolloverManager as rolloverExposureRolloverManager; using TermRepoCollateralManagerHarness as rolloverExposureRepaymentCollateralManager; @@ -47,8 +47,6 @@ rule openExposureOnRolloverNewIntegrity(env e) { uint256 expScale = 10 ^ 18; - require(rolloverExposureController.requireTreasuryWallet() == 100); - require(purchaseToken() == rolloverExposureToken); // bounds for test require(termRepoLocker() == rolloverExposureLocker); // bounds for test require(rolloverExposureLocker != previousTermRepoLocker); diff --git a/certora/specs/termRepoServicer/rules.spec b/certora/specs/termRepoServicer/rules.spec index 1ab9e0f..dbaaaea 100644 --- a/certora/specs/termRepoServicer/rules.spec +++ b/certora/specs/termRepoServicer/rules.spec @@ -25,6 +25,10 @@ methods { // function _.transferTokenFromWallet(address,address,uint256) external => DISPATCHER(true); // function _.transferTokenToWallet(address,address,uint256) external => DISPATCHER(true); + // TermController + function TermController.getTreasuryAddress() external => ALWAYS(100); + function TermController.getProtocolReserveAddress() external => ALWAYS(100); + // // TermRepoRolloverManager // function _.getRolloverInstructions(address) external => DISPATCHER(true); From 3488644e14d968aa0ee4c864589f7769f5968be0 Mon Sep 17 00:00:00 2001 From: Andrew Zhou Date: Mon, 24 Jun 2024 09:22:54 -0700 Subject: [PATCH 25/47] 100 address for treasury imported from rules for servicer --- certora/specs/termRepoServicer/rules.spec | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/certora/specs/termRepoServicer/rules.spec b/certora/specs/termRepoServicer/rules.spec index dbaaaea..f6d568c 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 TermController.getTreasuryAddress() external => ALWAYS(100); - function TermController.getProtocolReserveAddress() external => ALWAYS(100); + function TermController.getTreasuryAddress() external returns (address) => ALWAYS(100); + function TermController.getProtocolReserveAddress() external returns (address) => ALWAYS(100); // // TermRepoRolloverManager From d9e997afa75d7490205b2df6b11de42200cc3837 Mon Sep 17 00:00:00 2001 From: Andrew Zhou Date: Mon, 24 Jun 2024 16:18:05 -0700 Subject: [PATCH 26/47] further split tests --- .github/workflows/ci.yml | 2 + .../confs/termRepoServicer-mintIntegrity.conf | 41 +++++++++++++ .../termRepoServicer-rolloverReverts.conf | 42 +++++++++++++ certora/specs/termRepoServicer/rules.spec | 2 - .../termRepoServicer/rulesMintCollapse.spec | 1 - .../termRepoServicer/rulesMintIntegrity.spec | 58 ++++++++++++++++++ .../rulesRolloverReverts.spec | 60 +++++++++++++++++++ contracts/TermRepoServicer.sol | 1 - 8 files changed, 203 insertions(+), 4 deletions(-) create mode 100644 certora/confs/termRepoServicer-mintIntegrity.conf create mode 100644 certora/confs/termRepoServicer-rolloverReverts.conf create mode 100644 certora/specs/termRepoServicer/rulesMintIntegrity.spec create mode 100644 certora/specs/termRepoServicer/rulesRolloverReverts.spec diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 16c5eda..2021861 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -48,9 +48,11 @@ jobs: - "termRepoServicer-lockFulfill.conf" - "termRepoServicer-lockFulfillReverts.conf" - "termRepoServicer-mintCollapse.conf" + - "termRepoServicer-mintIntegrity.conf" - "termRepoServicer-mintCollapseReverts.conf" - "termRepoServicer-repaymentsRedemptions.conf" - "termRepoServicer-repaymentsRedemptionsReverts.conf" + - "termRepoServicer-rolloverReverts.conf" - "termRepoServicer-stateVariables.conf" - "termRepoServicer.conf" - "termRepoToken.conf" diff --git a/certora/confs/termRepoServicer-mintIntegrity.conf b/certora/confs/termRepoServicer-mintIntegrity.conf new file mode 100644 index 0000000..c5874f9 --- /dev/null +++ b/certora/confs/termRepoServicer-mintIntegrity.conf @@ -0,0 +1,41 @@ +{ + "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": [ + "-smt_initialSplitDepth 5", + "-depth 15", + "-mediumTimeout 2", + "-splitParallel true", + "-splitParallelTimelimit 7200", + "-splitParallelInitialDepth 5" + ], + "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-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/specs/termRepoServicer/rules.spec b/certora/specs/termRepoServicer/rules.spec index f6d568c..212c077 100644 --- a/certora/specs/termRepoServicer/rules.spec +++ b/certora/specs/termRepoServicer/rules.spec @@ -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/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"); From 7950d576ab032160ada07cb79f341835c9fb2947 Mon Sep 17 00:00:00 2001 From: Andrew Zhou Date: Mon, 24 Jun 2024 16:31:54 -0700 Subject: [PATCH 27/47] undo servicer update --- contracts/TermRepoServicer.sol | 1 + 1 file changed, 1 insertion(+) diff --git a/contracts/TermRepoServicer.sol b/contracts/TermRepoServicer.sol index 5a02065..673a5d9 100644 --- a/contracts/TermRepoServicer.sol +++ b/contracts/TermRepoServicer.sol @@ -46,6 +46,7 @@ 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"); From 726543b5eae487651f90a0c3ddb594a7e84bf9f7 Mon Sep 17 00:00:00 2001 From: Andrew Zhou Date: Mon, 24 Jun 2024 17:18:52 -0700 Subject: [PATCH 28/47] minting changes certora spec --- certora/specs/termRepoServicer/minting.spec | 5 +++-- contracts/TermRepoServicer.sol | 1 - 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/certora/specs/termRepoServicer/minting.spec b/certora/specs/termRepoServicer/minting.spec index 94557f0..2d36553 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; + + 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/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"); From 00723b09a1e0622f2bfc651202855e6d8e9bf5f4 Mon Sep 17 00:00:00 2001 From: Andrew Zhou Date: Mon, 24 Jun 2024 17:32:19 -0700 Subject: [PATCH 29/47] minting changes certora spec --- certora/specs/termRepoServicer/minting.spec | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/certora/specs/termRepoServicer/minting.spec b/certora/specs/termRepoServicer/minting.spec index 2d36553..b03b111 100644 --- a/certora/specs/termRepoServicer/minting.spec +++ b/certora/specs/termRepoServicer/minting.spec @@ -46,7 +46,7 @@ methods { function DummyERC20A.balanceOf(address) external returns(uint256) envfree; function DummyERC20A.totalSupply() external returns(uint256) envfree; - TermController.verifyMintExposureAccess(address) external returns (bool) envfree; + function TermController.verifyMintExposureAccess(address) external returns (bool) envfree; } From d9ba8a5a905ccad2bff824585deea6ccf845c0d5 Mon Sep 17 00:00:00 2001 From: Andrew Zhou Date: Tue, 25 Jun 2024 09:39:42 -0700 Subject: [PATCH 30/47] beta cli runs for errors in certora prod --- .github/workflows/ci.yml | 45 +++++++++++++++++++++++++++++++++++----- 1 file changed, 40 insertions(+), 5 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 2021861..99ab197 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -44,17 +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-rolloverReverts.conf" - "termRepoServicer-stateVariables.conf" - - "termRepoServicer.conf" - "termRepoToken.conf" steps: - uses: actions/checkout@master @@ -85,3 +80,43 @@ 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-repaymentsRedemptionsReverts.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 + From 5cce3b4c2fa806d82227c09ea6532d4fe79c5474 Mon Sep 17 00:00:00 2001 From: Andrew Zhou Date: Tue, 25 Jun 2024 10:30:47 -0700 Subject: [PATCH 31/47] add 2 new reverts for repayments in certora --- certora/specs/termRepoServicer/repayments.spec | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) 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); From aa7ce0284b0bb7009c01df6fcaed950007601844 Mon Sep 17 00:00:00 2001 From: Andrew Zhou Date: Tue, 25 Jun 2024 15:34:00 -0700 Subject: [PATCH 32/47] NONDET summary for access roles controller call for mint open exposure certora --- certora/specs/termRepoServicer/accessRoles.spec | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/certora/specs/termRepoServicer/accessRoles.spec b/certora/specs/termRepoServicer/accessRoles.spec index 21e664d..ff8dc1c 100644 --- a/certora/specs/termRepoServicer/accessRoles.spec +++ b/certora/specs/termRepoServicer/accessRoles.spec @@ -15,8 +15,8 @@ methods { function ROLLOVER_MANAGER() external returns (bytes32) envfree; function ROLLOVER_TARGET_AUCTIONEER_ROLE() external returns (bytes32) envfree; - function TermController.verifyMintExposureAccess(address) external returns(bool) envfree; -} + function TermController.verifyMintExposure(address) external returns(bool) => NONDET + } rule onlyRoleCanCallRevert(method f, calldataarg args, env e) filtered { From 78040d36e5a4c961b574db3b6d00d1d1e24120b4 Mon Sep 17 00:00:00 2001 From: Andrew Zhou Date: Tue, 25 Jun 2024 15:47:34 -0700 Subject: [PATCH 33/47] split repay and redemption revert certora specs --- .github/workflows/ci.yml | 3 +- .../termRepoServicer-redemptionsReverts.conf | 42 ++++++++++++++ ...> termRepoServicer-repaymentsReverts.conf} | 2 +- .../rulesRedemptionsReverts.spec | 57 +++++++++++++++++++ ...verts.spec => rulesRepaymentsReverts.spec} | 3 - 5 files changed, 102 insertions(+), 5 deletions(-) create mode 100644 certora/confs/termRepoServicer-redemptionsReverts.conf rename certora/confs/{termRepoServicer-repaymentsRedemptionsReverts.conf => termRepoServicer-repaymentsReverts.conf} (96%) create mode 100644 certora/specs/termRepoServicer/rulesRedemptionsReverts.spec rename certora/specs/termRepoServicer/{rulesRepaymentsRedemptionsReverts.spec => rulesRepaymentsReverts.spec} (97%) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 99ab197..6f94a69 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -87,7 +87,8 @@ jobs: matrix: ruleset: - "termRepoServicer-lockFulfillReverts.conf" - - "termRepoServicer-repaymentsRedemptionsReverts.conf" + - "termRepoServicer-repaymentsReverts.conf" + - "termRepoServicer-redemptionsReverts.conf" - "termRepoServicer-rolloverReverts.conf" - "termRepoServicer.conf" steps: diff --git a/certora/confs/termRepoServicer-redemptionsReverts.conf b/certora/confs/termRepoServicer-redemptionsReverts.conf new file mode 100644 index 0000000..01e5289 --- /dev/null +++ b/certora/confs/termRepoServicer-redemptionsReverts.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:termRepoRolloverManager=TermRepoRolloverManager", + "TermRepoCollateralManagerHarness:termRepoLocker=TermRepoLocker" + ], + "prover_args": [ + "-smt_initialSplitDepth 5", + "-depth 17", + "-mediumTimeout 2", + "-splitParallel true", + "-splitParallelTimelimit 7200", + "-splitParallelInitialDepth 5" + ], + "solc_optimize": "50", + "contract_compiler_skip_severe_warning_as_error": 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" + ], + "prover_version": "jtoman/finder-fixes-will-it-ever-end", + "verify": "TermRepoServicerHarness:certora/specs/termRepoServicer/rulesRedemptionsReverts.spec" +} \ No newline at end of file diff --git a/certora/confs/termRepoServicer-repaymentsRedemptionsReverts.conf b/certora/confs/termRepoServicer-repaymentsReverts.conf similarity index 96% rename from certora/confs/termRepoServicer-repaymentsRedemptionsReverts.conf rename to certora/confs/termRepoServicer-repaymentsReverts.conf index bc9a75c..7772a56 100644 --- a/certora/confs/termRepoServicer-repaymentsRedemptionsReverts.conf +++ b/certora/confs/termRepoServicer-repaymentsReverts.conf @@ -37,5 +37,5 @@ "@chainlink=node_modules/@chainlink", "@openzeppelin=node_modules/@openzeppelin" ], - "verify": "TermRepoServicerHarness:certora/specs/termRepoServicer/rulesRepaymentsRedemptionsReverts.spec" + "verify": "TermRepoServicerHarness:certora/specs/termRepoServicer/rulesRepaymentsReverts.spec" } \ No newline at end of file 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; From 47592d693dfaaf7d8de5764f20f7b7c517aa56f1 Mon Sep 17 00:00:00 2001 From: Andrew Zhou Date: Tue, 25 Jun 2024 21:45:03 -0700 Subject: [PATCH 34/47] add semicolon to end of summary in access roles servicer certora --- certora/specs/termRepoServicer/accessRoles.spec | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/certora/specs/termRepoServicer/accessRoles.spec b/certora/specs/termRepoServicer/accessRoles.spec index ff8dc1c..506f5a7 100644 --- a/certora/specs/termRepoServicer/accessRoles.spec +++ b/certora/specs/termRepoServicer/accessRoles.spec @@ -15,7 +15,7 @@ methods { function ROLLOVER_MANAGER() external returns (bytes32) envfree; function ROLLOVER_TARGET_AUCTIONEER_ROLE() external returns (bytes32) envfree; - function TermController.verifyMintExposure(address) external returns(bool) => NONDET + function TermController.verifyMintExposure(address) external returns(bool) => NONDET; } From a08d26ebf16c2abc64dadac3141dcf3f11dc8b6f Mon Sep 17 00:00:00 2001 From: Andrew Zhou Date: Tue, 25 Jun 2024 21:59:44 -0700 Subject: [PATCH 35/47] ignore solidity warnings certora --- certora/confs/termRepoServicer-redemptionsReverts.conf | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/certora/confs/termRepoServicer-redemptionsReverts.conf b/certora/confs/termRepoServicer-redemptionsReverts.conf index 01e5289..d32443f 100644 --- a/certora/confs/termRepoServicer-redemptionsReverts.conf +++ b/certora/confs/termRepoServicer-redemptionsReverts.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", From c38a54d22b39ce5377ad509ebed2dc46581826d8 Mon Sep 17 00:00:00 2001 From: Andrew Zhou Date: Tue, 25 Jun 2024 22:14:25 -0700 Subject: [PATCH 36/47] split repay and redemption revert certora specs --- certora/specs/termRepoServicer/redemptions.spec | 1 + 1 file changed, 1 insertion(+) 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; From 04460ac3611b2b8508ce055ab2f2988e30e3c8fd Mon Sep 17 00:00:00 2001 From: Andrew Zhou Date: Tue, 25 Jun 2024 22:36:03 -0700 Subject: [PATCH 37/47] verify mint exposure access methods certora --- certora/specs/termRepoServicer/accessRoles.spec | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/certora/specs/termRepoServicer/accessRoles.spec b/certora/specs/termRepoServicer/accessRoles.spec index 506f5a7..85ff150 100644 --- a/certora/specs/termRepoServicer/accessRoles.spec +++ b/certora/specs/termRepoServicer/accessRoles.spec @@ -15,7 +15,7 @@ methods { function ROLLOVER_MANAGER() external returns (bytes32) envfree; function ROLLOVER_TARGET_AUCTIONEER_ROLE() external returns (bytes32) envfree; - function TermController.verifyMintExposure(address) external returns(bool) => NONDET; + function TermController.verifyMintExposureAccess(address) external returns(bool) => NONDET; } From 246506f06a6fb7b38b95f60d60b5e90e86feda07 Mon Sep 17 00:00:00 2001 From: Andrew Zhou Date: Tue, 25 Jun 2024 22:48:02 -0700 Subject: [PATCH 38/47] add env to verifyMintExposureAccess calls --- certora/specs/termRepoServicer/accessRoles.spec | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/certora/specs/termRepoServicer/accessRoles.spec b/certora/specs/termRepoServicer/accessRoles.spec index 85ff150..cbcd025 100644 --- a/certora/specs/termRepoServicer/accessRoles.spec +++ b/certora/specs/termRepoServicer/accessRoles.spec @@ -43,7 +43,7 @@ rule onlyRoleCanCallRevert(method f, calldataarg args, env e) filtered { || hasRole(ROLLOVER_MANAGER(),e.msg.sender) || hasRole(ROLLOVER_TARGET_AUCTIONEER_ROLE(),e.msg.sender) || hasRole(INITIALIZER_ROLE(),e.msg.sender) - || servicerAccessController.verifyMintExposureAccess(e.msg.sender); + || servicerAccessController.verifyMintExposureAccess(e, e.msg.sender); } rule onlyRoleCanCallStorage(method f, calldataarg args, env e) filtered { @@ -71,5 +71,5 @@ rule onlyRoleCanCallStorage(method f, calldataarg args, env e) filtered { || hasRole(ROLLOVER_MANAGER(),e.msg.sender) || hasRole(ROLLOVER_TARGET_AUCTIONEER_ROLE(),e.msg.sender) || hasRole(INITIALIZER_ROLE(),e.msg.sender) - || servicerAccessController.verifyMintExposureAccess(e.msg.sender); + || servicerAccessController.verifyMintExposureAccess(e, e.msg.sender); } \ No newline at end of file From c2e66c61ad7866ba78641bcf47d4ddba7e45fd3d Mon Sep 17 00:00:00 2001 From: Andrew Zhou Date: Tue, 25 Jun 2024 23:39:03 -0700 Subject: [PATCH 39/47] DISPATCHER true verifyMintExposureAccess --- certora/specs/termRepoServicer/accessRoles.spec | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/certora/specs/termRepoServicer/accessRoles.spec b/certora/specs/termRepoServicer/accessRoles.spec index cbcd025..5260fa0 100644 --- a/certora/specs/termRepoServicer/accessRoles.spec +++ b/certora/specs/termRepoServicer/accessRoles.spec @@ -15,7 +15,7 @@ methods { function ROLLOVER_MANAGER() external returns (bytes32) envfree; function ROLLOVER_TARGET_AUCTIONEER_ROLE() external returns (bytes32) envfree; - function TermController.verifyMintExposureAccess(address) external returns(bool) => NONDET; + function TermController.verifyMintExposureAccess(address) external returns(bool) => DISPATCHER(true); } From 660f31513317d9384e22d1c53b3591a0437222b2 Mon Sep 17 00:00:00 2001 From: Andrew Zhou Date: Wed, 26 Jun 2024 00:14:43 -0700 Subject: [PATCH 40/47] trying to get linking to work --- certora/specs/termRepoServicer/collapses.spec | 3 +++ 1 file changed, 3 insertions(+) diff --git a/certora/specs/termRepoServicer/collapses.spec b/certora/specs/termRepoServicer/collapses.spec index 98e0b99..9b8aa71 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 returns(bool) => DISPATCHER(true); + } rule burnCollapseExposureMonotonicBehavior(env e) { From 0bdb6abae78cb1fe2ca662ebe94b52b261a00b4b Mon Sep 17 00:00:00 2001 From: Andrew Zhou Date: Wed, 26 Jun 2024 00:27:33 -0700 Subject: [PATCH 41/47] trying to get linking to work --- certora/specs/termRepoServicer/accessRoles.spec | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/certora/specs/termRepoServicer/accessRoles.spec b/certora/specs/termRepoServicer/accessRoles.spec index 5260fa0..0cb43b2 100644 --- a/certora/specs/termRepoServicer/accessRoles.spec +++ b/certora/specs/termRepoServicer/accessRoles.spec @@ -15,7 +15,7 @@ methods { function ROLLOVER_MANAGER() external returns (bytes32) envfree; function ROLLOVER_TARGET_AUCTIONEER_ROLE() external returns (bytes32) envfree; - function TermController.verifyMintExposureAccess(address) external returns(bool) => DISPATCHER(true); + function _.verifyMintExposureAccess(address) external returns(bool) => DISPATCHER(true); } From 5df7c54e25f7e7d610aef3ea6ed1b04de2142826 Mon Sep 17 00:00:00 2001 From: Andrew Zhou Date: Wed, 26 Jun 2024 00:37:04 -0700 Subject: [PATCH 42/47] trying to get linking to work --- certora/specs/termRepoServicer/collapses.spec | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/certora/specs/termRepoServicer/collapses.spec b/certora/specs/termRepoServicer/collapses.spec index 9b8aa71..ffee095 100644 --- a/certora/specs/termRepoServicer/collapses.spec +++ b/certora/specs/termRepoServicer/collapses.spec @@ -48,7 +48,7 @@ methods { function DummyERC20A.decimals() external returns(uint256) envfree; function DummyERC20A.totalSupply() external returns(uint256) envfree; - function verifyMintExposureAccess(address) external returns(bool) => DISPATCHER(true); + function _.verifyMintExposureAccess(address) external returns(bool) => DISPATCHER(true); } From 46741e8585f394b9ce7b80074a09d2d5f4dd3b9d Mon Sep 17 00:00:00 2001 From: Andrew Zhou Date: Wed, 26 Jun 2024 00:51:16 -0700 Subject: [PATCH 43/47] trying to get linking to work --- certora/specs/termRepoServicer/accessRoles.spec | 2 +- certora/specs/termRepoServicer/collapses.spec | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/certora/specs/termRepoServicer/accessRoles.spec b/certora/specs/termRepoServicer/accessRoles.spec index 0cb43b2..d467a72 100644 --- a/certora/specs/termRepoServicer/accessRoles.spec +++ b/certora/specs/termRepoServicer/accessRoles.spec @@ -15,7 +15,7 @@ methods { function ROLLOVER_MANAGER() external returns (bytes32) envfree; function ROLLOVER_TARGET_AUCTIONEER_ROLE() external returns (bytes32) envfree; - function _.verifyMintExposureAccess(address) external returns(bool) => DISPATCHER(true); + function _.verifyMintExposureAccess(address) external => DISPATCHER(true); } diff --git a/certora/specs/termRepoServicer/collapses.spec b/certora/specs/termRepoServicer/collapses.spec index ffee095..73164e3 100644 --- a/certora/specs/termRepoServicer/collapses.spec +++ b/certora/specs/termRepoServicer/collapses.spec @@ -48,7 +48,7 @@ methods { function DummyERC20A.decimals() external returns(uint256) envfree; function DummyERC20A.totalSupply() external returns(uint256) envfree; - function _.verifyMintExposureAccess(address) external returns(bool) => DISPATCHER(true); + function _.verifyMintExposureAccess(address) external => DISPATCHER(true); } From 743973ff12a4bc6a9b0ab220e37c079cedc04d74 Mon Sep 17 00:00:00 2001 From: Andrew Zhou Date: Wed, 26 Jun 2024 08:27:55 -0700 Subject: [PATCH 44/47] redemption reverts branch version removed --- certora/confs/termRepoServicer-redemptionsReverts.conf | 1 - 1 file changed, 1 deletion(-) diff --git a/certora/confs/termRepoServicer-redemptionsReverts.conf b/certora/confs/termRepoServicer-redemptionsReverts.conf index d32443f..0412b58 100644 --- a/certora/confs/termRepoServicer-redemptionsReverts.conf +++ b/certora/confs/termRepoServicer-redemptionsReverts.conf @@ -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/rulesRedemptionsReverts.spec" } \ No newline at end of file From 7a5b2d390812e8b6049f1899a26513a3b84b8cfe Mon Sep 17 00:00:00 2001 From: Andrew Zhou Date: Wed, 26 Jun 2024 11:21:11 -0700 Subject: [PATCH 45/47] redemption reverts branch version removed --- certora/confs/termRepoServicer-redemptionsReverts.conf | 8 ++------ 1 file changed, 2 insertions(+), 6 deletions(-) diff --git a/certora/confs/termRepoServicer-redemptionsReverts.conf b/certora/confs/termRepoServicer-redemptionsReverts.conf index 0412b58..86f89b6 100644 --- a/certora/confs/termRepoServicer-redemptionsReverts.conf +++ b/certora/confs/termRepoServicer-redemptionsReverts.conf @@ -17,12 +17,8 @@ "TermRepoCollateralManagerHarness:termRepoLocker=TermRepoLocker" ], "prover_args": [ - "-smt_initialSplitDepth 5", - "-depth 17", - "-mediumTimeout 2", - "-splitParallel true", - "-splitParallelTimelimit 7200", - "-splitParallelInitialDepth 5" + "-depth 15", + "-splitParallel true" ], "solc_optimize": "50", "ignore_solidity_warnings": true, From 335b4f3fdec9abada3795a3c5b2603c5baedaf76 Mon Sep 17 00:00:00 2001 From: Andrew Zhou Date: Wed, 26 Jun 2024 11:59:37 -0700 Subject: [PATCH 46/47] redemption reverts branch version removed --- certora/confs/termRepoServicer.conf | 8 ++------ 1 file changed, 2 insertions(+), 6 deletions(-) diff --git a/certora/confs/termRepoServicer.conf b/certora/confs/termRepoServicer.conf index bb7fa3b..de603df 100644 --- a/certora/confs/termRepoServicer.conf +++ b/certora/confs/termRepoServicer.conf @@ -18,12 +18,8 @@ "TermRepoCollateralManagerHarness:termRepoLocker=TermRepoLocker" ], "prover_args": [ - "-smt_initialSplitDepth 10", - "-depth 20", - "-mediumTimeout 2", - "-splitParallel true", - "-splitParallelTimelimit 7200", - "-splitParallelInitialDepth 10" + "-depth 15", + "-splitParallel true" ], "solc_optimize": "50", "loop_iter": "2", From ccb2ae4c79939ee708aa5e8b18d811fa1b96bc7d Mon Sep 17 00:00:00 2001 From: Andrew Zhou Date: Wed, 26 Jun 2024 22:50:57 -0700 Subject: [PATCH 47/47] get mint integrity to stop timing out --- certora/confs/termRepoServicer-mintIntegrity.conf | 6 +----- 1 file changed, 1 insertion(+), 5 deletions(-) diff --git a/certora/confs/termRepoServicer-mintIntegrity.conf b/certora/confs/termRepoServicer-mintIntegrity.conf index c5874f9..78fdf4f 100644 --- a/certora/confs/termRepoServicer-mintIntegrity.conf +++ b/certora/confs/termRepoServicer-mintIntegrity.conf @@ -17,12 +17,8 @@ "TermRepoCollateralManagerHarness:termRepoLocker=TermRepoLocker" ], "prover_args": [ - "-smt_initialSplitDepth 5", "-depth 15", - "-mediumTimeout 2", - "-splitParallel true", - "-splitParallelTimelimit 7200", - "-splitParallelInitialDepth 5" + "-splitParallel true" ], "solc_optimize": "50", "loop_iter": "2",