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

Issue:	Zero Max Repayment Allowed in burnCollapseExposure
Description:	In the case where a borrower (i) has an outstanding repurchase exposure that (ii) has also been submitted as an open rollover such that (iii) the amount they are able to collapse is 0, the burnCollapseExposure function nevertheless executes, calling 0 transfers and adding 0 to accounting for a burn collapse exposure . Although there is no harm done, this is a waste of gas for the user.
Mitigation/Fix:	Add a revert condition to burnCollapseExposure to revert execution if the max repayment a borrower can make is 0.
Rule coverage:	burnCollapseExposureIntegrity burnCollapseExposureRevertConditions

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";
}

1. 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

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

assert totalSupplyBefore <= totalSupplyAfter;

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

assert numberOfChangesOfBalancesAfter <= numberOfChangesOfBalancesBefore + 2;

1. 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";

1. 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);

1. 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);

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

f(e,args);
satisfy true;

1. 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)
);

1. 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 )
    );

1. 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;

1. 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.

1. 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;

1. 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;

1. 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;

1. 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;

1. 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;

1. 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;

1. 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;

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

assert balanceOf(addr2) == before;

1. 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;

1. 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);

1. 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];

1. 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;

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

assert balanceOf(addr2) == before;

1. 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);

1. 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;

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

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

1. 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];

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

assert allowance(holder, spender) == amount;

1. 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;

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

assert thirdPartyAllowanceBefore == thirdPartyAllowanceBefore;

1. 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);

1. 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;

1. 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;

1. 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);

1. 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);

1. 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);

1. 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);

1. 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;
}

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

f(e,args);
satisfy true;

1. 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;

1. 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;

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

pauseTransfers(e);
assert transfersPaused();

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

unpauseTransfers(e);
assert !transfersPaused();

1. 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);

1. 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
}

1. 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);

1. 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;

1. 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);

1. 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;

1. 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());

1. 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));

1. 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;

1. 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;

1. 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;

1. 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;

1. 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;

1. 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;

1. 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";

1. 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";

1. 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;

1. 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;

1. 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;

1. 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;

1. 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;

1. 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;

1. 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;

1. 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;

1. 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;

1. 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;

1. 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;

1. 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;

1. 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;

1. 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;

1. 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;

1. 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;

1. 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;

1. 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;

1. 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;

1. 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;

1. 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

1. 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;

1. 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;

1. 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;

1. 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;

1. 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;

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

    bool payable = e.msg.value > 0;
    bool callerNotRolloverTargetAuctioneer = !hasRole(ROLLOVER_TARGET_AUCTIONEER_ROLE(), e.msg.sender);
    bool beforeMaturity = e.block.timestamp < maturityTimestamp();
    bool afterRepurchaseWindow = e.block.timestamp >= endOfRepurchaseWindow();
    bool servicerDoesNotHaveRolloverFulfillerRole = !rolloverExposureRolloverManager.hasRole(rolloverExposureRolloverManager.ROLLOVER_BID_FULFILLER_ROLE(), currentContract);

    bool isExpectedToRevert = payable ||   callerNotRolloverTargetAuctioneer || beforeMaturity || afterRepurchaseWindow || servicerDoesNotHaveRolloverFulfillerRole;

    closeExposureOnRolloverExisting@withrevert(e, borrower, rolloverSettlementAmount);
    
    assert lastReverted <=> isExpectedToRevert;

1. Rule: fulfillOfferIntegrity - ensures repoTokens are properly minted to a user's address when their offer is fulfilled.

assert offerorRepoTokenBalanceAfter == offerorRepoTokenBalanceBefore + tokensMinted,

1. Rule: fulfillBidIntegrity - check that the bidder's token balance has decreased and protocol's token balance has increased after fulfillBid.

    // Check that the bidder's token balance has decreased.
    assert bidderTokenBalanceAfter == bidderTokenBalanceBefore + (to_mathint(purchasePrice) - protocolShare)

    // Check that the protocol's token balance has increased.
    assert protocolTokenBalanceAfter == protocolTokenBalanceBefore + protocolShare

1. Rule: fulfillOfferRevertsIfNotValid - ensure that fulfillOffer reverts if not valid.

bool notAuctioneer = !hasRole(AUCTIONEER(), e.msg.sender);
    bool servicerNotMinterRole = !repoTokenFulfill.hasRole(repoTokenFulfill.MINTER_ROLE(), currentContract);
    bool msgHasValue = e.msg.value != 0;
    bool divByZero = repoTokenFulfill.redemptionValue() == 0;
    bool overflow = (repurchasePrice * 10 ^ 36) > 2^256
        || ((repoTokenFulfill.redemptionValue() > 0) && (repoTokenFulfill.totalSupply() + (repurchasePrice * 10^18) / repoTokenFulfill.redemptionValue()) >= 2^256);
    bool mintingPaused = repoTokenFulfill.mintingPaused();
    bool zeroAddress = offeror == 0;
    fulfillOffer@withrevert(e, offeror, purchasePrice, repurchasePrice, offerId);
    assert lastReverted == (
        notAuctioneer ||
        msgHasValue ||
        divByZero ||
        servicerNotMinterRole ||
        overflow ||
        mintingPaused ||
        zeroAddress
    ), "fulfillOffer should revert if not valid";

1. Rule: fulfillBidRevertsIfNotValid - ensure that fulfillBid reverts if not valid.

bool notAuctioneer = !hasRole(AUCTIONEER(), e.msg.sender);
    bool servicerNotServicerRole = !collateralManagerFulfill.hasRole(collateralManagerFulfill.SERVICER_ROLE(), currentContract)
        || !lockerFulfill.hasRole(lockerFulfill.SERVICER_ROLE(), currentContract);
    bool afterMaturity = e.block.timestamp >= maturityTimestamp();
    bool msgHasValue = e.msg.value != 0;
    bool overflowRepurchaseExposureLedger = getBorrowerRepurchaseObligation(bidder) + repurchasePrice >= 2^256;
    bool overflowTotalOutstandingRepurchaseExposure = totalOutstandingRepurchaseExposure() + repurchasePrice >= 2^256;
    bool overflowLockedCollateralLedger0 = collateralManagerFulfill.harnessLockedCollateralLedger(bidder, collateralTokens[0]) + collateralAmounts[0] >= 2^256;
    bool overflowEncumberedCollateralBalance0 = collateralManagerFulfill.encumberedCollateralBalance(collateralTokens[0]) + collateralAmounts[0] >= 2^256;
    mathint dcfServicingFee = dayCountFractionMantissa * servicingFee();
    bool overflowDcfServicingFee = dcfServicingFee >= 2^256;
    mathint dcfServicingFeePrice = (dcfServicingFee / 10^18) * purchasePrice;
    bool overflowDcfServicingFeePrice = dcfServicingFeePrice >= 2^256;
    mathint protocolShare = dcfServicingFeePrice / 10^18;
    bool insufficientBalance = tokenFulfill.balanceOf(lockerFulfill) < purchasePrice;
    bool purchasePriceLessThanProtocolShare = to_mathint(purchasePrice) < protocolShare;
    bool transfersPaused = lockerFulfill.transfersPaused();
    bool overflowTreasuryBalance = tokenFulfill.balanceOf(100) + protocolShare >= 2^256;
    bool overflowBidderBalance = tokenFulfill.balanceOf(bidder) + purchasePrice - protocolShare >= 2^256;
    fulfillBid@withrevert(e, bidder, purchasePrice, repurchasePrice, collateralTokens, collateralAmounts, dayCountFractionMantissa);
    assert lastReverted == (
        notAuctioneer ||
        afterMaturity ||
        msgHasValue ||
        servicerNotServicerRole ||
        overflowRepurchaseExposureLedger ||
        overflowTotalOutstandingRepurchaseExposure ||
        overflowLockedCollateralLedger0 ||
        overflowEncumberedCollateralBalance0 ||
        overflowDcfServicingFee ||
        overflowDcfServicingFeePrice ||
        purchasePriceLessThanProtocolShare ||
        transfersPaused ||
        overflowBidderBalance ||
        overflowTreasuryBalance ||
        overflowBidderBalance ||
        insufficientBalance
    ), "fulfillBid should revert if not valid";

1. Rule: fulfillOfferDoesNotAffectThirdParty - verifies that fulfilling an offer belonging to one account does not affect the third party balances.

assert thirdPartyRepoTokenBalanceBefore == thirdPartyRepoTokenBalanceAfter

1. Rule: fulfillBidDoesNotAffectThirdParty - verifies that fulfilling a bid belonging to from one account does not affect the third party balances.

    assert thirdPartyTokenBalanceBefore == thirdPartyTokenBalanceAfter

1. Rule: lockOfferAmountIntegrity - ensures purchase tokens are properly deducted from a user's address when they lock an offer.

assert offerorPurchaseTokenBalanceAfter == offerorPurchaseTokenBalanceBefore - to_mathint(amount)

1. Rule: unlockOfferAmountIntegrity - ensures purchase tokens are properly transferred to a user's address when they unlock an offer.

assert offerorPurchaseTokenBalanceAfter == offerorPurchaseTokenBalanceBefore + to_mathint(amount)

1. Rule: lockOfferAmountDoesNotAffectThirdParty - verifies that locking an offer belonging to one account does not affect the third party balances.

assert thirdPartyPurchaseTokenBalanceBefore == thirdPartyPurchaseTokenBalanceAfter

1. Rule: unlockOfferAmountDoesNotAffectThirdParty - verifies that unlocking an offer belonging to one account does not affect the third party balances..

assert thirdPartyPurchaseTokenBalanceBefore == thirdPartyPurchaseTokenBalanceAfter

1. Rule: lockOfferAmountRevertsWhenInvalid - ensure that locking offers reverts if not valid

    bool includesValue = e.msg.value > 0;
    bool isAuctionLocker = hasRole(AUCTION_LOCKER(), e.msg.sender);
    bool servicerNotServicerRole = !lockerLocking.hasRole(lockerLocking.SERVICER_ROLE(), currentContract);
    bool isLockerPaused = lockerLocking.transfersPaused();
    bool insufficientBalance = purchaseTokenLocking.balanceOf(offeror) < amount;
    bool insufficientAllowance = purchaseTokenLocking.allowance(offeror, lockerLocking) < amount;
    bool overflow = amount + purchaseTokenLocking.balanceOf(lockerLocking) > 2 ^ 256 - 1 && amount > 0;

    lockOfferAmount@withrevert(e, offeror, amount);

assert (
    !isAuctionLocker ||
    includesValue ||
    isLockerPaused ||
    servicerNotServicerRole ||
    insufficientBalance ||
    insufficientAllowance ||
    overflow
) == lastReverted

1. Rule: unlockOfferAmountRevertsWhenInvalid - ensure that unlocking offers reverts if not valid

 bool includesValue = e.msg.value > 0;
    bool isAuctionLocker = hasRole(AUCTION_LOCKER(), e.msg.sender);
    bool servicerNotServicerRole = !lockerLocking.hasRole(lockerLocking.SERVICER_ROLE(), currentContract);
    bool isLockerPaused = lockerLocking.transfersPaused();
    bool insufficientBalance = purchaseTokenLocking.balanceOf(lockerLocking) < amount;
    bool overflow = amount + purchaseTokenLocking.balanceOf(offeror) > 2 ^ 256 - 1 && amount > 0;

    unlockOfferAmount@withrevert(e, offeror, amount);
