split repay and redemption revert certora specs

term-finance · Jun 25, 2024 · 78040d3 · 78040d3
1 parent aa7ce02
commit 78040d3
Show file tree

Hide file tree

Showing 5 changed files with 102 additions and 5 deletions.
diff --git 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
@@ -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"
+}
diff --git a/...ervicer-repaymentsRedemptionsReverts.conf → ...s/termRepoServicer-repaymentsReverts.conf b/...ervicer-repaymentsRedemptionsReverts.conf → ...s/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"
 }
diff --git a/certora/specs/termRepoServicer/rulesRedemptionsReverts.spec 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/...er/rulesRepaymentsRedemptionsReverts.spec → ...mRepoServicer/rulesRepaymentsReverts.spec b/...er/rulesRepaymentsRedemptionsReverts.spec → ...mRepoServicer/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;