Formal Verification

Summary

This report represents work and conclusions based on Term Labs using Certora’s Prover tool to formally verify security properties of Term's smart contracts. Term finalized formal verification of the protocol's smart contracts using Certora's Prover solutions with guidance and technical support provided by the Certora team. The work was undertaken from Dec. 1, 2023 to Mar. 23, 2024. Some of these tests were verified using beta and staging versions of Certora's Prover, which are scheduled to be deployed to their production service in the near future. The latest commit that was reviewed and ran through the Certora Prover was 831292726cdc22e9d4d2953d59051fa00fbd4f72.

The scope of this verification includes all Term Servicer contracts within Term Protocol. This includes the following.

• TermRepoToken.sol

• TermRepoLocker.sol

• TermRepoServicer.sol

• TermRepoCollateralManager.sol

• TermRepoRolloverManager.sol

Auction Contracts within Term Protocol were partially verified, with coverage on all functions except for those related to auction clearing, whose loop complexity is too elevated for formal verification. Runtime Verification was previously engaged to focus specifically on auditing and manually verifying this small but critical part of the codebase, see here. Contracts with partial coverage include:

• TermAuction.sol

• TermAuctionBidLocker.sol

• TermAuctionOfferLocker.sol

The Certora Prover proved the implementation of the protocol is correct with respect to formal specifications written by the Term Labs team.

List of Main Issues Discovered

Severity: Low

Disclaimer

The Certora Prover takes as input a contract and a specification and formally proves that the contract satisfies the specification in all scenarios. Importantly, the guarantees of the Certora Prover are scoped to the provided specification, and the Certora Prover does not check any cases not covered by the specification.

We hope that this information is useful, but provide no warranty of any kind, explicit or implied. The contents of this report should not be construed as a complete guarantee that the contract is secure in all dimensions. In no event shall Term, Certora or any of its or their respective employees be liable for any claim, damages or other liability, whether in an action of contract, tort or otherwise, arising from, out of or in connection with the results reported here.

Overview of the verification

Description of the system

The Term Finance Protocol enables noncustodial fixed-rate collateralized lending on-chain (Term Repos) modeled on tri-party repo arrangements common in TradFi. Borrowers and lenders are matched through a unique recurring auction process (Term Auctions) where borrowers submit sealed bids and lenders submit sealed offers that are used to determine an interest rate that clears the market for participants of that auction. Participants who bid more than the clearing rate receive loans and participants willing to lend below the clearing rate make loans, in each case at the market-clearing rate. All other participants’ bids and offers are said to be “left on the table.” At the conclusion of an auction, borrowers receive loan proceeds and lenders receive ERC-20 tokens (Term Repo Tokens), which are receipts that lenders will burn to redeem for principal plus interest at maturity. Protocol smart contracts service these transactions by ledgering repayments and monitoring collateral health and liquidations.

Description of the specification files

For each contract, spec rules are divided into separate spec files per business logic function type (separate spec for state variable rules), but during runtime are compiled together in a rules.spec file. For the termRepoCollateralManager, the rules.spec is further divided into a rules.spec and other spec files for liquidations and state variables, due to the nature of high verification fun times for those functions.

Assumptions and Simplifications

• Some loops were run with a fixed size of 1 in able to enable formal verification. Verifying beyond a 1st loop would have cause formal verification to time out.

• Token prices are fetched from a constant mapping in CVL instead of a live price feed. This enables easier comparison of expected calculations and actual token amounts.

• Some of the multiplications and divisions in liquidation functions in the smart contracts inherit a contract called ExponentialNoError, which scales and truncates multiplications and divisions in Solidity in a way that precision is not lost. The calculations in these functions were replaced with CVL equivalents in order to prevent timeouts of FV rules.

Contract Invariants and Rules

Common Rules

Applied to every contract in the protocol.

1. Rule: pairTermContractsRevertsWhenAlreadyPaired - constrain input space to only include contracts that have already been paired.

    require isTermContractPaired();

    pairTermContracts@withrevert(e, args);
    assert lastReverted,
        "pairTermContracts(...) should revert when calling it on an already paired contract";

    assert isTermContractPaired(),
        "termContractPaired should not change when calling pairTermContracts(...) on an already paired contract";
}

2. Rule: onlyPairTermContractsChangesIsTermContractPairedRule - ensures that only pairTermContracts(...) can change state of termContractPaired

bool isTermContractPairedBefore = isTermContractPaired();

    f(e, args);

    bool isTermContractPairedAfter = isTermContractPaired();

    assert isTermContractPairedBefore == isTermContractPairedAfter,
        "termContractPaired should not change when calling methods other than pairTermContracts(...)";

TermRepoToken.sol

1. Invariant totalSupplyIsSumOfBalances - ensures that the total supply of tokens always equals the sum of individual account balances, maintaining the principle of token conservation.

to_mathint(totalSupply()) == sumOfBalances

2. Rule: totalSupplyNeverOverflow - guarantees that the total supply of tokens cannot exceed the maximum value allowed by the system, preventing overflow errors.

assert totalSupplyBefore <= totalSupplyAfter;

3. Rule: noMethodChangesMoreThanTwoBalances - ensures that no single operation can alter more than two account balances at once.

assert numberOfChangesOfBalancesAfter <= numberOfChangesOfBalancesBefore + 2;

4. Rule: onlyAllowedMethodsMayChangeAllowance - verifies that changes to token allowances are restricted to approved methods, ensuring that delegated spending limits are securely managed.

definition canIncreaseAllowance(method f) returns bool = 
	f.selector == sig:approve(address,uint256).selector || 
    f.selector == sig:increaseAllowance(address,uint256).selector;
    

definition canDecreaseAllowance(method f) returns bool = 
	f.selector == sig:approve(address,uint256).selector ||
    f.selector == sig:decreaseAllowance(address,uint256).selector || 
	f.selector == sig:transferFrom(address,address,uint256).selector;

assert allowanceAfter > allowanceBefore => canIncreaseAllowance(f), "should not increase allowance";
assert allowanceAfter < allowanceBefore => canDecreaseAllowance(f), "should not decrease allowance";

5. Rule: onlyAllowedMethodsMayChangeBalance - verifies that token balance changes within accounts can only be done through approved methods, preventing unauthorized modifications.

definition canIncreaseBalance(method f) returns bool = 
	f.selector == sig:mintRedemptionValue(address,uint256).selector || 
    f.selector == sig:mintTokens(address,uint256).selector || 
	f.selector == sig:transfer(address,uint256).selector ||
	f.selector == sig:transferFrom(address,address,uint256).selector;

definition canDecreaseBalance(method f) returns bool = 
	f.selector == sig:burn(address,uint256).selector || 
    f.selector == sig:burnAndReturnValue(address,uint256).selector || 
	f.selector == sig:transfer(address,uint256).selector ||
	f.selector == sig:transferFrom(address,address,uint256).selector;

assert balanceAfter > balanceBefore => canIncreaseBalance(f);
assert balanceAfter < balanceBefore => canDecreaseBalance(f);

6. Rule: onlyAllowedMethodsMayChangeTotalSupply - verifies that changes to the total supply of tokens are conducted only through authorized methods, maintaining supply integrity.

definition canIncreaseTotalSupply(method f) returns bool = 
	f.selector == sig:mintRedemptionValue(address,uint256).selector || 
    f.selector == sig:mintTokens(address,uint256).selector;

definition canDecreaseTotalSupply(method f) returns bool = 
	f.selector == sig:burn(address,uint256).selector || 
    f.selector == sig:burnAndReturnValue(address,uint256).selector;

 assert totalSupplyAfter > totalSupplyBefore => canIncreaseTotalSupply(f);
 assert totalSupplyAfter < totalSupplyBefore => canDecreaseTotalSupply(f);

7. Rule: reachability - verifies that all non-initialization and non-upgrade methods can be executed, ensuring contract functionality is accessible.

f(e,args);
satisfy true;

8. Rule: onlyAuthorizedCanTransfer - verifies that token transfers can only be initiated by authorized entities.

assert (
    balanceAfter < balanceBefore
) => (
    f.selector == sig:burn(address,uint256).selector ||
    f.selector == sig:burnAndReturnValue(address,uint256).selector ||
    e.msg.sender == account ||
    balanceBefore - balanceAfter <= to_mathint(allowanceBefore)
);