assert (
    !isAuctionLocker ||
    includesValue ||
    isLockerPaused ||
    servicerNotServicerRole ||
    insufficientBalance ||
    overflow
) == lastReverted

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

assert !lastReverted =>
    hasRole(ADMIN_ROLE(),e.msg.sender)
    || hasRole(AUCTION_LOCKER(),e.msg.sender)
    || hasRole(AUCTIONEER(),e.msg.sender)
    || hasRole(COLLATERAL_MANAGER(),e.msg.sender)
    || hasRole(DEVOPS_ROLE(),e.msg.sender)
    || hasRole(SPECIALIST_ROLE(),e.msg.sender)
    || hasRole(ROLLOVER_MANAGER(),e.msg.sender)
    || hasRole(ROLLOVER_TARGET_AUCTIONEER_ROLE(),e.msg.sender)
    || hasRole(INITIALIZER_ROLE(),e.msg.sender);

1. 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.

assert storeBefore != storeAfter => hasRole(ADMIN_ROLE(),e.msg.sender)
    || hasRole(AUCTION_LOCKER(),e.msg.sender)
    || hasRole(AUCTIONEER(),e.msg.sender)
    || hasRole(COLLATERAL_MANAGER(),e.msg.sender)
    || hasRole(DEVOPS_ROLE(),e.msg.sender)
    || hasRole(SPECIALIST_ROLE(),e.msg.sender)
    || hasRole(ROLLOVER_MANAGER(),e.msg.sender)
    || hasRole(ROLLOVER_TARGET_AUCTIONEER_ROLE(),e.msg.sender)
    || hasRole(INITIALIZER_ROLE(),e.msg.sender);

TermRepoCollateralManager.sol

1. Rule: auctionLockCollateralIntegrity - ensures that all relevant balances are properly reflected on account of locking collateral when calling auctionLockCollateral

assert bidderCollateralBalanceAfter == bidderCollateralBalanceBefore;
assert encumberedCollateralBalanceAfter == encumberedCollateralBalanceBefore;
assert bidderCollateralTokenBalanceAfter + amount == bidderCollateralTokenBalanceBefore;
assert lockerCollateralBalanceBefore + amount == lockerCollateralBalanceAfter;

1. Rule: auctionLockCollateralThirdParty - verifies that locking collateral belonging to one account when calling lockBid does not affect the third party balances

assert thirdPartyBidderCollateralBalanceAfter == thirdPartyBidderCollateralBalanceBefore;
assert thirdPartyBidderCollateralTokenBalanceAfter == thirdPartyBidderCollateralTokenBalanceBefore;

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

bool payable = e.msg.value > 0;
    bool lockerTransfersPaused = lockingCollateralLocker.transfersPaused();
    bool lockerNotPaired = !lockingCollateralLocker.hasRole(lockingCollateralLocker.SERVICER_ROLE(), currentContract);
    bool allowanceTooLow = lockingCollateralToken.allowance( bidder, termRepoLocker()) < amount;
    bool borrowTokenBalanceTooLow = lockingCollateralToken.balanceOf(bidder) < amount;
    bool notAuctionLocker = !hasRole(AUCTION_LOCKER(), e.msg.sender);

    bool isExpectedToRevert = payable || lockerTransfersPaused || lockerNotPaired ||  borrowTokenBalanceTooLow || allowanceTooLow || notAuctionLocker;

    auctionLockCollateral@withrevert(e, bidder, lockingCollateralToken, amount);

assert lastReverted <=> isExpectedToRevert;

1. Rule: auctionUnlockCollateralIntegrity - ensures that all relevant balances are properly reflected on account of locking collateral when calling auctionUnlockCollateral

assert bidderCollateralBalanceAfter == bidderCollateralBalanceBefore;
assert encumberedCollateralBalanceAfter == encumberedCollateralBalanceBefore;
assert bidderCollateralTokenBalanceAfter == bidderCollateralTokenBalanceBefore + amount;
assert lockerCollateralBalanceBefore == lockerCollateralBalanceAfter + amount;

1. Rule: auctionUnlockCollateralThirdParty - verifies that unlocking collateral belonging to one account when calling auctionUnlockCollateral does not affect the third party balances

assert thirdPartyBidderCollateralBalanceAfter == thirdPartyBidderCollateralBalanceBefore;
assert thirdPartyBidderCollateralTokenBalanceAfter == thirdPartyBidderCollateralTokenBalanceBefore;

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

bool payable = e.msg.value > 0;
    bool lockerTransfersPaused = lockingCollateralLocker.transfersPaused();
    bool lockerNotPaired = !lockingCollateralLocker.hasRole(lockingCollateralLocker.SERVICER_ROLE(), currentContract);
    bool lockerTokenBalanceTooLow = lockingCollateralToken.balanceOf(lockingCollateralLocker) < amount;
    bool notAuctionLocker = !hasRole(AUCTION_LOCKER(), e.msg.sender);

    bool isExpectedToRevert = payable || lockerTransfersPaused || lockerNotPaired ||  lockerTokenBalanceTooLow || notAuctionLocker;

    auctionUnlockCollateral@withrevert(e, bidder, lockingCollateralToken, amount);
assert lastReverted <=> isExpectedToRevert;

1. Rule: journalBidCollateralToCollateralManagerIntegrity - ensures that all relevant balances are properly reflected on account of locking collateral when fulfilling a bid.

assert bidderCollateralBalanceAfter == require_uint256(bidderCollateralBalanceBefore + amount);
assert encumberedCollateralBalanceAfter == encumberedCollateralBalanceBefore + amount;
assert bidderCollateralTokenBalanceAfter == bidderCollateralTokenBalanceBefore;
assert lockerCollateralBalanceBefore == lockerCollateralBalanceAfter;

1. Rule: journalBidCollateralToCollateralManagerThirdParty - verifies that journaling collateral to the lockedCollateralLedger when fulfilling a bid belonging to one account does not affect the third party balances.

assert bidderCollateralBalanceAfter == bidderCollateralBalanceBefore;
assert bidderCollateralTokenBalanceAfter == bidderCollateralTokenBalanceBefore;

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

bool payable = e.msg.value > 0;
bool notServicerRole = !hasRole(SERVICER_ROLE(), e.msg.sender);

bool isExpectedToRevert = payable ||  notServicerRole;
assert lastReverted <=> isExpectedToRevert;

1. Rule: externalLockCollateralIntegrity - ensures that all relevant balances are properly reflected on account of locking collateral when calling externalLockCollateral.

assert borrowerCollateralBalanceAfter == borrowerCollateralBalanceBefore + amount;
assert encumberedCollateralBalanceAfter == encumberedCollateralBalanceBefore + amount;
assert borrowerCollateralTokenBalanceAfter + amount == borrowerCollateralTokenBalanceBefore;
assert lockerCollateralBalanceBefore + amount == lockerCollateralBalanceAfter;

1. Rule: externalLockCollateralThirdParty - verifies that locking collateral belonging to one account when calling externalLockCollateral does not affect the third party balances

assert thirdPartyBorrowerCollateralBalanceAfter == thirdPartyBorrowerCollateralBalanceBefore;
assert thirdPartyBorrowerCollateralTokenBalanceAfter == thirdPartyBorrowerCollateralTokenBalanceBefore;

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

bool payable = e.msg.value > 0;
    bool isNotCollateralToken = !isTokenCollateral(extLockingCollateralToken);
    bool collateralDepositClosed = e.block.timestamp > extLockingRepoServicer.endOfRepurchaseWindow();
    bool zeroBorrowerRepurchaseObligation = extLockingRepoServicer.getBorrowerRepurchaseObligation(e.msg.sender) == 0;
    bool lockerTransfersPaused = extLockingCollateralLocker.transfersPaused();
    bool lockerNotPaired = !extLockingCollateralLocker.hasRole(extLockingCollateralLocker.SERVICER_ROLE(), currentContract);
    bool allowanceTooLow = extLockingCollateralToken.allowance( e.msg.sender, termRepoLocker()) < amount;
    bool borrowTokenBalanceTooLow = extLockingCollateralToken.balanceOf(e.msg.sender) < amount;

    bool isExpectedToRevert = payable || isNotCollateralToken || collateralDepositClosed || zeroBorrowerRepurchaseObligation || lockerTransfersPaused || lockerNotPaired ||  borrowTokenBalanceTooLow || allowanceTooLow ;

    externalLockCollateral@withrevert(e, extLockingCollateralToken, amount);

1. Rule: externalUnlockCollateralIntegrity - ensures that all relevant balances are properly reflected on account of locking collateral when calling externalUnlockCollateral.

assert borrowerCollateralBalanceAfter + amount == borrowerCollateralBalanceBefore;
assert (extLockingRepoServicer.getBorrowerRepurchaseObligation(e.msg.sender) != 0) => encumberedCollateralBalanceAfter + amount  == encumberedCollateralBalanceBefore;
assert (extLockingRepoServicer.getBorrowerRepurchaseObligation(e.msg.sender) == 0) => encumberedCollateralBalanceAfter == encumberedCollateralBalanceBefore;
assert borrowerCollateralTokenBalanceAfter == borrowerCollateralTokenBalanceBefore + amount;
assert lockerCollateralBalanceBefore == lockerCollateralBalanceAfter + amount;

1. Rule: externalUnlockCollateralThirdParty - verifies that unlocking collateral belonging to one account when calling externalUnlockCollateraldoes not affect the third party balances

assert thirdPartyBorrowerCollateralBalanceAfter == thirdPartyBorrowerCollateralBalanceBefore;
assert thirdPartyBorrowerCollateralTokenBalanceAfter == thirdPartyBorrowerCollateralTokenBalanceBefore;

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

bool payable = e.msg.value > 0;
    bool zeroAmount = amount == 0;
    bool isNotCollateralToken = !isTokenCollateral(extLockingCollateralToken);
    bool borrowerEndsUpInShortfall = willBorrowerBeInShortfall(e.msg.sender,0,extLockingCollateralToken,amount); 
    bool collateralDepositClosed = e.block.timestamp >= extLockingRepoServicer.endOfRepurchaseWindow() && e.block.timestamp < extLockingRepoServicer.redemptionTimestamp();
    bool zeroBorrowerCollateralBalance = getCollateralBalance(e.msg.sender, extLockingCollateralToken) == 0;
    bool notEnoughCollateralToUnlock = getCollateralBalance(e.msg.sender, extLockingCollateralToken) < amount;
    bool lockerTransfersPaused = extLockingCollateralLocker.transfersPaused();
    bool lockerNotPaired = !extLockingCollateralLocker.hasRole(extLockingCollateralLocker.SERVICER_ROLE(), currentContract);

    bool isExpectedToRevert = payable || zeroAmount || isNotCollateralToken || borrowerEndsUpInShortfall || collateralDepositClosed || zeroBorrowerCollateralBalance || notEnoughCollateralToUnlock || lockerTransfersPaused || lockerNotPaired  ;

    externalUnlockCollateral@withrevert(e, extLockingCollateralToken, amount);

1. Rule: lockerCollateralTokenBalanceGreaterThanCollateralLedgerBalance - verifies the assumption that total collateral token balances is always less than or equal to the balance recorded in ledger

