# 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](https://github.com/term-finance/term-finance-contracts/commit/831292726cdc22e9d4d2953d59051fa00fbd4f72). The scope of this verification includes all [Term Servicer](https://developers.term.finance/term-finance-protocol/term-repo/term-servicer-group) contracts within Term Protocol. This includes the following. * `TermRepoToken.sol` * `TermRepoLocker.sol` * `TermRepoServicer.sol` * `TermRepoCollateralManager.sol` * `TermRepoRolloverManager.sol` [Auction Contracts](https://developers.term.finance/term-finance-protocol/term-repo/term-auction-group) 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](https://runtimeverification.com/blog/how-audits-can-optimize-code-base-term-finance-clearing-price-algorithm). 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](https://www.notion.so/protocol/term-repos)) modeled on tri-party repo arrangements common in TradFi. Borrowers and lenders are matched through a unique recurring auction process ([Term Auctions](https://www.notion.so/protocol/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](https://www.notion.so/protocol/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. {% code fullWidth="false" %} ```solidity 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"; } ``` {% endcode %} 2. **Rule:** `onlyPairTermContractsChangesIsTermContractPairedRule` - ensures that only pairTermContracts(...) can change state of `termContractPaired` ```solidity 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. ```solidity to_mathint(totalSupply()) == sumOfBalances ``` 2. **Rule:** `totalSupplyNeverOverflow` - guarantees that the total supply of tokens cannot exceed the maximum value allowed by the system, preventing overflow errors. ```solidity assert totalSupplyBefore <= totalSupplyAfter; ``` 3. **Rule:** `noMethodChangesMoreThanTwoBalances` - ensures that no single operation can alter more than two account balances at once. ```solidity assert numberOfChangesOfBalancesAfter <= numberOfChangesOfBalancesBefore + 2; ``` 4. **Rule:** `onlyAllowedMethodsMayChangeAllowance` - verifies that changes to token allowances are restricted to approved methods, ensuring that delegated spending limits are securely managed. ```solidity definition canIncreaseAllowance(method f) returns bool = f.selector == sig:approve(address,uint256).selector || f.selector == sig:increaseAllowance(address,uint256).selector; definition canDecreaseAllowance(method f) returns bool = f.selector == sig:approve(address,uint256).selector || f.selector == sig:decreaseAllowance(address,uint256).selector || f.selector == sig:transferFrom(address,address,uint256).selector; assert allowanceAfter > allowanceBefore => canIncreaseAllowance(f), "should not increase allowance"; assert allowanceAfter < allowanceBefore => canDecreaseAllowance(f), "should not decrease allowance"; ``` 5. **Rule:** `onlyAllowedMethodsMayChangeBalance` - verifies that token balance changes within accounts can only be done through approved methods, preventing unauthorized modifications. ```solidity definition canIncreaseBalance(method f) returns bool = f.selector == sig:mintRedemptionValue(address,uint256).selector || f.selector == sig:mintTokens(address,uint256).selector || f.selector == sig:transfer(address,uint256).selector || f.selector == sig:transferFrom(address,address,uint256).selector; definition canDecreaseBalance(method f) returns bool = f.selector == sig:burn(address,uint256).selector || f.selector == sig:burnAndReturnValue(address,uint256).selector || f.selector == sig:transfer(address,uint256).selector || f.selector == sig:transferFrom(address,address,uint256).selector; assert balanceAfter > balanceBefore => canIncreaseBalance(f); assert balanceAfter < balanceBefore => canDecreaseBalance(f); ``` 6. **Rule:** `onlyAllowedMethodsMayChangeTotalSupply` - verifies that changes to the total supply of tokens are conducted only through authorized methods, maintaining supply integrity. ```solidity definition canIncreaseTotalSupply(method f) returns bool = f.selector == sig:mintRedemptionValue(address,uint256).selector || f.selector == sig:mintTokens(address,uint256).selector; definition canDecreaseTotalSupply(method f) returns bool = f.selector == sig:burn(address,uint256).selector || f.selector == sig:burnAndReturnValue(address,uint256).selector; assert totalSupplyAfter > totalSupplyBefore => canIncreaseTotalSupply(f); assert totalSupplyAfter < totalSupplyBefore => canDecreaseTotalSupply(f); ``` 7. **Rule:** `reachability` - verifies that all non-initialization and non-upgrade methods can be executed, ensuring contract functionality is accessible. ```solidity f(e,args); satisfy true; ``` 8. **Rule:** `onlyAuthorizedCanTransfer` - verifies that token transfers can only be initiated by authorized entities. ```solidity assert ( balanceAfter < balanceBefore ) => ( f.selector == sig:burn(address,uint256).selector || f.selector == sig:burnAndReturnValue(address,uint256).selector || e.msg.sender == account || balanceBefore - balanceAfter <= to_mathint(allowanceBefore) ); ``` 9. **Rule:** `onlyHolderOfSpenderCanChangeAllowance` - verifies that changes to spending allowance, which is the limit set by the token holder for how much another account can spend on their behalf, can only be made by the token holder or a designated spender 
assert (
        allowanceAfter > allowanceBefore
    ) => (
        ((f.selector == sig:approve(address,uint256).selector || f.selector == sig:increaseAllowance(address,uint256).selector) && e.msg.sender == holder)
    );

    assert (
        allowanceAfter < allowanceBefore
    ) => (
        (f.selector == sig:transferFrom(address,address,uint256).selector && e.msg.sender == spender) ||
        ((f.selector == sig:approve(address,uint256).selector || f.selector == sig:decreaseAllowance(address,uint256).selector) && e.msg.sender == holder )
    );