9. Rule: onlyHolderOfSpenderCanChangeAllowance - verifies that changes to spending allowance, which is the limit set by the token holder for how much another account can spend on their behalf, can only be made by the token holder or a designated spender

assert (
        allowanceAfter > allowanceBefore
    ) => (
        ((f.selector == sig:approve(address,uint256).selector || f.selector == sig:increaseAllowance(address,uint256).selector) && e.msg.sender == holder)
    );

    assert (
        allowanceAfter < allowanceBefore
    ) => (
        (f.selector == sig:transferFrom(address,address,uint256).selector && e.msg.sender == spender) ||
        ((f.selector == sig:approve(address,uint256).selector || f.selector == sig:decreaseAllowance(address,uint256).selector) && e.msg.sender == holder )
    );

10. Rule: mintTokensIntegrity - ensures that after minting tokens, the balance of the minter and the total supply are correctly increased.

  assert to_mathint(balanceOf(to)) == toBalanceBefore   + amount;
  assert to_mathint(totalSupply()) == totalSupplyBefore + amount;

11. Rule: mintRedemptionValueIntegrity - ensures that after minting tokens and returning a value, the balance of the minter and the total supply are correctly increased.

mathint redemptValue = redemptionValue();
mathint expectedBalanceAfter = (balanceBefore + ( amount * expScale * expScale / redemptValue) / expScale);
mathint expectedTotalSupplyAfter = (totalSupply() + ( amount * expScale * expScale / redemptValue) / expScale);

assert balanceAfter == expectedBalanceAfter;
assert totalSupplyAfter == expectedTotalSupplyAfter;

where expScale = 10^ 18.

12. Rule: mintTokensRevertingConditions- check for revert under the defined expected conditions, ensuring operation adherence to defined rules.

bool paused = mintingPaused() == true;
bool payable = e.msg.value > 0;
bool toZeroAccount = account == 0;
bool notMinterRole = !hasRole(MINTER_ROLE(), e.msg.sender);

bool isExpectedToRevert = paused || payable || notMinterRole || toZeroAccount;

13. Rule: mintRedemptionValueRevertingConditions- check for revert under the defined expected conditions, ensuring operation adherence to defined rules.

bool paused = mintingPaused() == true;
bool payable = e.msg.value > 0;
bool toZeroAccount = account == 0;
bool notMinterRole = !hasRole(MINTER_ROLE(), e.msg.sender);

bool isExpectedToRevert = paused || payable || notMinterRole || toZeroAccount;

14. Rule: mintRedemptionValueDoesNotAffectThirdParty - verifies that when one account invokes mintRedemptionValue, this action does not affect third-party balances.

	require addr1 != addr2;
	
	uint256 before = balanceOf(addr2);
		
	mintRedemptionValue(e, addr1, amount);
	assert balanceOf(addr2) == before;

15. Rule: mintTokensDoesNotAffectThirdParty - verifies that when one account invokes mintOpenExposure, this action does not affect third-party balances.

	require addr1 != addr2;
		
	uint256 before = balanceOf(addr2);
		
	mintTokens(e, addr1, amount);
	assert balanceOf(addr2) == before;

16. Rule: burnIntegrity - ensures that after burning tokens, the balance of the burner and the total supply are correctly decreased.

 assert to_mathint(balanceOf(from)) == fromBalanceBefore   - amount;
 assert to_mathint(totalSupply())   == totalSupplyBefore - amount;

17. Rule: burnAndReturnValueIntegrity - ensures that after burning tokens and returning a value, the balance of the burner and the total supply are correctly decreased.

assert to_mathint(balanceOf(from)) == fromBalanceBefore - amount;
assert to_mathint(totalSupply()) == totalSupplyBefore - amount;

18. Rule: burnRevertingConditions - checks conditions under which a burn operation should revert, such as not having enough balance, the contract being paused, etc.

 bool payable = e.msg.value > 0;
 bool notEnoughBalance = balanceOf(account) < amount;
 bool notBurnerRole = !hasRole(BURNER_ROLE(), e.msg.sender);
 bool fromZeroAccount = account == 0;
 bool paused = burningPaused();
 bool isExpectedToRevert = notEnoughBalance || notBurnerRole || paused || fromZeroAccount || payable;

 assert lastReverted <=> isExpectedToRevert;

19. Rule: burnDoesNotAffectThirdParty - verifies that burning tokens from one account does not affect third party balances.

assert balanceOf(addr2) == before;

20. Rule: burnAndReturnValueDoesNotAffectThirdParty - confirms that burning tokens and returning a value from one account does not impact the balance of an unrelated account.

assert balanceOf(addr2) == before;

21. Rule: transferIntegrity - asserts that after a transfer, the balances of the sender and recipient are updated correctly, respecting the case when sender and recipient are the same.

assert to_mathint(balanceOf(holder)) == holderBalanceBefore - (holder == recipient ? 0 : amount);
assert to_mathint(balanceOf(recipient)) == recipientBalanceBefore + (holder == recipient ? 0 : amount);

22. Rule: transferIsOneWayAdditive - demonstrates that if a transfer of a combined amount succeeds, individual transfers of the components should also succeed without affecting the final state.

transfer(e, recipient, assert_uint256(sum));
	storage after1 = lastStorage;

	transfer@withrevert(e, recipient, amount_a) at init; // restores storage
		assert !lastReverted;	//if the transfer passed with sum, it should pass with both summands individually
	transfer@withrevert(e, recipient, amount_b);
		assert !lastReverted;
	storage after2 = lastStorage;

assert after1[currentContract] == after2[currentContract];

23. Rule: transferRevertingConditions- identifies conditions under which a transfer should revert, such as the sender not having enough balance.

    bool payable = e.msg.value != 0;
    bool zeroTo = account == 0;
    bool notEnoughBalance = balanceOf(e.msg.sender) < amount;
    bool isExpectedToRevert = payable || zeroTo || notEnoughBalance;

assert lastReverted <=> isExpectedToRevert;

24. Rule: transferDoesNotAffectThirdParty - ensures that a transfer between two accounts does not affect the balance of a third party.

assert balanceOf(addr2) == before;

25. Rule: transferFromIntegrity - confirms that after a transferFrom operation, the balances of the holder and recipient are correctly adjusted, and the allowance is updated appropriately.

assert to_mathint(allowance(holder, spender)) == (allowanceBefore == max_uint256 ? max_uint256 : allowanceBefore - amount);
assert to_mathint(balanceOf(holder)) == holderBalanceBefore - (holder == recipient ? 0 : amount);
assert to_mathint(balanceOf(recipient)) == recipientBalanceBefore + (holder == recipient ? 0 : amount);

26. Rule: transferFromRevertingConditions - checks for conditions that should cause a transferFrom to revert, such as insufficient allowance or balance.

bool sendEthToNotPayable = e.msg.value != 0;
    bool ownerZero = owner == 0;
    bool recepientZero = recepient == 0;
	bool allowanceIsLow = allowed < transfered;
    bool notEnoughBalance = balanceOf(owner) < transfered;

    bool isExpectedToRevert = sendEthToNotPayable  || allowanceIsLow || notEnoughBalance || ownerZero || recepientZero;

assert lastReverted <=> isExpectedToRevert;

27. Rule: transferFromDoesNotAffectThirdParty - verifies that a transferFrom operation does not impact the balance or allowance of third parties.

assert thirdPartyBalanceBefore == thirdPartyBalanceAfter;
assert thirdPartyAllowanceBefore == thirdPartyAllowanceAfter;

28. Rule: transferFromIsOneWayAdditive - shows that if a transferFrom for a combined amount is successful, then separate transferFrom operations for each component of the amount should also succeed, without altering the final state.

transferFrom(e, owner, recipient, assert_uint256(sum));
	storage after1 = lastStorage;

	transferFrom@withrevert(e, owner, recipient, amount_a) at init; // restores storage
		assert !lastReverted;	//if the transfer passed with sum, it should pass with both summands individually
	transferFrom@withrevert(e, owner, recipient, amount_b);
		assert !lastReverted;
	storage after2 = lastStorage;

assert after1[currentContract] == after2[currentContract];

29. Rule: approveIntegrity - ensures that the allowance is correctly set after an approve operation.

assert allowance(holder, spender) == amount;

30. Rule: approveRevertingConditions - identifies scenarios in which an approve operation should revert, such as when trying to approve from a zero address.