assert sumOfCollateralBalances <= to_mathint((stateToken.balanceOf(stateLocker)));

1. Rule: onlyAllowedMethodsMayChangeEncumberedCollateralBalances - verifies that changes to the balances of encumbered collateral to specific methods, ensuring that such modifications are controlled and intentional.

assert encumberedCollateralBalanceAfter > encumberedCollateralBalanceBefore => canIncreaseEncumberedCollateralBalances(f);
assert encumberedCollateralBalanceAfter < encumberedCollateralBalanceBefore => canDecreaseEncumberedCollateralBalances(f);

1. Rule: encumberedCollateralBalancesNeverOverflows - ensure that encumberedCollateralBalances never overflows

assert encumberedCollateralBalanceBefore <= encumberedCollateralBalanceAfter;

1. Rule: noMethodsChangeTermRepoId - verifies that termRepoIds are immutable.

assert termRepoIdBefore == termRepoIdAfter;

1. Rule: noMethodsChangeNumOfAcceptedCollateralTokens - verifies that the number of accepted collateral tokens are immutable.

assert numOfAcceptedCollateralTokensBefore == numOfAcceptedCollateralTokensAfter;

1. Rule: noMethodsChangeDeMinimisMarginThreshold - verifies that the deminimisMarginThreshold is immutable.

assert deMinimisMarginThresholdBefore == deMinimisMarginThresholdAfter;

1. Rule: noMethodsChangeLiquidateDamagesDueToProtocol - verifies that the liquidated damages due to protocol is immutable.

assert liquidateDamagesDueToProtocolBefore == liquidateDamagesDueToProtocolAfter;

1. Rule: noMethodsChangeNetExposureCapOnLiquidation - verifies that the netExposureCapOnLiquidation parameter of a termRepo is immutable.

assert netExposureCapOnLiquidationBefore == netExposureCapOnLiquidationAfter;

1. Rule: noMethodsChangePurchaseToken - verifies that the purchaseToken associated with a termRepo is immutable.

assert purchaseTokenBefore == purchaseTokenAfter;

1. Rule: onlyAllowedMethodsChangeTermContracts - verifies that changes to term contracts addresses are restricted to certain allowed methods.

assert servicerBefore == servicerAfter;
assert oracleBefore == oracleAfter;
assert lockerBefore == lockerAfter;
assert controllerBefore == controllerAfter;
assert emitterBefore == emitterAfter;

1. Rule: noMethodsChangeMaintenanceCollateralRatios - verifies that maintenance collateral ratios associated with a termRepo are immutable.

assert maintenanceCollateralRatioBefore == maintenanceCollateralRatioAfter;

1. Rule: noMethodsChangeInitialCollateralRatios - verifies that initial collateral ratios associated with a termRepo are immutable.

assert initialCollateralRatioBefore == initialCollateralRatioAfter;

1. Rule: noMethodsChangeLiquidatedDamages - verifies that liquidated damages associated with a termRepo are immutable.

assert liquidatedDamagesBefore == liquidatedDamagesAfter;

1. Rule: onlyAllowedMethodsChangeLockedCollateralLedger - verifies that changes t othe collateral ledger is restricted to certain approved methods.

assert lockedCollateralLedgerBefore == lockedCollateralLedgerAfter;

1. Rule: sumOfCollateralBalancesLessThanEncumberedBalances - verifes the assumption that the total sum of all collateral balances is always less than the encumbered collateral balance.

mathint encumberedCollateralBalanceAfter = encumberedCollateralBalance(stateToken);
mathint sumOfCollateralBalancesAfter = sumOfCollateralBalances;

assert sumOfCollateralBalancesAfter <= encumberedCollateralBalanceAfter;

1. Rule: batchLiquidationSuccessfullyLiquidates - assert that the locker's balances, the liquidator's balances and protocol reserve's balances have changed by the correct amount after bathLiquidate

    // Assert that the locker's balances have changed by the correct amount.
    assert(lockerCollateralTokenBalanceBefore - lockerCollateralTokenBalanceAfter == liquidationIncentiveAmount);
    assert(lockerPurchaseTokenBalanceAfter - lockerPurchaseTokenBalanceBefore == to_mathint(closureAmount));

    // Assert that the liquidator's balances have changed by the correct amount.
    assert(liquidatorCollateralTokenBalanceAfter - liquidatorCollateralTokenBalanceBefore == liquidationIncentiveAmount - protocolLiquidatedDamagesAmount);
    assert(liquidatorPurchaseTokenBalanceBefore - liquidatorPurchaseTokenBalanceAfter == to_mathint(closureAmount));

    // Assert that the reserve's balances have changed by the correct amount.
    assert(reserveCollateralTokenBalanceAfter - reserveCollateralTokenBalanceBefore == protocolLiquidatedDamagesAmount);

1. Rule: batchLiquidateWithRepoTokenSuccessfullyLiquidates - assert that the locker's balances, liquidators balances and protocol reserve blances have changed by the correct amount after calling batchLiquidatedWithRepoToken

    // Assert that the locker's balances have changed by the correct amount.
    assert(lockerCollateralTokenBalanceBefore - lockerCollateralTokenBalanceAfter == liquidationIncentiveAmount);

    // Assert that the liquidator's balances have changed by the correct amount.
    assert(liquidatorCollateralTokenBalanceAfter - liquidatorCollateralTokenBalanceBefore == liquidationIncentiveAmount - protocolLiquidatedDamagesAmount);
    assert(liquidatorRepoTokenBalanceBefore - liquidatorRepoTokenBalanceAfter == to_mathint(closureRepoTokenAmount));

    // Assert that the reserve's balances have changed by the correct amount.
    assert(reserveCollateralTokenBalanceAfter - reserveCollateralTokenBalanceBefore == protocolLiquidatedDamagesAmount);
}

1. Rule: batchDefaultSuccessfullyDefaults - assert that the locker's balances, liquidator's balances and protocol reserve balances have changed by the correct amount after callingbatchDefault

// Assert that the locker's balances have changed by the correct amount.
assert(lockerCollateralTokenBalanceBefore - lockerCollateralTokenBalanceAfter == liquidationIncentiveAmount);
assert(lockerPurchaseTokenBalanceAfter - lockerPurchaseTokenBalanceBefore == to_mathint(closureAmount));

// Assert that the liquidator's balances have changed by the correct amount.
assert(liquidatorCollateralTokenBalanceAfter - liquidatorCollateralTokenBalanceBefore == liquidationIncentiveAmount - protocolLiquidatedDamagesAmount);
assert(liquidatorPurchaseTokenBalanceBefore - liquidatorPurchaseTokenBalanceAfter == to_mathint(closureAmount));

// Assert that the reserve's balances have changed by the correct amount.
assert(reserveCollateralTokenBalanceAfter - reserveCollateralTokenBalanceBefore == protocolLiquidatedDamagesAmount);
// assert(reservePurchaseTokenBalanceAfter == reservePurchaseTokenBalanceBefore);

1. Rule: batchLiquidationDoesNotAffectThirdParty - verifies that liquidating collateral belonging to one account does not affect the third party balances.

batchLiquidation(e, borrower, [closureAmount]);

    assert(otherBorrowerRepurchaseObligationBefore == otherBorrowerRepurchaseObligationAfter);
    assert(otherBorrowerCollateralBalanceBefore == otherBorrowerCollateralBalanceAfter);

1. Rule: batchLiquidationWithRepoTokenDoesNotAffectThirdParty - verifies that liquidating collateral using batchLiquidationWithRepoToken belonging to one account does not affect the third party balances.

batchLiquidationWithRepoToken(e, borrower, [closureAmount]);

    assert(otherBorrowerRepurchaseObligationBefore == otherBorrowerRepurchaseObligationAfter);
    assert(otherBorrowerCollateralBalanceBefore == otherBorrowerCollateralBalanceAfter);

1. Rule: batchDefaultDoesNotAffectThirdParty - verifies that liquidating collateral belonging to one account when calling batchDefault does not affect the third party balances.

batchDefault(e, borrower, [closureAmount]);

    assert(otherBorrowerRepurchaseObligationBefore == otherBorrowerRepurchaseObligationAfter);
    assert(otherBorrowerCollateralBalanceBefore == otherBorrowerCollateralBalanceAfter);

1. Rule: batchLiquidationRevertsIfInvalid - ensures that batchLiquidate reverts if not valid.

    bool liquidationsClosed = e.block.timestamp > servicerLiquidations.endOfRepurchaseWindow();
    bool selfLiquidation = borrower == e.msg.sender;
    bool invalidParameters = harnessCollateralTokensLength() != closureAmounts.length;
    bool zeroBorrowerRepurchaseObligation = servicerLiquidations.getBorrowerRepurchaseObligation(borrower) == 0;
    bool borrowerNotInShortfall = !isBorrowerInShortfall(borrower);
    bool exceedsNetExposureCapOnLiquidation = !willBeWithinNetExposureCapOnLiquidation(borrower,  closureAmounts[0], collateralTokenLiquidations, collateralSeizure) && !allowFullLiquidation(borrower, closureAmounts);
    bool servicerNoLockerAccess = !lockerLiquidations.hasRole(lockerLiquidations.SERVICER_ROLE(), servicerLiquidations);
    bool noLockerAccess = !lockerLiquidations.hasRole(lockerLiquidations.SERVICER_ROLE(), currentContract);
    bool lockerTransfersPaused = lockerLiquidations.transfersPaused();
    bool totalClosureIsZero = closureAmounts[0] == 0;
    bool closureAmountIsUIntMax = closureAmounts[0] == max_uint256;
    bool closureAmountMoreThanBorrowObligation = closureAmounts[0] > servicerLiquidations.getBorrowerRepurchaseObligation(borrower);
    bool noAccessToServicer = !servicerLiquidations.hasRole(servicerLiquidations.COLLATERAL_MANAGER(), currentContract);
    bool liquidatorDoesNotHaveEnoughFunds = purchaseTokenLiquidations.balanceOf(e.msg.sender) < closureAmounts[0];
    bool liquidatorAllowanceFoLockerTooLow = purchaseTokenLiquidations.allowance(e.msg.sender, lockerLiquidations) < closureAmounts[0];
    bool notEnoughCollateralToLiquidate = collateralSeizure > getCollateralBalance(borrower,collateralTokenLiquidations);
    bool msgHasValue = e.msg.value != 0;

    batchLiquidation@withrevert(e, borrower, closureAmounts);
    assert lastReverted == (
        liquidationsClosed ||
        selfLiquidation ||
        invalidParameters ||
        zeroBorrowerRepurchaseObligation ||
        borrowerNotInShortfall ||
        exceedsNetExposureCapOnLiquidation ||
        servicerNoLockerAccess ||
        noLockerAccess ||
        lockerTransfersPaused ||
        totalClosureIsZero ||
        closureAmountIsUIntMax ||
        closureAmountMoreThanBorrowObligation ||
        noAccessToServicer ||
        liquidatorDoesNotHaveEnoughFunds ||
        liquidatorAllowanceFoLockerTooLow ||
        notEnoughCollateralToLiquidate ||
        liquidationsPaused() ||
        msgHasValue
    ), "Expected revert";

