From 36af4cb2ed5d0ceed073009330f209d2e3b9e44f Mon Sep 17 00:00:00 2001
From: Andrew Zhou <andrew@termfinance.io>
Date: Sat, 22 Jun 2024 22:22:59 -0700
Subject: [PATCH] 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);