bool payable = e.msg.value != 0;
    bool spenderIsZero = spender == 0;
	bool isExpectedToRevert = payable || spenderIsZero;

assert lastReverted <=> isExpectedToRevert;

31. Rule: approveDoesNotAffectThirdParty - confirms that an approve operation between two parties does not affect the allowance of a third party.

assert thirdPartyAllowanceBefore == thirdPartyAllowanceBefore;

32. Rule: onlyAllowedMethodsMayChangeMintExposureCap - ensures that only specific methods can modify the mint exposure cap. Methods like minting, burning, or resetting the cap are allowed to change it.

assert mintExposureCapAfter > mintExposureCapBefore => canIncreaseMintExposureCap(f);
assert mintExposureCapAfter < mintExposureCapBefore => canDecreaseMintExposureCap(f);

33. Rule: mintExposureCapNeverOverflow - verifies that when the mint exposure cap is increased, this action does not cause it to overflow, ensuring the cap's value remains within safe limits.

assert mintExposureCapBefore <= mintExposureCapAfter;

34. Rule: noMethodChangesRedemptionValue - confirms that the redemption value remains unchanged across transactions, except by methods explicitly intended to modify it. This rule ensures stability in the redemption value.

assert redemptionValueBefore == redemptionValueAfter;

35. Rule: onlyRoleCanCallRevert - checks if a method call that is not a view and requires specific roles to execute successfully, does not revert if the caller has the necessary role.

assert !lastReverted => hasRole(MINTER_ROLE(),e.msg.sender)
    || hasRole(BURNER_ROLE(),e.msg.sender)
    || hasRole(ADMIN_ROLE(),e.msg.sender)
    || hasRole(DEVOPS_ROLE(),e.msg.sender)
    || hasRole(INITIALIZER_ROLE(),e.msg.sender);

36. Rule: onlyRoleCanCallStorage - ensures that changes to storage by non-view method calls can only be performed by addresses with specific roles, guarding against unauthorized modifications.

storage storeBefore = lastStorage;
currentContract.f(e,args);
storage storeAfter = lastStorage;

assert storeBefore != storeAfter => hasRole(MINTER_ROLE(),e.msg.sender)
    || hasRole(BURNER_ROLE(),e.msg.sender)
    || hasRole(ADMIN_ROLE(),e.msg.sender)
    || hasRole(DEVOPS_ROLE(),e.msg.sender)
    || hasRole(INITIALIZER_ROLE(),e.msg.sender);

TermRepoLocker.sol

1. Rule: onlyAllowedMethodsMayChangeTransfersPaused - ensures that the state of transfers being paused can only be altered by specific methods designated for pausing or unpausing transfers.

bool transfersPausedBefore = transfersPaused();
f(e, args);
bool transfersPausedAfter = transfersPaused();

assert(transfersPausedBefore == transfersPausedAfter);

2. Rule: noMethodChangesTermRepoId - confirms that the Term Repo ID remains constant and is not changed by any method calls, ensuring its immutability post-initialization.

bytes32 termRepoIdBefore = termRepoId();
f(e, args);
bytes32 termRepoIdAfter = termRepoId();

assert(termRepoIdBefore == termRepoIdAfter);

3. Rule: onlyAllowedMethodsMayChangeEmitter - verifies that the emitter's address can only be changed through specific methods, preserving the integrity and security of the emitter identification.

address emitterBefore = emitterAddress();
f(e, args);
address emitterAfter = emitterAddress();

assert(emitterBefore == emitterAfter);

4. Rule: onlyAllowedMethodsMayChangeBalance - checks if the treasury balance is correctly updated by allowed methods and remains unchanged by others.

uint256 balanceBefore = token.balanceOf(currentContract);
f(e, args);
uint256 balanceAfter = token.balanceOf(currentContract);

// For increasing treasury balance
if (canIncreaseTreasuryBalance(f)) {
    assert balanceAfter > balanceBefore => (sender != currentContract) && (amount != 0);
    assert balanceAfter == balanceBefore => (sender == currentContract) || (amount == 0);
}
// For decreasing treasury balance
else if (canDecreaseTreasuryBalance(f)) {
    assert balanceAfter < balanceBefore => (recipient != currentContract) && (amount != 0);
    assert balanceAfter == balanceBefore => (recipient == currentContract) || (amount == 0);
}
// For other methods
else {
    assert balanceAfter == balanceBefore;
}

5. Rule: reachability - verifies that all non-initialization and non-upgrade methods can be executed, ensuring contract functionality is accessible.

f(e,args);
satisfy true;

6. Rule: transferTokenFromWalletIntegrity - validates the integrity of transferring tokens from the wallet, checking the update in treasury and sender balances post-transaction.

mathint treasuryBalanceBefore = to_mathint(token.balanceOf(currentContract));
mathint senderBalanceBefore = to_mathint(token.balanceOf(sender));

transferTokenFromWallet(e, sender, token, amount);

mathint treasuryBalanceAfter = to_mathint(token.balanceOf(currentContract));
mathint senderBalanceAfter = to_mathint(token.balanceOf(sender));

mathint expectedDiff = (isSelf || !isServicer || transfersPaused || isOverspend) ? 0 : to_mathint(amount);

// Asserting balance changes based on conditions
assert treasuryBalanceAfter == treasuryBalanceBefore + expectedDiff;
assert senderBalanceAfter == senderBalanceBefore - expectedDiff;
assert transfersPaused() == transfersPaused;

7. Rule: transferTokenToWalletIntegrity - ensures the correct adjustment of balances when tokens are transferred to the wallet, factoring in role permissions and pause status.

mathint treasuryBalanceBefore = to_mathint(token.balanceOf(currentContract));
mathint recipientBalanceBefore = to_mathint(token.balanceOf(recipient));

transferTokenToWallet(e, recipient, token, amount);

mathint treasuryBalanceAfter = to_mathint(token.balanceOf(currentContract));
mathint recipientBalanceAfter = to_mathint(token.balanceOf(recipient));

mathint expectedDiff = (isSelf || !isServicer || transfersPaused || isOverspend) ? 0 : to_mathint(amount);

// Verifying the outcome matches expectations
assert recipientBalanceAfter == recipientBalanceBefore + expectedDiff;
assert treasuryBalanceAfter == treasuryBalanceBefore - expectedDiff;
assert transfersPaused() == transfersPaused;

8. Rule: pauseTransfersIntegrity - validates that transfers can be paused correctly by the authorized role, ensuring the state is changed as expected.

pauseTransfers(e);
assert transfersPaused();

9. Rule: unpauseTransfersIntegrity - confirms that transfers can be unpaused accurately, reverting the paused state and allowing transactions to proceed.

unpauseTransfers(e);
assert !transfersPaused();

10. Rule: onlyRoleCanCallRevert - ensures that methods not related to initialization, upgrade, or role management only revert if the caller lacks the necessary roles. This rule safeguards against unauthorized actions while allowing legitimate operations.

currentContract.f@withrevert(e,args);

// Verification if the method didn't revert, the caller must possess one of the specified roles.
assert !lastReverted => hasRole(SERVICER_ROLE(),e.msg.sender)
    || hasRole(ADMIN_ROLE(),e.msg.sender)
    || hasRole(DEVOPS_ROLE(),e.msg.sender)
    || hasRole(INITIALIZER_ROLE(),e.msg.sender);

11. Rule: onlyRoleCanCallStorage - verifies that storage modifications by non-view methods are properly guarded by role checks, preventing unauthorized changes to the contract's state. This rule enforces role-based access control for sensitive operations.

storage storeBefore = lastStorage;
currentContract.f(e,args);
storage storeAfter = lastStorage;

// Conditionally asserts that if storage was altered, the action must have been performed by an entity with an appropriate role.
assert storeBefore != storeAfter => hasRole(SERVICER_ROLE(),e.msg.sender)
    || hasRole(ADMIN_ROLE(),e.msg.sender)
    || hasRole(DEVOPS_ROLE(),e.msg.sender)
    || hasRole(INITIALIZER_ROLE(),e.msg.sender);

TermRepoServicer.sol

1. Invariant: totalOutstandingRepurchaseExposureIsSumOfRepurchases - asserts that the total outstanding repurchase exposure is equal to the sum of all individual repurchase exposures, ensuring consistency within the ledger.