1. Rule: batchLiquidationWithRepoTokenRevertsIfInvalid - ensure that batchLiquidateWithRepoToken reverts if not valid.

    bool liquidationsClosed = e.block.timestamp > servicerLiquidations.endOfRepurchaseWindow();
    bool selfLiquidation = borrower == e.msg.sender;
    bool invalidParameters = harnessCollateralTokensLength() != closureAmounts.length;
    bool zeroBorrowerRepurchaseObligation = servicerLiquidations.getBorrowerRepurchaseObligation(borrower) == 0;
    bool borrowerNotInShortfall = !isBorrowerInShortfall(borrower);
    bool exceedsNetExposureCapOnLiquidation = !willBeWithinNetExposureCapOnLiquidation(borrower,  closureAmountInPurchaseToken, collateralTokenLiquidations, collateralSeizure) && !allowFullLiquidation(borrower, closureAmounts);
    bool noLockerAccess = !lockerLiquidations.hasRole(lockerLiquidations.SERVICER_ROLE(), currentContract);
    bool burningPaused = repoTokenLiquidations.burningPaused();
    bool noServicerAccessToTokenBurns = !repoTokenLiquidations.hasRole(repoTokenLiquidations.BURNER_ROLE(), servicerLiquidations);
    bool lockerTransfersPaused = lockerLiquidations.transfersPaused();
    bool totalClosureIsZero = closureAmounts[0] == 0;
    bool closureAmountIsUIntMax = closureAmounts[0] == max_uint256;
    bool closureAmountMoreThanBorrowObligation = closureAmountInPurchaseToken > servicerLiquidations.getBorrowerRepurchaseObligation(borrower);
    bool noAccessToServicer = !servicerLiquidations.hasRole(servicerLiquidations.COLLATERAL_MANAGER(), currentContract);
    bool liquidatorDoesNotHaveEnoughFunds = repoTokenLiquidations.balanceOf(e.msg.sender) < closureAmounts[0];
    bool notEnoughCollateralToLiquidate = collateralSeizure > getCollateralBalance(borrower,collateralTokenLiquidations);
    bool servicerIsNotTermRepoBalanced = (servicerLiquidations.totalOutstandingRepurchaseExposure() - closureAmountInPurchaseToken + servicerLiquidations.totalRepurchaseCollected() ) / (10 ^ 4) != (((((repoTokenLiquidations.totalSupply() -  closureAmounts[0]) * expScale * redemptionVal) / expScale ) / expScale) / 10 ^ 4);
    bool msgHasValue = e.msg.value != 0;
    bool liquidatorIsZero = e.msg.sender == 0;

    batchLiquidationWithRepoToken@withrevert(e, borrower, closureAmounts);
    assert lastReverted == (
        liquidationsClosed ||
        selfLiquidation ||
        invalidParameters ||
        zeroBorrowerRepurchaseObligation ||
        borrowerNotInShortfall ||
        exceedsNetExposureCapOnLiquidation ||
        noLockerAccess ||
        burningPaused ||
        noServicerAccessToTokenBurns ||
        lockerTransfersPaused ||
        totalClosureIsZero ||
        closureAmountIsUIntMax ||
        closureAmountMoreThanBorrowObligation ||
        noAccessToServicer ||
        liquidatorDoesNotHaveEnoughFunds ||
        notEnoughCollateralToLiquidate ||
        liquidationsPaused() ||
        servicerIsNotTermRepoBalanced ||
        msgHasValue || liquidatorIsZero
    ), "Expected revert";

1. Rule: batchDefaultRevertsIfInvalid - ensure that batchDefault reverts if not valid.

bool defaultsClosed = e.block.timestamp <= servicerLiquidations.endOfRepurchaseWindow();
bool selfLiquidation = borrower == e.msg.sender;
bool invalidParameters = harnessCollateralTokensLength() != closureAmounts.length;
bool zeroBorrowerRepurchaseObligation = servicerLiquidations.getBorrowerRepurchaseObligation(borrower) == 0;
bool servicerNoLockerAccess = !lockerLiquidations.hasRole(lockerLiquidations.SERVICER_ROLE(), servicerLiquidations);
bool noLockerAccess = !lockerLiquidations.hasRole(lockerLiquidations.SERVICER_ROLE(), currentContract);
bool lockerTransfersPaused = lockerLiquidations.transfersPaused();
bool totalClosureIsZero = closureAmounts[0] == 0;
bool closureAmountIsUIntMax = closureAmounts[0] == max_uint256;
bool closureAmountMoreThanBorrowObligation = closureAmounts[0] > servicerLiquidations.getBorrowerRepurchaseObligation(borrower);
bool noAccessToServicer = !servicerLiquidations.hasRole(servicerLiquidations.COLLATERAL_MANAGER(), currentContract);
bool liquidatorDoesNotHaveEnoughFunds = purchaseTokenLiquidations.balanceOf(e.msg.sender) < closureAmounts[0];
bool liquidatorAllowanceFoLockerTooLow = purchaseTokenLiquidations.allowance(e.msg.sender, lockerLiquidations) < closureAmounts[0];
bool notEnoughCollateralToLiquidate = collateralSeizure > getCollateralBalance(borrower, collateralTokenLiquidations);

bool msgHasValue = e.msg.value != 0;

batchDefault@withrevert(e, borrower, closureAmounts);
assert lastReverted == (
    defaultsClosed ||
    selfLiquidation ||
    invalidParameters ||
    zeroBorrowerRepurchaseObligation ||
    liquidationsPaused() ||
    servicerNoLockerAccess ||
    noLockerAccess ||
    lockerTransfersPaused ||
    totalClosureIsZero ||
    closureAmountIsUIntMax ||
    closureAmountMoreThanBorrowObligation ||
    noAccessToServicer ||

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

    assert !lastReverted =>
        hasRole(ADMIN_ROLE(),e.msg.sender)
        || hasRole(AUCTION_LOCKER(),e.msg.sender)
        || hasRole(DEVOPS_ROLE(),e.msg.sender)
        || hasRole(INITIALIZER_ROLE(),e.msg.sender)
        || hasRole(SERVICER_ROLE(),e.msg.sender)
        || hasRole(ROLLOVER_MANAGER(),e.msg.sender)
        || hasRole(ROLLOVER_TARGET_AUCTIONEER_ROLE(),e.msg.sender);

1. 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.

    assert storeBefore != storeAfter =>
        hasRole(ADMIN_ROLE(),e.msg.sender)
        || hasRole(AUCTION_LOCKER(),e.msg.sender)
        || hasRole(DEVOPS_ROLE(),e.msg.sender)
        || hasRole(INITIALIZER_ROLE(),e.msg.sender)
        || hasRole(SERVICER_ROLE(),e.msg.sender)
        || hasRole(ROLLOVER_MANAGER(),e.msg.sender)
        || hasRole(ROLLOVER_TARGET_AUCTIONEER_ROLE(),e.msg.sender);

TermRepoRolloverManager

1. Rule: noMethodsChangeTermRepoId - ensures that the termRepoId is immutable.

env e, method f, calldataarg args filtered {
    f -> !f.isView &&
    f.selector != initialize(string,address,address,address,address).selector &&
    f.selector != upgradeToAndCall(address,bytes).selector &&
    f.selector != upgradeTo(address).selector
} {
    bytes32 termRepoIdBefore = termRepoId();
    f(e, args);
    bytes32 termRepoIdAfter = termRepoId();

    assert termRepoIdBefore == termRepoIdAfter,
        "termRepoId cannot be changed";
}

1. Rule: onlyAllowedMethodsChangeTermContracts - verifies that changes to term contracts addresses are restricted to certain allowed methods.

// Restricts contract changes to specific methods.
env e, method f, calldataarg args filtered {
    f -> !f.isView &&
    f.selector != initialize(string,address,address,address,address).selector &&
    f.selector != upgradeToAndCall(address,bytes).selector &&
    f.selector != upgradeTo(address).selector &&
    f.selector != pairTermContracts(address,address,address,address).selector
} {
    address collateralManagerBefore = collateralManager();
    address servicerBefore = repoServicer();
    address controllerBefore = controller();
    address eventEmitterBefore = eventEmitter();
    f(e, args);
    address collateralManagerAfter = collateralManager();
    address servicerAfter = repoServicer();
    address controllerAfter = controller();
    address eventEmitterAfter = eventEmitter();

    assert collateralManagerBefore == collateralManagerAfter,
        "collateralManager cannot be changed";
    assert servicerBefore == servicerAfter,
        "servicer cannot be changed";
    assert controllerBefore == controllerAfter,
        "controller cannot be changed";
    assert eventEmitterBefore == eventEmitterAfter,
        "eventEmitter cannot be changed";
}

1. Rule: onlyAllowedMethodsChangeApprovedRolloverAuctionBidLockers - verifies that changes to approved rollover contracts are restricted to certain allowed methods.

// Specifies which methods can change the approval status of rollover auction bid lockers.
env e, method f, calldataarg args, address bidLocker filtered {
    f -> !f.isView &&
    f.selector != initialize(string,address,address,address,address).selector &&
    f.selector != upgradeToAndCall(address,bytes).selector &&
    f.selector != upgradeTo(address).selector &&
    f.selector != electRollover(TermRepoRolloverManagerHarness.TermRepoRolloverElectionSubmission).selector &&
    f.selector != approveRolloverAuction(address).selector &&
    f.selector != revokeRolloverApproval(address).selector
} {
    bool isRolloverAuctionApprovedBefore = isRolloverAuctionApproved(bidLocker);
    f(e, args);
    bool isRolloverAuctionApprovedAfter = isRolloverAuctionApproved(bidLocker);

    assert isRolloverAuctionApprovedBefore == isRolloverAuctionApprovedAfter,
        "only the approveRolloverAuction method can change the approved rollover auction bid lockers";
}

1. Rule: onlyAllowedMethodsChangeRolloverElections - verifies that changes to rollover elections are restricted to certain allowed methods.

// Limits which methods can modify rollover elections.
env e, method f, calldataarg args, address bidder filtered {
    f -> !f.isView &&
    f.selector != initialize(string,address,address,address,address).selector &&
    f.selector != upgradeToAndCall(address,bytes).selector &&
    f.selector != upgradeTo(address).selector &&
    f.selector != electRollover(TermRepoRolloverManagerHarness.TermRepoRolloverElectionSubmission).selector &&
    f.selector != cancelRollover().selector &&
    f.selector != fulfillRollover(address).selector
} {
    TermRepoRolloverManagerHarness.TermRepoRolloverElection electionBefore = getRolloverInstructions(bidder);
    f(e, args);
    TermRepoRolloverManagerHarness.TermRepoRolloverElection electionAfter = getRolloverInstructions(bidder);

    assert electionBefore.rolloverAuctionBidLocker == electionAfter.rolloverAuctionBidLocker &&
           electionBefore.rollover

1. Rule: electRolloverIntegrity - ensures that all relevant balances are properly reflected when electing to roll-over a loan.

    TermRepoRolloverManagerHarness.TermRepoRolloverElectionSubmission submission;

    require(repoServicer() == electionRepoServicer);
    electRollover(e, submission);
    uint256 rolloverAmount = getRolloverInstructions(e.msg.sender).rolloverAmount;
    bytes32 rolloverBidPriceHash = getRolloverInstructions(e.msg.sender).rolloverBidPriceHash;
    address rolloverAuctionBidLocker = getRolloverInstructions(e.msg.sender).rolloverAuctionBidLocker;

    assert submission.rolloverAmount == rolloverAmount;
    assert submission.rolloverBidPriceHash == rolloverBidPriceHash;
    assert submission.rolloverAuctionBidLocker == rolloverAuctionBidLocker;
    assert rolloverAmount <= electionRepoServicer.getBorrowerRepurchaseObligation(e.msg.sender); // Rollover amount cannot exceed borrower's obligation.
}

1. Rule: electRolloverDoesNotAffectThirdParty - verifies that the action of one account electing to roll over their loan does not impact third-party balances.

TermRepoRolloverManagerHarness.TermRepoRolloverElectionSubmission submission;
address otherBorrower;

require(otherBorrower != e.msg.sender);

uint256 thirdPartyRolloverAmountBefore = getRolloverInstructions(otherBorrower).rolloverAmount;
bytes32 thirdPartyRolloverBidPriceHashBefore = getRolloverInstructions(otherBorrower).rolloverBidPriceHash;
address thirdPartyRolloverAuctionBidLockerBefore = getRolloverInstructions(otherBorrower).rolloverAuctionBidLocker;

electRollover(e, submission);

uint256 thirdPartyRolloverAmountAfter = getRolloverInstructions(otherBorrower).rolloverAmount;
bytes32 thirdPartyRolloverBidPriceHashAfter = getRolloverInstructions(otherBorrower).rolloverBidPriceHash;
address thirdPartyRolloverAuctionBidLockerAfter = getRolloverInstructions(otherBorrower).rolloverAuctionBidLocker;

assert thirdPartyRolloverAmountBefore == thirdPartyRolloverAmountAfter;
assert thirdPartyRolloverBidPriceHashBefore == thirdPartyRolloverBidPriceHashAfter;
assert thirdPartyRolloverAuctionBidLockerBefore == thirdPartyRolloverAuctionBidLockerAfter;

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

TermRepoRolloverManagerHarness.TermRepoRolloverElectionSubmission submission;

// Define various conditions that lead to reversion (simplified for clarity).
bool isExpectedToRevert = /* conditions leading to revert */;

electRollover@withrevert(e, submission);

assert lastReverted <=> isExpectedToRevert;

1. Rule: cancelRolloverIntegrity - ensures that all relevant balances are properly reflected when cancelling a roll-over election.

assert rolloverAmount == 0;
assert rolloverBidPriceHash == to_bytes32(0);
assert rolloverAuctionBidLocker == 0;

1. Rule cancelRolloverDoesNotAffectThirdParty - verifies that the action of one account cancelling their roll over election does not impact third-party balances.

assert thirdPartyRolloverAmountBefore == thirdPartyRolloverAmountAfter;
assert thirdPartyRolloverBidPriceHashBefore == thirdPartyRolloverBidPriceHashAfter;
assert thirdPartyRolloverAuctionBidLockerBefore == thirdPartyRolloverAuctionBidLockerAfter;

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

bool payable = e.msg.value > 0;
bool zeroBorrowerRepurchaseObligation = electionRepoServicer.getBorrowerRepurchaseObligation(e.msg.sender) == 0;
bool noRolloverToCancel = getRolloverInstructions(e.msg.sender).rolloverAmount == 0;
bool rolloverAlreadyProcessed = getRolloverInstructions(e.msg.sender).processed;
bool lockingPausedForRolloverAuction = electionBidLocker.lockingPaused();
bool noRolloverManagerAccessToBidLocker = !electionBidLocker.hasRole(electionBidLocker.ROLLOVER_MANAGER(), currentContract);
bool beyondAuctionRevealTime = e.block.timestamp > electionBidLocker.revealTime();
bool nonExistentRolloverBid = existingRolloverBidAmount == 0;

bool isExpectedToRevert = payable || zeroBorrowerRepurchaseObligation || noRolloverToCancel || rolloverAlreadyProcessed || lockingPausedForRolloverAuction || noRolloverManagerAccessToBidLocker || beyondAuctionRevealTime || nonExistentRolloverBid;
cancelRollover@withrevert(e);

assert lastReverted <=> isExpectedToRevert;

1. Rule: fulfillRolloverIntegrity - ensures that a rollover election is properly marked as processed when fulfilled.

    fulfillRollover(e, borrower);

    bool rolloverProcessed = getRolloverInstructions(borrower).processed;

    assert rolloverProcessed, "The rollover should be marked as processed.";

1. Rule: fulfillRolloverDoesNotAffectThirdParty - verifies that fulfilling a rollover election submitted by one account does not affect the third party balances

    bool thirdPartyRolloverProcessedBefore = getRolloverInstructions(borrower2).processed;

    fulfillRollover(e, borrower);

    bool thirdPartyRolloverProcessedAfter = getRolloverInstructions(borrower2).processed;

    assert thirdPartyRolloverProcessedBefore == thirdPartyRolloverProcessedAfter, "Third party's rollover state should remain unaffected.";
}

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

    bool payable = e.msg.value > 0;
    bool callerNotRolloverBidFulfillerRole = !hasRole(ROLLOVER_BID_FULFILLER_ROLE(), e.msg.sender);

    bool isExpectedToRevert = payable || callerNotRolloverBidFulfillerRole;
    fulfillRollover@withrevert(e, borrower);

    assert lastReverted <=> isExpectedToRevert, "fulfillRollover should only revert under specific conditions.";

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

    assert !lastReverted =>
        hasRole(ADMIN_ROLE(),e.msg.sender)
        || hasRole(DEVOPS_ROLE(),e.msg.sender)
        || hasRole(ROLLOVER_BID_FULFILLER_ROLE(),e.msg.sender)
        || hasRole(INITIALIZER_ROLE(),e.msg.sender), "Function should only be callable by specific roles without reverting.";
}