10. **Rule:** `mintTokensIntegrity` - ensures that after minting tokens, the balance of the minter and the total supply are correctly increased. ```solidity assert to_mathint(balanceOf(to)) == toBalanceBefore + amount; assert to_mathint(totalSupply()) == totalSupplyBefore + amount; ``` 11. **Rule:** `mintRedemptionValueIntegrity` - ensures that after minting tokens and returning a value, the balance of the minter and the total supply are correctly increased. ```solidity mathint redemptValue = redemptionValue(); mathint expectedBalanceAfter = (balanceBefore + ( amount * expScale * expScale / redemptValue) / expScale); mathint expectedTotalSupplyAfter = (totalSupply() + ( amount * expScale * expScale / redemptValue) / expScale); assert balanceAfter == expectedBalanceAfter; assert totalSupplyAfter == expectedTotalSupplyAfter; ``` where `expScale` = 10^ 18. 12. **Rule:** `mintTokensRevertingConditions`- check for revert under the defined expected conditions, ensuring operation adherence to defined rules. ```solidity bool paused = mintingPaused() == true; bool payable = e.msg.value > 0; bool toZeroAccount = account == 0; bool notMinterRole = !hasRole(MINTER_ROLE(), e.msg.sender); bool isExpectedToRevert = paused || payable || notMinterRole || toZeroAccount; ``` 13. **Rule:** `mintRedemptionValueRevertingConditions`- check for revert under the defined expected conditions, ensuring operation adherence to defined rules. ```solidity bool paused = mintingPaused() == true; bool payable = e.msg.value > 0; bool toZeroAccount = account == 0; bool notMinterRole = !hasRole(MINTER_ROLE(), e.msg.sender); bool isExpectedToRevert = paused || payable || notMinterRole || toZeroAccount; ``` 14. **Rule:** `mintRedemptionValueDoesNotAffectThirdParty` - verifies that when one account invokes `mintRedemptionValue`, this action does not affect third-party balances. ```solidity require addr1 != addr2; uint256 before = balanceOf(addr2); mintRedemptionValue(e, addr1, amount); assert balanceOf(addr2) == before; ``` 15. **Rule:** `mintTokensDoesNotAffectThirdParty` - verifies that when one account invokes `mintOpenExposure`, this action does not affect third-party balances. ```solidity require addr1 != addr2; uint256 before = balanceOf(addr2); mintTokens(e, addr1, amount); assert balanceOf(addr2) == before; ``` 16. **Rule:** `burnIntegrity` - ensures that after burning tokens, the balance of the burner and the total supply are correctly decreased. ```solidity assert to_mathint(balanceOf(from)) == fromBalanceBefore - amount; assert to_mathint(totalSupply()) == totalSupplyBefore - amount; ``` 17. **Rule:** `burnAndReturnValueIntegrity` - ensures that after burning tokens and returning a value, the balance of the burner and the total supply are correctly decreased. ```solidity assert to_mathint(balanceOf(from)) == fromBalanceBefore - amount; assert to_mathint(totalSupply()) == totalSupplyBefore - amount; ``` 18. **Rule:** `burnRevertingConditions` - checks conditions under which a burn operation should revert, such as not having enough balance, the contract being paused, etc. ```solidity bool payable = e.msg.value > 0; bool notEnoughBalance = balanceOf(account) < amount; bool notBurnerRole = !hasRole(BURNER_ROLE(), e.msg.sender); bool fromZeroAccount = account == 0; bool paused = burningPaused(); bool isExpectedToRevert = notEnoughBalance || notBurnerRole || paused || fromZeroAccount || payable; assert lastReverted <=> isExpectedToRevert; ``` 19. **Rule:** `burnDoesNotAffectThirdParty` - verifies that burning tokens from one account does not affect third party balances. ```solidity assert balanceOf(addr2) == before; ``` 20. **Rule:** `burnAndReturnValueDoesNotAffectThirdParty` - confirms that burning tokens and returning a value from one account does not impact the balance of an unrelated account. ```solidity assert balanceOf(addr2) == before; ``` 21. **Rule:** `transferIntegrity` - asserts that after a transfer, the balances of the sender and recipient are updated correctly, respecting the case when sender and recipient are the same. ```solidity assert to_mathint(balanceOf(holder)) == holderBalanceBefore - (holder == recipient ? 0 : amount); assert to_mathint(balanceOf(recipient)) == recipientBalanceBefore + (holder == recipient ? 0 : amount); ``` 22. **Rule:** `transferIsOneWayAdditive` - demonstrates that if a transfer of a combined amount succeeds, individual transfers of the components should also succeed without affecting the final state. ```solidity transfer(e, recipient, assert_uint256(sum)); storage after1 = lastStorage; transfer@withrevert(e, recipient, amount_a) at init; // restores storage assert !lastReverted; //if the transfer passed with sum, it should pass with both summands individually transfer@withrevert(e, recipient, amount_b); assert !lastReverted; storage after2 = lastStorage; assert after1[currentContract] == after2[currentContract]; ``` 23. **Rule:** `transferRevertingConditions`- identifies conditions under which a transfer should revert, such as the sender not having enough balance. ```solidity bool payable = e.msg.value != 0; bool zeroTo = account == 0; bool notEnoughBalance = balanceOf(e.msg.sender) < amount; bool isExpectedToRevert = payable || zeroTo || notEnoughBalance; assert lastReverted <=> isExpectedToRevert; ``` 24. **Rule:** `transferDoesNotAffectThirdParty` - ensures that a transfer between two accounts does not affect the balance of a third party. ```solidity assert balanceOf(addr2) == before; ``` 25. **Rule:** `transferFromIntegrity` - confirms that after a transferFrom operation, the balances of the holder and recipient are correctly adjusted, and the allowance is updated appropriately. ```solidity assert to_mathint(allowance(holder, spender)) == (allowanceBefore == max_uint256 ? max_uint256 : allowanceBefore - amount); assert to_mathint(balanceOf(holder)) == holderBalanceBefore - (holder == recipient ? 0 : amount); assert to_mathint(balanceOf(recipient)) == recipientBalanceBefore + (holder == recipient ? 0 : amount); ``` 26. **Rule:** `transferFromRevertingConditions` - checks for conditions that should cause a transferFrom to revert, such as insufficient allowance or balance. ```solidity bool sendEthToNotPayable = e.msg.value != 0; bool ownerZero = owner == 0; bool recepientZero = recepient == 0; bool allowanceIsLow = allowed < transfered; bool notEnoughBalance = balanceOf(owner) < transfered; bool isExpectedToRevert = sendEthToNotPayable || allowanceIsLow || notEnoughBalance || ownerZero || recepientZero; assert lastReverted <=> isExpectedToRevert; ``` 27. **Rule:** `transferFromDoesNotAffectThirdParty` - verifies that a `transferFrom` operation does not impact the balance or allowance of third parties. ```solidity assert thirdPartyBalanceBefore == thirdPartyBalanceAfter; assert thirdPartyAllowanceBefore == thirdPartyAllowanceAfter; ``` 28. **Rule:** `transferFromIsOneWayAdditive` - shows that if a `transferFrom` for a combined amount is successful, then separate `transferFrom` operations for each component of the amount should also succeed, without altering the final state. ```solidity transferFrom(e, owner, recipient, assert_uint256(sum)); storage after1 = lastStorage; transferFrom@withrevert(e, owner, recipient, amount_a) at init; // restores storage assert !lastReverted; //if the transfer passed with sum, it should pass with both summands individually transferFrom@withrevert(e, owner, recipient, amount_b); assert !lastReverted; storage after2 = lastStorage; assert after1[currentContract] == after2[currentContract]; ``` 29. **Rule:** `approveIntegrity` - ensures that the allowance is correctly set after an approve operation. ```solidity assert allowance(holder, spender) == amount; ``` 30. **Rule:** `approveRevertingConditions` - identifies scenarios in which an approve operation should revert, such as when trying to approve from a zero address. ```solidity bool payable = e.msg.value != 0; bool spenderIsZero = spender == 0; bool isExpectedToRevert = payable || spenderIsZero; assert lastReverted <=> isExpectedToRevert; ``` 31. **Rule:** `approveDoesNotAffectThirdParty` - confirms that an approve operation between two parties does not affect the allowance of a third party. ```solidity assert thirdPartyAllowanceBefore == thirdPartyAllowanceBefore; ``` 32. **Rule:** `onlyAllowedMethodsMayChangeMintExposureCap` - ensures that only specific methods can modify the mint exposure cap. Methods like minting, burning, or resetting the cap are allowed to change it. ```solidity assert mintExposureCapAfter > mintExposureCapBefore => canIncreaseMintExposureCap(f); assert mintExposureCapAfter < mintExposureCapBefore => canDecreaseMintExposureCap(f); ``` 33. **Rule:** `mintExposureCapNeverOverflow` - verifies that when the mint exposure cap is increased, this action does not cause it to overflow, ensuring the cap's value remains within safe limits. ```solidity assert mintExposureCapBefore <= mintExposureCapAfter; ``` 34. **Rule:** `noMethodChangesRedemptionValue` - confirms that the redemption value remains unchanged across transactions, except by methods explicitly intended to modify it. This rule ensures stability in the redemption value. ```solidity assert redemptionValueBefore == redemptionValueAfter; ``` 35. **Rule:** `onlyRoleCanCallRevert` - checks if a method call that is not a view and requires specific roles to execute successfully, does not revert if the caller has the necessary role. ```solidity assert !lastReverted => hasRole(MINTER_ROLE(),e.msg.sender) || hasRole(BURNER_ROLE(),e.msg.sender) || hasRole(ADMIN_ROLE(),e.msg.sender) || hasRole(DEVOPS_ROLE(),e.msg.sender) || hasRole(INITIALIZER_ROLE(),e.msg.sender); ``` 36. **Rule:** `onlyRoleCanCallStorage` - ensures that changes to storage by non-view method calls can only be performed by addresses with specific roles, guarding against unauthorized modifications. ```solidity 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. ```solidity bool transfersPausedBefore = transfersPaused(); f(e, args); bool transfersPausedAfter = transfersPaused(); assert(transfersPausedBefore == transfersPausedAfter); ``` 2. **Rule:** `noMethodChangesTermRepoId` - confirms that the Term Repo ID remains constant and is not changed by any method calls, ensuring its immutability post-initialization. ```solidity bytes32 termRepoIdBefore = termRepoId(); f(e, args); bytes32 termRepoIdAfter = termRepoId(); assert(termRepoIdBefore == termRepoIdAfter); ``` 3. **Rule:** `onlyAllowedMethodsMayChangeEmitter` - verifies that the emitter's address can only be changed through specific methods, preserving the integrity and security of the emitter identification. ```solidity address emitterBefore = emitterAddress(); f(e, args); address emitterAfter = emitterAddress(); assert(emitterBefore == emitterAfter); ``` 4. **Rule:** `onlyAllowedMethodsMayChangeBalance` - checks if the treasury balance is correctly updated by allowed methods and remains unchanged by others. ```solidity uint256 balanceBefore = token.balanceOf(currentContract); f(e, args); uint256 balanceAfter = token.balanceOf(currentContract); // For increasing treasury balance if (canIncreaseTreasuryBalance(f)) { assert balanceAfter > balanceBefore => (sender != currentContract) && (amount != 0); assert balanceAfter == balanceBefore => (sender == currentContract) || (amount == 0); } // For decreasing treasury balance else if (canDecreaseTreasuryBalance(f)) { assert balanceAfter < balanceBefore => (recipient != currentContract) && (amount != 0); assert balanceAfter == balanceBefore => (recipient == currentContract) || (amount == 0); } // For other methods else { assert balanceAfter == balanceBefore; } ``` 5. **Rule:** `reachability` - verifies that all non-initialization and non-upgrade methods can be executed, ensuring contract functionality is accessible. ```solidity f(e,args); satisfy true; ``` 6. **Rule:** `transferTokenFromWalletIntegrity` - validates the integrity of transferring tokens from the wallet, checking the update in treasury and sender balances post-transaction. ```solidity mathint treasuryBalanceBefore = to_mathint(token.balanceOf(currentContract)); mathint senderBalanceBefore = to_mathint(token.balanceOf(sender)); transferTokenFromWallet(e, sender, token, amount); mathint treasuryBalanceAfter = to_mathint(token.balanceOf(currentContract)); mathint senderBalanceAfter = to_mathint(token.balanceOf(sender)); mathint expectedDiff = (isSelf || !isServicer || transfersPaused || isOverspend) ? 0 : to_mathint(amount); // Asserting balance changes based on conditions assert treasuryBalanceAfter == treasuryBalanceBefore + expectedDiff; assert senderBalanceAfter == senderBalanceBefore - expectedDiff; assert transfersPaused() == transfersPaused; ``` 7. **Rule:** `transferTokenToWalletIntegrity` - ensures the correct adjustment of balances when tokens are transferred to the wallet, factoring in role permissions and pause status. ```solidity mathint treasuryBalanceBefore = to_mathint(token.balanceOf(currentContract)); mathint recipientBalanceBefore = to_mathint(token.balanceOf(recipient)); transferTokenToWallet(e, recipient, token, amount); mathint treasuryBalanceAfter = to_mathint(token.balanceOf(currentContract)); mathint recipientBalanceAfter = to_mathint(token.balanceOf(recipient)); mathint expectedDiff = (isSelf || !isServicer || transfersPaused || isOverspend) ? 0 : to_mathint(amount); // Verifying the outcome matches expectations assert recipientBalanceAfter == recipientBalanceBefore + expectedDiff; assert treasuryBalanceAfter == treasuryBalanceBefore - expectedDiff; assert transfersPaused() == transfersPaused; ``` 8. **Rule:** `pauseTransfersIntegrity` - validates that transfers can be paused correctly by the authorized role, ensuring the state is changed as expected. ```solidity pauseTransfers(e); assert transfersPaused(); ``` 9. **Rule:** `unpauseTransfersIntegrity` - confirms that transfers can be unpaused accurately, reverting the paused state and allowing transactions to proceed. ```solidity unpauseTransfers(e); assert !transfersPaused(); ``` 10. **Rule:** `onlyRoleCanCallRevert` - ensures that methods not related to initialization, upgrade, or role management only revert if the caller lacks the necessary roles. This rule safeguards against unauthorized actions while allowing legitimate operations. ```solidity currentContract.f@withrevert(e,args); // Verification if the method didn't revert, the caller must possess one of the specified roles. assert !lastReverted => hasRole(SERVICER_ROLE(),e.msg.sender) || hasRole(ADMIN_ROLE(),e.msg.sender) || hasRole(DEVOPS_ROLE(),e.msg.sender) || hasRole(INITIALIZER_ROLE(),e.msg.sender); ``` 11. **Rule:** `onlyRoleCanCallStorage` - verifies that storage modifications by non-view methods are properly guarded by role checks, preventing unauthorized changes to the contract's state. This rule enforces role-based access control for sensitive operations. ```solidity 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. ```solidity to_mathint(totalOutstandingRepurchaseExposure()) == sumOfRepurchases filtered { m -> m.selector != sig:initialize(string,uint256,uint256,uint256,uint256,address,address,address,address).selector && m.selector != sig:upgradeToAndCall(address,bytes).selector && m.selector != sig:upgradeTo(address).selector } ``` 2. **Rule:** `onlyAllowedMethodsMayChangeTotalOutstandingRepurchaseExposure` - specifies that only particular methods can increase or decrease the total outstanding repurchase exposure, aligning changes with expected business logic operations. ```solidity definition canIncreaseTotalOutstandingRepurchaseExposure(method f) returns bool = f.selector == sig:fulfillBid(address,uint256,uint256,address[],uint256[],uint256).selector || f.selector == sig:openExposureOnRolloverNew(address,uint256,uint256,address,uint256).selector || f.selector == sig:mintOpenExposure(uint256,uint256[]).selector; definition canDecreaseTotalOutstandingRepurchaseExposure(method f) returns bool = f.selector == sig:submitRepurchasePayment(uint256).selector || f.selector == sig:closeExposureOnRolloverExisting(address,uint256).selector || f.selector == sig:liquidatorCoverExposureWithRepoToken(address,address,uint256).selector || f.selector == sig:liquidatorCoverExposure(address,address,uint256).selector || f.selector == sig:burnCollapseExposure(uint256).selector; uint256 totalOutstandingRepurchaseExposureBefore = totalOutstandingRepurchaseExposure(); f(e, args); uint256 totalOutstandingRepurchaseExposureAfter = totalOutstandingRepurchaseExposure(); assert totalOutstandingRepurchaseExposureAfter > totalOutstandingRepurchaseExposureBefore => canIncreaseTotalOutstandingRepurchaseExposure(f); assert totalOutstandingRepurchaseExposureAfter < totalOutstandingRepurchaseExposureBefore => canDecreaseTotalOutstandingRepurchaseExposure(f); ``` 3. **Rule:** `totalOutstandingRepurchaseExposureNeverOverflows` - ensures that actions intended to increase the total outstanding repurchase exposure do not result in an overflow, preserving the integrity of financial calculations. ```solidity uint256 totalOutstandingRepurchaseExposureBefore = totalOutstandingRepurchaseExposure(); f(e, args); uint256 totalOutstandingRepurchaseExposureAfter = totalOutstandingRepurchaseExposure(); assert totalOutstandingRepurchaseExposureBefore <= totalOutstandingRepurchaseExposureAfter; ``` 4. **Rule:** `onlyAllowedMethodsMayChangeTotalRepurchaseCollected` - identifies methods permitted to increase or decrease the total repurchase collected, ensuring that financial metrics reflect actual repurchase activity accurately. ```solidity definition canIncreaseTotalRepurchaseCollected(method f) returns bool = f.selector == sig:submitRepurchasePayment(uint256).selector || f.selector == sig:closeExposureOnRolloverExisting(address,uint256).selector || f.selector == sig:liquidatorCoverExposure(address,address,uint256).selector; definition canDecreaseTotalRepurchaseCollected(method f) returns bool = f.selector == sig:redeemTermRepoTokens(address,uint256).selector; uint256 totalRepurchaseCollectedBefore = totalRepurchaseCollected(); f(e, args); uint256 totalRepurchaseCollectedAfter = totalRepurchaseCollected(); assert totalRepurchaseCollectedAfter > totalRepurchaseCollectedBefore => canIncreaseTotalRepurchaseCollected(f); assert totalRepurchaseCollectedAfter < totalRepurchaseCollectedBefore => canDecreaseTotalRepurchaseCollected(f); ``` 5. **Rule:** `totalRepurchaseCollectedNeverOverflows` - verifies that the total repurchase collected metric cannot overflow as a result of any operation, maintaining the system's financial stability. ```solidity uint256 totalRepurchaseCollectedBefore = totalRepurchaseCollected(); f(e, args); uint256 totalRepurchaseCollectedAfter = totalRepurchaseCollected(); assert totalRepurchaseCollectedBefore <= totalRepurchaseCollectedAfter; ``` 6. **Rule:**`shortfallHaircutMantissaAlwaysZeroBeforeRedemptionAndLessThanExpScaleAfter` - confirms the shortfall haircut mantissa remains zero before the redemption timestamp and falls within expected bounds after, ensuring fair and predictable financial adjustments. ```solidity require(shortfallHaircutMantissa() == 0); f(e, args); assert (e.block.timestamp <= redemptionTimestamp()) => (shortfallHaircutMantissa() == 0); assert (shortfallHaircutMantissa() > 0 && shortfallHaircutMantissa() < 10 ^ 18) => (e.block.timestamp > redemptionTimestamp()); ``` 7. **Rule:** `totalRepurchaseCollectedLessThanOrEqualToLockerPurchaseTokenBalance` - ensures that the total repurchase collected does not exceed the locker's purchase token balance, preventing overestimation of collected repurchases. ```solidity require(termRepoLocker() == stateLocker); // bounds for test require(purchaseToken() == stateToken); // bounds for test require(totalRepurchaseCollected() <= stateToken.balanceOf(stateLocker)); // starting condition require(e.msg.sender != stateLocker); // repo locker contract does not have calls to servicer require(!isTokenCollateral(stateToken)); // token will not be both purchase and collateral token f(e, args); assert (totalRepurchaseCollected() <= stateToken.balanceOf(stateLocker)); ``` 8. **Rule:** `noMethodsChangeMaturityTimestamp` - validates that no method changes the maturity timestamp, ensuring consistency in the term's length and financial obligations. ```solidity uint256 maturityTimestampBefore = maturityTimestamp(); f(e, args); uint256 maturityTimestampAfter = maturityTimestamp(); assert maturityTimestampBefore == maturityTimestampAfter; ``` 9. **Rule:** `noMethodsChangeEndOfRepurchaseWindow` - confirms the end of the repurchase window is immutable across all contract interactions, preserving the predetermined timeframe for repurchases, which is critical for contractual agreements. ```solidity uint256 endOfRepurchaseWindowBefore = endOfRepurchaseWindow(); f(e, args); uint256 endOfRepurchaseWindowAfter = endOfRepurchaseWindow(); assert endOfRepurchaseWindowBefore == endOfRepurchaseWindowAfter; ``` 10. **Rule:** `noMethodsChangeRedemptionTimestamp` - ensures the redemption timestamp remains constant across all contract interactions, guaranteeing the redemption period's stability and predictability. ```solidity uint256 redemptionTimestampBefore = redemptionTimestamp(); f(e, args); uint256 redemptionTimestampAfter = redemptionTimestamp(); assert redemptionTimestampBefore == redemptionTimestampAfter; ``` 11. **Rule:** `noMethodsChangeServicingFee` - verifies that the servicing fee rate is maintained across all transactions, ensuring consistent fee calculations and financial expectations for parties involved. ```solidity uint256 servicingFeeBefore = servicingFee(); f(e, args); uint256 servicingFeeAfter = servicingFee(); assert servicingFeeBefore == servicingFeeAfter; ``` 12. **Rule:** `onlyAllowedMethodsChangeShortfallHaircutMantissa` - restricts adjustments to the shortfall haircut mantissa to specific authorized methods, safeguarding the metric's integrity against unauthorized modifications. ```solidity uint256 shortfallHaircutMantissaBefore = shortfallHaircutMantissa(); f(e, args); uint256 shortfallHaircutMantissaAfter = shortfallHaircutMantissa(); assert shortfallHaircutMantissaBefore == shortfallHaircutMantissaAfter; ``` 13. **Rule:** `noMethodChangesPurchaseToken` - confirms the purchase token's address remains unaltered through contract operations, ensuring continuity and reliability in financial mechanisms involving the token. ```solidity address purchaseTokenBefore = purchaseToken(); f(e, args); address purchaseTokenAfter = purchaseToken(); assert purchaseTokenBefore == purchaseTokenAfter; ``` 14. **Rule:** `onlyAllowedMethodsMayChangeTermContracts` - specifies that term contract addresses can only be modified through designated methods, preventing unauthorized updates and maintaining contract ecosystem integrity. ```solidity address termRepoCollateralManagerBefore = termRepoCollateralManager(); address termRepoRolloverManagerBefore = termRepoRolloverManager(); address termRepoLockerBefore = termRepoLocker(); address termRepoTokenBefore = termRepoToken(); address termControllerBefore = termControllerAddress(); address emitterBefore = emitterAddress(); f(e, args); assert termRepoCollateralManager() == termRepoCollateralManagerBefore, "termRepoCollateralManager cannot be changed"; assert termRepoRolloverManager() == termRepoRolloverManagerBefore, "termRepoRolloverManager cannot be changed"; assert termRepoLocker() == termRepoLockerBefore, "termRepoLocker cannot be changed"; assert termRepoToken() == termRepoTokenBefore, "termRepoToken cannot be changed"; assert termControllerAddress() == termControllerBefore, "termController cannot be changed"; assert emitterAddress() == emitterBefore, "emitter cannot be changed"; ``` 15. **Rule:** `onlyAllowedMethodsMayChangeRepurchaseExposureLedger` - limits the conditions under which the repurchase exposure ledger can be altered, ensuring that changes are strictly governed and reflect actual repurchase activities. ```solidity uint256 repurchaseExposureLedgerBefore = repurchaseExposureLedger(borrower); f(e, args); uint256 repurchaseExposureLedgerAfter = repurchaseExposureLedger(borrower); assert repurchaseExposureLedgerAfter == repurchaseExposureLedgerBefore, "repurchaseExposureLedger cannot be changed"; ``` 16. **Rule:** `burnCollapseExposureMonotonicBehavior` - verifies that burning to collapse exposure reduces the caller's repo token balance, their repurchase obligation, and the total outstanding repurchase exposure monotonically, ensuring systemic risk reduction and individual accountability. ```solidity uint256 collapserRepoTokenBalanceBefore = collapsingRepoToken.balanceOf(e.msg.sender); uint256 collapserRepoExposureBefore = getBorrowerRepurchaseObligation(e.msg.sender); uint256 totalOutstandingRepurchaseExposureBefore = totalOutstandingRepurchaseExposure(); burnCollapseExposure(e, amount); uint256 collapserRepoTokenBalanceAfter = collapsingRepoToken.balanceOf(e.msg.sender); uint256 collapserRepoExposureAfter = getBorrowerRepurchaseObligation(e.msg.sender); uint256 totalOutstandingRepurchaseExposureAfter = totalOutstandingRepurchaseExposure(); assert collapserRepoTokenBalanceBefore >= collapserRepoTokenBalanceAfter; assert collapserRepoExposureBefore >= collapserRepoExposureAfter; assert totalOutstandingRepurchaseExposureBefore >= totalOutstandingRepurchaseExposureAfter; ``` 17. **Rule:** `burnCollapseExposureIntegrity` - ensures that burning for exposure collapse adjusts the repo token balance, repurchase obligation, and total outstanding repurchase exposure by the expected amounts, reflecting accurate and fair financial adjustments. ```solidity uint256 collapserRepoTokenBalanceBefore = collapsingRepoToken.balanceOf(e.msg.sender); uint256 collapserRepoExposureBefore = getBorrowerRepurchaseObligation(e.msg.sender); uint256 totalOutstandingRepurchaseExposureBefore = totalOutstandingRepurchaseExposure(); burnCollapseExposure(e, amount); uint256 collapserRepoTokenBalanceAfter = collapsingRepoToken.balanceOf(e.msg.sender); uint256 collapserRepoExposureAfter = getBorrowerRepurchaseObligation(e.msg.sender); uint256 totalOutstandingRepurchaseExposureAfter = totalOutstandingRepurchaseExposure(); assert collapserRepoTokenBalanceBefore - collapserRepoTokenBalanceAfter == expectedTokenBalanceDecrease; assert collapserRepoExposureBefore - collapserRepoExposureAfter == expectedObligationDecrease; assert totalOutstandingRepurchaseExposureBefore - totalOutstandingRepurchaseExposureAfter == expectedExposureDecrease; ``` 18. **Rule:** `burnCollapseExposureDoesNotAffectThirdParty` - confirms that an individual's action to burn repo tokens to collapse exposure does not impact the financial positions (token balances or repurchase obligations) of unrelated third parties, maintaining isolation of financial activities. ```solidity uint256 thirdPartyRepoTokenBalanceBefore = collapsingRepoToken.balanceOf(thirdParty); uint256 thirdPartyRepoExposureBefore = getBorrowerRepurchaseObligation(thirdParty); burnCollapseExposure(e, amount); uint256 thirdPartyRepoTokenBalanceAfter = collapsingRepoToken.balanceOf(thirdParty); uint256 thirdPartyRepoExposureAfter = getBorrowerRepurchaseObligation(thirdParty); assert thirdPartyRepoTokenBalanceBefore == thirdPartyRepoTokenBalanceAfter; assert thirdPartyRepoExposureBefore == thirdPartyRepoExposureAfter; ``` 19. **Rule:** `burnCollapseExposureRevertConditions`- check for revert under the defined expected conditions, ensuring operation adherence to defined rules. ```solidity bool payable = e.msg.value > 0; bool zeroAddressSender = e.msg.sender == 0; bool pastRepurchaseWindow = e.block.timestamp >= endOfRepurchaseWindow(); bool zeroBorrowerRepurchaseObligation = getBorrowerRepurchaseObligation(e.msg.sender) == 0; bool zeroMaxRepayment = maxRepayment == 0; bool servicerNotHaveRepoTokenBurnerRole = !collapsingRepoToken.hasRole(collapsingRepoToken.BURNER_ROLE(), currentContract); bool borrowerRepoTokenBalanceTooLow = (collapserRepoTokenBalanceBefore < collapseAmount && repaymentInTokens == collapseAmount) || (collapserRepoTokenBalanceBefore < maxRepaymentInRepoTokens && maxRepaymentInRepoTokens <= collapseAmount); bool repoTokenBurningPaused = collapsingRepoToken.burningPaused(); bool noServicerRoleOnCollateralManager = !collapsingCollateralManager.hasRole(collapsingCollateralManager.SERVICER_ROLE(), currentContract) && maxRepaymentInRepoTokens <= collapseAmount; bool collatManagerDoesNotHaveLockerServicerRole = !collapsingLocker.hasRole(collapsingLocker.SERVICER_ROLE(), collapsingCollateralManager) && maxRepaymentInRepoTokens <= collapseAmount && totalCollateral(e.msg.sender) > 0; bool lockerTransfersPaused = collapsingLocker.transfersPaused() && maxRepaymentInRepoTokens <= collapseAmount && totalCollateral(e.msg.sender) > 0; // Only in the case of full repayment bool termRepoUnbalanced = (totalOutstandingRepurchaseExposure() - repaymentInPurchaseToken + totalRepurchaseCollected() ) / (10 ^ 4) != (((((collapsingRepoToken.totalSupply() - repaymentInTokens) * expScale * collapsingRepoToken.redemptionValue()) / expScale ) / expScale) / 10 ^ 4); bool isExpectedToRevert = payable || zeroAddressSender || pastRepurchaseWindow || zeroBorrowerRepurchaseObligation || zeroMaxRepayment || servicerNotHaveRepoTokenBurnerRole || borrowerRepoTokenBalanceTooLow || repoTokenBurningPaused || noServicerRoleOnCollateralManager || collatManagerDoesNotHaveLockerServicerRole || lockerTransfersPaused || termRepoUnbalanced ; assert lastReverted <=> isExpectedToRevert; ``` 20. **Rule:** `mintOpenExposureMonotonicBehavior` - ensures that minting open exposure increases the minter's repo token balance, their repurchase obligation, and the total outstanding repurchase exposure, as well as the minter's collateral balance, indicating correct operation and accountability in minting activities. ```solidity uint256 minterRepoTokenBalanceBefore = mintingRepoToken.balanceOf(e.msg.sender); uint256 minterRepoExposureBefore = getBorrowerRepurchaseObligation(e.msg.sender); uint256 totalOutstandingRepurchaseExposureBefore = totalOutstandingRepurchaseExposure(); uint256 collateralBalanceBefore = mintingCollateralManager.getCollateralBalance(e.msg.sender, collateralTokenAddress); mintOpenExposure(e, amount, collateralAmounts); uint256 minterRepoTokenBalanceAfter = mintingRepoToken.balanceOf(e.msg.sender); uint256 minterRepoExposureAfter = getBorrowerRepurchaseObligation(e.msg.sender); uint256 totalOutstandingRepurchaseExposureAfter = totalOutstandingRepurchaseExposure(); uint256 collateralBalanceAfter = mintingCollateralManager.getCollateralBalance(e.msg.sender, collateralTokenAddress); assert minterRepoTokenBalanceBefore <= minterRepoTokenBalanceAfter; assert minterRepoExposureBefore <= minterRepoExposureAfter; assert totalOutstandingRepurchaseExposureBefore <= totalOutstandingRepurchaseExposureAfter; assert collateralBalanceBefore <= collateralBalanceAfter; ``` 21. **Rule:** `mintOpenExposureIntegrity` - confirms that minting for open exposure results in expected increases in the minter's repo token balance and repurchase obligation, as well as the total outstanding repurchase exposure, demonstrating the transaction's impact aligns with predefined financial mechanisms. ```solidity uint256 minterRepoTokenBalanceBefore = mintingRepoToken.balanceOf(e.msg.sender); uint256 minterRepoExposureBefore = getBorrowerRepurchaseObligation(e.msg.sender); uint256 totalOutstandingRepurchaseExposureBefore = totalOutstandingRepurchaseExposure(); mintOpenExposure(e, amount, collateralAmounts); uint256 minterRepoTokenBalanceAfter = mintingRepoToken.balanceOf(e.msg.sender); uint256 minterRepoExposureAfter = getBorrowerRepurchaseObligation(e.msg.sender); uint256 totalOutstandingRepurchaseExposureAfter = totalOutstandingRepurchaseExposure(); assert minterRepoTokenBalanceAfter - minterRepoTokenBalanceBefore == expectedIncrease; assert minterRepoExposureAfter - minterRepoExposureBefore == expectedIncrease; assert totalOutstandingRepurchaseExposureAfter - totalOutstandingRepurchaseExposureBefore == expectedIncrease; ``` 22. **Rule:** `mintOpenExposureDoesNotAffectThirdParty` - verifies that a minter's action to open exposure does not alter the repo token balances of unrelated third parties, ensuring the isolation of minting effects within the financial ecosystem. ```solidity uint256 thirdPartyBalanceBefore = mintingRepoToken.balanceOf(thirdParty); mintOpenExposure(e, amount, collateralAmounts); uint256 thirdPartyBalanceAfter = mintingRepoToken.balanceOf(thirdParty); assert thirdPartyBalanceBefore == thirdPartyBalanceAfter; ``` 23. **Rule:** `mintOpenExposureRevertConditions` - check for revert under the defined expected conditions, ensuring operation adherence to defined rules. ```solidity bool payable = e.msg.value > 0; bool callerNotSpecialist = !hasRole(SPECIALIST_ROLE(), e.msg.sender); bool noMinterRole = !mintingRepoToken.hasRole(mintingRepoToken.MINTER_ROLE(), currentContract); bool noServicerRoleToCollatManager = !mintingCollateralManager.hasRole(mintingCollateralManager.SERVICER_ROLE(), currentContract); bool borrowerNotEnoughCollateralBalance = mintingToken.balanceOf(e.msg.sender) < collateralAmounts[0]; bool lockerTransfersPaused = mintingLocker.transfersPaused(); bool noLockerServicerAccessForCollatManager = !mintingLocker.hasRole(locker.SERVICER_ROLE(), mintingCollateralManager); bool collateralAmountsNotProperLength = assert_uint8(collateralAmounts.length) != mintingCollateralManager.numOfAcceptedCollateralTokens(); bool afterMaturity = e.block.timestamp > maturityTimestamp(); bool noServicerRoleOnCollateralManager = !repaymentCollateralManager.hasRole(repaymentCollateralManager.SERVICER_ROLE(), currentContract); bool isExpectedToRevert = payable || callerNotSpecialist || noMinterRole || noServicerRoleToCollatManager || borrowerNotEnoughCollateralBalance || lockerTransfersPaused || noLockerServicerAccessForCollatManager || collateralAmountsNotProperLength || afterMaturity || noServicerRoleOnCollateralManager; mintOpenExposure@withrevert(e, amount, collateralAmounts); assert lastReverted <=> isExpectedToRevert; ``` 24. **Rule:** `redemptionsMonotonicBehavior` - verifies that redemption operations result in expected changes to the balances and obligations involved, ensuring that the redeemer's repo token balance decreases, their purchase token balance increases, and the overall repurchase obligations and available tokens within the locker adjust accordingly. ```solidity uint256 redeemerRepoTokenBalanceBefore = repoTokenRedempt.balanceOf(redeemer); uint256 totalRepurchaseCollectedBefore = totalRepurchaseCollected(); uint256 redeemerPurchaseTokenBalanceBefore = tokenRedempt.balanceOf(redeemer); uint256 lockerPurchaseTokenBalanceBefore = tokenRedempt.balanceOf(lockerRedempt); redeemTermRepoTokens(e, redeemer, amount); uint256 redeemerRepoTokenBalanceAfter = repoTokenRedempt.balanceOf(redeemer); uint256 totalRepurchaseCollectedAfter = totalRepurchaseCollected(); uint256 redeemerPurchaseTokenBalanceAfter = tokenRedempt.balanceOf(redeemer); uint256 lockerPurchaseTokenBalanceAfter = tokenRedempt.balanceOf(lockerRedempt); assert redeemerRepoTokenBalanceBefore >= redeemerRepoTokenBalanceAfter; assert totalRepurchaseCollectedBefore >= totalRepurchaseCollectedAfter; assert redeemerPurchaseTokenBalanceBefore <= redeemerPurchaseTokenBalanceAfter; assert lockerPurchaseTokenBalanceBefore >= lockerPurchaseTokenBalanceAfter; ``` 25. **Rule:** `redemptionsIntegrity` - confirms that the redemption of repo tokens by a redeemer leads to the precise adjustments in the total repurchase collected, the repo token balance of the redeemer, and the purchase token balance in accordance with the redemption value and terms defined, reflecting the accurate financial transaction and impact. ```solidity uint256 redeemerRepoTokenBalanceBefore = repoTokenRedempt.balanceOf(redeemer); uint256 totalRepurchaseCollectedBefore = totalRepurchaseCollected(); uint256 redeemerPurchaseTokenBalanceBefore = tokenRedempt.balanceOf(redeemer); uint256 lockerPurchaseTokenBalanceBefore = tokenRedempt.balanceOf(lockerRedempt); redeemTermRepoTokens(e, redeemer, amount); uint256 redeemerRepoTokenBalanceAfter = repoTokenRedempt.balanceOf(redeemer); uint256 totalRepurchaseCollectedAfter = totalRepurchaseCollected(); uint256 redeemerPurchaseTokenBalanceAfter = tokenRedempt.balanceOf(redeemer); uint256 lockerPurchaseTokenBalanceAfter = tokenRedempt.balanceOf(lockerRedempt); assert redeemerRepoTokenBalanceBefore - amount == redeemerRepoTokenBalanceAfter; assert totalRepurchaseCollectedBefore - expectedRedemption == totalRepurchaseCollectedAfter; assert redeemerPurchaseTokenBalanceAfter - expectedRedemption == redeemerPurchaseTokenBalanceBefore; assert lockerPurchaseTokenBalanceBefore - expectedRedemption == lockerPurchaseTokenBalanceAfter; ``` 26. **Rule:** `redemptionsDoesNotAffectThirdParty` - ensures that a redemption action taken by one participant does not inadvertently alter the financial position or balances of unrelated third parties, maintaining the integrity and isolation of individual transactions within the ecosystem. ```solidity uint256 thirdPartyRepoTokenBalanceBefore = repoTokenRedempt.balanceOf(thirdParty); uint256 thirdPartyPurchaseTokenBalanceBefore = tokenRedempt.balanceOf(thirdParty); redeemTermRepoTokens(e, redeemer, amount); uint256 thirdPartyRepoTokenBalanceAfter = repoTokenRedempt.balanceOf(thirdParty); uint256 thirdPartyPurchaseTokenBalanceAfter = tokenRedempt.balanceOf(thirdParty); assert thirdPartyRepoTokenBalanceBefore == thirdPartyRepoTokenBalanceAfter; assert thirdPartyPurchaseTokenBalanceBefore == thirdPartyPurchaseTokenBalanceAfter; ``` 27. **Rule:** `redemptionsRevertConditions` - evaluates whether the operation correctly reverts under the prescribed conditions, ensuring compliance with defined contractual behaviors and protections. ```solidity bool payable = e.msg.value > 0; bool zeroAddress = redeemer == 0; bool beforeRedemption = e.block.timestamp <= redemptionTimestamp(); bool zeroRepoTokens = repoTokenRedempt.balanceOf(redeemer) == 0; bool encumberedCollateralRemaining = collateralManagerRedempt.encumberedCollateralRemaining() && (repoTokenRedempt.totalRedemptionValue() > assert_uint256(totalRepurchaseCollected() + 10 ^ 4)); bool servicerNotHaveRepoTokenBurnerRole = !repoTokenRedempt.hasRole(repoTokenRedempt.BURNER_ROLE(), currentContract); bool repoTokenBurningPaused = repoTokenRedempt.burningPaused(); bool noServicerAccessToLocker = !lockerRedempt.hasRole(lockerRedempt.SERVICER_ROLE(), currentContract); bool lockerTransfersPaused = lockerRedempt.transfersPaused(); bool notEnoughRepoTokens = repoTokenRedempt.balanceOf(redeemer) < amount; bool termRepoUnbalanced = (termRepoUnbalancedLeftSide) / (10 ^ 4) != (totalRedemptionValueExpected / 10 ^ 4); bool isExpectedToRevert = payable || zeroAddress || beforeRedemption || zeroRepoTokens || encumberedCollateralRemaining || servicerNotHaveRepoTokenBurnerRole || repoTokenBurningPaused || lockerTransfersPaused || noServicerAccessToLocker || notEnoughRepoTokens || termRepoUnbalanced; redeemTermRepoTokens@withrevert(e, redeemer, amount); assert lastReverted <=> isExpectedToRevert; ``` 28. **Rule:** `repaymentsMonotonicBehavior` - validates that repayments lead to expected monotonic changes in borrower obligations and system totals, ensuring borrower balances and overall repurchase exposures decrease as payments are made, while the total repurchase collected and potentially the collateral values adjust accordingly. ```solidity uint256 borrowerBalanceBefore = getBorrowerRepurchaseObligation(borrower); uint256 totalOutstandingRepurchaseExposureBefore = totalOutstandingRepurchaseExposure(); uint256 totalRepurchaseCollectedBefore = totalRepurchaseCollected(); uint256 borrowerCollateralBefore = totalCollateral(borrower); submitRepurchasePayment(e, repayment); uint256 borrowerBalanceAfter = getBorrowerRepurchaseObligation(borrower); uint256 totalOutstandingRepurchaseExposureAfter = totalOutstandingRepurchaseExposure(); uint256 totalRepurchaseCollectedAfter = totalRepurchaseCollected(); uint256 borrowerCollateralAfter = totalCollateral(borrower); assert borrowerBalanceBefore >= borrowerBalanceAfter; assert totalOutstandingRepurchaseExposureBefore >= totalOutstandingRepurchaseExposureAfter; assert totalRepurchaseCollectedBefore <= totalRepurchaseCollectedAfter; assert borrowerCollateralAfter <= borrowerCollateralBefore; ``` 29. **Rule:** `repaymentsIntegrity` - ensures the integrity of repayments by verifying that the repayments correctly decrease the borrower's obligations and appropriately adjust the system's repurchase exposure and collected totals, with specific attention to the treatment of collateral in the event of complete repayment. ```solidity uint256 borrowerBalanceBefore = getBorrowerRepurchaseObligation(borrower); uint256 totalOutstandingRepurchaseExposureBefore = totalOutstandingRepurchaseExposure(); uint256 totalRepurchaseCollectedBefore = totalRepurchaseCollected(); submitRepurchasePayment(e, repayment); uint256 borrowerBalanceAfter = getBorrowerRepurchaseObligation(borrower); uint256 totalOutstandingRepurchaseExposureAfter = totalOutstandingRepurchaseExposure(); uint256 totalRepurchaseCollectedAfter = totalRepurchaseCollected(); assert borrowerBalanceBefore - repayment == borrowerBalanceAfter; assert totalOutstandingRepurchaseExposureBefore - repayment == totalOutstandingRepurchaseExposureAfter; assert totalRepurchaseCollectedBefore + repayment == totalRepurchaseCollectedAfter; assert borrowerBalanceAfter == 0 ? totalCollateral(borrower) == 0 : totalCollateral(borrower) remains unchanged; ``` 30. **Rule:** `repaymentsDoesNotAffectThirdParty` - confirms that a borrower's repayment activity does not inadvertently affect the financial obligations or collateral standings of any unrelated third parties, preserving the isolation and accuracy of individual account statuses within the system. ```solidity uint256 thirdPartyObligationBefore = getBorrowerRepurchaseObligation(thirdParty); submitRepurchasePayment(e, repayment); uint256 thirdPartyObligationAfter = getBorrowerRepurchaseObligation(thirdParty); assert thirdPartyObligationBefore == thirdPartyObligationAfter; ``` 31. **Rule:** `repaymentsRevertingConditions` - check if the operation correctly reverts under specified conditions, ensuring adherence to defined contractual behaviors and safeguards. ```solidity bool payable = e.msg.value > 0; bool lockerTransfersPaused = locker.transfersPaused(); bool noLockerServicerAccess = !locker.hasRole(locker.SERVICER_ROLE(), currentContract); bool allowanceTooLow = token.allowance( borrower, termRepoLocker()) < repayment; bool borrowTokenBalanceTooLow = token.balanceOf(borrower) < repayment; bool afterRepurchaseWindow = e.block.timestamp >= endOfRepurchaseWindow(); bool borrowerZeroObligation = getBorrowerRepurchaseObligation(borrower) == 0; bool uintMaxRepayment = repayment == max_uint256; bool repaymentGreaterThanMax = repaymentAmount > maxRepayment; bool noServicerRoleOnCollateralManager = !repaymentCollateralManager.hasRole(repaymentCollateralManager.SERVICER_ROLE(), currentContract); bool isExpectedToRevert = payable || lockerTransfersPaused || noLockerServicerAccess || borrowTokenBalanceTooLow || allowanceTooLow || afterRepurchaseWindow || borrowerZeroObligation || uintMaxRepayment || repaymentGreaterThanMax || noServicerRoleOnCollateralManager; submitRepurchasePayment@withrevert(e, repayment); assert lastReverted <=> isExpectedToRevert; ``` 32. **Rule:** `liquidatorCoverExposureIntegrity` - validates the integrity of a liquidation process where a liquidator covers the exposure of a borrower using purchase tokens. It checks that balances and obligations adjust correctly, reflecting the liquidation payment in system totals and individual accounts. ```solidity uint256 borrowerObligationBefore = getBorrowerRepurchaseObligation(borrower); uint256 totalOutstandingBefore = totalOutstandingRepurchaseExposure(); uint256 totalCollectedBefore = totalRepurchaseCollected(); uint256 liquidatorBalanceBefore = liquidationRepaymentExposureToken.balanceOf(liquidator); uint256 lockerBalanceBefore = liquidationRepaymentExposureToken.balanceOf(termRepoLocker()); liquidatorCoverExposure(e, borrower, liquidator, amountToCover); uint256 borrowerObligationAfter = getBorrowerRepurchaseObligation(borrower); uint256 totalOutstandingAfter = totalOutstandingRepurchaseExposure(); uint256 totalCollectedAfter = totalRepurchaseCollected(); uint256 liquidatorBalanceAfter = liquidationRepaymentExposureToken.balanceOf(liquidator); uint256 lockerBalanceAfter = liquidationRepaymentExposureToken.balanceOf(termRepoLocker()); assert borrowerObligationBefore - borrowerObligationAfter == amountToCover; assert totalOutstandingBefore - totalOutstandingAfter == amountToCover; assert totalCollectedAfter - totalCollectedBefore == amountToCover; assert liquidatorBalanceBefore - liquidatorBalanceAfter == amountToCover; assert lockerBalanceAfter - lockerBalanceBefore == amountToCover; ``` 33. **Rule:** `liquidatorCoverExposureDoesNotAffectThirdParty` - ensures that the liquidation process does not inadvertently impact the financial status or obligations of any third parties, maintaining the precision and isolation of account transactions within the system. ```solidity uint256 thirdPartyObligationBefore = getBorrowerRepurchaseObligation(thirdParty); uint256 thirdPartyBalanceBefore = liquidationRepaymentExposureToken.balanceOf(thirdParty); liquidatorCoverExposure(e, borrower, liquidator, amountToCover); uint256 thirdPartyObligationAfter = getBorrowerRepurchaseObligation(thirdParty); uint256 thirdPartyBalanceAfter = liquidationRepaymentExposureToken.balanceOf(thirdParty); assert thirdPartyObligationBefore == thirdPartyObligationAfter; assert thirdPartyBalanceBefore == thirdPartyBalanceAfter; ``` 34. **Rule:** `liquidatorCoverExposureRevertConditions` - evaluate if the transaction reverts as expected under identified conditions, ensuring compliance with system rules and safeguards. ```solidity bool payable = e.msg.value > 0; bool callerNotCollateralManager = !hasRole(COLLATERAL_MANAGER(), e.msg.sender); bool servicerDoesNotHaveLockerServicerRole = !liquidationRepaymentExposureLocker.hasRole(liquidationRepaymentExposureLocker.SERVICER_ROLE(), currentContract); bool lockerTransfersPaused = liquidationRepaymentExposureLocker.transfersPaused(); bool allowanceTooLow = liquidationRepaymentExposureToken.allowance( liquidator, termRepoLocker()) < amountToCover; bool liquidatorTokenBalanceTooLow = liquidationRepaymentExposureToken.balanceOf(liquidator) < amountToCover; bool borrowBalancecLowerThanCoverAmount = getBorrowerRepurchaseObligation(borrower) < amountToCover; bool isExpectedToRevert = payable || callerNotCollateralManager || servicerDoesNotHaveLockerServicerRole || lockerTransfersPaused || liquidatorTokenBalanceTooLow || allowanceTooLow || borrowBalancecLowerThanCoverAmount ; liquidatorCoverExposure@withrevert(e, borrower, liquidator, amountToCover); assert lastReverted <=> isExpectedToRevert; ``` 35. **Rule:** `liquidatorCoverExposureWithRepoTokenIntegrity` - examines the proper functioning of liquidation via repo tokens, verifying that such transactions correctly reduce borrower obligations and adjust system and participant balances in accordance with the repo tokens used in the liquidation. ```solidity uint256 borrowerObligationBefore = getBorrowerRepurchaseObligation(borrower); uint256 totalOutstandingBefore = totalOutstandingRepurchaseExposure(); uint256 liquidatorRepoBalanceBefore = liquidationRepaymentExposureRepoToken.balanceOf(liquidator); uint256 repoTotalSupplyBefore = liquidationRepaymentExposureRepoToken.totalSupply(); liquidatorCoverExposureWithRepoToken(e, borrower, liquidator, amountOfRepoToken); uint256 borrowerObligationAfter = getBorrowerRepurchaseObligation(borrower); uint256 totalOutstandingAfter = totalOutstandingRepurchaseExposure(); uint256 liquidatorRepoBalanceAfter = liquidationRepaymentExposureRepoToken.balanceOf(liquidator); uint256 repoTotalSupplyAfter = liquidationRepaymentExposureRepoToken.totalSupply(); assert borrowerObligationBefore - borrowerObligationAfter == calculatedAmountCovered; assert totalOutstandingBefore - totalOutstandingAfter == calculatedAmountCovered; assert liquidatorRepoBalanceBefore - liquidatorRepoBalanceAfter == amountOfRepoToken; assert repoTotalSupplyBefore - repoTotalSupplyAfter == amountOfRepoToken; ``` 36. **Rule:** `liquidatorCoverExposureWithRepoTokenRevertConditions` - define conditions that would lead to a transaction revert; aggregate revert conditions to determine expectation; eliquidation attempt with potential revert and validate against expected outcome; ensure actual revert aligns with expectations based on identified conditions. ```solidity bool payable = e.msg.value > 0; bool callerNotCollateralManager = !hasRole(COLLATERAL_MANAGER(), e.msg.sender); bool liquidatorIsAddressZero = liquidator == 0; bool servicerNotHaveRepoTokenBurnerRole = !liquidationRepaymentExposureRepoToken.hasRole(liquidationRepaymentExposureRepoToken.BURNER_ROLE(), currentContract); bool liquidatorTokenBalanceTooLow = liquidationRepaymentExposureRepoToken.balanceOf(liquidator) < amountOfRepoToken; bool repoTokenBurningPaused = liquidationRepaymentExposureRepoToken.burningPaused(); bool termPoolBalanceThresholdBreached = ((totalOutstandingRepurchaseExposure() - amountToCover + totalRepurchaseCollected()) / 10^4) != (((((liquidationRepaymentExposureRepoToken.totalSupply() - amountOfRepoToken) * expScale * liquidationRepaymentExposureRepoToken.redemptionValue()) / expScale) / expScale) / 10^4); bool borrowBalanceLowerThanCoverAmount = borrowerObligationBefore < amountToCover; // Aggregate revert conditions to determine expectation isExpectedToRevert = payable || callerNotCollateralManager || liquidatorIsAddressZero || servicerNotHaveRepoTokenBurnerRole || liquidatorTokenBalanceTooLow || repoTokenBurningPaused || termPoolBalanceThresholdBreached || borrowBalanceLowerThanCoverAmount; // Execute liquidation attempt with potential revert and validate against expected outcome liquidatorCoverExposureWithRepoToken@withrevert(e, borrower, liquidator, amountOfRepoToken); assert lastReverted <=> isExpectedToRevert; // Ensure actual revert aligns with expectations based on identified conditions ``` 37. **Rule:** `openExposureOnRolloverNewIntegrity` - ensures that all relevant balances properly accounted for after opening a repoExposure on account of a successful rollover. ```solidity assert balanceAfter == balanceBefore + repurchasePrice; assert totalOutstandingRepurchaseExposureAfter == totalOutstandingRepurchaseExposureBefore + repurchasePrice; assert tokenBalanceTermRepoLockerAfter + purchasePrice == tokenBalanceTermRepoLockerBefore; assert tokenBalancePreviousTermRepoLockerAfter == tokenBalancePreviousTermRepoLockerBefore + previousRepoLockerRepayment; assert tokenBalanceTreasuryAfter == tokenBalanceTreasuryBefore + protocolShare; ``` 38. **Rule:** `openExposureOnRolloverNewDoesNotAffectThirdParty` - verifies that rolling over loan exposures from one account does not affect third-party balances. ```solidity mathint balanceBefore = getBorrowerRepurchaseObligation(borrower2); openExposureOnRolloverNew(e, borrower, purchasePrice, repurchasePrice, previousTermRepoLocker, dayCountFractionMantissa); mathint balanceAfter = getBorrowerRepurchaseObligation(borrower2); assert balanceAfter == balanceBefore; ``` 39. **Rule:** `openExposureOnRolloverNewRevertConditions`- check for revert under the defined expected conditions, ensuring operation adherence to defined rules. ```solidity bool payable = e.msg.value > 0; bool callerNotAuctioneer = !hasRole(AUCTIONEER(), e.msg.sender); bool afterMaturity = e.block.timestamp >= maturityTimestamp(); bool lockerTransfersPaused = rolloverExposureLocker.transfersPaused(); bool servicerNoLockerAccess = !rolloverExposureLocker.hasRole(rolloverExposureLocker.SERVICER_ROLE(), currentContract); bool lockerTokenBalanceTooLow = rolloverExposureToken.balanceOf(rolloverExposureLocker) < purchasePrice; bool isExpectedToRevert = payable || callerNotAuctioneer || afterMaturity || lockerTransfersPaused || servicerNoLockerAccess || lockerTokenBalanceTooLow; openExposureOnRolloverNew@withrevert(e, borrower, purchasePrice, repurchasePrice, previousTermRepoLocker, dayCountFractionMantissa); assert lastReverted <=> isExpectedToRevert; ``` 40. **Rule:** `closeExposureOnRolloverExistingIntegrity` - ensures that all relevant balances properly accounted for after closing a repoExposure on account of a successful rollover. ```solidity assert balanceBefore == balanceAfter + actualRolloverSettlementAmount; assert totalOutstandingRepurchaseExposureBefore == totalOutstandingRepurchaseExposureAfter + actualRolloverSettlementAmount; assert amountCollectedAfter == amountCollectedBefore + actualRolloverSettlementAmount; assert rolloverExposureRolloverManager.getRolloverInstructions(borrower).processed; ``` 41. **Rule:** `closeExposureOnRolloverExistingDoesNotAffectThirdParty` - verifies that rolling over loan exposures from one account does not affect third-party balances. ```solidity mathint balanceBefore = getBorrowerRepurchaseObligation(borrower2); closeExposureOnRolloverExisting(e, borrower, rolloverSettlementAmount); mathint balanceAfter = getBorrowerRepurchaseObligation(borrower2); assert balanceBefore == balanceAfter; ``` 42. **Rule:** `closeExposureOnRolloverExistingRevertConditions`- check for revert under the defined expected conditions, ensuring operation adherence to defined rules. ```solidity 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; ``` 43. **Rule:** `fulfillOfferIntegrity` - ensures repoTokens are properly minted to a user's address when their offer is fulfilled. ```solidity assert offerorRepoTokenBalanceAfter == offerorRepoTokenBalanceBefore + tokensMinted, ``` 44. **Rule:** `fulfillBidIntegrity` - check that the bidder's token balance has decreased and protocol's token balance has increased after `fulfillBid`. ```solidity // 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 ``` 45. **Rule:** `fulfillOfferRevertsIfNotValid` - ensure that `fulfillOffer` reverts if not valid. ```solidity 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"; ``` 46. **Rule:** `fulfillBidRevertsIfNotValid` - ensure that `fulfillBid` reverts if not valid. ```solidity 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"; ``` 47. **Rule:** `fulfillOfferDoesNotAffectThirdParty` - verifies that fulfilling an offer belonging to one account does not affect the third party balances. ```solidity assert thirdPartyRepoTokenBalanceBefore == thirdPartyRepoTokenBalanceAfter ``` 48. **Rule:** `fulfillBidDoesNotAffectThirdParty` - verifies that fulfilling a bid belonging to from one account does not affect the third party balances. ```solidity assert thirdPartyTokenBalanceBefore == thirdPartyTokenBalanceAfter ``` 49. **Rule:** `lockOfferAmountIntegrity` - ensures purchase tokens are properly deducted from a user's address when they lock an offer. ```solidity assert offerorPurchaseTokenBalanceAfter == offerorPurchaseTokenBalanceBefore - to_mathint(amount) ``` 50. **Rule:** `unlockOfferAmountIntegrity` - ensures purchase tokens are properly transferred to a user's address when they unlock an offer. ```solidity assert offerorPurchaseTokenBalanceAfter == offerorPurchaseTokenBalanceBefore + to_mathint(amount) ``` 51. **Rule:** `lockOfferAmountDoesNotAffectThirdParty` - verifies that locking an offer belonging to one account does not affect the third party balances. ```solidity assert thirdPartyPurchaseTokenBalanceBefore == thirdPartyPurchaseTokenBalanceAfter ``` 52. **Rule:** `unlockOfferAmountDoesNotAffectThirdParty` - verifies that unlocking an offer belonging to one account does not affect the third party balances.. ```solidity assert thirdPartyPurchaseTokenBalanceBefore == thirdPartyPurchaseTokenBalanceAfter ``` 53. **Rule:** `lockOfferAmountRevertsWhenInvalid` - ensure that locking offers reverts if not valid ```solidity 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 ``` 54. **Rule:** `unlockOfferAmountRevertsWhenInvalid` - ensure that unlocking offers reverts if not valid ```solidity 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 ``` 55. **Rule:** `onlyRoleCanCallRevert` - checks if a method call requires specific roles to execute successfully, does not revert if the caller has the necessary role. ```solidity 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); ``` 56. **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. ```solidity 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` ```solidity assert bidderCollateralBalanceAfter == bidderCollateralBalanceBefore; assert encumberedCollateralBalanceAfter == encumberedCollateralBalanceBefore; assert bidderCollateralTokenBalanceAfter + amount == bidderCollateralTokenBalanceBefore; assert lockerCollateralBalanceBefore + amount == lockerCollateralBalanceAfter; ``` 2. **Rule:** `auctionLockCollateralThirdParty` - verifies that locking collateral belonging to one account when calling `lockBid` does not affect the third party balances ```solidity assert thirdPartyBidderCollateralBalanceAfter == thirdPartyBidderCollateralBalanceBefore; assert thirdPartyBidderCollateralTokenBalanceAfter == thirdPartyBidderCollateralTokenBalanceBefore; ``` 3. **Rule:** `auctionLockCollateralRevertConditions`- check for revert under the defined expected conditions, ensuring operation adherence to defined rules. ```solidity 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; ``` 4. **Rule:** `auctionUnlockCollateralIntegrity` - ensures that all relevant balances are properly reflected on account of locking collateral when calling `auctionUnlockCollateral` ```solidity assert bidderCollateralBalanceAfter == bidderCollateralBalanceBefore; assert encumberedCollateralBalanceAfter == encumberedCollateralBalanceBefore; assert bidderCollateralTokenBalanceAfter == bidderCollateralTokenBalanceBefore + amount; assert lockerCollateralBalanceBefore == lockerCollateralBalanceAfter + amount; ``` 5. **Rule:** `auctionUnlockCollateralThirdParty` - verifies that unlocking collateral belonging to one account when calling `auctionUnlockCollateral` does not affect the third party balances ```solidity assert thirdPartyBidderCollateralBalanceAfter == thirdPartyBidderCollateralBalanceBefore; assert thirdPartyBidderCollateralTokenBalanceAfter == thirdPartyBidderCollateralTokenBalanceBefore; ``` 6. **Rule:** `auctionUnlockCollateralRevertConditions`- check for revert under the defined expected conditions, ensuring operation adherence to defined rules. ```solidity 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; ``` 7. **Rule:** `journalBidCollateralToCollateralManagerIntegrity` - ensures that all relevant balances are properly reflected on account of locking collateral when fulfilling a bid. ```solidity assert bidderCollateralBalanceAfter == require_uint256(bidderCollateralBalanceBefore + amount); assert encumberedCollateralBalanceAfter == encumberedCollateralBalanceBefore + amount; assert bidderCollateralTokenBalanceAfter == bidderCollateralTokenBalanceBefore; assert lockerCollateralBalanceBefore == lockerCollateralBalanceAfter; ``` 8. **Rule:** `journalBidCollateralToCollateralManagerThirdParty` - verifies that journaling collateral to the `lockedCollateralLedger` when fulfilling a bid belonging to one account does not affect the third party balances. ```solidity assert bidderCollateralBalanceAfter == bidderCollateralBalanceBefore; assert bidderCollateralTokenBalanceAfter == bidderCollateralTokenBalanceBefore; ``` 9. **Rule:** `journalBidCollateralToCollateralManagerRevertConditions`- check for revert under the defined expected conditions, ensuring operation adherence to defined rules. ```solidity bool payable = e.msg.value > 0; bool notServicerRole = !hasRole(SERVICER_ROLE(), e.msg.sender); bool isExpectedToRevert = payable || notServicerRole; assert lastReverted <=> isExpectedToRevert; ``` 10. **Rule:** `externalLockCollateralIntegrity` - ensures that all relevant balances are properly reflected on account of locking collateral when calling `externalLockCollateral`. ```solidity assert borrowerCollateralBalanceAfter == borrowerCollateralBalanceBefore + amount; assert encumberedCollateralBalanceAfter == encumberedCollateralBalanceBefore + amount; assert borrowerCollateralTokenBalanceAfter + amount == borrowerCollateralTokenBalanceBefore; assert lockerCollateralBalanceBefore + amount == lockerCollateralBalanceAfter; ``` 11. **Rule:** `externalLockCollateralThirdParty` - verifies that locking collateral belonging to one account when calling `externalLockCollateral` does not affect the third party balances ```solidity assert thirdPartyBorrowerCollateralBalanceAfter == thirdPartyBorrowerCollateralBalanceBefore; assert thirdPartyBorrowerCollateralTokenBalanceAfter == thirdPartyBorrowerCollateralTokenBalanceBefore; ``` 12. **Rule:** `externalLockCollateralRevertConditions`- check for revert under the defined expected conditions, ensuring operation adherence to defined rules. ```solidity 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); ``` 13. **Rule:** `externalUnlockCollateralIntegrity` - ensures that all relevant balances are properly reflected on account of locking collateral when calling `externalUnlockCollateral`. ```solidity 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; ``` 14. **Rule:** `externalUnlockCollateralThirdParty` - verifies that unlocking collateral belonging to one account when calling `externalUnlockCollateral`does not affect the third party balances ```solidity assert thirdPartyBorrowerCollateralBalanceAfter == thirdPartyBorrowerCollateralBalanceBefore; assert thirdPartyBorrowerCollateralTokenBalanceAfter == thirdPartyBorrowerCollateralTokenBalanceBefore; ``` 15. **Rule:** `externalUnlockCollateralRevertConditions`- check for revert under the defined expected conditions, ensuring operation adherence to defined rules. ```solidity 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); ``` 16. **Rule:** `lockerCollateralTokenBalanceGreaterThanCollateralLedgerBalance` - verifies the assumption that total collateral token balances is always less than or equal to the balance recorded in ledger ```solidity assert sumOfCollateralBalances <= to_mathint((stateToken.balanceOf(stateLocker))); ``` 17. **Rule:** `onlyAllowedMethodsMayChangeEncumberedCollateralBalances` - verifies that changes to the balances of encumbered collateral to specific methods, ensuring that such modifications are controlled and intentional. ```solidity assert encumberedCollateralBalanceAfter > encumberedCollateralBalanceBefore => canIncreaseEncumberedCollateralBalances(f); assert encumberedCollateralBalanceAfter < encumberedCollateralBalanceBefore => canDecreaseEncumberedCollateralBalances(f); ``` 18. **Rule:** `encumberedCollateralBalancesNeverOverflows` - ensure that `encumberedCollateralBalances` never overflows ```solidity assert encumberedCollateralBalanceBefore <= encumberedCollateralBalanceAfter; ``` 19. **Rule:** `noMethodsChangeTermRepoId` - verifies that termRepoIds are immutable. ```solidity assert termRepoIdBefore == termRepoIdAfter; ``` 20. **Rule:** `noMethodsChangeNumOfAcceptedCollateralTokens` - verifies that the number of accepted collateral tokens are immutable. ```solidity assert numOfAcceptedCollateralTokensBefore == numOfAcceptedCollateralTokensAfter; ``` 21. **Rule:** `noMethodsChangeDeMinimisMarginThreshold` - verifies that the `deminimisMarginThreshold` is immutable. ```solidity assert deMinimisMarginThresholdBefore == deMinimisMarginThresholdAfter; ``` 22. **Rule:** `noMethodsChangeLiquidateDamagesDueToProtocol` - verifies that the liquidated damages due to protocol is immutable. ```solidity assert liquidateDamagesDueToProtocolBefore == liquidateDamagesDueToProtocolAfter; ``` 23. **Rule:** `noMethodsChangeNetExposureCapOnLiquidation` - verifies that the `netExposureCapOnLiquidation` parameter of a termRepo is immutable. ```solidity assert netExposureCapOnLiquidationBefore == netExposureCapOnLiquidationAfter; ``` 24. **Rule:** `noMethodsChangePurchaseToken` - verifies that the purchaseToken associated with a termRepo is immutable. ```solidity assert purchaseTokenBefore == purchaseTokenAfter; ``` 25. **Rule:** `onlyAllowedMethodsChangeTermContracts` - verifies that changes to term contracts addresses are restricted to certain allowed methods. ```solidity assert servicerBefore == servicerAfter; assert oracleBefore == oracleAfter; assert lockerBefore == lockerAfter; assert controllerBefore == controllerAfter; assert emitterBefore == emitterAfter; ``` 26. **Rule:** `noMethodsChangeMaintenanceCollateralRatios` - verifies that maintenance collateral ratios associated with a termRepo are immutable. ```solidity assert maintenanceCollateralRatioBefore == maintenanceCollateralRatioAfter; ``` 27. **Rule:** `noMethodsChangeInitialCollateralRatios` - verifies that initial collateral ratios associated with a termRepo are immutable. ```solidity assert initialCollateralRatioBefore == initialCollateralRatioAfter; ``` 28. **Rule:** `noMethodsChangeLiquidatedDamages` - verifies that liquidated damages associated with a termRepo are immutable. ```solidity assert liquidatedDamagesBefore == liquidatedDamagesAfter; ``` 29. **Rule:** `onlyAllowedMethodsChangeLockedCollateralLedger` - verifies that changes t othe collateral ledger is restricted to certain approved methods. ```solidity assert lockedCollateralLedgerBefore == lockedCollateralLedgerAfter; ``` 30. **Rule:** `sumOfCollateralBalancesLessThanEncumberedBalances` - verifes the assumption that the total sum of all collateral balances is always less than the encumbered collateral balance. ```solidity mathint encumberedCollateralBalanceAfter = encumberedCollateralBalance(stateToken); mathint sumOfCollateralBalancesAfter = sumOfCollateralBalances; assert sumOfCollateralBalancesAfter <= encumberedCollateralBalanceAfter; ``` 31. **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` ```solidity // 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); ``` 32. **Rule:** `batchLiquidateWithRepoTokenSuccessfullyLiquidates` - assert that the locker's balances, liquidators balances and protocol reserve blances have changed by the correct amount after calling `batchLiquidatedWithRepoToken` ```solidity // 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); } ``` 33. **Rule:** `batchDefaultSuccessfullyDefaults` - assert that the locker's balances, liquidator's balances and protocol reserve balances have changed by the correct amount after calling`batchDefault` ```solidity // 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); ``` 34. **Rule:** `batchLiquidationDoesNotAffectThirdParty` - verifies that liquidating collateral belonging to one account does not affect the third party balances. ```solidity batchLiquidation(e, borrower, [closureAmount]); assert(otherBorrowerRepurchaseObligationBefore == otherBorrowerRepurchaseObligationAfter); assert(otherBorrowerCollateralBalanceBefore == otherBorrowerCollateralBalanceAfter); ``` 35. Rule: `batchLiquidationWithRepoTokenDoesNotAffectThirdParty` - verifies that liquidating collateral using `batchLiquidationWithRepoToken` belonging to one account does not affect the third party balances. ```solidity batchLiquidationWithRepoToken(e, borrower, [closureAmount]); assert(otherBorrowerRepurchaseObligationBefore == otherBorrowerRepurchaseObligationAfter); assert(otherBorrowerCollateralBalanceBefore == otherBorrowerCollateralBalanceAfter); ``` 36. `Rule: batchDefaultDoesNotAffectThirdParty` - verifies that liquidating collateral belonging to one account when calling `batchDefault` does not affect the third party balances. ```solidity batchDefault(e, borrower, [closureAmount]); assert(otherBorrowerRepurchaseObligationBefore == otherBorrowerRepurchaseObligationAfter); assert(otherBorrowerCollateralBalanceBefore == otherBorrowerCollateralBalanceAfter); ``` 37. **Rule:** `batchLiquidationRevertsIfInvalid` - ensures that `batchLiquidate` reverts if not valid. ```solidity 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"; ``` 38. **Rule:** `batchLiquidationWithRepoTokenRevertsIfInvalid` - ensure that `batchLiquidateWithRepoToken` reverts if not valid. ```solidity 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"; ``` 39. **Rule:** `batchDefaultRevertsIfInvalid` - ensure that `batchDefault` reverts if not valid. ```solidity 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 || ``` 40. **Rule:** `onlyRoleCanCallRevert` - checks if a method call requires specific roles to execute successfully, does not revert if the caller has the necessary role. ```solidity 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); ``` 41. **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. ```solidity 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. ```solidity 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"; } ``` 2. **Rule:** `onlyAllowedMethodsChangeTermContracts` - verifies that changes to term contracts addresses are restricted to certain allowed methods. ```solidity // 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"; } ``` 3. **Rule:** `onlyAllowedMethodsChangeApprovedRolloverAuctionBidLockers` - verifies that changes to approved rollover contracts are restricted to certain allowed methods. ```solidity // 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"; } ``` 4. **Rule:** `onlyAllowedMethodsChangeRolloverElections` - verifies that changes to rollover elections are restricted to certain allowed methods. ```solidity // 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 ``` 5. **Rule:** `electRolloverIntegrity` - ensures that all relevant balances are properly reflected when electing to roll-over a loan. ```solidity 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. } ``` 6. **Rule:** `electRolloverDoesNotAffectThirdParty` - verifies that the action of one account electing to roll over their loan does not impact third-party balances. ```solidity 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; ``` 7. **Rule:** `electRolloverRevertConditions`- check for revert under the defined expected conditions, ensuring operation adherence to defined rules. ```solidity 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; ``` 8. **Rule:** `cancelRolloverIntegrity` - ensures that all relevant balances are properly reflected when cancelling a roll-over election. ```solidity assert rolloverAmount == 0; assert rolloverBidPriceHash == to_bytes32(0); assert rolloverAuctionBidLocker == 0; ``` 9. **Rule** `cancelRolloverDoesNotAffectThirdParty` - verifies that the action of one account cancelling their roll over election does not impact third-party balances. ```solidity assert thirdPartyRolloverAmountBefore == thirdPartyRolloverAmountAfter; assert thirdPartyRolloverBidPriceHashBefore == thirdPartyRolloverBidPriceHashAfter; assert thirdPartyRolloverAuctionBidLockerBefore == thirdPartyRolloverAuctionBidLockerAfter; ``` 10. **Rule:** `cancelRolloverRevertConditions`- check for revert under the defined expected conditions, ensuring operation adherence to defined rules. ```solidity 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; ``` 11. **Rule:** `fulfillRolloverIntegrity` - ensures that a rollover election is properly marked as processed when fulfilled. ```solidity fulfillRollover(e, borrower); bool rolloverProcessed = getRolloverInstructions(borrower).processed; assert rolloverProcessed, "The rollover should be marked as processed."; ``` 12. **Rule:** `fulfillRolloverDoesNotAffectThirdParty` - verifies that fulfilling a rollover election submitted by one account does not affect the third party balances ```solidity bool thirdPartyRolloverProcessedBefore = getRolloverInstructions(borrower2).processed; fulfillRollover(e, borrower); bool thirdPartyRolloverProcessedAfter = getRolloverInstructions(borrower2).processed; assert thirdPartyRolloverProcessedBefore == thirdPartyRolloverProcessedAfter, "Third party's rollover state should remain unaffected."; } ``` 13. **Rule:** `fulfillRolloverRevertConditions`- check for revert under the defined expected conditions, ensuring operation adherence to defined rules. ```solidity 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."; ``` 14. **Rule:** `onlyRoleCanCallRevert` - checks if a method call requires specific roles to execute successfully, does not revert if the caller has the necessary role. ```solidity 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."; } ``` 15. **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. ```solidity 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. ```solidity require lockingPaused() == true; f@withrevert(e, args); assert lastReverted, "lockBids(...) should revert when bid locking is paused"; ``` 2. **Rule:** `UnpauseLockingAllowsBidLocking` - verifies that unpausing locking allows users to lock bids. ```solidity require lockingPaused() == false; f(e, args); assert !lastReverted, "lockBids(...) should not revert when bid locking is not paused"; ``` 3. **Rule:** `PauseUnlockingCausesBidUnlockingToRevert` - verifies that pausing unlocking reverts any attempts at unlocking offers. ```solidity require unlockingPaused() == true; unlockBids@withrevert(e, ids); assert lastReverted, "unlockBids(...) should revert when bid unlocking is paused"; ``` 4. **Rule:** `UnpauseUnlockingAllowsBidUnlocking` - verifies that unpausing locking allows users to unlock bids. ```solidity require unlockingPaused() == false; require harnessGetInternalBids(id).id == id; unlockBids(e, [id]); assert !lastReverted, "unlockBids(...) should not revert when bid unlocking is not paused"; ``` 5. **Rule:** `lockerCollateralTokenBalanceGreaterThanCollateralLedgerBalance` - verified the assumption that the total amount of collateral locked is always greater than or equal to the amount recorded in ledger. ```solidity require(bidLockerStateCollateralToken.balanceOf(lockerBidLockingState) + bidSubmissions[0].collateralAmounts[0] <= max_uint256); f(e, args); assert sumOfCollateralBalances <= to_mathint((bidLockerStateCollateralToken.balanceOf(lockerBidLockingState))); ``` 6. **Invariant:** `LockedBidIdAlwaysMatchesIndex` - verifies the assumption that the bidId matches the ledger. ```solidity harnessGetInternalBidId(bidId) == bidId || harnessGetInternalBidId(bidId) == to_bytes32(0); ``` 7. **Invariant:** `BidCountAlwaysMatchesNumberOfStoredBids` - verifies the assumption that the bidCount matches the ledger. ```solidity to_mathint(bidCount()) == lockedBidCount; ``` 8. **Rule:** `LockBidsIntegrity` - ensures that collateral token balances are properly transferred to the repo locker when locking bids. ```solidity 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"; ``` 9. **Rule:** `LockBidsDoesNotAffectThirdParty` - verifies that locking bids belonging to one account does not affect the third party balances. ```solidity 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"; ``` 10. **Rule:** `lockBidsMonotonicBehavior` - verifies that locking a bid is monotonically increasing in the bid count. ```solidity uint256 bidCountBefore = bidCount(); lockBids(e, bidSubmissions); uint256 bidCountAfter = bidCount(); assert bidCountAfter >= bidCountBefore, "bidCount should either increase or stay the same after lockBids is called"; ``` 11. **Rule:** `LockBidsRevertConditions`- check for revert under the defined expected conditions, ensuring operation adherence to defined rules. ```solidity 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) 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) isExpectedToRevert, "lockBidsWithReferral should revert when one of the revert conditions is reached"; ``` 15. **Rule:** `lockBidsWithReferralMonotonicBehavior` - verifies that locking a bid with referral is monotonically increasing in the bid count. ```solidity assert bidCountAfter >= bidCountBefore, "bidCount should either increase or stay the same after lockBidsWithReferral is called"; ``` 16. **Rule:** `UnlockBidsIntegrity` - ensures that collateral token balances are properly transferred from the repo locker to the user when unlocking bids. ```solidity 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"; ``` 17. **Rule:** `UnlockBidsDoesNotAffectThirdParty` - verifies that unlocking bids belonging to one account does not affect the third party balances. ```solidity 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"; ``` 18. **Rule:** `UnlockBidsRevertConditions`- check for revert under the defined expected conditions, ensuring operation adherence to defined rules. ```solidity 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"; ``` 19. **Rule:** `UnlockBidsMonotonicBehavior` - verifies that unlocking a bid is monotonically decreasing in the bid count. ```solidity assert bidCountAfter <= bidCountBefore, "unlockBids should decrease or maintain bid count"; ``` 20. **Rule:** `AuctionUnlockBidIntegrity` - ensures that collateral token balances are properly transferred from the repo locker to the user when unlocking bids. ```solidity 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"; ``` 21. **Rule:** `AuctionUnlockBidDoesNotAffectThirdParty` - verifies that unlocking bids belonging to one account does not affect the third party balances. ```solidity 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"; ``` 22. **Rule:** `AuctionUnlockBidRevertConditions`- check for revert under the defined expected conditions, ensuring operation adherence to defined rules. ```solidity 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"; ``` 23. **Rule:** `AuctionUnlockBidMonotonicBehavior` - verifies that `auctionUnlockCollateral` monotonically decreases the bid count. ```solidity assert bidCountAfter <= bidCountBefore, "auctionUnlockBid should decrease or maintain bid count"; ``` 24. **Rule:** `RevealBidsIntegrity` - ensures that prices are revealed when revealing bids. ```solidity assert isRevealedAfter && revealedPriceAfter == price, "revealBids should not revert"; ``` 25. **Rule:** `RevealBidsDoesNotAffectThirdParty` - verifies that revealing a bid belonging to one account does not affect the third party balances. ```solidity assert !isThirdPartyRevealedAfter, "revealBids should not reveal third party bids"; ``` 26. **Rule:** `RevealBidsRevertConditions`- check for revert under the defined expected conditions, ensuring operation adherence to defined rules. ```solidity 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"; ``` 27. **Rule:** `RevealBidsMonotonicBehavior` - verifies that `revealBids` does not change the bid count. ```solidity assert bidCountBefore == bidCountAfter, "revealBids should not change bid count"; ``` 28. **Rule:** `OnlyRoleCanCallRevert` - checks if a method call requires specific roles to execute successfully, does not revert if the caller has the necessary role. ```solidity 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); ``` 29. **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. ```solidity 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. ```solidity require lockingPaused() == true; f@withrevert(e, args); assert lastReverted, "lockOffers(...) should revert when trying to lock a paused contract"; ``` 2. **Rule:** `UnpauseLockingAllowsOfferLocking` - verifies that unpausing locking allows users to lock offers. ```solidity require lockingPaused() == false; f(e, args); assert !lastReverted, "lockOffers(...) should not revert when trying to lock offers on an unpaused contract"; ``` 3. **Rule:** `PauseUnlockingCausesOfferUnlockingToRevert` - verifies that pausing unlocking reverts any attempts at unlocking offers. ```solidity require unlockingPaused() == true; unlockOffers@withrevert(e, ids); assert lastReverted, "unlockOffers(...) should revert when trying to unlock offers on a paused contract"; ``` 4. **Rule:** `UnpauseUnlockingAllowsOfferUnlocking` - verifies that unpausing unlocking allows users to unlock offers. ```solidity 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"; ``` 5. **Invariant:** `LockedOfferIdAlwaysMatchesIndex` - verifies the assumption that the offerId matches the ledger. ```solidity harnessGetInternalOfferId(offerId) == offerId || harnessGetInternalOfferId(offerId) == to_bytes32(0); ``` 6. **Invariant:** `OfferCountAlwaysMatchesNumberOfStoredOffers` - verifies the assumption that the offerCount always matches the ledger. ```solidity to_mathint(offerCount()) == lockedOfferCount; ``` 7. **Rule:** `lockerPurchaseTokenBalanceGreaterThanOfferLedgerBalance` - verifies the assumption that total purchaseToken balances are always greater than or equal to the amount recorded in ledger. ```solidity require(sumOfOfferBalances <= to_mathint((offerStatePurchaseToken.balanceOf(repoLockerOfferState)))); // starting condition f(e, args); assert sumOfOfferBalances <= to_mathint((offerStatePurchaseToken.balanceOf(repoLockerOfferState))); ``` 8. **Rule:** `LockOffersIntegrity` - ensures that purchase token balances are properly transferred to the repo locker when locking offers. ```solidity assert (purchaseTokenOneBalanceAfter == purchaseTokenBalanceBefore - amountToLock), "lockOffers should transfer collateral tokens from offeror to contract"; ``` 9. **Rule:** `LockOffersDoesNotAffectThirdParty` - verifies that locking offers belonging to one account does not affect the third party balances. ```solidity 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"; ``` 10. **Rule:** `LockOffersMonotonicBehavior` - verifies that locking offers is monotonically increasing in the offer count. ```solidity assert offerCountAfter >= offerCountBefore, "offerCount should increment or maintain the same value after locking an offer"; ``` 11. **Rule:** `LockOffersRevertConditions`- check for revert under the defined expected conditions, ensuring operation adherence to defined rules. ```solidity 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"; ``` 12. **Rule:** `LockOffersWithReferralIntegrity` - ensures that purchase token balances are properly transferred to the repo locker when locking offers with referral. ```solidity assert (purchaseTokenOneBalanceAfter == purchaseTokenBalanceBefore - amountToLock), "lockOffers should transfer collateral tokens from offeror to contract"; ``` 13. **Rule:** `LockOffersWithReferralDoesNotAffectThirdParty` - verifies that locking offers belonging to one account when calling `lockOffersWithReferral` does not affect the third party balances ```solidity 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"; ``` 14. **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";
15. **Rule:** `LockOffersWithReferralMonotonicBehavior` - verifies that locking offers with referral is monotonically increasing in the offer count. ```solidity assert offerCountAfter >= offerCountBefore, "offerCount should increment or maintain the same value after locking an offer"; ``` 16. **Rule:** `UnlockOffersIntegrity` - ensures that purchase token balances are properly transferred to user when unlocking offers. ```solidity assert (purchaseTokenBalanceAfter == (purchaseTokenBalanceBefore + purchaseTokenAmountToUnlock)), "unlockOffers should not revert"; ``` 17. **Rule:** `UnlockOffersDoesNotAffectThirdParty` - verifies that unlocking offers belonging to one account does not affect the third party balances ```solidity assert thirdPartyOfferAffected, "unlockOffers should not modify offers that are not in args"; ``` 18. **Rule:** `UnlockOffersRevertConditions`- check for revert under the defined expected conditions, ensuring operation adherence to defined rules. ```solidity 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"; ``` 19. **Rule:** `UnlockOffersMonotonicBehavior` - verifies that unlocking offers is monotonically decreasing in the offer count. ```solidity assert offerCountAfter == assert_uint256(offerCountBefore - unlockOfferIds.length), "offerCount should decrement by the number of offer ids submitted to unlock"; ``` 20. **Rule:** `UnlockOfferPartialIntegrity` - ensures that purchase token balances are properly transferred to user when partially unlocking offers. ```solidity assert purchaseTokenBalancAfter == purchaseTokenBalanceBefore + amount, "purchase token balance should increase by the provided amount"; ``` 21. **Rule:** `UnlockOfferPartialDoesNotAffectThirdParty` - verifies that partially unlocking offers belonging to one account does not affect the third party balances ```solidity assert thirdPartyOfferNotAffected, "unlockOfferPartial should not modify offers that are not in args"; ``` 22. **Rule:** `UnlockOfferPartialRevertConditions`- check for revert under the defined expected conditions, ensuring operation adherence to defined rules. ```solidity 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"; ``` 23. **Rule:** `UnlockOfferPartialMonotonicBehavior` - verifies that partially unlocking offers does not change the offer count. ```solidity assert offerCountAfter == offerCountBefore, "unlockOfferPartial should not affect the offerCount"; } ``` 24. **Rule:** `RevealOffersIntegrity` - ensures that prices are revealed when revealing offers. ```solidity assert isRevealedAfter && revealedPriceAfter == price, "revealOffers should successfully reveal offers"; ``` 25. **Rule:** `RevealOffersDoesNotAffectThirdParty` - verifies that revealing offers belonging to one account does not affect the third party balances ```solidity assert !isThirdPartyRevealedAfter, "revealOffers should not affect third-party offers"; } ``` 26. **Rule:** `RevealOffersRevertConditions`- check for revert under the defined expected conditions, ensuring operation adherence to defined rules. ```solidity 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"; ``` 27. **Rule:** `RevealOffersMonotonicBehavior` - verifies that revealing offers does not change the offer count. ```solidity assert offerCountBefore == offerCountAfter, "revealOffers should not change the offer count"; ``` 28. **Rule:** `OnlyRoleCanCallRevert` - checks if a method call requires specific roles to execute successfully, does not revert if the caller has the necessary role. ```solidity 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); ``` 29. **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. ```solidity 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. ```solidity assert !lastReverted => hasRole(ADMIN_ROLE(), e.msg.sender) || hasRole(DEVOPS_ROLE(), e.msg.sender) || hasRole(INITIALIZER_ROLE(), e.msg.sender); ``` 2. **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. ```solidity assert storeBefore != storeAfter => hasRole(ADMIN_ROLE(), e.msg.sender) || hasRole(DEVOPS_ROLE(), e.msg.sender) || hasRole(INITIALIZER_ROLE(), e.msg.sender); ``` 3. **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. ```solidity assert !lastReverted => hasRole(ADMIN_ROLE(), e.msg.sender) || (completeAuctionInput.unrevealedBidSubmissions.length == 0 && completeAuctionInput.unrevealedOfferSubmissions.length == 0); ``` 4. **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. ```solidity 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]()` 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 ``` --- # Agent Instructions: Querying This Documentation If you need additional information that is not directly available in this page, you can query the documentation dynamically by asking a question. Perform an HTTP GET request on the current page URL with the `ask` query parameter: ``` GET https://developers.term.finance/deployed-contracts/formal-verification.md?ask= ``` The question should be specific, self-contained, and written in natural language. The response will contain a direct answer to the question and relevant excerpts and sources from the documentation. Use this mechanism when the answer is not explicitly present in the current page, you need clarification or additional context, or you want to retrieve related documentation sections.