to_mathint(totalOutstandingRepurchaseExposure()) == sumOfRepurchases
filtered { m ->
    m.selector != sig:initialize(string,uint256,uint256,uint256,uint256,address,address,address,address).selector &&
    m.selector != sig:upgradeToAndCall(address,bytes).selector &&
    m.selector != sig:upgradeTo(address).selector
}

2. Rule: onlyAllowedMethodsMayChangeTotalOutstandingRepurchaseExposure - specifies that only particular methods can increase or decrease the total outstanding repurchase exposure, aligning changes with expected business logic operations.

definition canIncreaseTotalOutstandingRepurchaseExposure(method f) returns bool = 
	f.selector == sig:fulfillBid(address,uint256,uint256,address[],uint256[],uint256).selector || 
    f.selector == sig:openExposureOnRolloverNew(address,uint256,uint256,address,uint256).selector ||
    f.selector == sig:mintOpenExposure(uint256,uint256[]).selector;

definition canDecreaseTotalOutstandingRepurchaseExposure(method f) returns bool = 
	f.selector == sig:submitRepurchasePayment(uint256).selector || 
    f.selector == sig:closeExposureOnRolloverExisting(address,uint256).selector ||
    f.selector == sig:liquidatorCoverExposureWithRepoToken(address,address,uint256).selector ||
    f.selector == sig:liquidatorCoverExposure(address,address,uint256).selector ||
    f.selector == sig:burnCollapseExposure(uint256).selector;

uint256 totalOutstandingRepurchaseExposureBefore = totalOutstandingRepurchaseExposure();
f(e, args);
uint256 totalOutstandingRepurchaseExposureAfter = totalOutstandingRepurchaseExposure();

assert totalOutstandingRepurchaseExposureAfter > totalOutstandingRepurchaseExposureBefore => canIncreaseTotalOutstandingRepurchaseExposure(f);
assert totalOutstandingRepurchaseExposureAfter < totalOutstandingRepurchaseExposureBefore => canDecreaseTotalOutstandingRepurchaseExposure(f);

3. Rule: totalOutstandingRepurchaseExposureNeverOverflows - ensures that actions intended to increase the total outstanding repurchase exposure do not result in an overflow, preserving the integrity of financial calculations.

uint256 totalOutstandingRepurchaseExposureBefore = totalOutstandingRepurchaseExposure();
f(e, args);
uint256 totalOutstandingRepurchaseExposureAfter = totalOutstandingRepurchaseExposure();

assert totalOutstandingRepurchaseExposureBefore <= totalOutstandingRepurchaseExposureAfter;

4. Rule: onlyAllowedMethodsMayChangeTotalRepurchaseCollected - identifies methods permitted to increase or decrease the total repurchase collected, ensuring that financial metrics reflect actual repurchase activity accurately.

definition canIncreaseTotalRepurchaseCollected(method f) returns bool = 
    f.selector == sig:submitRepurchasePayment(uint256).selector || 
    f.selector == sig:closeExposureOnRolloverExisting(address,uint256).selector ||
    f.selector == sig:liquidatorCoverExposure(address,address,uint256).selector;

definition canDecreaseTotalRepurchaseCollected(method f) returns bool = 
    f.selector == sig:redeemTermRepoTokens(address,uint256).selector;

uint256 totalRepurchaseCollectedBefore = totalRepurchaseCollected();
f(e, args);
uint256 totalRepurchaseCollectedAfter = totalRepurchaseCollected();

assert totalRepurchaseCollectedAfter > totalRepurchaseCollectedBefore => canIncreaseTotalRepurchaseCollected(f);
assert totalRepurchaseCollectedAfter < totalRepurchaseCollectedBefore => canDecreaseTotalRepurchaseCollected(f);

5. Rule: totalRepurchaseCollectedNeverOverflows - verifies that the total repurchase collected metric cannot overflow as a result of any operation, maintaining the system's financial stability.

uint256 totalRepurchaseCollectedBefore = totalRepurchaseCollected();
f(e, args);
uint256 totalRepurchaseCollectedAfter = totalRepurchaseCollected();

assert totalRepurchaseCollectedBefore <= totalRepurchaseCollectedAfter;

6. Rule:shortfallHaircutMantissaAlwaysZeroBeforeRedemptionAndLessThanExpScaleAfter - confirms the shortfall haircut mantissa remains zero before the redemption timestamp and falls within expected bounds after, ensuring fair and predictable financial adjustments.

require(shortfallHaircutMantissa() == 0);

f(e, args);

assert (e.block.timestamp <= redemptionTimestamp()) => (shortfallHaircutMantissa() == 0);
assert (shortfallHaircutMantissa() > 0  && shortfallHaircutMantissa() < 10 ^ 18) => (e.block.timestamp > redemptionTimestamp());

7. Rule: totalRepurchaseCollectedLessThanOrEqualToLockerPurchaseTokenBalance - ensures that the total repurchase collected does not exceed the locker's purchase token balance, preventing overestimation of collected repurchases.

require(termRepoLocker() == stateLocker); // bounds for test
require(purchaseToken() == stateToken); // bounds for test
require(totalRepurchaseCollected() <= stateToken.balanceOf(stateLocker)); // starting condition
require(e.msg.sender != stateLocker); // repo locker contract does not have calls to servicer
require(!isTokenCollateral(stateToken)); // token will not be both purchase and collateral token

f(e, args);

assert (totalRepurchaseCollected() <= stateToken.balanceOf(stateLocker));

8. Rule: noMethodsChangeMaturityTimestamp - validates that no method changes the maturity timestamp, ensuring consistency in the term's length and financial obligations.

uint256 maturityTimestampBefore = maturityTimestamp();
f(e, args);
uint256 maturityTimestampAfter = maturityTimestamp();

assert maturityTimestampBefore == maturityTimestampAfter;

9. Rule: noMethodsChangeEndOfRepurchaseWindow - confirms the end of the repurchase window is immutable across all contract interactions, preserving the predetermined timeframe for repurchases, which is critical for contractual agreements.

uint256 endOfRepurchaseWindowBefore = endOfRepurchaseWindow();
f(e, args);
uint256 endOfRepurchaseWindowAfter = endOfRepurchaseWindow();
assert endOfRepurchaseWindowBefore == endOfRepurchaseWindowAfter;

10. Rule: noMethodsChangeRedemptionTimestamp - ensures the redemption timestamp remains constant across all contract interactions, guaranteeing the redemption period's stability and predictability.

uint256 redemptionTimestampBefore = redemptionTimestamp();
f(e, args);
uint256 redemptionTimestampAfter = redemptionTimestamp();
assert redemptionTimestampBefore == redemptionTimestampAfter;

11. Rule: noMethodsChangeServicingFee - verifies that the servicing fee rate is maintained across all transactions, ensuring consistent fee calculations and financial expectations for parties involved.

uint256 servicingFeeBefore = servicingFee();
f(e, args);
uint256 servicingFeeAfter = servicingFee();
assert servicingFeeBefore == servicingFeeAfter;

12. Rule: onlyAllowedMethodsChangeShortfallHaircutMantissa - restricts adjustments to the shortfall haircut mantissa to specific authorized methods, safeguarding the metric's integrity against unauthorized modifications.

uint256 shortfallHaircutMantissaBefore = shortfallHaircutMantissa();
f(e, args);
uint256 shortfallHaircutMantissaAfter = shortfallHaircutMantissa();
assert shortfallHaircutMantissaBefore == shortfallHaircutMantissaAfter;

13. Rule: noMethodChangesPurchaseToken - confirms the purchase token's address remains unaltered through contract operations, ensuring continuity and reliability in financial mechanisms involving the token.

address purchaseTokenBefore = purchaseToken();
f(e, args);
address purchaseTokenAfter = purchaseToken();
assert purchaseTokenBefore == purchaseTokenAfter;

14. Rule: onlyAllowedMethodsMayChangeTermContracts - specifies that term contract addresses can only be modified through designated methods, preventing unauthorized updates and maintaining contract ecosystem integrity.

