minting changes certora spec

term-finance · Jun 25, 2024 · 726543b · 726543b
1 parent 7950d57
commit 726543b
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 3 deletions.
diff --git 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
@@ -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");