1. 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.

    assert storeBefore != storeAfter =>
        hasRole(ADMIN_ROLE(),e.msg.sender)
        || hasRole(DEVOPS_ROLE(),e.msg.sender)
        || hasRole(ROLLOVER_BID_FULFILLER_ROLE(),e.msg.sender)
        || hasRole(INITIALIZER_ROLE(),e.msg.sender), "Only specific roles should be able to cause state changes.";

TermAuctionBidLocker

1. Rule: PauseLockingCausesBidLockingToRevert - verifies that pausing locking reverts any attempts at locking bids.

    require lockingPaused() == true;
    f@withrevert(e, args);
    assert lastReverted, "lockBids(...) should revert when bid locking is paused";

1. Rule: UnpauseLockingAllowsBidLocking - verifies that unpausing locking allows users to lock bids.

    require lockingPaused() == false;
    f(e, args);
    assert !lastReverted, "lockBids(...) should not revert when bid locking is not paused";

1. Rule: PauseUnlockingCausesBidUnlockingToRevert - verifies that pausing unlocking reverts any attempts at unlocking offers.

    require unlockingPaused() == true;
    unlockBids@withrevert(e, ids);
    assert lastReverted, "unlockBids(...) should revert when bid unlocking is paused";

1. Rule: UnpauseUnlockingAllowsBidUnlocking - verifies that unpausing locking allows users to unlock bids.

    require unlockingPaused() == false;
    require harnessGetInternalBids(id).id == id;
    unlockBids(e, [id]);
    assert !lastReverted, "unlockBids(...) should not revert when bid unlocking is not paused";

1. Rule: lockerCollateralTokenBalanceGreaterThanCollateralLedgerBalance - verified the assumption that the total amount of collateral locked is always greater than or equal to the amount recorded in ledger.

require(bidLockerStateCollateralToken.balanceOf(lockerBidLockingState) + bidSubmissions[0].collateralAmounts[0] <= max_uint256);

f(e, args);

assert sumOfCollateralBalances <= to_mathint((bidLockerStateCollateralToken.balanceOf(lockerBidLockingState)));

1. Invariant: LockedBidIdAlwaysMatchesIndex - verifies the assumption that the bidId matches the ledger.

    harnessGetInternalBidId(bidId) == bidId || harnessGetInternalBidId(bidId) == to_bytes32(0);

1. Invariant: BidCountAlwaysMatchesNumberOfStoredBids - verifies the assumption that the bidCount matches the ledger.

    to_mathint(bidCount()) == lockedBidCount;

1. Rule: LockBidsIntegrity - ensures that collateral token balances are properly transferred to the repo locker when locking bids.

assert
    (collateralTokenOneBalanceAfter == collateralTokenOneBalanceBefore - collateralOneAmountToLock),
    "lockBids should transfer collateral tokens from bidder to contract";
  assert
    (collateralTokenTwoBalanceAfter == collateralTokenTwoBalanceBefore - collateralTwoAmountToLock),
    "lockBids should transfer collateral tokens from bidder to contract";

1. Rule: LockBidsDoesNotAffectThirdParty - verifies that locking bids belonging to one account does not affect the third party balances.

assert bidIdBefore == bidIdAfter,
    "lockBids should not modify bid id";
  assert bidderBefore == bidderAfter,
    "lockBids should not modify bidder";
  assert bidPriceHashBefore == bidPriceHashAfter,
    "lockBids should not modify bid price hash";
  assert bidRevealedPriceBefore == bidRevealedPriceAfter,
    "lockBids should not modify bid revealed price";
  assert bidAmountBefore == bidAmountAfter,
    "lockBids should not modify bid amount";
  assert bidCollateralAmountBefore == bidCollateralAmountAfter,
    "lockBids should not modify bid collateral amounts";
  assert bidIsRolloverBefore == bidIsRolloverAfter,
    "lockBids should not modify bid rollover status";
  assert bidRolloverAddressBefore == bidRolloverAddressAfter,
    "lockBids should not modify bid rollover address";
  assert bidIsRevealedBefore == bidIsRevealedAfter,
    "lockBids should not modify bid revealed status";

1. Rule: lockBidsMonotonicBehavior - verifies that locking a bid is monotonically increasing in the bid count.

