100 address for treasury imported from rules for servicer

term-finance · Jun 23, 2024 · 36af4cb · 36af4cb
1 parent 8937188
commit 36af4cb
Show file tree

Hide file tree

Showing 5 changed files with 9 additions and 18 deletions.
diff --git 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
diff --git 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
@@ -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
@@ -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);