address termRepoCollateralManagerBefore = termRepoCollateralManager();
address termRepoRolloverManagerBefore = termRepoRolloverManager();
address termRepoLockerBefore = termRepoLocker();
address termRepoTokenBefore = termRepoToken();
address termControllerBefore = termControllerAddress();
address emitterBefore = emitterAddress();
f(e, args);
assert termRepoCollateralManager() == termRepoCollateralManagerBefore, "termRepoCollateralManager cannot be changed";
assert termRepoRolloverManager() == termRepoRolloverManagerBefore, "termRepoRolloverManager cannot be changed";
assert termRepoLocker() == termRepoLockerBefore, "termRepoLocker cannot be changed";
assert termRepoToken() == termRepoTokenBefore, "termRepoToken cannot be changed";
assert termControllerAddress() == termControllerBefore, "termController cannot be changed";
assert emitterAddress() == emitterBefore, "emitter cannot be changed";

15. Rule: onlyAllowedMethodsMayChangeRepurchaseExposureLedger - limits the conditions under which the repurchase exposure ledger can be altered, ensuring that changes are strictly governed and reflect actual repurchase activities.

uint256 repurchaseExposureLedgerBefore = repurchaseExposureLedger(borrower);
f(e, args);
uint256 repurchaseExposureLedgerAfter = repurchaseExposureLedger(borrower);
assert repurchaseExposureLedgerAfter == repurchaseExposureLedgerBefore, "repurchaseExposureLedger cannot be changed";

16. Rule: burnCollapseExposureMonotonicBehavior - verifies that burning to collapse exposure reduces the caller's repo token balance, their repurchase obligation, and the total outstanding repurchase exposure monotonically, ensuring systemic risk reduction and individual accountability.

uint256 collapserRepoTokenBalanceBefore = collapsingRepoToken.balanceOf(e.msg.sender);
uint256 collapserRepoExposureBefore = getBorrowerRepurchaseObligation(e.msg.sender);
uint256 totalOutstandingRepurchaseExposureBefore = totalOutstandingRepurchaseExposure();

burnCollapseExposure(e, amount);

uint256 collapserRepoTokenBalanceAfter = collapsingRepoToken.balanceOf(e.msg.sender);
uint256 collapserRepoExposureAfter = getBorrowerRepurchaseObligation(e.msg.sender);
uint256 totalOutstandingRepurchaseExposureAfter = totalOutstandingRepurchaseExposure();

assert collapserRepoTokenBalanceBefore >= collapserRepoTokenBalanceAfter;
assert collapserRepoExposureBefore >= collapserRepoExposureAfter;
assert totalOutstandingRepurchaseExposureBefore >= totalOutstandingRepurchaseExposureAfter;

17. Rule: burnCollapseExposureIntegrity - ensures that burning for exposure collapse adjusts the repo token balance, repurchase obligation, and total outstanding repurchase exposure by the expected amounts, reflecting accurate and fair financial adjustments.

uint256 collapserRepoTokenBalanceBefore = collapsingRepoToken.balanceOf(e.msg.sender);
uint256 collapserRepoExposureBefore = getBorrowerRepurchaseObligation(e.msg.sender);
uint256 totalOutstandingRepurchaseExposureBefore = totalOutstandingRepurchaseExposure();

burnCollapseExposure(e, amount);

uint256 collapserRepoTokenBalanceAfter = collapsingRepoToken.balanceOf(e.msg.sender);
uint256 collapserRepoExposureAfter = getBorrowerRepurchaseObligation(e.msg.sender);
uint256 totalOutstandingRepurchaseExposureAfter = totalOutstandingRepurchaseExposure();

assert collapserRepoTokenBalanceBefore - collapserRepoTokenBalanceAfter == expectedTokenBalanceDecrease;
assert collapserRepoExposureBefore - collapserRepoExposureAfter == expectedObligationDecrease;
assert totalOutstandingRepurchaseExposureBefore - totalOutstandingRepurchaseExposureAfter == expectedExposureDecrease;

18. Rule: burnCollapseExposureDoesNotAffectThirdParty - confirms that an individual's action to burn repo tokens to collapse exposure does not impact the financial positions (token balances or repurchase obligations) of unrelated third parties, maintaining isolation of financial activities.

uint256 thirdPartyRepoTokenBalanceBefore = collapsingRepoToken.balanceOf(thirdParty);
uint256 thirdPartyRepoExposureBefore = getBorrowerRepurchaseObligation(thirdParty);

burnCollapseExposure(e, amount);

uint256 thirdPartyRepoTokenBalanceAfter = collapsingRepoToken.balanceOf(thirdParty);
uint256 thirdPartyRepoExposureAfter = getBorrowerRepurchaseObligation(thirdParty);

assert thirdPartyRepoTokenBalanceBefore == thirdPartyRepoTokenBalanceAfter;
assert thirdPartyRepoExposureBefore == thirdPartyRepoExposureAfter;

19. Rule: burnCollapseExposureRevertConditions- check for revert under the defined expected conditions, ensuring operation adherence to defined rules.

bool payable = e.msg.value > 0;
    bool zeroAddressSender = e.msg.sender == 0;
    bool pastRepurchaseWindow = e.block.timestamp >= endOfRepurchaseWindow();
    bool zeroBorrowerRepurchaseObligation = getBorrowerRepurchaseObligation(e.msg.sender) == 0;
    bool zeroMaxRepayment = maxRepayment == 0;
    bool servicerNotHaveRepoTokenBurnerRole = !collapsingRepoToken.hasRole(collapsingRepoToken.BURNER_ROLE(), currentContract);
    bool borrowerRepoTokenBalanceTooLow = (collapserRepoTokenBalanceBefore < collapseAmount && repaymentInTokens == collapseAmount) || (collapserRepoTokenBalanceBefore < maxRepaymentInRepoTokens && maxRepaymentInRepoTokens <= collapseAmount);
    bool repoTokenBurningPaused = collapsingRepoToken.burningPaused();
    bool noServicerRoleOnCollateralManager = !collapsingCollateralManager.hasRole(collapsingCollateralManager.SERVICER_ROLE(), currentContract) && maxRepaymentInRepoTokens <= collapseAmount;
    bool collatManagerDoesNotHaveLockerServicerRole = !collapsingLocker.hasRole(collapsingLocker.SERVICER_ROLE(), collapsingCollateralManager) && maxRepaymentInRepoTokens <= collapseAmount && totalCollateral(e.msg.sender) > 0; 
    bool lockerTransfersPaused = collapsingLocker.transfersPaused() && maxRepaymentInRepoTokens <= collapseAmount && totalCollateral(e.msg.sender) > 0; // Only in the case of full repayment
    bool termRepoUnbalanced = (totalOutstandingRepurchaseExposure() - repaymentInPurchaseToken + totalRepurchaseCollected() ) / (10 ^ 4) != (((((collapsingRepoToken.totalSupply() -  repaymentInTokens) * expScale * collapsingRepoToken.redemptionValue()) / expScale ) / expScale) / 10 ^ 4);

    bool isExpectedToRevert = payable || zeroAddressSender || pastRepurchaseWindow  || zeroBorrowerRepurchaseObligation || zeroMaxRepayment || servicerNotHaveRepoTokenBurnerRole || borrowerRepoTokenBalanceTooLow || repoTokenBurningPaused || noServicerRoleOnCollateralManager ||  collatManagerDoesNotHaveLockerServicerRole || lockerTransfersPaused || termRepoUnbalanced ;

    assert lastReverted <=> isExpectedToRevert;

20. Rule: mintOpenExposureMonotonicBehavior - ensures that minting open exposure increases the minter's repo token balance, their repurchase obligation, and the total outstanding repurchase exposure, as well as the minter's collateral balance, indicating correct operation and accountability in minting activities.

uint256 minterRepoTokenBalanceBefore = mintingRepoToken.balanceOf(e.msg.sender);
uint256 minterRepoExposureBefore = getBorrowerRepurchaseObligation(e.msg.sender);
uint256 totalOutstandingRepurchaseExposureBefore = totalOutstandingRepurchaseExposure();
uint256 collateralBalanceBefore = mintingCollateralManager.getCollateralBalance(e.msg.sender, collateralTokenAddress);

mintOpenExposure(e, amount, collateralAmounts);

uint256 minterRepoTokenBalanceAfter = mintingRepoToken.balanceOf(e.msg.sender);
uint256 minterRepoExposureAfter = getBorrowerRepurchaseObligation(e.msg.sender);
uint256 totalOutstandingRepurchaseExposureAfter = totalOutstandingRepurchaseExposure();
uint256 collateralBalanceAfter = mintingCollateralManager.getCollateralBalance(e.msg.sender, collateralTokenAddress);