uint256 bidCountBefore = bidCount();
  lockBids(e, bidSubmissions);
  uint256 bidCountAfter = bidCount();

  assert bidCountAfter >= bidCountBefore,
    "bidCount should either increase or stay the same after lockBids is called";

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

  bool msgValueIsNotZero = e.msg.value != 0;
  bool reentrant = harnessReentrancyGuardEntered();
  bool auctionNotOpen = e.block.timestamp < auctionStartTime() || e.block.timestamp > revealTime(); // AuctionNotOpen
  bool lockingPaused = lockingPaused(); // LockingPaused
  bool bidSubmissionNotOwned = bidSubmissions[0].bidder != e.msg.sender; // BidNotOwned
  bool maxBidCountReached = bidCount() >= MAX_BID_COUNT(); // MaxBidCountReached
  bool bidIdAlreadyExists = existingGeneratedBid.amount != 0 && existingBid.amount == 0 ; // BidIdAlreadyExists

  bool editingBidNotOwned = existingBidAmount != 0
    && existingBidder != bidSubmissions[0].bidder; // BidNotOwned
  bool purchaseTokenNotApproved = bidSubmissions[0].purchaseToken != purchaseToken(); // PurchaseTokenNotApproved
  bool firstCollateralTokenNotApproved = !collateralTokens(bidSubmissions[0].collateralTokens[0]); // CollateralTokenNotApproved
  bool secondCollateralTokenNotApproved = !collateralTokens(bidSubmissions[0].collateralTokens[1]); // CollateralTokenNotApproved
  bool bidAmountTooLow = bidSubmissions[0].amount < minimumTenderAmount(); // BidAmountTooLow
  bool collateralBalanceTooLow = ((existingBid.collateralAmounts[0] < bidSubmissions[0].collateralAmounts[0]) && lockingAuctionCollateralTokenOne.balanceOf(bidSubmissions[0].bidder) < bidCollat1Diff) || ((existingBid.collateralAmounts[1] < bidSubmissions[0].collateralAmounts[1]) && lockingAuctionCollateralTokenTwo.balanceOf(bidSubmissions[0].bidder) <bidCollat2Diff);
  bool collateralApprovalsTooLow = ((existingBid.collateralAmounts[0] < bidSubmissions[0].collateralAmounts[0]) && lockingAuctionCollateralTokenOne.allowance(bidSubmissions[0].bidder, lockerLocking) < bidCollat1Diff) || ((existingBid.collateralAmounts[1] < bidSubmissions[0].collateralAmounts[1]) && lockingAuctionCollateralTokenTwo.allowance(bidSubmissions[0].bidder, lockerLocking) < bidCollat2Diff);
  bool collateralAmountTooLow = harnessIsInInitialCollateralShortFall(
    bidSubmissions[0].amount,
    bidSubmissions[0].collateralTokens,
    bidSubmissions[0].collateralAmounts
  ); // CollateralAmountTooLow
  bool lockerTransfersPaused = (bidCollat1Diff != 0 || bidCollat2Diff != 0) && lockerLocking.transfersPaused();
  bool collateralManagerNotPairedToLocker = (bidCollat1Diff != 0 || bidCollat2Diff != 0) && !lockerLocking.hasRole(lockerLocking.SERVICER_ROLE(), collateralManagerLocking);
  bool bidLockerNotPairedToCollatManager = (bidCollat1Diff != 0 || bidCollat2Diff != 0) && !collateralManagerLocking.hasRole(collateralManagerLocking.AUCTION_LOCKER(), currentContract);

  bool isExpectedToRevert =
    msgValueIsNotZero ||
    reentrant ||
    auctionNotOpen ||
    lockingPaused ||
    bidSubmissionNotOwned ||
    maxBidCountReached ||
    bidIdAlreadyExists || 
    editingBidNotOwned ||
    bidAmountTooLow ||
    purchaseTokenNotApproved ||
    firstCollateralTokenNotApproved ||
    secondCollateralTokenNotApproved ||
    bidAmountTooLow ||
    collateralBalanceTooLow ||
    collateralApprovalsTooLow || 
    collateralAmountTooLow || 
    lockerTransfersPaused || 
    collateralManagerNotPairedToLocker ||
    bidLockerNotPairedToCollatManager
    ;

  assert lastReverted == isExpectedToRevert,
    "lockBids should revert when one of the revert conditions is reached";

1. Rule: lockBidsWithReferralIntegrity - ensures that collateral token balances are properly transferred to the repo locker when locking bids with a referral.

  assert
    (collateralTokenOneBalanceAfter == collateralTokenOneBalanceBefore - collateralOneAmountToLock) &&
    (collateralTokenTwoBalanceAfter == collateralTokenTwoBalanceBefore - collateralTwoAmountToLock),
    "lockBids should transfer collateral tokens from bidder to contract";

1. Rule: lockBidsWithReferralDoesNotAffectThirdParty - verifies that locking bids belonging to one account when calling lockBidsWithReferral does not affect the third party balances.

assert bidIdBefore == bidIdAfter,
    "lockBidsWithReferral should not modify bid id";
  assert bidderBefore == bidderAfter,
    "lockBidsWithReferral should not modify bidder";
  assert bidPriceHashBefore == bidPriceHashAfter,
    "lockBidsWithReferral should not modify bid price hash";
  assert bidRevealedPriceBefore == bidRevealedPriceAfter,
    "lockBidsWithReferral should not modify bid revealed price";
  assert bidAmountBefore == bidAmountAfter,
    "lockBidsWithReferral should not modify bid amount";
  assert bidCollateralAmountBefore == bidCollateralAmountAfter,
    "lockBidsWithReferral should not modify bid collateral amounts";
  assert bidIsRolloverBefore == bidIsRolloverAfter,
    "lockBidsWithReferral should not modify bid rollover status";
  assert bidRolloverAddressBefore == bidRolloverAddressAfter,
    "lockBidsWithReferral should not modify bid rollover address";
  assert bidIsRevealedBefore == bidIsRevealedAfter,
    "lockBidsWithReferral should not modify bid revealed status";

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

 bool auctionNotOpen = e.block.timestamp < auctionStartTime() || e.block.timestamp > revealTime(); // AuctionNotOpen
  bool lockingPaused = lockingPaused(); // LockingPaused
  bool reentrant = harnessReentrancyGuardEntered();
  bool sameReferral = (refer == e.msg.sender ? true : false); // InvalidSelfReferral
  bool bidSubmissionNotOwned = bidSubmissions[0].bidder != e.msg.sender ? true : false; // BidNotOwned
  bool maxBidCountReached = bidCount() >= MAX_BID_COUNT() ? true : false; // MaxBidCountReached
  bool bidIdAlreadyExists = existingGeneratedBid.amount != 0 && existingBid.amount == 0 ; // BidIdAlreadyExists

  bool editingBidNotOwned = existingBid.amount != 0 && existingBid.bidder != bidSubmissions[0].bidder; // BidNotOwned
  bool purchaseTokenNotApproved = bidSubmissions[0].purchaseToken != purchaseToken() ? true : false; // PurchaseTokenNotApproved
  bool firstCollateralTokenNotApproved = !collateralTokens(bidSubmissions[0].collateralTokens[0]); // CollateralTokenNotApproved
  bool secondCollateralTokenNotApproved = !collateralTokens(bidSubmissions[0].collateralTokens[1]); // CollateralTokenNotApproved
  bool bidAmountTooLow = bidSubmissions[0].amount < minimumTenderAmount(); // BidAmountTooLow
    bool collateralBalanceTooLow = ((existingBid.collateralAmounts[0] < bidSubmissions[0].collateralAmounts[0]) && lockingAuctionCollateralTokenOne.balanceOf(bidSubmissions[0].bidder) < bidCollat1Diff) || ((existingBid.collateralAmounts[1] < bidSubmissions[0].collateralAmounts[1]) && lockingAuctionCollateralTokenTwo.balanceOf(bidSubmissions[0].bidder) <bidCollat2Diff);
  bool collateralApprovalsTooLow = ((existingBid.collateralAmounts[0] < bidSubmissions[0].collateralAmounts[0]) && lockingAuctionCollateralTokenOne.allowance(bidSubmissions[0].bidder, lockerLocking) < bidCollat1Diff) || ((existingBid.collateralAmounts[1] < bidSubmissions[0].collateralAmounts[1]) && lockingAuctionCollateralTokenTwo.allowance(bidSubmissions[0].bidder, lockerLocking) < bidCollat2Diff);
  bool lockerTransfersPaused = (bidCollat1Diff != 0 || bidCollat2Diff != 0) && lockerLocking.transfersPaused();
  bool collateralManagerNotPairedToLocker = (bidCollat1Diff != 0 || bidCollat2Diff != 0) && !lockerLocking.hasRole(lockerLocking.SERVICER_ROLE(), collateralManagerLocking);
  bool bidLockerNotPairedToCollatManager = (bidCollat1Diff != 0 || bidCollat2Diff != 0) && !collateralManagerLocking.hasRole(collateralManagerLocking.AUCTION_LOCKER(), currentContract);
 bool collateralAmountTooLow = harnessIsInInitialCollateralShortFall(
    bidSubmissions[0].amount,
    bidSubmissions[0].collateralTokens,
    bidSubmissions[0].collateralAmounts
  ); // CollateralAmountTooLow
  bool msgValueNotZero = e.msg.value != 0;
  bool isExpectedToRevert =
    auctionNotOpen || lockingPaused || reentrant || sameReferral ||
    bidSubmissionNotOwned || maxBidCountReached ||  bidIdAlreadyExists || 
    editingBidNotOwned ||
    bidAmountTooLow || collateralBalanceTooLow || collateralApprovalsTooLow || purchaseTokenNotApproved ||
    firstCollateralTokenNotApproved || secondCollateralTokenNotApproved ||
    bidAmountTooLow || collateralAmountTooLow || lockerTransfersPaused || collateralManagerNotPairedToLocker || bidLockerNotPairedToCollatManager || msgValueNotZero;

  assert lastReverted <=> isExpectedToRevert,
    "lockBidsWithReferral should revert when one of the revert conditions is reached";

1. Rule: lockBidsWithReferralMonotonicBehavior - verifies that locking a bid with referral is monotonically increasing in the bid count.

assert bidCountAfter >= bidCountBefore,
    "bidCount should either increase or stay the same after lockBidsWithReferral is called";

1. Rule: UnlockBidsIntegrity - ensures that collateral token balances are properly transferred from the repo locker to the user when unlocking bids.

if (collateralTokenCount > 1) {
    assert collateralTokenTwoBalanceAfter == collateralTokenTwoBalanceBefore + idOneTokenTwoAmountToUnlock + (ids.length > 1 ? idTwoTokenTwoAmountToUnlock : 0),
      "collateral token two balance should increase by the amount of collateral token two";
  }
  assert collateralTokenOneBalanceAfter == collateralTokenOneBalanceBefore + idOneTokenOneAmountToUnlock + (ids.length > 1 ? idTwoTokenOneAmountToUnlock : 0),
    "collateral token one balance should increase by the amount of collateral token one";

1. Rule: UnlockBidsDoesNotAffectThirdParty - verifies that unlocking bids belonging to one account does not affect the third party balances.

 assert bidIdBefore == bidIdAfter,
    "lockBids should not modify bid id";
  assert bidderBefore == bidderAfter,
    "lockBids should not modify bidder";
  assert bidPriceHashBefore == bidPriceHashAfter,
    "lockBids should not modify bid price hash";
  assert bidRevealedPriceBefore == bidRevealedPriceAfter,
    "lockBids should not modify bid revealed price";
  assert bidAmountBefore == bidAmountAfter,
    "lockBids should not modify bid amount";
  assert bidCollateralAmountBefore == bidCollateralAmountAfter,
    "lockBids should not modify bid collateral amounts";
  assert bidIsRolloverBefore == bidIsRolloverAfter,
    "lockBids should not modify bid rollover status";
  assert bidRolloverAddressBefore == bidRolloverAddressAfter,
    "lockBids should not modify bid rollover address";
  assert bidIsRevealedBefore == bidIsRevealedAfter,
    "lockBids should not modify bid revealed status";

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

  bool unlockingPaused = unlockingPaused(); // UnlockingPaused
  bool reentrant = harnessReentrancyGuardEntered();
  bool auctionNotOpen = e.block.timestamp < auctionStartTime(); // AuctionNotOpen
  bool auctionNotCancelledForWithdrawal = e.block.timestamp > revealTime() && !termAuction.auctionCancelledForWithdrawal(); // AuctionNotOpen
  bool nonExistentBid = harnessGetInternalBids(unlockBidId).amount == 0; // NonExistentBid

  bool bidNotOwned = harnessGetInternalBids(unlockBidId).bidder != e.msg.sender; // BidNotOwned
  bool rolloverBid = harnessGetInternalBids(unlockBidId).isRollover; // RolloverBid
  bool lockerTransfersPaused = lockerUnlocking.transfersPaused();
  bool collateralManagerNotPairedToLocker = !lockerUnlocking.hasRole(lockerUnlocking.SERVICER_ROLE(), collateralManagerLocking);
  bool bidLockerNotPairedToCollatManager = !collateralManagerUnlocking.hasRole(collateralManagerUnlocking.AUCTION_LOCKER(), currentContract);

  bool nonZeroMsgValue = e.msg.value != 0;

  bool isExpectedToRevert = unlockingPaused || reentrant || auctionNotOpen || auctionNotCancelledForWithdrawal || nonExistentBid || bidNotOwned || rolloverBid ||
  lockerTransfersPaused || collateralManagerNotPairedToLocker || bidLockerNotPairedToCollatManager || nonZeroMsgValue;

  assert isExpectedToRevert <=> lastReverted,
    "unlockBids should revert when revert conditions are met";

