Skip to content

Commit

Permalink
100 address for treasury imported from rules for servicer
Browse files Browse the repository at this point in the history
  • Loading branch information
aazhou1 committed Jun 22, 2024
1 parent 8468755 commit 7da828e
Showing 1 changed file with 0 additions and 6 deletions.
6 changes: 0 additions & 6 deletions certora/specs/termRepoServicer/rolloverExposure.spec
Original file line number Diff line number Diff line change
Expand Up @@ -36,8 +36,6 @@ methods {
function DummyERC20A.balanceOf(address) external returns(uint256) envfree;
function DummyERC20A.totalSupply() external returns(uint256) envfree;

function TermController.getTreasuryAddress() external => ALWAYS(100);

}

rule openExposureOnRolloverNewIntegrity(env e) {
Expand All @@ -54,11 +52,7 @@ rule openExposureOnRolloverNewIntegrity(env e) {
require(rolloverExposureLocker != previousTermRepoLocker);
require(rolloverExposureLocker != 100); // Protecting locker from using treasury address;
require(previousTermRepoLocker != 100); // Protecting previous locker from using treasury address;
require(rolloverExposureController.getTreasuryAddress() != e.msg.sender); // Protecting treasury from calling this function
require(rolloverExposureController.getTreasuryAddress() != rolloverExposureLocker); // Protecting locker from using treasury address;
require(rolloverExposureController.getTreasuryAddress() != previousTermRepoLocker); // Protecting previous locker from using treasury address;
require(e.msg.sender != 0); // Protecting from zero address
require(rolloverExposureController.getTreasuryAddress() != borrower); // Protecting from borrower address

mathint balanceBefore = getBorrowerRepurchaseObligation(borrower);
mathint tokenBalanceTermRepoLockerBefore = rolloverExposureToken.balanceOf(rolloverExposureLocker);
Expand Down

0 comments on commit 7da828e

Please sign in to comment.