assert minterRepoTokenBalanceBefore <= minterRepoTokenBalanceAfter;
assert minterRepoExposureBefore <= minterRepoExposureAfter;
assert totalOutstandingRepurchaseExposureBefore <= totalOutstandingRepurchaseExposureAfter;
assert collateralBalanceBefore <= collateralBalanceAfter;

21. Rule: mintOpenExposureIntegrity - confirms that minting for open exposure results in expected increases in the minter's repo token balance and repurchase obligation, as well as the total outstanding repurchase exposure, demonstrating the transaction's impact aligns with predefined financial mechanisms.

uint256 minterRepoTokenBalanceBefore = mintingRepoToken.balanceOf(e.msg.sender);
uint256 minterRepoExposureBefore = getBorrowerRepurchaseObligation(e.msg.sender);
uint256 totalOutstandingRepurchaseExposureBefore = totalOutstandingRepurchaseExposure();

mintOpenExposure(e, amount, collateralAmounts);

uint256 minterRepoTokenBalanceAfter = mintingRepoToken.balanceOf(e.msg.sender);
uint256 minterRepoExposureAfter = getBorrowerRepurchaseObligation(e.msg.sender);
uint256 totalOutstandingRepurchaseExposureAfter = totalOutstandingRepurchaseExposure();

assert minterRepoTokenBalanceAfter - minterRepoTokenBalanceBefore == expectedIncrease;
assert minterRepoExposureAfter - minterRepoExposureBefore == expectedIncrease;
assert totalOutstandingRepurchaseExposureAfter - totalOutstandingRepurchaseExposureBefore == expectedIncrease;

22. Rule: mintOpenExposureDoesNotAffectThirdParty - verifies that a minter's action to open exposure does not alter the repo token balances of unrelated third parties, ensuring the isolation of minting effects within the financial ecosystem.

uint256 thirdPartyBalanceBefore = mintingRepoToken.balanceOf(thirdParty);

mintOpenExposure(e, amount, collateralAmounts);

uint256 thirdPartyBalanceAfter = mintingRepoToken.balanceOf(thirdParty);

assert thirdPartyBalanceBefore == thirdPartyBalanceAfter;

23. Rule: mintOpenExposureRevertConditions - check for revert under the defined expected conditions, ensuring operation adherence to defined rules.

 bool payable = e.msg.value > 0;
    bool callerNotSpecialist = !hasRole(SPECIALIST_ROLE(), 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];
    bool lockerTransfersPaused = mintingLocker.transfersPaused();
    bool noLockerServicerAccessForCollatManager = !mintingLocker.hasRole(locker.SERVICER_ROLE(), mintingCollateralManager);
    bool collateralAmountsNotProperLength = assert_uint8(collateralAmounts.length) != mintingCollateralManager.numOfAcceptedCollateralTokens();
    bool afterMaturity = e.block.timestamp > maturityTimestamp();
    bool noServicerRoleOnCollateralManager = !repaymentCollateralManager.hasRole(repaymentCollateralManager.SERVICER_ROLE(), currentContract);

    bool isExpectedToRevert = payable || callerNotSpecialist || noMinterRole || noServicerRoleToCollatManager || borrowerNotEnoughCollateralBalance || lockerTransfersPaused || noLockerServicerAccessForCollatManager || collateralAmountsNotProperLength  || afterMaturity || noServicerRoleOnCollateralManager;

mintOpenExposure@withrevert(e, amount, collateralAmounts);

assert lastReverted <=> isExpectedToRevert;

24. Rule: redemptionsMonotonicBehavior - verifies that redemption operations result in expected changes to the balances and obligations involved, ensuring that the redeemer's repo token balance decreases, their purchase token balance increases, and the overall repurchase obligations and available tokens within the locker adjust accordingly.

uint256 redeemerRepoTokenBalanceBefore = repoTokenRedempt.balanceOf(redeemer);
uint256 totalRepurchaseCollectedBefore = totalRepurchaseCollected();
uint256 redeemerPurchaseTokenBalanceBefore = tokenRedempt.balanceOf(redeemer);
uint256 lockerPurchaseTokenBalanceBefore = tokenRedempt.balanceOf(lockerRedempt);

redeemTermRepoTokens(e, redeemer, amount);

uint256 redeemerRepoTokenBalanceAfter = repoTokenRedempt.balanceOf(redeemer);
uint256 totalRepurchaseCollectedAfter = totalRepurchaseCollected();
uint256 redeemerPurchaseTokenBalanceAfter = tokenRedempt.balanceOf(redeemer);
uint256 lockerPurchaseTokenBalanceAfter = tokenRedempt.balanceOf(lockerRedempt);

assert redeemerRepoTokenBalanceBefore >= redeemerRepoTokenBalanceAfter;
assert totalRepurchaseCollectedBefore >= totalRepurchaseCollectedAfter;
assert redeemerPurchaseTokenBalanceBefore <= redeemerPurchaseTokenBalanceAfter;
assert lockerPurchaseTokenBalanceBefore >= lockerPurchaseTokenBalanceAfter;

25. Rule: redemptionsIntegrity - confirms that the redemption of repo tokens by a redeemer leads to the precise adjustments in the total repurchase collected, the repo token balance of the redeemer, and the purchase token balance in accordance with the redemption value and terms defined, reflecting the accurate financial transaction and impact.

uint256 redeemerRepoTokenBalanceBefore = repoTokenRedempt.balanceOf(redeemer);
uint256 totalRepurchaseCollectedBefore = totalRepurchaseCollected();
uint256 redeemerPurchaseTokenBalanceBefore = tokenRedempt.balanceOf(redeemer);
uint256 lockerPurchaseTokenBalanceBefore = tokenRedempt.balanceOf(lockerRedempt);

redeemTermRepoTokens(e, redeemer, amount);

uint256 redeemerRepoTokenBalanceAfter = repoTokenRedempt.balanceOf(redeemer);
uint256 totalRepurchaseCollectedAfter = totalRepurchaseCollected();
uint256 redeemerPurchaseTokenBalanceAfter = tokenRedempt.balanceOf(redeemer);
uint256 lockerPurchaseTokenBalanceAfter = tokenRedempt.balanceOf(lockerRedempt);

assert redeemerRepoTokenBalanceBefore - amount == redeemerRepoTokenBalanceAfter;
assert totalRepurchaseCollectedBefore - expectedRedemption == totalRepurchaseCollectedAfter;
assert redeemerPurchaseTokenBalanceAfter - expectedRedemption == redeemerPurchaseTokenBalanceBefore;
assert lockerPurchaseTokenBalanceBefore - expectedRedemption == lockerPurchaseTokenBalanceAfter;

26. Rule: redemptionsDoesNotAffectThirdParty - ensures that a redemption action taken by one participant does not inadvertently alter the financial position or balances of unrelated third parties, maintaining the integrity and isolation of individual transactions within the ecosystem.

uint256 thirdPartyRepoTokenBalanceBefore = repoTokenRedempt.balanceOf(thirdParty);
uint256 thirdPartyPurchaseTokenBalanceBefore = tokenRedempt.balanceOf(thirdParty);

redeemTermRepoTokens(e, redeemer, amount);

uint256 thirdPartyRepoTokenBalanceAfter = repoTokenRedempt.balanceOf(thirdParty);
uint256 thirdPartyPurchaseTokenBalanceAfter = tokenRedempt.balanceOf(thirdParty);

assert thirdPartyRepoTokenBalanceBefore == thirdPartyRepoTokenBalanceAfter;
assert thirdPartyPurchaseTokenBalanceBefore == thirdPartyPurchaseTokenBalanceAfter;

27. Rule: redemptionsRevertConditions - evaluates whether the operation correctly reverts under the prescribed conditions, ensuring compliance with defined contractual behaviors and protections.

