From 42a611ee1fa22f4d3770d6aefd8d7909e510c5cf Mon Sep 17 00:00:00 2001
From: Andrew Zhou <andrew@termfinance.io>
Date: Fri, 21 Jun 2024 16:01:39 -0700
Subject: [PATCH] no zero address msg sender in exposure opening on new
 rollover certora

---
 certora/specs/termRepoServicer/rolloverExposure.spec | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/certora/specs/termRepoServicer/rolloverExposure.spec b/certora/specs/termRepoServicer/rolloverExposure.spec
index 6c6bc90..a9d699a 100644
--- a/certora/specs/termRepoServicer/rolloverExposure.spec
+++ b/certora/specs/termRepoServicer/rolloverExposure.spec
@@ -56,7 +56,8 @@ rule openExposureOnRolloverNewIntegrity(env e) {
     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
+    
     mathint balanceBefore = getBorrowerRepurchaseObligation(borrower);
     mathint tokenBalanceTermRepoLockerBefore = rolloverExposureToken.balanceOf(rolloverExposureLocker);
     mathint tokenBalancePreviousTermRepoLockerBefore = rolloverExposureToken.balanceOf(previousTermRepoLocker);