1. Rule: UnlockBidsMonotonicBehavior - verifies that unlocking a bid is monotonically decreasing in the bid count.

 assert bidCountAfter <= bidCountBefore,
    "unlockBids should decrease or maintain bid count";

1. Rule: AuctionUnlockBidIntegrity - ensures that collateral token balances are properly transferred from the repo locker to the user when unlocking bids.

if (bidCollateralTokens.length > 1) {
    assert collateralTokenTwoBalanceAfter == collateralTokenTwoBalanceBefore + amounts[1],
      "collateral token two balance should increase by the amount of collateral token two";
  }
  assert bidCollateralTokens.length == 0 || collateralTokenOneBalanceAfter == collateralTokenOneBalanceBefore + amounts[0],
    "collateral token one balance should increase by the amount of collateral token one";

1. Rule: AuctionUnlockBidDoesNotAffectThirdParty - verifies that unlocking bids belonging to one account does not affect the third party balances.

  assert bidIdBefore == bidIdAfter,
    "lockBids should not modify bid id";
  assert bidderBefore == bidderAfter,
    "lockBids should not modify bidder";
  assert bidPriceHashBefore == bidPriceHashAfter,
    "lockBids should not modify bid price hash";
  assert bidRevealedPriceBefore == bidRevealedPriceAfter,
    "lockBids should not modify bid revealed price";
  assert bidAmountBefore == bidAmountAfter,
    "lockBids should not modify bid amount";
  assert bidCollateralAmountBefore == bidCollateralAmountAfter,
    "lockBids should not modify bid collateral amounts";
  assert bidIsRolloverBefore == bidIsRolloverAfter,
    "lockBids should not modify bid rollover status";
  assert bidRolloverAddressBefore == bidRolloverAddressAfter,
    "lockBids should not modify bid rollover address";
  assert bidIsRevealedBefore == bidIsRevealedAfter,
    "lockBids should not modify bid revealed status";

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

bool isRollover = harnessGetInternalBidIsRollover(unlockBidId); // RolloverBid
  bool msgValueIsNotZero = e.msg.value != 0;
  bool callerNotAuctioneer = !hasRole(AUCTIONEER_ROLE(), e.msg.sender);
  bool lockerTransfersPaused = lockerUnlocking.transfersPaused();
  bool collateralManagerNotPairedToLocker = !lockerUnlocking.hasRole(lockerUnlocking.SERVICER_ROLE(), collateralManagerLocking);
  bool bidLockerNotPairedToCollatManager = !collateralManagerUnlocking.hasRole(collateralManagerUnlocking.AUCTION_LOCKER(), currentContract);
  bool insufficientLockerBalance = amounts[0] > unlockingAuctionCollateralTokenOne.balanceOf(lockerUnlocking) ||  amounts[1] > unlockingAuctionCollateralTokenTwo.balanceOf(lockerUnlocking);

  bool isExpectedToRevert = isRollover || msgValueIsNotZero || callerNotAuctioneer || lockerTransfersPaused || collateralManagerNotPairedToLocker || bidLockerNotPairedToCollatManager || insufficientLockerBalance;

  assert isExpectedToRevert <=> lastReverted,
    "auctionUnlockBid should revert if it tries to unlock a rollover bid";

1. Rule: AuctionUnlockBidMonotonicBehavior - verifies that auctionUnlockCollateral monotonically decreases the bid count.

assert bidCountAfter <= bidCountBefore,
    "auctionUnlockBid should decrease or maintain bid count";

1. Rule: RevealBidsIntegrity - ensures that prices are revealed when revealing bids.

  assert isRevealedAfter && revealedPriceAfter == price,
    "revealBids should not revert";

1. Rule: RevealBidsDoesNotAffectThirdParty - verifies that revealing a bid belonging to one account does not affect the third party balances.

  assert !isThirdPartyRevealedAfter,
    "revealBids should not reveal third party bids";

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

bool isNotInRevealPhase = e.block.timestamp < revealTime(); // AuctionNotRevealing
  bool isBidPriceModified = harnessGenerateBidPriceHash(price, nonce) != harnessGetInternalBidBidPriceHash(id); // BidPriceModified
  bool isTenderPriceTooHigh = price > MAX_BID_PRICE(); // TenderPriceTooHigh
  bool msgValueNotZero = e.msg.value != 0;

  bool isExpectedToRevert = isNotInRevealPhase || isBidPriceModified || isTenderPriceTooHigh || msgValueNotZero;

  assert lastReverted <=> isExpectedToRevert,
    "revealBids should revert if conditions are met";

1. Rule: RevealBidsMonotonicBehavior - verifies that revealBids does not change the bid count.

assert bidCountBefore == bidCountAfter,
    "revealBids should not change bid count";
    

1. Rule: OnlyRoleCanCallRevert - checks if a method call requires specific roles to execute successfully, does not revert if the caller has the necessary role.

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

1. 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.

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

TermAuctionOfferLocker

1. Rule: PauseLockingCausesOfferLockingToRevert - verifies that pausing locking reverts any attempts at locking offers.

require lockingPaused() == true;
    f@withrevert(e, args);
    assert lastReverted,
      "lockOffers(...) should revert when trying to lock a paused contract";

1. Rule: UnpauseLockingAllowsOfferLocking - verifies that unpausing locking allows users to lock offers.

    require lockingPaused() == false;
    f(e, args);
    assert !lastReverted, "lockOffers(...) should not revert when trying to lock offers on an unpaused contract";

1. Rule: PauseUnlockingCausesOfferUnlockingToRevert - verifies that pausing unlocking reverts any attempts at unlocking offers.

    require unlockingPaused() == true;
    unlockOffers@withrevert(e, ids);
    assert lastReverted, "unlockOffers(...) should revert when trying to unlock offers on a paused contract";

1. Rule: UnpauseUnlockingAllowsOfferUnlocking - verifies that unpausing unlocking allows users to unlock offers.

    require unlockingPaused() == false;
    require harnessGetInternalOffers(id).id == id;
    unlockOffers(e, [id]);
    assert !lastReverted, "unlockOffers(...) should not revert when trying to unlock offers on an unpaused contract";

1. Invariant: LockedOfferIdAlwaysMatchesIndex - verifies the assumption that the offerId matches the ledger.

    harnessGetInternalOfferId(offerId) == offerId || harnessGetInternalOfferId(offerId) == to_bytes32(0);

1. Invariant: OfferCountAlwaysMatchesNumberOfStoredOffers - verifies the assumption that the offerCount always matches the ledger.

    to_mathint(offerCount()) == lockedOfferCount;

1. Rule: lockerPurchaseTokenBalanceGreaterThanOfferLedgerBalance - verifies the assumption that total purchaseToken balances are always greater than or equal to the amount recorded in ledger.

    require(sumOfOfferBalances <= to_mathint((offerStatePurchaseToken.balanceOf(repoLockerOfferState)))); // starting condition

    f(e, args);

    assert sumOfOfferBalances <= to_mathint((offerStatePurchaseToken.balanceOf(repoLockerOfferState)));

1. Rule: LockOffersIntegrity - ensures that purchase token balances are properly transferred to the repo locker when locking offers.

assert (purchaseTokenOneBalanceAfter == purchaseTokenBalanceBefore - amountToLock),
    "lockOffers should transfer collateral tokens from offeror to contract";

1. Rule: LockOffersDoesNotAffectThirdParty - verifies that locking offers belonging to one account does not affect the third party balances.

assert offerIdBefore == offerIdAfter,
    "lockRolloverOffer should not modify offer id";
  assert offerorBefore == offerorAfter,
    "lockRolloverOffer should not modify offeror";
  assert offerPriceHashBefore == offerPriceHashAfter,
    "lockRolloverOffer should not modify offer price hash";
  assert offerRevealedPriceBefore == offerRevealedPriceAfter,
    "lockRolloverOffer should not modify offer revealed price";
  assert offerAmountBefore == offerAmountAfter,
    "lockRolloverOffer should not modify offer amount";
  assert offerIsRevealedBefore == offerIsRevealedAfter,
    "lockRolloverOffer should not modify offer revealed status";

1. Rule: LockOffersMonotonicBehavior - verifies that locking offers is monotonically increasing in the offer count.

assert offerCountAfter >= offerCountBefore,
    "offerCount should increment or maintain the same value after locking an offer";

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

 bool offerIdAlreadyExists = existingGeneratedOffer.amount != 0 && existingOffer.amount == 0 ; // OfferIdAlreadyExists

  bool auctionNotOpen = e.block.timestamp < auctionStartTime() || e.block.timestamp > revealTime(); // AuctionNotOpen
  bool lockingPaused = lockingPaused(); // LockingPaused
  bool reentrant = harnessReentrancyGuardEntered();
  bool notSameOfferor = offerSubmissions[0].offeror != e.msg.sender ? true : false; // OfferNotOwned
  bool offerCountReached = offerCount() >= MAX_OFFER_COUNT() ? true : false; // MaxOfferCountReached
  bool offerNotOwned = harnessGetInternalOffers(offerSubmissions[0].id).amount != 0 && harnessGetInternalOffers(offerSubmissions[0].id).offeror != offerSubmissions[0].offeror; // OfferNotOwned

  bool editingOfferNotOwned = existingOfferAmount != 0
    && existingOfferor != offerSubmissions[0].offeror; // OfferNotOwned
  
  bool purchaseTokenNotApproved = offerSubmissions[0].purchaseToken != purchaseToken() ? true : false; // PurchaseTokenNotApproved
  bool offerAmountTooLow = offerSubmissions[0].amount < minimumTenderAmount(); // OfferAmountTooLow
  bool purchaseTokenBalanceTooLow = existingOfferAmount < offerSubmissions[0].amount  && lockingAuctionPurchaseToken.balanceOf(offerSubmissions[0].offeror) < offerDiff;
  bool purchaseTokenApprovalsTooLow = existingOfferAmount < offerSubmissions[0].amount && lockingAuctionPurchaseToken.allowance(offerSubmissions[0].offeror, repoLockerUnlocking) < offerDiff;
  bool lockerTransfersPaused = existingOfferAmount != offerSubmissions[0].amount && repoLockerOfferLocking.transfersPaused();
  bool repoServicerNotPairedToLocker = existingOfferAmount != offerSubmissions[0].amount && !repoLockerOfferLocking.hasRole(repoLockerOfferLocking.SERVICER_ROLE(), repoServicerLocking);
  bool offerLockerNotPairedToRepoServicer = existingOfferAmount != offerSubmissions[0].amount && !repoServicerLocking.hasRole(repoServicerLocking.AUCTION_LOCKER(), currentContract);

  bool nonZeroMsgValue = e.msg.value != 0;

  bool isExpectedToRevert =
    auctionNotOpen || lockingPaused || reentrant || notSameOfferor ||
    offerCountReached || offerNotOwned || editingOfferNotOwned || offerIdAlreadyExists ||
    purchaseTokenNotApproved || offerAmountTooLow || purchaseTokenBalanceTooLow || purchaseTokenApprovalsTooLow || lockerTransfersPaused 
    || repoServicerNotPairedToLocker || offerLockerNotPairedToRepoServicer || nonZeroMsgValue;
    
    assert lastReverted <=> isExpectedToRevert,
    "lockOffers should revert when one of the revert conditions is reached";