bool payable = e.msg.value > 0;
    bool zeroAddress = redeemer == 0;
    bool beforeRedemption = e.block.timestamp <= redemptionTimestamp();
    bool zeroRepoTokens = repoTokenRedempt.balanceOf(redeemer) == 0;
    bool encumberedCollateralRemaining = collateralManagerRedempt.encumberedCollateralRemaining() && (repoTokenRedempt.totalRedemptionValue() > assert_uint256(totalRepurchaseCollected() + 10 ^ 4));
    bool servicerNotHaveRepoTokenBurnerRole = !repoTokenRedempt.hasRole(repoTokenRedempt.BURNER_ROLE(), currentContract);
    bool repoTokenBurningPaused = repoTokenRedempt.burningPaused();
    bool noServicerAccessToLocker = !lockerRedempt.hasRole(lockerRedempt.SERVICER_ROLE(), currentContract);
    bool lockerTransfersPaused = lockerRedempt.transfersPaused();
    bool notEnoughRepoTokens = repoTokenRedempt.balanceOf(redeemer) < amount; 
    bool termRepoUnbalanced = (termRepoUnbalancedLeftSide) / (10 ^ 4) != (totalRedemptionValueExpected / 10 ^ 4);

    bool isExpectedToRevert = payable || zeroAddress || beforeRedemption || zeroRepoTokens || encumberedCollateralRemaining || servicerNotHaveRepoTokenBurnerRole || repoTokenBurningPaused || lockerTransfersPaused || noServicerAccessToLocker ||  notEnoughRepoTokens || termRepoUnbalanced;

redeemTermRepoTokens@withrevert(e, redeemer, amount);

assert lastReverted <=> isExpectedToRevert;

28. Rule: repaymentsMonotonicBehavior - validates that repayments lead to expected monotonic changes in borrower obligations and system totals, ensuring borrower balances and overall repurchase exposures decrease as payments are made, while the total repurchase collected and potentially the collateral values adjust accordingly.

uint256 borrowerBalanceBefore = getBorrowerRepurchaseObligation(borrower);
uint256 totalOutstandingRepurchaseExposureBefore = totalOutstandingRepurchaseExposure();
uint256 totalRepurchaseCollectedBefore = totalRepurchaseCollected();
uint256 borrowerCollateralBefore = totalCollateral(borrower);

submitRepurchasePayment(e, repayment);

uint256 borrowerBalanceAfter = getBorrowerRepurchaseObligation(borrower);
uint256 totalOutstandingRepurchaseExposureAfter = totalOutstandingRepurchaseExposure();
uint256 totalRepurchaseCollectedAfter = totalRepurchaseCollected();
uint256 borrowerCollateralAfter = totalCollateral(borrower);

assert borrowerBalanceBefore >= borrowerBalanceAfter;
assert totalOutstandingRepurchaseExposureBefore >= totalOutstandingRepurchaseExposureAfter;
assert totalRepurchaseCollectedBefore <= totalRepurchaseCollectedAfter;
assert borrowerCollateralAfter <= borrowerCollateralBefore;

29. Rule: repaymentsIntegrity - ensures the integrity of repayments by verifying that the repayments correctly decrease the borrower's obligations and appropriately adjust the system's repurchase exposure and collected totals, with specific attention to the treatment of collateral in the event of complete repayment.

uint256 borrowerBalanceBefore = getBorrowerRepurchaseObligation(borrower);
uint256 totalOutstandingRepurchaseExposureBefore = totalOutstandingRepurchaseExposure();
uint256 totalRepurchaseCollectedBefore = totalRepurchaseCollected();

submitRepurchasePayment(e, repayment);

uint256 borrowerBalanceAfter = getBorrowerRepurchaseObligation(borrower);
uint256 totalOutstandingRepurchaseExposureAfter = totalOutstandingRepurchaseExposure();
uint256 totalRepurchaseCollectedAfter = totalRepurchaseCollected();

assert borrowerBalanceBefore - repayment == borrowerBalanceAfter;
assert totalOutstandingRepurchaseExposureBefore - repayment == totalOutstandingRepurchaseExposureAfter;
assert totalRepurchaseCollectedBefore + repayment == totalRepurchaseCollectedAfter;
assert borrowerBalanceAfter == 0 ? totalCollateral(borrower) == 0 : totalCollateral(borrower) remains unchanged;

30. Rule: repaymentsDoesNotAffectThirdParty - confirms that a borrower's repayment activity does not inadvertently affect the financial obligations or collateral standings of any unrelated third parties, preserving the isolation and accuracy of individual account statuses within the system.

uint256 thirdPartyObligationBefore = getBorrowerRepurchaseObligation(thirdParty);

submitRepurchasePayment(e, repayment);

uint256 thirdPartyObligationAfter = getBorrowerRepurchaseObligation(thirdParty);

assert thirdPartyObligationBefore == thirdPartyObligationAfter;

31. Rule: repaymentsRevertingConditions - check if the operation correctly reverts under specified conditions, ensuring adherence to defined contractual behaviors and safeguards.

bool payable = e.msg.value > 0;
    bool lockerTransfersPaused = locker.transfersPaused();
    bool noLockerServicerAccess = !locker.hasRole(locker.SERVICER_ROLE(), currentContract);
    bool allowanceTooLow = token.allowance( borrower, termRepoLocker()) < repayment;
    bool borrowTokenBalanceTooLow = token.balanceOf(borrower) < repayment;
    bool afterRepurchaseWindow = e.block.timestamp >= endOfRepurchaseWindow();
    bool borrowerZeroObligation = getBorrowerRepurchaseObligation(borrower) == 0;
    bool uintMaxRepayment = repayment == max_uint256;
    bool repaymentGreaterThanMax = repaymentAmount > maxRepayment;
    bool noServicerRoleOnCollateralManager = !repaymentCollateralManager.hasRole(repaymentCollateralManager.SERVICER_ROLE(), currentContract);

    bool isExpectedToRevert = payable || lockerTransfersPaused || noLockerServicerAccess || borrowTokenBalanceTooLow || allowanceTooLow || afterRepurchaseWindow || borrowerZeroObligation || uintMaxRepayment || repaymentGreaterThanMax || noServicerRoleOnCollateralManager;

submitRepurchasePayment@withrevert(e, repayment);

assert lastReverted <=> isExpectedToRevert;

32. Rule: liquidatorCoverExposureIntegrity - validates the integrity of a liquidation process where a liquidator covers the exposure of a borrower using purchase tokens. It checks that balances and obligations adjust correctly, reflecting the liquidation payment in system totals and individual accounts.

uint256 borrowerObligationBefore = getBorrowerRepurchaseObligation(borrower);
uint256 totalOutstandingBefore = totalOutstandingRepurchaseExposure();
uint256 totalCollectedBefore = totalRepurchaseCollected();
uint256 liquidatorBalanceBefore = liquidationRepaymentExposureToken.balanceOf(liquidator);
uint256 lockerBalanceBefore = liquidationRepaymentExposureToken.balanceOf(termRepoLocker());

liquidatorCoverExposure(e, borrower, liquidator, amountToCover);

uint256 borrowerObligationAfter = getBorrowerRepurchaseObligation(borrower);
uint256 totalOutstandingAfter = totalOutstandingRepurchaseExposure();
uint256 totalCollectedAfter = totalRepurchaseCollected();
uint256 liquidatorBalanceAfter = liquidationRepaymentExposureToken.balanceOf(liquidator);
uint256 lockerBalanceAfter = liquidationRepaymentExposureToken.balanceOf(termRepoLocker());

assert borrowerObligationBefore - borrowerObligationAfter == amountToCover;
assert totalOutstandingBefore - totalOutstandingAfter == amountToCover;
assert totalCollectedAfter - totalCollectedBefore == amountToCover;
assert liquidatorBalanceBefore - liquidatorBalanceAfter == amountToCover;
assert lockerBalanceAfter - lockerBalanceBefore == amountToCover;

33. Rule: liquidatorCoverExposureDoesNotAffectThirdParty - ensures that the liquidation process does not inadvertently impact the financial status or obligations of any third parties, maintaining the precision and isolation of account transactions within the system.

uint256 thirdPartyObligationBefore = getBorrowerRepurchaseObligation(thirdParty);
uint256 thirdPartyBalanceBefore = liquidationRepaymentExposureToken.balanceOf(thirdParty);

liquidatorCoverExposure(e, borrower, liquidator, amountToCover);

uint256 thirdPartyObligationAfter = getBorrowerRepurchaseObligation(thirdParty);
uint256 thirdPartyBalanceAfter = liquidationRepaymentExposureToken.balanceOf(thirdParty);

assert thirdPartyObligationBefore == thirdPartyObligationAfter;
assert thirdPartyBalanceBefore == thirdPartyBalanceAfter;

34. Rule: liquidatorCoverExposureRevertConditions - evaluate if the transaction reverts as expected under identified conditions, ensuring compliance with system rules and safeguards.

