From 5cce3b4c2fa806d82227c09ea6532d4fe79c5474 Mon Sep 17 00:00:00 2001 From: Andrew Zhou Date: Tue, 25 Jun 2024 10:30:47 -0700 Subject: [PATCH] add 2 new reverts for repayments in certora --- certora/specs/termRepoServicer/repayments.spec | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/certora/specs/termRepoServicer/repayments.spec b/certora/specs/termRepoServicer/repayments.spec index 4762d06..2d6313e 100644 --- a/certora/specs/termRepoServicer/repayments.spec +++ b/certora/specs/termRepoServicer/repayments.spec @@ -170,6 +170,8 @@ rule repaymentsRevertingConditions(env e){ } bool payable = e.msg.value > 0; + bool zeroRepayment = repayment == 0; + bool maxRepaymentZero = maxRepayment == 0; bool lockerTransfersPaused = locker.transfersPaused(); bool noLockerServicerAccess = !locker.hasRole(locker.SERVICER_ROLE(), currentContract); bool allowanceTooLow = token.allowance( borrower, termRepoLocker()) < repayment; @@ -180,7 +182,7 @@ rule repaymentsRevertingConditions(env e){ bool repaymentGreaterThanMax = repaymentAmount > maxRepayment; bool noServicerRoleOnCollateralManager = !repaymentCollateralManager.hasRole(repaymentCollateralManager.SERVICER_ROLE(), currentContract); - bool isExpectedToRevert = payable || lockerTransfersPaused || noLockerServicerAccess || borrowTokenBalanceTooLow || allowanceTooLow || afterRepurchaseWindow || borrowerZeroObligation || uintMaxRepayment || repaymentGreaterThanMax || noServicerRoleOnCollateralManager; + bool isExpectedToRevert = payable || zeroRepayment || maxRepaymentZero || lockerTransfersPaused || noLockerServicerAccess || borrowTokenBalanceTooLow || allowanceTooLow || afterRepurchaseWindow || borrowerZeroObligation || uintMaxRepayment || repaymentGreaterThanMax || noServicerRoleOnCollateralManager; submitRepurchasePayment@withrevert(e, repayment);