1. Rule: LockOffersWithReferralIntegrity - ensures that purchase token balances are properly transferred to the repo locker when locking offers with referral.

assert (purchaseTokenOneBalanceAfter == purchaseTokenBalanceBefore - amountToLock),
    "lockOffers should transfer collateral tokens from offeror to contract";

1. Rule: LockOffersWithReferralDoesNotAffectThirdParty - verifies that locking offers belonging to one account when calling lockOffersWithReferral does not affect the third party balances

   assert offerIdBefore == offerIdAfter,
    "lockRolloverOffer should not modify offer id";
  assert offerorBefore == offerorAfter,
    "lockRolloverOffer should not modify offeror";
  assert offerPriceHashBefore == offerPriceHashAfter,
    "lockRolloverOffer should not modify offer price hash";
  assert offerRevealedPriceBefore == offerRevealedPriceAfter,
    "lockRolloverOffer should not modify offer revealed price";
  assert offerAmountBefore == offerAmountAfter,
    "lockRolloverOffer should not modify offer amount";
  assert offerIsRevealedBefore == offerIsRevealedAfter,
    "lockRolloverOffer should not modify offer revealed status";

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

  bool auctionNotOpen = e.block.timestamp < auctionStartTime() || e.block.timestamp > revealTime(); // AuctionNotOpen
  bool lockingPaused = lockingPaused(); // LockingPaused
  bool sameReferral = e.msg.sender == referrer; // InvalidSelfReferral
  bool notSameOfferor = offerSubmissions[0].offeror != e.msg.sender ? true : false; // OfferNotOwned
  bool offerCountReached = offerCount() >= MAX_OFFER_COUNT() ? true : false; // MaxOfferCountReached
  bool offerNotOwned = harnessGetInternalOffers(offerSubmissions[0].id).amount != 0 && harnessGetInternalOffers(offerSubmissions[0].id).offeror != offerSubmissions[0].offeror; // OfferNotOwned
  bool purchaseTokenNotApproved = offerSubmissions[0].purchaseToken != purchaseToken() ? true : false; // PurchaseTokenNotApproved
  bool offerAmountTooLow = offerSubmissions[0].amount < minimumTenderAmount(); // OfferAmountTooLow

  bool isExpectedToRevert =
    auctionNotOpen || lockingPaused || notSameOfferor ||
    offerCountReached || offerNotOwned ||
    purchaseTokenNotApproved || offerAmountTooLow;

  assert lastReverted <=> isExpectedToRevert,
    "lockOffersWithReferral should revert when one of the revert conditions is reached";

1. Rule: LockOffersWithReferralMonotonicBehavior - verifies that locking offers with referral is monotonically increasing in the offer count.

assert offerCountAfter >= offerCountBefore,
    "offerCount should increment or maintain the same value after locking an offer";

1. Rule: UnlockOffersIntegrity - ensures that purchase token balances are properly transferred to user when unlocking offers.

 assert (purchaseTokenBalanceAfter == (purchaseTokenBalanceBefore + purchaseTokenAmountToUnlock)),
    "unlockOffers should not revert";

1. Rule: UnlockOffersDoesNotAffectThirdParty - verifies that unlocking offers belonging to one account does not affect the third party balances

   assert thirdPartyOfferAffected,
     "unlockOffers should not modify offers that are not in args"; 

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

  bool unlockingPaused = unlockingPaused(); // UnlockingPaused
  bool reentrant = harnessReentrancyGuardEntered();
  bool auctionNotOpen = e.block.timestamp < auctionStartTime(); // AuctionNotOpen
  bool auctionNotCancelledForWithdrawal = e.block.timestamp > revealTime() && !termAuction.auctionCancelledForWithdrawal(); // AuctionNotOpen
  bool nonExistentOffer = harnessGetInternalOffers(unlockOfferId).amount == 0; // NonExistentOffer
  bool offerNotOwned = harnessGetInternalOffers(unlockOfferId).offeror != e.msg.sender; // OfferNotOwned

  bool lockerTransfersPaused = repoLockerUnlocking.transfersPaused();
  bool repoServicerNotPairedToLocker = !repoLockerUnlocking.hasRole(repoLockerUnlocking.SERVICER_ROLE(), repoServicerUnlocking);
  bool offerLockerNotPairedToRepoServicer = !repoServicerUnlocking.hasRole(repoServicerUnlocking.AUCTION_LOCKER(), currentContract);

  bool nonZeroMsgValue = e.msg.value != 0;

  bool isExpectedToRevert = unlockingPaused || reentrant || auctionNotOpen || auctionNotCancelledForWithdrawal || nonExistentOffer || offerNotOwned 
  || lockerTransfersPaused || repoServicerNotPairedToLocker ||  offerLockerNotPairedToRepoServicer || nonZeroMsgValue;

  assert isExpectedToRevert <=> lastReverted,
    "unlockOffers should revert when revert conditions are met";

1. Rule: UnlockOffersMonotonicBehavior - verifies that unlocking offers is monotonically decreasing in the offer count.

assert offerCountAfter == assert_uint256(offerCountBefore - unlockOfferIds.length),
    "offerCount should decrement by the number of offer ids submitted to unlock";

1. Rule: UnlockOfferPartialIntegrity - ensures that purchase token balances are properly transferred to user when partially unlocking offers.

assert purchaseTokenBalancAfter == purchaseTokenBalanceBefore + amount,
    "purchase token balance should increase by the provided amount";

1. Rule: UnlockOfferPartialDoesNotAffectThirdParty - verifies that partially unlocking offers belonging to one account does not affect the third party balances

assert thirdPartyOfferNotAffected,
    "unlockOfferPartial should not modify offers that are not in args";

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

bool msgValueNotZero = e.msg.value != 0;
  bool notAuctioneer = !hasRole(AUCTIONEER_ROLE(), e.msg.sender);
  bool lockerNotAuctionLocker = !repoServicerUnlocking.hasRole(repoServicerUnlocking.AUCTION_LOCKER(), currentContract);
  bool servicerNotServicer = !repoLockerUnlocking.hasRole(repoLockerUnlocking.SERVICER_ROLE(), repoServicerUnlocking);
  bool insufficientLockerBalance = amount > unlockingAuctionPurchaseToken.balanceOf(repoLockerUnlocking);
  bool lockerTransfersPaused = repoLockerUnlocking.transfersPaused();

  bool isExpectedToRevert =
    msgValueNotZero ||
    notAuctioneer ||
    lockerNotAuctionLocker ||
    servicerNotServicer ||
    insufficientLockerBalance ||
    lockerTransfersPaused;

  assert isExpectedToRevert == lastReverted,
    "unlockOfferPartial should revert when revert conditions are met";

1. Rule: UnlockOfferPartialMonotonicBehavior - verifies that partially unlocking offers does not change the offer count.

assert offerCountAfter == offerCountBefore,
    "unlockOfferPartial should not affect the offerCount";
}

1. Rule: RevealOffersIntegrity - ensures that prices are revealed when revealing offers.

    assert isRevealedAfter && revealedPriceAfter == price, "revealOffers should successfully reveal offers";

1. Rule: RevealOffersDoesNotAffectThirdParty - verifies that revealing offers belonging to one account does not affect the third party balances

    assert !isThirdPartyRevealedAfter, "revealOffers should not affect third-party offers";
}

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

  bool isNotInRevealPhase = e.block.timestamp < revealTime(); // AuctionNotRevealing
  bool isOfferPriceModified = harnessGenerateOfferPriceHash(price, nonce) != harnessGetInternalOfferOfferPriceHash(id); // OfferPriceModified
  bool isTenderPriceTooHigh = price > MAX_OFFER_PRICE(); // TenderPriceTooHigh
  bool msgValueNotZero = e.msg.value != 0;

  bool isExpectedToRevert = isNotInRevealPhase || isOfferPriceModified || isTenderPriceTooHigh || msgValueNotZero;

  assert lastReverted <=> isExpectedToRevert,
    "revealOffers should revert if conditions are met";

1. Rule: RevealOffersMonotonicBehavior - verifies that revealing offers does not change the offer count.

    assert offerCountBefore == offerCountAfter, "revealOffers should not change the offer count";

1. Rule: OnlyRoleCanCallRevert - checks if a method call requires specific roles to execute successfully, does not revert if the caller has the necessary role.

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

1. 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.

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

TermAuction

1. Rule: OnlyRoleCanCallRevert - checks if a method call requires specific roles to execute successfully, does not revert if the caller has the necessary role.

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

1. 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.

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

1. Rule: OnlyRoleCanCallRevertCompleteAuction and OnlyRoleCanCallStorageCompleteAuction - verifies that the completeAuction call where unrevealed bids exists requires specific roles to execute successfully, does not revert if the caller has the necessary role.

    assert !lastReverted =>
        hasRole(ADMIN_ROLE(), e.msg.sender) ||
        (completeAuctionInput.unrevealedBidSubmissions.length == 0 && completeAuctionInput.unrevealedOfferSubmissions.length == 0);

1. Rule: OnlyRoleCanCallStorageCompleteAuction - ensures that changes to storage by the completeAuction call where unrevealed bids exists can only be performed by addresses with the admin role, guarding against unauthorized auction clearing where unrevealed bids exist.

    assert storeBefore != storeAfter =>
        hasRole(ADMIN_ROLE(), e.msg.sender) ||
        (completeAuctionInput.unrevealedBidSubmissions.length == 0 && completeAuctionInput.unrevealedOfferSubmissions.length == 0);

Getting Started

Install certora-cli package with pip install certora-cli. To verify specification files, pass to certoraRun the corresponding configuration file in the [certora/confs](<https://github.com/morpho-org/morpho-blue/blob/2ffb6821815ec542c78e0d0379b5e7094d6fd37a/certora/confs>) folder. It requires having set the CERTORAKEY environment variable to a valid Certora key. You can also pass additional arguments, notably to verify a specific rule. For example, at the root of the repository:

certoraRun certora/confs/termRepoServicer.conf --rule mintOpenExposureIntegrity