further split tests

term-finance · Jun 24, 2024 · d9e997a · d9e997a
1 parent 3488644
commit d9e997a
Show file tree

Hide file tree

Showing 8 changed files with 203 additions and 4 deletions.
diff --git 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
@@ -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"
+}
diff --git a/certora/confs/termRepoServicer-rolloverReverts.conf 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"
+}
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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");