bool payable = e.msg.value > 0;
    bool callerNotCollateralManager = !hasRole(COLLATERAL_MANAGER(), e.msg.sender);
    bool servicerDoesNotHaveLockerServicerRole = !liquidationRepaymentExposureLocker.hasRole(liquidationRepaymentExposureLocker.SERVICER_ROLE(), currentContract);
    bool lockerTransfersPaused = liquidationRepaymentExposureLocker.transfersPaused();
    bool allowanceTooLow = liquidationRepaymentExposureToken.allowance( liquidator, termRepoLocker()) < amountToCover;
    bool liquidatorTokenBalanceTooLow = liquidationRepaymentExposureToken.balanceOf(liquidator) < amountToCover;
    bool borrowBalancecLowerThanCoverAmount = getBorrowerRepurchaseObligation(borrower) < amountToCover;

    bool isExpectedToRevert = payable || callerNotCollateralManager || servicerDoesNotHaveLockerServicerRole  || lockerTransfersPaused || liquidatorTokenBalanceTooLow || allowanceTooLow || borrowBalancecLowerThanCoverAmount ;

liquidatorCoverExposure@withrevert(e, borrower, liquidator, amountToCover);

assert lastReverted <=> isExpectedToRevert;

35. Rule: liquidatorCoverExposureWithRepoTokenIntegrity - examines the proper functioning of liquidation via repo tokens, verifying that such transactions correctly reduce borrower obligations and adjust system and participant balances in accordance with the repo tokens used in the liquidation.

uint256 borrowerObligationBefore = getBorrowerRepurchaseObligation(borrower);
uint256 totalOutstandingBefore = totalOutstandingRepurchaseExposure();
uint256 liquidatorRepoBalanceBefore = liquidationRepaymentExposureRepoToken.balanceOf(liquidator);
uint256 repoTotalSupplyBefore = liquidationRepaymentExposureRepoToken.totalSupply();

liquidatorCoverExposureWithRepoToken(e, borrower, liquidator, amountOfRepoToken);

uint256 borrowerObligationAfter = getBorrowerRepurchaseObligation(borrower);
uint256 totalOutstandingAfter = totalOutstandingRepurchaseExposure();
uint256 liquidatorRepoBalanceAfter = liquidationRepaymentExposureRepoToken.balanceOf(liquidator);
uint256 repoTotalSupplyAfter = liquidationRepaymentExposureRepoToken.totalSupply();

assert borrowerObligationBefore - borrowerObligationAfter == calculatedAmountCovered;
assert totalOutstandingBefore - totalOutstandingAfter == calculatedAmountCovered;
assert liquidatorRepoBalanceBefore - liquidatorRepoBalanceAfter == amountOfRepoToken;
assert repoTotalSupplyBefore - repoTotalSupplyAfter == amountOfRepoToken;

36. Rule: liquidatorCoverExposureWithRepoTokenRevertConditions - define conditions that would lead to a transaction revert; aggregate revert conditions to determine expectation; eliquidation attempt with potential revert and validate against expected outcome; ensure actual revert aligns with expectations based on identified conditions.

bool payable = e.msg.value > 0;
bool callerNotCollateralManager = !hasRole(COLLATERAL_MANAGER(), e.msg.sender);
bool liquidatorIsAddressZero = liquidator == 0;
bool servicerNotHaveRepoTokenBurnerRole = !liquidationRepaymentExposureRepoToken.hasRole(liquidationRepaymentExposureRepoToken.BURNER_ROLE(), currentContract);
bool liquidatorTokenBalanceTooLow = liquidationRepaymentExposureRepoToken.balanceOf(liquidator) < amountOfRepoToken;
bool repoTokenBurningPaused = liquidationRepaymentExposureRepoToken.burningPaused();
bool termPoolBalanceThresholdBreached = ((totalOutstandingRepurchaseExposure() - amountToCover + totalRepurchaseCollected()) / 10^4) != (((((liquidationRepaymentExposureRepoToken.totalSupply() - amountOfRepoToken) * expScale * liquidationRepaymentExposureRepoToken.redemptionValue()) / expScale) / expScale) / 10^4);
bool borrowBalanceLowerThanCoverAmount = borrowerObligationBefore < amountToCover;

// Aggregate revert conditions to determine expectation
isExpectedToRevert = payable || callerNotCollateralManager || liquidatorIsAddressZero || servicerNotHaveRepoTokenBurnerRole || liquidatorTokenBalanceTooLow || repoTokenBurningPaused || termPoolBalanceThresholdBreached || borrowBalanceLowerThanCoverAmount;

// Execute liquidation attempt with potential revert and validate against expected outcome
liquidatorCoverExposureWithRepoToken@withrevert(e, borrower, liquidator, amountOfRepoToken);
assert lastReverted <=> isExpectedToRevert; // Ensure actual revert aligns with expectations based on identified conditions

37. Rule: openExposureOnRolloverNewIntegrity - ensures that all relevant balances properly accounted for after opening a repoExposure on account of a successful rollover.

assert balanceAfter == balanceBefore + repurchasePrice;
    assert totalOutstandingRepurchaseExposureAfter == totalOutstandingRepurchaseExposureBefore + repurchasePrice;
    assert tokenBalanceTermRepoLockerAfter + purchasePrice == tokenBalanceTermRepoLockerBefore;
    assert tokenBalancePreviousTermRepoLockerAfter == tokenBalancePreviousTermRepoLockerBefore + previousRepoLockerRepayment;
    assert  tokenBalanceTreasuryAfter == tokenBalanceTreasuryBefore + protocolShare;

38. Rule: openExposureOnRolloverNewDoesNotAffectThirdParty - verifies that rolling over loan exposures from one account does not affect third-party balances.

mathint balanceBefore = getBorrowerRepurchaseObligation(borrower2);

    openExposureOnRolloverNew(e, borrower, purchasePrice, repurchasePrice, previousTermRepoLocker, dayCountFractionMantissa);

    mathint balanceAfter = getBorrowerRepurchaseObligation(borrower2);

    assert balanceAfter == balanceBefore;

39. Rule: openExposureOnRolloverNewRevertConditions- check for revert under the defined expected conditions, ensuring operation adherence to defined rules.

bool payable = e.msg.value > 0;
    bool callerNotAuctioneer = !hasRole(AUCTIONEER(), e.msg.sender);
    bool afterMaturity = e.block.timestamp >= maturityTimestamp();
    bool lockerTransfersPaused = rolloverExposureLocker.transfersPaused();
    bool servicerNoLockerAccess = !rolloverExposureLocker.hasRole(rolloverExposureLocker.SERVICER_ROLE(), currentContract);

    bool lockerTokenBalanceTooLow = rolloverExposureToken.balanceOf(rolloverExposureLocker) < purchasePrice;

    bool isExpectedToRevert = payable ||   callerNotAuctioneer || afterMaturity || lockerTransfersPaused  || servicerNoLockerAccess  || lockerTokenBalanceTooLow;

    openExposureOnRolloverNew@withrevert(e, borrower, purchasePrice, repurchasePrice, previousTermRepoLocker, dayCountFractionMantissa);

    
    assert lastReverted <=> isExpectedToRevert;

40. Rule: closeExposureOnRolloverExistingIntegrity - ensures that all relevant balances properly accounted for after closing a repoExposure on account of a successful rollover.

assert balanceBefore == balanceAfter + actualRolloverSettlementAmount;
    assert totalOutstandingRepurchaseExposureBefore == totalOutstandingRepurchaseExposureAfter + actualRolloverSettlementAmount;
    assert amountCollectedAfter == amountCollectedBefore + actualRolloverSettlementAmount;
    assert rolloverExposureRolloverManager.getRolloverInstructions(borrower).processed;

41. Rule: closeExposureOnRolloverExistingDoesNotAffectThirdParty - verifies that rolling over loan exposures from one account does not affect third-party balances.

    mathint balanceBefore = getBorrowerRepurchaseObligation(borrower2);

    closeExposureOnRolloverExisting(e, borrower, rolloverSettlementAmount);

    mathint balanceAfter = getBorrowerRepurchaseObligation(borrower2);

    assert balanceBefore == balanceAfter;

42. Rule: closeExposureOnRolloverExistingRevertConditions- check for revert under the defined expected conditions, ensuring operation adherence to defined rules.