diff --git a/kontrol.toml b/kontrol.toml index df91602d..65092d29 100644 --- a/kontrol.toml +++ b/kontrol.toml @@ -1,7 +1,7 @@ [build.default] foundry-project-root = '.' -regen = true -rekompile = true +regen = false +rekompile = false verbose = false debug = false require = 'src/test/kontrol/term-lemmas.k' @@ -38,7 +38,7 @@ break-on-basic-blocks = false break-on-cheatcodes = false auto_abstract = true run-constructor = false -bmc-depth = 3 +bmc-depth = 2 match-test = [ "RepoTokenListInvariantsTest.setUp", "TermAuctionListInvariantsTest.setUp", @@ -47,7 +47,7 @@ ast = true [prove.tests] foundry-project-root = '.' -verbose = false +verbose = true debug = false max-depth = 100000 max-iterations = 10000 @@ -78,9 +78,19 @@ match-test = [ "RepoTokenListInvariantsTest.testInsertSortedNewToken", "RepoTokenListInvariantsTest.testInsertSortedDuplicateToken", "RepoTokenListInvariantsTest.testRemoveAndRedeemMaturedTokens", + "RepoTokenListInvariantsTest.testGetCumulativeDataEmpty", + "RepoTokenListInvariantsTest.testGetPresentValueEmpty", + "RepoTokenListInvariantsTest.testGetPresentTotalValue", + "RepoTokenListInvariantsTest.testGetCumulativeRepoTokenData", "TermAuctionListInvariantsTest.testInsertPendingNewOffer", "TermAuctionListInvariantsTest.testInsertPendingDuplicateOffer", "TermAuctionListInvariantsTest.testRemoveCompleted", + "TermAuctionListInvariantsTest.testGetCumulativeDataEmpty", + "TermAuctionListInvariantsTest.testGetPresentValueEmpty", + "TermAuctionListInvariantsTest.testGetCumulativeDataNoCompletedAuctions", + "TermAuctionListInvariantsTest.testGetCumulativeDataCompletedAuctions", + "TermAuctionListInvariantsTest.testGetCumulativeOfferData", + "TermAuctionListInvariantsTest.testGetPresentTotalValue", ] ast = true diff --git a/src/RepoTokenList.sol b/src/RepoTokenList.sol index 5cc35643..e5d56354 100644 --- a/src/RepoTokenList.sol +++ b/src/RepoTokenList.sol @@ -177,17 +177,13 @@ library RepoTokenList { * @param listData The list data * @param discountRateAdapter The discount rate adapter * @param purchaseTokenPrecision The precision of the purchase token - * @param prevTermController The previous term controller - * @param currTermController The current term controller * @return totalPresentValue The total present value of the repoTokens * @dev Aggregates the present value of all repoTokens in the list. */ function getPresentValue( RepoTokenListData storage listData, ITermDiscountRateAdapter discountRateAdapter, - uint256 purchaseTokenPrecision, - ITermController prevTermController, - ITermController currTermController + uint256 purchaseTokenPrecision ) internal view returns (uint256 totalPresentValue) { // If the list is empty, return 0 if (listData.head == NULL_NODE) return 0; @@ -425,7 +421,7 @@ library RepoTokenList { uint256 currentMaturity = getRepoTokenMaturity(current); - // Insert repoToken before current if its maturity is less than or equal + // Insert repoToken before current if its maturity is less than current maturity if (maturityToInsert < currentMaturity) { if (prev == NULL_NODE) { listData.head = repoToken; diff --git a/src/Strategy.sol b/src/Strategy.sol index 6364ab43..8ddb639c 100644 --- a/src/Strategy.sol +++ b/src/Strategy.sol @@ -524,8 +524,6 @@ contract Strategy is BaseStrategy, Pausable, AccessControl { repoTokenListData, strategyState.discountRateAdapter, PURCHASE_TOKEN_PRECISION, - strategyState.prevTermController, - strategyState.currTermController, repoToken ); } @@ -582,16 +580,12 @@ contract Strategy is BaseStrategy, Pausable, AccessControl { liquidBalance + repoTokenListData.getPresentValue( strategyState.discountRateAdapter, - PURCHASE_TOKEN_PRECISION, - prevTermController, - currTermController + PURCHASE_TOKEN_PRECISION ) + termAuctionListData.getPresentValue( repoTokenListData, strategyState.discountRateAdapter, PURCHASE_TOKEN_PRECISION, - prevTermController, - currTermController, address(0) ); } diff --git a/src/TermAuctionList.sol b/src/TermAuctionList.sol index 917a9b4c..7ae55a64 100644 --- a/src/TermAuctionList.sol +++ b/src/TermAuctionList.sol @@ -242,8 +242,6 @@ library TermAuctionList { * @param repoTokenListData The repoToken list data * @param discountRateAdapter The discount rate adapter * @param purchaseTokenPrecision The precision of the purchase token - * @param prevTermController The previous term controller - * @param currTermController The current term controller * @param repoTokenToMatch The address of the repoToken to match (optional) * @return totalValue The total present value of the offers * @@ -257,8 +255,6 @@ library TermAuctionList { RepoTokenListData storage repoTokenListData, ITermDiscountRateAdapter discountRateAdapter, uint256 purchaseTokenPrecision, - ITermController prevTermController, - ITermController currTermController, address repoTokenToMatch ) internal view returns (uint256 totalValue) { // Return 0 if the list is empty @@ -282,7 +278,7 @@ library TermAuctionList { // Handle new or unseen repo tokens /// @dev offer processed, but auctionClosed not yet called and auction is new so repoToken not on List and wont be picked up /// checking repoTokendiscountRates to make sure we are not double counting on re-openings - if (repoTokenListData.discountRates[offer.repoToken] == 0 && offer.termAuction.auctionCompleted()) { + if (offer.termAuction.auctionCompleted() && repoTokenListData.discountRates[offer.repoToken] == 0) { if (edgeCaseAuction != address(offer.termAuction)) { uint256 repoTokenAmountInBaseAssetPrecision = RepoTokenUtils.getNormalizedRepoTokenAmount( offer.repoToken, @@ -357,7 +353,7 @@ library TermAuctionList { // Handle new repo tokens or reopening auctions /// @dev offer processed, but auctionClosed not yet called and auction is new so repoToken not on List and wont be picked up /// checking repoTokendiscountRates to make sure we are not double counting on re-openings - if (repoTokenListData.discountRates[offer.repoToken] == 0 && offer.termAuction.auctionCompleted()) { + if (offer.termAuction.auctionCompleted() && repoTokenListData.discountRates[offer.repoToken] == 0) { // use normalized repoToken amount if repoToken is not in the list if (edgeCaseAuction != address(offer.termAuction)) { offerAmount = RepoTokenUtils.getNormalizedRepoTokenAmount( diff --git a/src/test/kontrol/KontrolTest.sol b/src/test/kontrol/KontrolTest.sol index 1cb57cba..83e0650f 100644 --- a/src/test/kontrol/KontrolTest.sol +++ b/src/test/kontrol/KontrolTest.sol @@ -11,7 +11,7 @@ contract KontrolTest is Test, KontrolCheats { // Note: 2 ** 35 takes us to year 3058 uint256 constant timeUpperBound = 2 ** 35; - function infoAssert(bool condition, string memory message) external { + function infoAssert(bool condition, string memory message) external pure { if (!condition) { revert(message); } @@ -35,27 +35,75 @@ contract KontrolTest is Test, KontrolCheats { } } - function _loadUInt256(address contractAddress, uint256 slot) internal view returns (uint256) { - return uint256(vm.load(contractAddress, bytes32(slot))); + function _loadData( + address contractAddress, + uint256 slot, + uint256 offset, + uint256 width + ) internal view returns (uint256) { + // `offset` and `width` must not overflow the slot + assert(offset + width <= 32); + + // Slot read mask + uint256 mask; + unchecked { + mask = (2 ** (8 * width)) - 1; + } + // Value right shift + uint256 shift = 8 * offset; + + // Current slot value + uint256 slotValue = uint256(vm.load(contractAddress, bytes32(slot))); + + // Isolate and return data to retrieve + return mask & (slotValue >> shift); } - function _loadAddress(address contractAddress, uint256 slot) internal view returns (address) { - return address(uint160(uint256(vm.load(contractAddress, bytes32(slot))))); + function _storeData(address contractAddress, uint256 slot, uint256 offset, uint256 width, uint256 value) internal { + // `offset` and `width` must not overflow the slot + assert(offset + width <= 32); + // and `value` must fit into the designated part + assert(width == 32 || value < 2 ** (8 * width)); + + // Slot update mask + uint256 maskLeft; + unchecked { + maskLeft = ~((2 ** (8 * (offset + width))) - 1); + } + uint256 maskRight = (2 ** (8 * offset)) - 1; + uint256 mask = maskLeft | maskRight; + + value = (2 ** (8 * offset)) * value; + + // Current slot value + uint256 slotValue = uint256(vm.load(contractAddress, bytes32(slot))); + // Updated slot value + slotValue = value | (mask & slotValue); + + vm.store(contractAddress, bytes32(slot), bytes32(slotValue)); } - function _storeBytes32(address contractAddress, uint256 slot, bytes32 value) internal { - vm.store(contractAddress, bytes32(slot), value); + function _loadUInt256(address contractAddress, uint256 slot) internal view returns (uint256) { + return _loadData(contractAddress, slot, 0, 32); + } + + function _loadAddress(address contractAddress, uint256 slot) internal view returns (address) { + return address(uint160(_loadData(contractAddress, slot, 0, 20))); } function _storeUInt256(address contractAddress, uint256 slot, uint256 value) internal { - vm.store(contractAddress, bytes32(slot), bytes32(value)); + _storeData(contractAddress, slot, 0, 32, value); } function _storeAddress(address contractAddress, uint256 slot, address value) internal { - vm.store(contractAddress, bytes32(slot), bytes32(uint256(uint160(value)))); + _storeData(contractAddress, slot, 0, 20, uint160(value)); + } + + function _storeBytes32(address contractAddress, uint256 slot, bytes32 value) internal { + _storeUInt256(contractAddress, slot, uint256(value)); } - function _assumeNoOverflow(uint256 augend, uint256 addend) internal { + function _assumeNoOverflow(uint256 augend, uint256 addend) internal pure { unchecked { vm.assume(augend < augend + addend); } diff --git a/src/test/kontrol/RepoToken.sol b/src/test/kontrol/RepoToken.sol index 6654e15b..84375a84 100644 --- a/src/test/kontrol/RepoToken.sol +++ b/src/test/kontrol/RepoToken.sol @@ -48,7 +48,7 @@ contract RepoToken is ITermRepoToken, KontrolTest { _storeUInt256(address(this), termRepoCollateralManagerSlot, uint256(uint160(address(termRepoCollateralManager)))); } - function decimals() public view returns (uint8) { + function decimals() public pure returns (uint8) { return 18; } diff --git a/src/test/kontrol/RepoTokenListInvariants.t.sol b/src/test/kontrol/RepoTokenListInvariants.t.sol index c243a85c..bef6aa32 100644 --- a/src/test/kontrol/RepoTokenListInvariants.t.sol +++ b/src/test/kontrol/RepoTokenListInvariants.t.sol @@ -8,12 +8,11 @@ import "src/RepoTokenList.sol"; import "src/test/kontrol/Constants.sol"; import "src/test/kontrol/RepoToken.sol"; +import "src/test/kontrol/RepoTokenListTest.t.sol"; -contract RepoTokenListInvariantsTest is KontrolTest { +contract RepoTokenListInvariantsTest is RepoTokenListTest { using RepoTokenList for RepoTokenListData; - RepoTokenListData _repoTokenList; - function setUp() public { // Make storage of this contract completely symbolic kevm.symbolicStorage(address(this)); @@ -22,233 +21,6 @@ contract RepoTokenListInvariantsTest is KontrolTest { _initializeRepoTokenList(); } - /** - * Deploy a new RepoToken with symbolic storage. - */ - function _newRepoToken() internal returns (address) { - RepoToken repoToken = new RepoToken(); - repoToken.initializeSymbolic(); - - return address(repoToken); - } - - /** - * Return the maturity timestamp of the given RepoToken. - */ - function _getRepoTokenMaturity(address repoToken) internal returns (uint256 redemptionTimestamp) { - (redemptionTimestamp, , ,) = ITermRepoToken(repoToken).config(); - } - - /** - * Return the this contract's balance in the given RepoToken. - */ - function _getRepoTokenBalance(address repoToken) internal returns (uint256) { - return ITermRepoToken(repoToken).balanceOf(address(this)); - } - - /** - * Initialize _repoTokenList to a RepoTokenList of arbitrary size, where all - * items are distinct RepoTokens with symbolic storage. - */ - function _initializeRepoTokenList() internal { - address previous = RepoTokenList.NULL_NODE; - - while (kevm.freshBool() != 0) { - address current = _newRepoToken(); - - if (previous == RepoTokenList.NULL_NODE) { - _repoTokenList.head = current; - } else { - _repoTokenList.nodes[previous].next = current; - } - - previous = current; - } - - if (previous == RepoTokenList.NULL_NODE) { - _repoTokenList.head = RepoTokenList.NULL_NODE; - } else { - _repoTokenList.nodes[previous].next = RepoTokenList.NULL_NODE; - } - } - - /** - * Assume or assert that the tokens in the list are sorted by maturity. - */ - function _establishSortedByMaturity(Mode mode) internal { - address previous = RepoTokenList.NULL_NODE; - address current = _repoTokenList.head; - - while (current != RepoTokenList.NULL_NODE) { - if (previous != RepoTokenList.NULL_NODE) { - uint256 previousMaturity = _getRepoTokenMaturity(previous); - uint256 currentMaturity = _getRepoTokenMaturity(current); - _establish(mode, previousMaturity <= currentMaturity); - } - - previous = current; - current = _repoTokenList.nodes[current].next; - } - } - - /** - * Assume or assert that there are no duplicate tokens in the list. - */ - function _establishNoDuplicateTokens(Mode mode) internal { - address current = _repoTokenList.head; - - while (current != RepoTokenList.NULL_NODE) { - address other = _repoTokenList.nodes[current].next; - - while (other != RepoTokenList.NULL_NODE) { - _establish(mode, current != other); - other = _repoTokenList.nodes[other].next; - } - - current = _repoTokenList.nodes[current].next; - } - } - - /** - * Assume or assert that there are no tokens in the list have matured - * (i.e. all token maturities are greater than the current timestamp). - */ - function _establishNoMaturedTokens(Mode mode) internal { - address current = _repoTokenList.head; - - while (current != RepoTokenList.NULL_NODE) { - uint256 currentMaturity = _getRepoTokenMaturity(current); - - _establish(mode, block.timestamp < currentMaturity); - - current = _repoTokenList.nodes[current].next; - } - } - - /** - * Assume or assert that all tokens in the list have balance > 0. - */ - function _establishPositiveBalance(Mode mode) internal { - address current = _repoTokenList.head; - - while (current != RepoTokenList.NULL_NODE) { - uint256 repoTokenBalance = _getRepoTokenBalance(current); - - _establish(mode, 0 < repoTokenBalance); - - current = _repoTokenList.nodes[current].next; - } - } - - /** - * Weaker version of the above invariant that allows matured tokens to have - * a balance of 0. - * - * Note: This is equivalent to the above invariant if the NoMaturedTokens - * invariant also holds. - */ - function _establishPositiveBalanceForNonMaturedTokens(Mode mode) internal { - address current = _repoTokenList.head; - - while (current != RepoTokenList.NULL_NODE) { - uint256 currentMaturity = _getRepoTokenMaturity(current); - uint256 repoTokenBalance = _getRepoTokenBalance(current); - - if (block.timestamp < currentMaturity) { - _establish(mode, 0 < repoTokenBalance); - } - - current = _repoTokenList.nodes[current].next; - } - } - - /** - * Count the number of nodes in the list. - * - * Note that this function guarantees the following postconditions: - * - The head of the list is NULL_NODE iff the count is 0. - * - If the count is N, the Nth node in the list is followed by NULL_NODE. - */ - function _countNodesInList() internal returns (uint256) { - uint256 count = 0; - address current = _repoTokenList.head; - - while (current != RepoTokenList.NULL_NODE) { - ++count; - current = _repoTokenList.nodes[current].next; - } - - return count; - } - - /** - * Return true if the given RepoToken is in the list, and false otherwise. - */ - function _repoTokenInList(address repoToken) internal returns (bool) { - address current = _repoTokenList.head; - - while (current != RepoTokenList.NULL_NODE) { - if (current == repoToken) { - return true; - } - - current = _repoTokenList.nodes[current].next; - } - - return false; - } - - function _repoTokensListToArray(uint256 length) internal view returns (address[] memory repoTokens) { - address current = _repoTokenList.head; - uint256 i; - repoTokens = new address[](length); - - while (current != RepoTokenList.NULL_NODE) { - repoTokens[i++] = current; - current = _repoTokenList.nodes[current].next; - } - } - - function _establishInsertListPreservation(address insertedRepoToken, address[] memory repoTokens, uint256 repoTokensCount) internal view { - address current = _repoTokenList.head; - uint256 i = 0; - - if(insertedRepoToken != address(0)) { - - while (current != RepoTokenList.NULL_NODE && i < repoTokensCount) { - if(current != repoTokens[i]) { - assert (current == insertedRepoToken); - current = _repoTokenList.nodes[current].next; - break; - } - i++; - current = _repoTokenList.nodes[current].next; - } - - if (current != RepoTokenList.NULL_NODE && i == repoTokensCount) { - assert (current == insertedRepoToken); - } - } - - while (current != RepoTokenList.NULL_NODE && i < repoTokensCount) { - assert(current == repoTokens[i++]); - current = _repoTokenList.nodes[current].next; - } - } - - function _establishRemoveListPreservation(address[] memory repoTokens, uint256 repoTokensCount) internal view { - address current = _repoTokenList.head; - uint256 i = 0; - - while (current != RepoTokenList.NULL_NODE && i < repoTokensCount) { - if(current == repoTokens[i++]) { - current = _repoTokenList.nodes[current].next; - } - } - - assert(current == RepoTokenList.NULL_NODE); - } - /** * Test that insertSorted preserves the list invariants when a new RepoToken * is added (that was not present in the list before). @@ -336,21 +108,6 @@ contract RepoTokenListInvariantsTest is KontrolTest { _establishPositiveBalance(Mode.Assert); } - /** - * Configure the model of the RepoServicer for every token in the list to - * follow the assumption that redeemTermRepoTokens will not revert. - */ - function _guaranteeRedeemAlwaysSucceeds() internal { - address current = _repoTokenList.head; - - while (current != RepoTokenList.NULL_NODE) { - (, , address repoServicer,) = ITermRepoToken(current).config(); - TermRepoServicer(repoServicer).guaranteeRedeemAlwaysSucceeds(); - - current = _repoTokenList.nodes[current].next; - } - } - /** * Test that removeAndRedeemMaturedTokens preserves the list invariants. */ @@ -386,4 +143,135 @@ contract RepoTokenListInvariantsTest is KontrolTest { _establishNoMaturedTokens(Mode.Assert); _establishPositiveBalance(Mode.Assert); } + + function testGetCumulativeDataEmpty( + address repoToken, + uint256 repoTokenAmount, + uint256 purchaseTokenPrecision + ) external { + _initializeRepoTokenListEmpty(); + + TermDiscountRateAdapter discountRateAdapter = + new TermDiscountRateAdapter(); + + ( + uint256 cumulativeWeightedTimeToMaturity, + uint256 cumulativeRepoTokenAmount, + bool found + ) = _repoTokenList.getCumulativeRepoTokenData( + ITermDiscountRateAdapter(address(discountRateAdapter)), + repoToken, + repoTokenAmount, + purchaseTokenPrecision + ); + + assert(cumulativeWeightedTimeToMaturity == 0); + assert(cumulativeRepoTokenAmount == 0); + assert(found == false); + } + + + function testGetPresentValueEmpty( + uint256 purchaseTokenPrecision + ) external { + _initializeRepoTokenListEmpty(); + + TermDiscountRateAdapter discountRateAdapter = + new TermDiscountRateAdapter(); + + uint256 totalPresentValue = _repoTokenList.getPresentValue( + ITermDiscountRateAdapter(address(discountRateAdapter)), + purchaseTokenPrecision + ); + + assert(totalPresentValue == 0); + } + + function testGetCumulativeRepoTokenData( + address repoToken, + uint256 repoTokenAmount, + uint256 purchaseTokenPrecision + ) external { + // Assume relevant invariants + _establishPositiveBalance(Mode.Assume); + + // Initialize a DiscountRateAdapter with symbolic storage + TermDiscountRateAdapter discountRateAdapter = + new TermDiscountRateAdapter(); + _initializeDiscountRateAdapter(discountRateAdapter); + + // Consider only the case where we are not trying to match a token + vm.assume(repoToken == address(0)); + vm.assume(purchaseTokenPrecision <= 18); + + ( + uint256 cumulativeWeightedTimeToMaturity, + uint256 cumulativeRepoTokenAmount, + bool found + ) = _repoTokenList.getCumulativeRepoTokenData( + discountRateAdapter, + repoToken, + repoTokenAmount, + purchaseTokenPrecision + ); + + assert(!found); + + // Removes matured tokens and returns their total value + uint256 cumulativeRepoTokenAmountMatured + = _filterMaturedTokensGetTotalValue( + discountRateAdapter, + purchaseTokenPrecision + ); + + // Simplified calculation for no matured tokens + ( + uint256 cumulativeWeightedTimeToMaturityNotMatured, + uint256 cumulativeRepoTokenAmountNotMatured + ) = _cumulativeRepoTokenDataNotMatured( + discountRateAdapter, + purchaseTokenPrecision + ); + + assert( + cumulativeWeightedTimeToMaturity == + cumulativeWeightedTimeToMaturityNotMatured + ); + + assert( + cumulativeRepoTokenAmount == + cumulativeRepoTokenAmountMatured + cumulativeRepoTokenAmountNotMatured + ); + } + + + function testGetPresentTotalValue( + uint256 purchaseTokenPrecision + ) external { + // Initialize a DiscountRateAdapter with symbolic storage + TermDiscountRateAdapter discountRateAdapter = + new TermDiscountRateAdapter(); + _initializeDiscountRateAdapter(discountRateAdapter); + + vm.assume(0 < purchaseTokenPrecision); + vm.assume(purchaseTokenPrecision <= 18); + + uint256 totalPresentValue = _repoTokenList.getPresentValue( + discountRateAdapter, + purchaseTokenPrecision + ); + + // Removes matured tokens and returns their total value + uint256 totalPresentValueMatured = _filterMaturedTokensGetTotalValue( + discountRateAdapter, + purchaseTokenPrecision + ); + + uint256 totalPresentValueNotMatured = _totalPresentValueNotMatured( + discountRateAdapter, + purchaseTokenPrecision + ); + + assert(totalPresentValue == totalPresentValueMatured + totalPresentValueNotMatured); + } } diff --git a/src/test/kontrol/RepoTokenListTest.t.sol b/src/test/kontrol/RepoTokenListTest.t.sol new file mode 100644 index 00000000..4b67d985 --- /dev/null +++ b/src/test/kontrol/RepoTokenListTest.t.sol @@ -0,0 +1,399 @@ +pragma solidity 0.8.23; + +import "forge-std/Vm.sol"; +import "forge-std/Test.sol"; +import "kontrol-cheatcodes/KontrolCheats.sol"; + +import "src/RepoTokenList.sol"; +import "src/TermAuctionList.sol"; + +import "src/test/kontrol/Constants.sol"; +import "src/test/kontrol/RepoToken.sol"; +import "src/test/kontrol/TermAuction.sol"; +import "src/test/kontrol/TermAuctionOfferLocker.sol"; +import "src/test/kontrol/TermDiscountRateAdapter.sol"; + + +contract RepoTokenListTest is KontrolTest { + using RepoTokenList for RepoTokenListData; + + RepoTokenListData _repoTokenList; + + /** + * Deploy a new RepoToken with symbolic storage. + */ + function _newRepoToken() internal returns (address) { + RepoToken repoToken = new RepoToken(); + repoToken.initializeSymbolic(); + + return address(repoToken); + } + + /** + * Return the maturity timestamp of the given RepoToken. + */ + function _getRepoTokenMaturity(address repoToken) internal view returns (uint256 redemptionTimestamp) { + (redemptionTimestamp, , ,) = ITermRepoToken(repoToken).config(); + } + + /** + * Return the this contract's balance in the given RepoToken. + */ + function _getRepoTokenBalance(address repoToken) internal view returns (uint256) { + return ITermRepoToken(repoToken).balanceOf(address(this)); + } + + function _initializeRepoTokenListEmpty() internal { + _repoTokenList.head = RepoTokenList.NULL_NODE; + } + + /** + * Initialize _repoTokenList to a RepoTokenList of arbitrary size, where all + * items are distinct RepoTokens with symbolic storage. + */ + function _initializeRepoTokenList() internal { + address previous = RepoTokenList.NULL_NODE; + + while (kevm.freshBool() != 0) { + address current = _newRepoToken(); + + if (previous == RepoTokenList.NULL_NODE) { + _repoTokenList.head = current; + } else { + _repoTokenList.nodes[previous].next = current; + } + + previous = current; + } + + if (previous == RepoTokenList.NULL_NODE) { + _repoTokenList.head = RepoTokenList.NULL_NODE; + } else { + _repoTokenList.nodes[previous].next = RepoTokenList.NULL_NODE; + } + } + + /** + * Count the number of nodes in the list. + * + * Note that this function guarantees the following postconditions: + * - The head of the list is NULL_NODE iff the count is 0. + * - If the count is N, the Nth node in the list is followed by NULL_NODE. + */ + function _countNodesInList() internal view returns (uint256) { + uint256 count = 0; + address current = _repoTokenList.head; + + while (current != RepoTokenList.NULL_NODE) { + ++count; + current = _repoTokenList.nodes[current].next; + } + + return count; + } + + /** + * Return true if the given RepoToken is in the list, and false otherwise. + */ + function _repoTokenInList(address repoToken) internal view returns (bool) { + address current = _repoTokenList.head; + + while (current != RepoTokenList.NULL_NODE) { + if (current == repoToken) { + return true; + } + + current = _repoTokenList.nodes[current].next; + } + + return false; + } + + function _repoTokensListToArray(uint256 length) internal view returns (address[] memory repoTokens) { + address current = _repoTokenList.head; + uint256 i; + repoTokens = new address[](length); + + while (current != RepoTokenList.NULL_NODE) { + repoTokens[i++] = current; + current = _repoTokenList.nodes[current].next; + } + } + + /** + * Initialize the TermDiscountRateAdapter to a symbolic state, ensuring that + * it has a symbolic discount rate for every token in the RepoTokenList. + */ + function _initializeDiscountRateAdapter( + TermDiscountRateAdapter discountRateAdapter + ) internal { + discountRateAdapter.initializeSymbolic(); + + address current = _repoTokenList.head; + + while (current != RepoTokenList.NULL_NODE) { + discountRateAdapter.initializeSymbolicParamsFor(current); + + current = _repoTokenList.nodes[current].next; + } + } + + // Calculates the cumulative data assuming that no tokens have matured + function _cumulativeRepoTokenDataNotMatured( + ITermDiscountRateAdapter discountRateAdapter, + uint256 purchaseTokenPrecision + ) internal view returns ( + uint256 cumulativeWeightedTimeToMaturity, + uint256 cumulativeRepoTokenAmount + ) { + address current = _repoTokenList.head; + + while (current != RepoTokenList.NULL_NODE) { + (uint256 currentMaturity, , ,) = ITermRepoToken(current).config(); + uint256 repoTokenBalance = ITermRepoToken(current).balanceOf(address(this)); + uint256 repoRedemptionHaircut = discountRateAdapter.repoRedemptionHaircut(current); + uint256 timeToMaturity = currentMaturity - block.timestamp; + + uint256 repoTokenAmountInBaseAssetPrecision = + RepoTokenUtils.getNormalizedRepoTokenAmount( + current, + repoTokenBalance, + purchaseTokenPrecision, + repoRedemptionHaircut + ); + + uint256 weightedTimeToMaturity = + timeToMaturity * repoTokenAmountInBaseAssetPrecision; + + cumulativeWeightedTimeToMaturity += weightedTimeToMaturity; + cumulativeRepoTokenAmount += repoTokenAmountInBaseAssetPrecision; + + current = _repoTokenList.nodes[current].next; + } + } + + // Calculates the total present of matured tokens and removes them from the list + function _filterMaturedTokensGetTotalValue( + ITermDiscountRateAdapter discountRateAdapter, + uint256 purchaseTokenPrecision + ) internal returns (uint256) { + address current = _repoTokenList.head; + address prev = current; + uint256 totalPresentValue = 0; + + while (current != RepoTokenList.NULL_NODE) { + address next = _repoTokenList.nodes[current].next; + + (uint256 currentMaturity, , ,) = ITermRepoToken(current).config(); + + if (currentMaturity <= block.timestamp) { + uint256 repoTokenBalance = ITermRepoToken(current).balanceOf(address(this)); + uint256 repoRedemptionHaircut = discountRateAdapter.repoRedemptionHaircut(current); + + totalPresentValue += + RepoTokenUtils.getNormalizedRepoTokenAmount( + current, + repoTokenBalance, + purchaseTokenPrecision, + repoRedemptionHaircut + ); + + if (current == _repoTokenList.head) { + _repoTokenList.head = next; + } + else { + _repoTokenList.nodes[prev].next = next; + current = prev; + } + } + + prev = current; + current = next; + } + + return totalPresentValue; + } + + // Calculates the total present value for non matured tokens + function _totalPresentValueNotMatured( + ITermDiscountRateAdapter discountRateAdapter, + uint256 purchaseTokenPrecision + ) internal view returns (uint256) { + address current = _repoTokenList.head; + uint256 totalPresentValue = 0; + + while (current != RepoTokenList.NULL_NODE) { + (uint256 currentMaturity, , ,) = ITermRepoToken(current).config(); + uint256 repoTokenBalance = ITermRepoToken(current).balanceOf(address(this)); + uint256 repoRedemptionHaircut = discountRateAdapter.repoRedemptionHaircut(current); + uint256 discountRate = discountRateAdapter.getDiscountRate(current); + uint256 timeToMaturity = currentMaturity - block.timestamp; + + uint256 repoTokenAmountInBaseAssetPrecision = + RepoTokenUtils.getNormalizedRepoTokenAmount( + current, + repoTokenBalance, + purchaseTokenPrecision, + repoRedemptionHaircut + ); + + uint256 timeLeftToMaturityDayFraction = + (timeToMaturity * purchaseTokenPrecision) / 360 days; + + uint256 presentValue = + (repoTokenAmountInBaseAssetPrecision * purchaseTokenPrecision) / + (purchaseTokenPrecision + (discountRate * timeLeftToMaturityDayFraction / 1e18)); + + totalPresentValue += presentValue; + + current = _repoTokenList.nodes[current].next; + } + + return totalPresentValue; + } + + function _establishInsertListPreservation(address insertedRepoToken, address[] memory repoTokens, uint256 repoTokensCount) internal view { + address current = _repoTokenList.head; + uint256 i = 0; + + if(insertedRepoToken != address(0)) { + + while (current != RepoTokenList.NULL_NODE && i < repoTokensCount) { + if(current != repoTokens[i]) { + assert (current == insertedRepoToken); + current = _repoTokenList.nodes[current].next; + break; + } + i++; + current = _repoTokenList.nodes[current].next; + } + + if (current != RepoTokenList.NULL_NODE && i == repoTokensCount) { + assert (current == insertedRepoToken); + } + } + + while (current != RepoTokenList.NULL_NODE && i < repoTokensCount) { + assert(current == repoTokens[i++]); + current = _repoTokenList.nodes[current].next; + } + } + + function _establishRemoveListPreservation(address[] memory repoTokens, uint256 repoTokensCount) internal view { + address current = _repoTokenList.head; + uint256 i = 0; + + while (current != RepoTokenList.NULL_NODE && i < repoTokensCount) { + if(current == repoTokens[i++]) { + current = _repoTokenList.nodes[current].next; + } + } + + assert(current == RepoTokenList.NULL_NODE); + } + + /** + * Assume or assert that the tokens in the list are sorted by maturity. + */ + function _establishSortedByMaturity(Mode mode) internal view { + address previous = RepoTokenList.NULL_NODE; + address current = _repoTokenList.head; + + while (current != RepoTokenList.NULL_NODE) { + if (previous != RepoTokenList.NULL_NODE) { + uint256 previousMaturity = _getRepoTokenMaturity(previous); + uint256 currentMaturity = _getRepoTokenMaturity(current); + _establish(mode, previousMaturity <= currentMaturity); + } + + previous = current; + current = _repoTokenList.nodes[current].next; + } + } + + /** + * Assume or assert that there are no duplicate tokens in the list. + */ + function _establishNoDuplicateTokens(Mode mode) internal view { + address current = _repoTokenList.head; + + while (current != RepoTokenList.NULL_NODE) { + address other = _repoTokenList.nodes[current].next; + + while (other != RepoTokenList.NULL_NODE) { + _establish(mode, current != other); + other = _repoTokenList.nodes[other].next; + } + + current = _repoTokenList.nodes[current].next; + } + } + + /** + * Assume or assert that there are no tokens in the list have matured + * (i.e. all token maturities are greater than the current timestamp). + */ + function _establishNoMaturedTokens(Mode mode) internal view { + address current = _repoTokenList.head; + + while (current != RepoTokenList.NULL_NODE) { + uint256 currentMaturity = _getRepoTokenMaturity(current); + + _establish(mode, block.timestamp < currentMaturity); + + current = _repoTokenList.nodes[current].next; + } + } + + /** + * Assume or assert that all tokens in the list have balance > 0. + */ + function _establishPositiveBalance(Mode mode) internal view { + address current = _repoTokenList.head; + + while (current != RepoTokenList.NULL_NODE) { + uint256 repoTokenBalance = _getRepoTokenBalance(current); + + _establish(mode, 0 < repoTokenBalance); + + current = _repoTokenList.nodes[current].next; + } + } + + /** + * Weaker version of the above invariant that allows matured tokens to have + * a balance of 0. + * + * Note: This is equivalent to the above invariant if the NoMaturedTokens + * invariant also holds. + */ + function _establishPositiveBalanceForNonMaturedTokens(Mode mode) internal view { + address current = _repoTokenList.head; + + while (current != RepoTokenList.NULL_NODE) { + uint256 currentMaturity = _getRepoTokenMaturity(current); + uint256 repoTokenBalance = _getRepoTokenBalance(current); + + if (block.timestamp < currentMaturity) { + _establish(mode, 0 < repoTokenBalance); + } + + current = _repoTokenList.nodes[current].next; + } + } + + /** + * Configure the model of the RepoServicer for every token in the list to + * follow the assumption that redeemTermRepoTokens will not revert. + */ + function _guaranteeRedeemAlwaysSucceeds() internal { + address current = _repoTokenList.head; + + while (current != RepoTokenList.NULL_NODE) { + (, , address repoServicer,) = ITermRepoToken(current).config(); + TermRepoServicer(repoServicer).guaranteeRedeemAlwaysSucceeds(); + + current = _repoTokenList.nodes[current].next; + } + } +} \ No newline at end of file diff --git a/src/test/kontrol/TermAuctionListInvariants.t.sol b/src/test/kontrol/TermAuctionListInvariants.t.sol index ecca714c..c8c8826f 100644 --- a/src/test/kontrol/TermAuctionListInvariants.t.sol +++ b/src/test/kontrol/TermAuctionListInvariants.t.sol @@ -11,403 +11,24 @@ import "src/test/kontrol/Constants.sol"; import "src/test/kontrol/RepoToken.sol"; import "src/test/kontrol/RepoTokenListInvariants.t.sol"; import "src/test/kontrol/TermAuction.sol"; +import "src/test/kontrol/TermAuctionListTest.t.sol"; import "src/test/kontrol/TermAuctionOfferLocker.sol"; import "src/test/kontrol/TermDiscountRateAdapter.sol"; -contract TermAuctionListInvariantsTest is KontrolTest { +contract TermAuctionListInvariantsTest is RepoTokenListTest, TermAuctionListTest { using TermAuctionList for TermAuctionListData; using RepoTokenList for RepoTokenListData; - TermAuctionListData _termAuctionList; - address _referenceAuction; - RepoTokenListData _repoTokenList; - - uint256 private auctionListSlot; - function setUp() public { // Make storage of this contract completely symbolic kevm.symbolicStorage(address(this)); - // We will copy the code of this deployed auction contract - // into all auctions in the list - uint256 referenceAuctionSlot; - assembly { - referenceAuctionSlot := _referenceAuction.slot - sstore(auctionListSlot.slot, _termAuctionList.slot) - } - _storeUInt256(address(this), referenceAuctionSlot, uint256(uint160(address(new TermAuction())))); - - // For simplicity, assume that the RepoTokenList is empty - _repoTokenList.head = RepoTokenList.NULL_NODE; + _setReferenceAuction(); // Initialize TermAuctionList of arbitrary size _initializeTermAuctionList(); } - function auctionListOfferSlot(bytes32 offerId) internal view returns (uint256) { - return uint256(keccak256(abi.encodePacked(uint256(offerId), uint256(auctionListSlot + 2)))); - } - - /** - * Set pending offer using slot manipulation directly - */ - function setPendingOffer(bytes32 offerId, address repoToken, uint256 offerAmount, address auction, address offerLocker) internal { - uint256 offerSlot = auctionListOfferSlot(offerId); - _storeUInt256(address(this), offerSlot, uint256(uint160(repoToken))); - _storeUInt256(address(this), offerSlot + 1, offerAmount); - _storeUInt256(address(this), offerSlot + 2, uint256(uint160(auction))); - _storeUInt256(address(this), offerSlot + 3, uint256(uint160(offerLocker))); - } - - /** - * Return the auction for a given offer in the list. - */ - function _getAuction(bytes32 offerId) internal returns(address) { - return address(_termAuctionList.offers[offerId].termAuction); - } - - /** - * Deploy & initialize RepoToken and OfferLocker with the same RepoServicer - */ - function newRepoTokenAndOfferLocker() public returns ( - RepoToken repoToken, - TermAuctionOfferLocker offerLocker - ) { - repoToken = new RepoToken(); - repoToken.initializeSymbolic(); - (, , address termRepoServicer,) = repoToken.config(); - - offerLocker = new TermAuctionOfferLocker(); - offerLocker.initializeSymbolic(termRepoServicer); - } - - /** - * Initialize _termAuctionList to a TermAuctionList of arbitrary size, - * comprised of offers with distinct ids. - */ - function _initializeTermAuctionList() internal { - bytes32 previous = TermAuctionList.NULL_NODE; - uint256 count = 0; - - while (kevm.freshBool() != 0) { - (RepoToken repoToken, TermAuctionOfferLocker offerLocker) = - this.newRepoTokenAndOfferLocker(); - - // Assign each offer an ID based on Strategy._generateOfferId() - bytes32 current = keccak256( - abi.encodePacked(count, address(this), address(offerLocker)) - ); - // Register offer in offer locker - offerLocker.initializeSymbolicLockedOfferFor(current); - - if (previous == TermAuctionList.NULL_NODE) { - _termAuctionList.head = current; - } else { - _termAuctionList.nodes[previous].next = current; - } - - // Create sequential addresses to ensure that list is sorted - address auction = address(uint160(1000 + 2 * count)); - // Etch the code of the auction contract into this address - this.etch(auction, _referenceAuction); - TermAuction(auction).initializeSymbolic(); - - // Build PendingOffer - setPendingOffer(current, address(repoToken), freshUInt256(), auction, address(offerLocker)); - - previous = current; - ++count; - } - - if (previous == TermAuctionList.NULL_NODE) { - _termAuctionList.head = TermAuctionList.NULL_NODE; - } else { - _termAuctionList.nodes[previous].next = TermAuctionList.NULL_NODE; - } - } - - /** - * Initialize the TermDiscountRateAdapter to a symbolic state, ensuring that - * it has a symbolic discount rate for every token in the PendingOffers. - */ - function _initializeDiscountRateAdapter( - TermDiscountRateAdapter discountRateAdapter - ) internal { - discountRateAdapter.initializeSymbolic(); - - bytes32 current = _termAuctionList.head; - - while (current != TermAuctionList.NULL_NODE) { - address repoToken = _termAuctionList.offers[current].repoToken; - discountRateAdapter.initializeSymbolicParamsFor(repoToken); - - current = _termAuctionList.nodes[current].next; - } - } - - /** - * Assume or assert that the offers in the list are sorted by auction. - */ - function _establishSortedByAuctionId(Mode mode) internal { - bytes32 previous = TermAuctionList.NULL_NODE; - bytes32 current = _termAuctionList.head; - - while (current != TermAuctionList.NULL_NODE) { - if (previous != TermAuctionList.NULL_NODE) { - address previousAuction = _getAuction(previous); - address currentAuction = _getAuction(current); - _establish(mode, previousAuction <= currentAuction); - } - - previous = current; - current = _termAuctionList.nodes[current].next; - } - } - - /** - * Assume or assert that there are no duplicate offers in the list. - */ - function _establishNoDuplicateOffers(Mode mode) internal { - bytes32 current = _termAuctionList.head; - - while (current != TermAuctionList.NULL_NODE) { - bytes32 other = _termAuctionList.nodes[current].next; - - while (other != TermAuctionList.NULL_NODE) { - _establish(mode, current != other); - other = _termAuctionList.nodes[other].next; - } - - current = _termAuctionList.nodes[current].next; - } - } - - /** - * Assume or assert that there are no completed auctions in the list. - */ - function _establishNoCompletedOrCancelledAuctions(Mode mode) internal { - bytes32 current = _termAuctionList.head; - - while (current != TermAuctionList.NULL_NODE) { - PendingOffer storage offer = _termAuctionList.offers[current]; - _establish(mode, !offer.termAuction.auctionCompleted()); - _establish(mode, !offer.termAuction.auctionCancelledForWithdrawal()); - - current = _termAuctionList.nodes[current].next; - } - } - - /** - * Assume or assert that all offer amounts are > 0. - */ - function _establishPositiveOfferAmounts(Mode mode) internal { - bytes32 current = _termAuctionList.head; - - while (current != TermAuctionList.NULL_NODE) { - PendingOffer storage offer = _termAuctionList.offers[current]; - _establish(mode, 0 < offer.offerAmount); - - current = _termAuctionList.nodes[current].next; - } - } - - /** - * Assume or assert that the offer amounts recorded in the list are the same - * as the offer amounts in the offer locker. - */ - function _establishOfferAmountMatchesAmountLocked(Mode mode, bytes32 offerId) internal { - bytes32 current = _termAuctionList.head; - - while (current != TermAuctionList.NULL_NODE) { - if(offerId == 0 || offerId != current) { - PendingOffer storage offer = _termAuctionList.offers[current]; - uint256 offerAmount = TermAuctionOfferLocker(address(offer.offerLocker)).lockedOfferAmount(current); - _establish(mode, offer.offerAmount == offerAmount); - } - - current = _termAuctionList.nodes[current].next; - } - } - - /** - * Count the number of offers in the list. - * - * Note that this function guarantees the following postconditions: - * - The head of the list is NULL_NODE iff the count is 0. - * - If the count is N, the Nth node in the list is followed by NULL_NODE. - */ - function _countOffersInList() internal returns (uint256) { - uint256 count = 0; - bytes32 current = _termAuctionList.head; - - while (current != TermAuctionList.NULL_NODE) { - ++count; - current = _termAuctionList.nodes[current].next; - } - - return count; - } - - /** - * Return true if the given offer id is in the list, and false otherwise. - */ - function _offerInList(bytes32 offerId) internal returns (bool) { - bytes32 current = _termAuctionList.head; - - while (current != TermAuctionList.NULL_NODE) { - if (current == offerId) { - return true; - } - - current = _termAuctionList.nodes[current].next; - } - - return false; - } - - /** - * Assume that the address doesn't overlap with any preexisting addresses. - * This is necessary in order to use cheatcodes on a symbolic address that - * change its code or storage. - */ - function _assumeNewAddress(address freshAddress) internal { - vm.assume(10 <= uint160(freshAddress)); - - vm.assume(freshAddress != address(this)); - vm.assume(freshAddress != address(vm)); - vm.assume(freshAddress != address(kevm)); - - vm.assume(freshAddress != address(_referenceAuction)); - - bytes32 current = _termAuctionList.head; - - while (current != TermAuctionList.NULL_NODE) { - PendingOffer storage offer = _termAuctionList.offers[current]; - (,, address termRepoServicer, address termRepoCollateralManager) = - ITermRepoToken(offer.repoToken).config(); - - vm.assume(freshAddress != offer.repoToken); - vm.assume(freshAddress != address(offer.termAuction)); - vm.assume(freshAddress != address(offer.offerLocker)); - vm.assume(freshAddress != termRepoServicer); - vm.assume(freshAddress != termRepoCollateralManager); - - current = _termAuctionList.nodes[current].next; - } - } - - function _assumeRepoTokenValidate(address repoToken, address asset, bool assumeTimestamp) internal view { - ( - uint256 redemptionTimestamp, - address purchaseToken, - , - address collateralManager - ) = ITermRepoToken(repoToken).config(); - - vm.assume(purchaseToken == asset); - if(assumeTimestamp) { - vm.assume(block.timestamp <= redemptionTimestamp); - } - - uint256 numTokens = ITermRepoCollateralManager(collateralManager).numOfAcceptedCollateralTokens(); - - for (uint256 i; i < numTokens; i++) { - address currentToken = ITermRepoCollateralManager(collateralManager).collateralTokens(i); - uint256 minCollateralRatio = _repoTokenList.collateralTokenParams[currentToken]; - - vm.assume(minCollateralRatio != 0); - vm.assume(ITermRepoCollateralManager(collateralManager).maintenanceCollateralRatios(currentToken) >= minCollateralRatio); - } - } - - function _assumeRepoTokensValidate(address asset, bool assumeTimestamp) internal view { - bytes32 current = _termAuctionList.head; - - while (current != TermAuctionList.NULL_NODE) { - address repoToken = _termAuctionList.offers[current].repoToken; - if(assumeTimestamp) { - _assumeRepoTokenValidate(repoToken, asset, true); - } - else { - bool auctionCompleted = _termAuctionList.offers[current].termAuction.auctionCompleted(); - _assumeRepoTokenValidate(repoToken, asset, !auctionCompleted); - } - - current = _termAuctionList.nodes[current].next; - } - } - - function _assertRepoTokensValidate(address asset) internal view { - bytes32 current = _termAuctionList.head; - - while (current != TermAuctionList.NULL_NODE) { - address repoToken = _termAuctionList.offers[current].repoToken; - (bool isRepoTokenValid, ) = _repoTokenList.validateRepoToken(ITermRepoToken(repoToken), asset); - assert(isRepoTokenValid); - - current = _termAuctionList.nodes[current].next; - } - } - - function _termAuctionListToArray(uint256 length) internal view returns (bytes32[] memory offerIds) { - bytes32 current = _termAuctionList.head; - uint256 i; - offerIds = new bytes32[](length); - - while (current != TermAuctionList.NULL_NODE) { - offerIds[i++] = current; - current = _termAuctionList.nodes[current].next; - } - } - - function _establishInsertListPreservation(bytes32 newOfferId, bytes32[] memory offerIds, uint256 offerIdsCount) internal view { - bytes32 current = _termAuctionList.head; - uint256 i = 0; - - if(newOfferId != bytes32(0)) { - - while (current != TermAuctionList.NULL_NODE && i < offerIdsCount) { - if(current != offerIds[i]) { - assert (current == newOfferId); - current = _termAuctionList.nodes[current].next; - break; - } - i++; - current = _termAuctionList.nodes[current].next; - } - - if (current != TermAuctionList.NULL_NODE && i == offerIdsCount) { - assert (current == newOfferId); - } - } - - while (current != TermAuctionList.NULL_NODE && i < offerIdsCount) { - assert(current == offerIds[i++]); - current = _termAuctionList.nodes[current].next; - } - } - - function _establishRemoveListPreservation(bytes32[] memory offerIds, uint256 offerIdsCount) internal view { - bytes32 current = _termAuctionList.head; - uint256 i = 0; - - while (current != TermAuctionList.NULL_NODE && i < offerIdsCount) { - if(current == offerIds[i++]) { - current = _termAuctionList.nodes[current].next; - } - } - - assert(current == TermAuctionList.NULL_NODE); - } - - /** - * Etch the code at a given address to a given address in an external call, - * reducing memory consumption in the caller function - */ - function etch(address dest, address src) public { - vm.etch(dest, src.code); - } - /** * Test that insertPending preserves the list invariants when a new offer * is added (that was not present in the list before). @@ -552,34 +173,81 @@ contract TermAuctionListInvariantsTest is KontrolTest { } /** - * Configure the model of the OfferLocker for every offer in the list to - * follow the assumption that unlockOffers will not revert. + * Assume that all RepoTokens in the PendingOffers have no discount rate + * set in the RepoTokenList. */ - function _guaranteeUnlockAlwaysSucceeds() internal { + function _assumeNoDiscountRatesSet() internal view { + bytes32 current = _termAuctionList.head; + + while (current != TermAuctionList.NULL_NODE) { + address repoToken = _termAuctionList.offers[current].repoToken; + uint256 discountRate = _repoTokenList.discountRates[repoToken]; + vm.assume(discountRate == RepoTokenList.INVALID_AUCTION_RATE); + + current = _termAuctionList.nodes[current].next; + } + } + + function _assumeRepoTokenValidate(address repoToken, address asset, bool assumeTimestamp) internal view { + ( + uint256 redemptionTimestamp, + address purchaseToken, + , + address collateralManager + ) = ITermRepoToken(repoToken).config(); + + vm.assume(purchaseToken == asset); + if(assumeTimestamp) { + vm.assume(block.timestamp <= redemptionTimestamp); + } + + uint256 numTokens = ITermRepoCollateralManager(collateralManager).numOfAcceptedCollateralTokens(); + + for (uint256 i; i < numTokens; i++) { + address currentToken = ITermRepoCollateralManager(collateralManager).collateralTokens(i); + uint256 minCollateralRatio = _repoTokenList.collateralTokenParams[currentToken]; + + vm.assume(minCollateralRatio != 0); + vm.assume(ITermRepoCollateralManager(collateralManager).maintenanceCollateralRatios(currentToken) >= minCollateralRatio); + } + } + + function _assumeRepoTokensValidate(address asset, bool assumeTimestamp) internal view { bytes32 current = _termAuctionList.head; while (current != TermAuctionList.NULL_NODE) { - PendingOffer storage offer = _termAuctionList.offers[current]; - TermAuctionOfferLocker offerLocker = - TermAuctionOfferLocker(address(offer.offerLocker)); + address repoToken = _termAuctionList.offers[current].repoToken; + if(assumeTimestamp) { + _assumeRepoTokenValidate(repoToken, asset, true); + } + else { + bool auctionCompleted = _termAuctionList.offers[current].termAuction.auctionCompleted(); + _assumeRepoTokenValidate(repoToken, asset, !auctionCompleted); + } + + current = _termAuctionList.nodes[current].next; + } + } + + function _assertRepoTokensValidate(address asset) internal view { + bytes32 current = _termAuctionList.head; - offerLocker.guaranteeUnlockAlwaysSucceeds(); + while (current != TermAuctionList.NULL_NODE) { + address repoToken = _termAuctionList.offers[current].repoToken; + (bool isRepoTokenValid, ) = _repoTokenList.validateRepoToken(ITermRepoToken(repoToken), asset); + assert(isRepoTokenValid); current = _termAuctionList.nodes[current].next; } } - /** - * Assume that all RepoTokens in the PendingOffers have no discount rate - * set in the RepoTokenList. - */ - function _assumeNoDiscountRatesSet() internal { + function _guaranteeRedeemOfferRepoTokenAlwaysSucceeds() internal { bytes32 current = _termAuctionList.head; while (current != TermAuctionList.NULL_NODE) { address repoToken = _termAuctionList.offers[current].repoToken; - uint256 discountRate = _repoTokenList.discountRates[repoToken]; - vm.assume(discountRate == RepoTokenList.INVALID_AUCTION_RATE); + (, , address repoServicer,) = ITermRepoToken(repoToken).config(); + TermRepoServicer(repoServicer).guaranteeRedeemAlwaysSucceeds(); current = _termAuctionList.nodes[current].next; } @@ -589,10 +257,12 @@ contract TermAuctionListInvariantsTest is KontrolTest { * Test that removeCompleted preserves the list invariants. */ function testRemoveCompleted(address asset) external { + // For simplicity, assume that the RepoTokenList is empty + _repoTokenList.head = RepoTokenList.NULL_NODE; // Initialize a DiscountRateAdapter with symbolic storage TermDiscountRateAdapter discountRateAdapter = new TermDiscountRateAdapter(); - _initializeDiscountRateAdapter(discountRateAdapter); + _initializeDiscountRateAdapterOffers(discountRateAdapter); // Our initialization procedure guarantees these invariants, // so we assert instead of assuming @@ -637,4 +307,255 @@ contract TermAuctionListInvariantsTest is KontrolTest { _establishPositiveOfferAmounts(Mode.Assert); _assertRepoTokensValidate(asset); } + + function testGetCumulativeDataEmpty( + address repoToken, + uint256 newOfferAmount, + uint256 purchaseTokenPrecision + ) external { + _initializeTermAuctionListEmpty(); + + TermDiscountRateAdapter discountRateAdapter = + new TermDiscountRateAdapter(); + + ( + uint256 cumulativeWeightedTimeToMaturity, + uint256 cumulativeOfferAmount, + bool found + ) = _termAuctionList.getCumulativeOfferData( + _repoTokenList, + ITermDiscountRateAdapter(address(discountRateAdapter)), + repoToken, + newOfferAmount, + purchaseTokenPrecision + ); + + assert(cumulativeWeightedTimeToMaturity == 0); + assert(cumulativeOfferAmount == 0); + assert(found == false); + } + + function testGetPresentValueEmpty( + uint256 purchaseTokenPrecision, + address repoTokenToMatch + ) external { + _initializeTermAuctionListEmpty(); + + TermDiscountRateAdapter discountRateAdapter = + new TermDiscountRateAdapter(); + + uint256 totalPresentValue = _termAuctionList.getPresentValue( + _repoTokenList, + ITermDiscountRateAdapter(address(discountRateAdapter)), + purchaseTokenPrecision, + repoTokenToMatch + ); + + assert(totalPresentValue == 0); + } + + /* If there are no completed auctions in the list then getCumulativeOfferData should return the sum + of the amount in the lockedOffer for all offers + */ + function testGetCumulativeDataNoCompletedAuctions( + address repoToken, + uint256 newOfferAmount, + uint256 purchaseTokenPrecision + ) external { + // Initialize a DiscountRateAdapter with symbolic storage + TermDiscountRateAdapter discountRateAdapter = + new TermDiscountRateAdapter(); + _initializeDiscountRateAdapterOffers(discountRateAdapter); + + _establishNoCompletedAuctions(Mode.Assume); + _assumeOfferAmountLocked(); + + vm.assume(newOfferAmount < ETH_UPPER_BOUND); + vm.assume(purchaseTokenPrecision <= 18); + + ( + uint256 cumulativeWeightedTimeToMaturity, + uint256 cumulativeOfferAmount, + bool found + ) = _termAuctionList.getCumulativeOfferData( + _repoTokenList, + ITermDiscountRateAdapter(address(discountRateAdapter)), + repoToken, + newOfferAmount, + purchaseTokenPrecision + ); + + ( + uint256 cumulativeWeightedTimeToMaturityNoCompletedAuctions, + uint256 cumulativeOfferAmountNoCompletedAuctions, + bool foundNoCompletedAuctions + ) = _getCumulativeOfferTimeAndAmount( + repoToken, + newOfferAmount ); + + assert(cumulativeWeightedTimeToMaturity == cumulativeWeightedTimeToMaturityNoCompletedAuctions); + assert(cumulativeOfferAmount == cumulativeOfferAmountNoCompletedAuctions); + assert(found == foundNoCompletedAuctions); + + } + + /* If there are no completed auctions in the list then getCumulativeOfferData should return the sum + of the amount in the lockedOffer for all offers + */ + function testGetCumulativeDataCompletedAuctions( + address repoToken, + uint256 newOfferAmount, + uint256 purchaseTokenPrecision + ) external { + // Initialize a DiscountRateAdapter with symbolic storage + TermDiscountRateAdapter discountRateAdapter = + new TermDiscountRateAdapter(); + _initializeDiscountRateAdapterOffers(discountRateAdapter); + + _establishCompletedAuctions(Mode.Assume); + _assumeOfferAmountLocked(); + _assumeNoDiscountRatesSet(); + _assumeRedemptionValueAndBalancePositive(); + + // Consider only the case where we are not trying to match a token + vm.assume(repoToken == address(0)); + vm.assume(newOfferAmount < ETH_UPPER_BOUND); + vm.assume(purchaseTokenPrecision <= 18); + vm.assume(purchaseTokenPrecision > 0); + + ( + uint256 cumulativeWeightedTimeToMaturity, + uint256 cumulativeOfferAmount, + bool found + ) = _termAuctionList.getCumulativeOfferData( + _repoTokenList, + ITermDiscountRateAdapter(address(discountRateAdapter)), + repoToken, + newOfferAmount, + purchaseTokenPrecision + ); + + ( + uint256 cumulativeWeightedTimeToMaturityCompletedAuctions, + uint256 cumulativeOfferAmountCompletedAuctions + ) = _getGroupedOfferTimeAndAmount( + ITermDiscountRateAdapter(address(discountRateAdapter)), + purchaseTokenPrecision + ); + + assert(cumulativeWeightedTimeToMaturity == cumulativeWeightedTimeToMaturityCompletedAuctions); + assert(cumulativeOfferAmount == cumulativeOfferAmountCompletedAuctions); + } + + function _filterDiscountRateSet() internal { + bytes32 current = _termAuctionList.head; + bytes32 prev = current; + + while (current != TermAuctionList.NULL_NODE) { + bytes32 next = _termAuctionList.nodes[current].next; + + address repoToken = _termAuctionList.offers[current].repoToken; + uint256 discountRate = _repoTokenList.discountRates[repoToken]; + + if (discountRate != RepoTokenList.INVALID_AUCTION_RATE) { + // Update the list to remove the current node + delete _termAuctionList.nodes[current]; + delete _termAuctionList.offers[current]; + if (current == _termAuctionList.head) { + _termAuctionList.head = next; + } + else { + _termAuctionList.nodes[prev].next = next; + current = prev; + } + } + prev = current; + current = next; + } + } + + function testGetCumulativeOfferData( + address repoToken, + uint256 newOfferAmount, + uint256 purchaseTokenPrecision + ) external { + // Initialize a DiscountRateAdapter with symbolic storage + TermDiscountRateAdapter discountRateAdapter = + new TermDiscountRateAdapter(); + _initializeDiscountRateAdapterOffers(discountRateAdapter); + + _assumeNonMaturedRepoTokens(); + _assumeOfferAmountLocked(); + _assumeRedemptionValueAndBalancePositive(); + + // Consider only the case where we are not trying to match a token + vm.assume(repoToken == address(0)); + vm.assume(newOfferAmount < ETH_UPPER_BOUND); + vm.assume(purchaseTokenPrecision <= 18); + vm.assume(purchaseTokenPrecision > 0); + + ( + uint256 cumulativeWeightedTimeToMaturity, + uint256 cumulativeOfferAmount, + bool found + ) = _termAuctionList.getCumulativeOfferData( + _repoTokenList, + ITermDiscountRateAdapter(address(discountRateAdapter)), + repoToken, + newOfferAmount, + purchaseTokenPrecision + ); + + assert(!found); + + ( + uint256 cumulativeWeightedTimeToMaturityIncompletedAuctions, + uint256 cumulativeOfferAmountIncompletedAuctions + ) = _filterCompletedAuctionsGetCumulativeOfferData(); + + _filterDiscountRateSet(); + _filterRepeatedAuctions(); + + ( + uint256 cumulativeWeightedTimeToMaturityCompletedAuctions, + uint256 cumulativeOfferAmountCompletedAuctions + ) = _getCumulativeOfferDataCompletedAuctions(discountRateAdapter, purchaseTokenPrecision); + + assert(cumulativeWeightedTimeToMaturity == cumulativeWeightedTimeToMaturityIncompletedAuctions + cumulativeWeightedTimeToMaturityCompletedAuctions); + assert(cumulativeOfferAmount == cumulativeOfferAmountIncompletedAuctions + cumulativeOfferAmountCompletedAuctions); + } + + function testGetPresentTotalValue( + uint256 purchaseTokenPrecision, + address repoTokenToMatch + ) external { + // Initialize a DiscountRateAdapter with symbolic storage + TermDiscountRateAdapter discountRateAdapter = + new TermDiscountRateAdapter(); + _initializeDiscountRateAdapterOffers(discountRateAdapter); + + _assumeOfferAmountLocked(); + + // Consider only the case where we are not trying to match a token + vm.assume(repoTokenToMatch == address(0)); + vm.assume(purchaseTokenPrecision <= 18); + vm.assume(purchaseTokenPrecision > 0); + + uint256 totalPresentValue = _termAuctionList.getPresentValue( + _repoTokenList, + ITermDiscountRateAdapter(address(discountRateAdapter)), + purchaseTokenPrecision, + repoTokenToMatch + ); + + uint256 totalValueNonCompletedAuctions = _filterCompletedAuctionsGetTotalValue(); + + _filterDiscountRateSet(); + _filterRepeatedAuctions(); + + uint256 totalValueCompletedAuctions = _getTotalValueCompletedAuctions(ITermDiscountRateAdapter(address(discountRateAdapter)), purchaseTokenPrecision); + + assert(totalPresentValue == totalValueNonCompletedAuctions + totalValueCompletedAuctions); + } + } diff --git a/src/test/kontrol/TermAuctionListTest.t.sol b/src/test/kontrol/TermAuctionListTest.t.sol new file mode 100644 index 00000000..44661585 --- /dev/null +++ b/src/test/kontrol/TermAuctionListTest.t.sol @@ -0,0 +1,646 @@ +pragma solidity 0.8.23; + +import "forge-std/Vm.sol"; +import "forge-std/Test.sol"; +import "kontrol-cheatcodes/KontrolCheats.sol"; + +import "src/RepoTokenList.sol"; +import "src/TermAuctionList.sol"; + +import "src/test/kontrol/Constants.sol"; +import "src/test/kontrol/RepoToken.sol"; +import "src/test/kontrol/TermAuction.sol"; +import "src/test/kontrol/TermAuctionOfferLocker.sol"; +import "src/test/kontrol/TermDiscountRateAdapter.sol"; + + +contract TermAuctionListTest is KontrolTest { + using TermAuctionList for TermAuctionListData; + using RepoTokenList for RepoTokenListData; + + TermAuctionListData _termAuctionList; + address _referenceAuction; + + uint256 private _auctionListSlot; + + function _auctionListOfferSlot(bytes32 offerId) internal view returns (uint256) { + return uint256(keccak256(abi.encodePacked(uint256(offerId), uint256(_auctionListSlot + 2)))); + } + + function _setReferenceAuction() internal { + // We will copy the code of this deployed auction contract + // into all auctions in the list + uint256 referenceAuctionSlot; + assembly { + referenceAuctionSlot := _referenceAuction.slot + sstore(_auctionListSlot.slot, _termAuctionList.slot) + } + _storeUInt256(address(this), referenceAuctionSlot, uint256(uint160(address(new TermAuction())))); + } + + /** + * Set pending offer using slot manipulation directly + */ + function _setPendingOffer(bytes32 offerId, address repoToken, uint256 offerAmount, address auction, address offerLocker) internal { + uint256 offerSlot = _auctionListOfferSlot(offerId); + _storeUInt256(address(this), offerSlot, uint256(uint160(repoToken))); + _storeUInt256(address(this), offerSlot + 1, offerAmount); + _storeUInt256(address(this), offerSlot + 2, uint256(uint160(auction))); + _storeUInt256(address(this), offerSlot + 3, uint256(uint160(offerLocker))); + } + + /** + * Return the auction for a given offer in the list. + */ + function _getAuction(bytes32 offerId) internal view returns(address) { + return address(_termAuctionList.offers[offerId].termAuction); + } + + /** + * Deploy & initialize RepoToken and OfferLocker with the same RepoServicer + */ + function newRepoTokenAndOfferLocker() public returns ( + RepoToken repoToken, + TermAuctionOfferLocker offerLocker + ) { + repoToken = new RepoToken(); + repoToken.initializeSymbolic(); + (, , address termRepoServicer,) = repoToken.config(); + + offerLocker = new TermAuctionOfferLocker(); + offerLocker.initializeSymbolic(termRepoServicer); + } + + /** + * Etch the code at a given address to a given address in an external call, + * reducing memory consumption in the caller function + */ + function etch(address dest, address src) public { + vm.etch(dest, src.code); + } + + function _initializeTermAuctionListEmpty() internal { + _termAuctionList.head = TermAuctionList.NULL_NODE; + } + + /** + * Initialize _termAuctionList to a TermAuctionList of arbitrary size, + * comprised of offers with distinct ids. + */ + function _initializeTermAuctionList() internal { + bytes32 previous = TermAuctionList.NULL_NODE; + uint256 count = 0; + address auction; + RepoToken repoToken; + TermAuctionOfferLocker offerLocker; + + while (kevm.freshBool() != 0) { + // Create a new auction + if(count == 0 || kevm.freshBool() != 0) { + // Create sequential addresses to ensure that list is sorted + auction = address(uint160(1000 + 2 * count)); + // Etch the code of the auction contract into this address + this.etch(auction, _referenceAuction); + + TermAuction(auction).initializeSymbolic(); + (repoToken, offerLocker) = this.newRepoTokenAndOfferLocker(); + } + // Else the aution is the same as the previous one on the list + + // Assign each offer an ID based on Strategy._generateOfferId() + bytes32 current = keccak256( + abi.encodePacked(count, address(this), address(offerLocker)) + ); + // Register offer in offer locker + offerLocker.initializeSymbolicLockedOfferFor(current); + + if (previous == TermAuctionList.NULL_NODE) { + _termAuctionList.head = current; + } else { + _termAuctionList.nodes[previous].next = current; + } + + // Build PendingOffer + _setPendingOffer(current, address(repoToken), freshUInt256(), auction, address(offerLocker)); + + previous = current; + ++count; + } + + if (previous == TermAuctionList.NULL_NODE) { + _termAuctionList.head = TermAuctionList.NULL_NODE; + } else { + _termAuctionList.nodes[previous].next = TermAuctionList.NULL_NODE; + } + } + + /** + * Initialize the TermDiscountRateAdapter to a symbolic state, ensuring that + * it has a symbolic discount rate for every token in the PendingOffers. + */ + function _initializeDiscountRateAdapterOffers( + TermDiscountRateAdapter discountRateAdapter + ) internal { + discountRateAdapter.initializeSymbolic(); + + bytes32 current = _termAuctionList.head; + + while (current != TermAuctionList.NULL_NODE) { + address repoToken = _termAuctionList.offers[current].repoToken; + discountRateAdapter.initializeSymbolicParamsFor(repoToken); + + current = _termAuctionList.nodes[current].next; + } + } + + /** + * Assume or assert that there are no completed auctions in the list. + */ + function _establishNoCompletedAuctions(Mode mode) internal view { + bytes32 current = _termAuctionList.head; + + while (current != TermAuctionList.NULL_NODE) { + PendingOffer storage offer = _termAuctionList.offers[current]; + _establish(mode, !offer.termAuction.auctionCompleted()); + + current = _termAuctionList.nodes[current].next; + } + } + + /** + * Assume or assert that all auctions in the list are completed. + */ + function _establishCompletedAuctions(Mode mode) internal view { + bytes32 current = _termAuctionList.head; + + while (current != TermAuctionList.NULL_NODE) { + PendingOffer storage offer = _termAuctionList.offers[current]; + _establish(mode, offer.termAuction.auctionCompleted()); + + current = _termAuctionList.nodes[current].next; + } + } + + /** + * There are no matured tokens in the offers list + */ + function _assumeNonMaturedRepoTokens() internal view { + bytes32 current = _termAuctionList.head; + + while (current != TermAuctionList.NULL_NODE) { + (uint256 currentMaturity, , ,) = ITermRepoToken(_termAuctionList.offers[current].repoToken).config(); + vm.assume(currentMaturity > block.timestamp); + + current = _termAuctionList.nodes[current].next; + } + } + + /** + * Assume or assert that the offer amounts in the offer locker for completed auctions is 0 + * and for non-completed auctions is greater than 0 + */ + function _assumeOfferAmountLocked() internal view { + bytes32 current = _termAuctionList.head; + + while (current != TermAuctionList.NULL_NODE) { + PendingOffer storage offer = _termAuctionList.offers[current]; + uint256 offerAmount = TermAuctionOfferLocker(address(offer.offerLocker)).lockedOfferAmount(current); + if (offer.termAuction.auctionCompleted()) { + vm.assume(offerAmount == 0); + } + else { + vm.assume(offerAmount > 0); + } + + current = _termAuctionList.nodes[current].next; + } + } + + function _assumeRedemptionValueAndBalancePositive() internal view { + bytes32 current = _termAuctionList.head; + + while (current != TermAuctionList.NULL_NODE) { + address repoToken = _termAuctionList.offers[current].repoToken; + uint256 redemptionValue = ITermRepoToken(repoToken).redemptionValue(); + uint256 repoTokenBalance = ITermRepoToken(repoToken).balanceOf(address(this)); + vm.assume(0 < redemptionValue); + vm.assume(0 < repoTokenBalance); + + current = _termAuctionList.nodes[current].next; + } + } + + + function _filterCompletedAuctionsGetCumulativeOfferData() internal returns (uint256 cumulativeWeightedTimeToMaturity, uint256 cumulativeOfferAmount) { + bytes32 current = _termAuctionList.head; + bytes32 prev = current; + + while (current != TermAuctionList.NULL_NODE) { + bytes32 next = _termAuctionList.nodes[current].next; + + PendingOffer storage offer = _termAuctionList.offers[current]; + uint256 offerAmount = TermAuctionOfferLocker(address(offer.offerLocker)).lockedOfferAmount(current); + if (!offer.termAuction.auctionCompleted()) { + cumulativeWeightedTimeToMaturity += RepoTokenList.getRepoTokenWeightedTimeToMaturity(offer.repoToken, offerAmount); + cumulativeOfferAmount += offerAmount; + + // Update the list to remove the current node + delete _termAuctionList.nodes[current]; + delete _termAuctionList.offers[current]; + if (current == _termAuctionList.head) { + _termAuctionList.head = next; + } + else { + _termAuctionList.nodes[prev].next = next; + current = prev; + } + } + prev = current; + current = next; + } + } + + function _filterRepeatedAuctions() internal { + bytes32 current = _termAuctionList.head; + bytes32 prev = current; + address prevAuction = address(0); + + while (current != TermAuctionList.NULL_NODE) { + bytes32 next = _termAuctionList.nodes[current].next; + + address offerAuction = address(_termAuctionList.offers[current].termAuction); + if (offerAuction == prevAuction) { + // Update the list to remove the current node + delete _termAuctionList.nodes[current]; + delete _termAuctionList.offers[current]; + if (current == _termAuctionList.head) { + _termAuctionList.head = next; + } + else { + _termAuctionList.nodes[prev].next = next; + current = prev; + } + } + prevAuction = offerAuction; + prev = current; + current = next; + } + } + + + function _getCumulativeOfferTimeAndAmount( + address repoToken, + uint256 newOfferAmount + ) internal view returns (uint256 cumulativeWeightedTimeToMaturity, uint256 cumulativeOfferAmount, bool found) { + + bytes32 current = _termAuctionList.head; + + while (current != TermAuctionList.NULL_NODE) { + PendingOffer storage offer = _termAuctionList.offers[current]; + uint256 offerAmount; + + if (offer.repoToken == repoToken) { + offerAmount = newOfferAmount; + found = true; + } else { + offerAmount = offer.offerLocker.lockedOffer(current).amount; + } + + cumulativeWeightedTimeToMaturity += RepoTokenList.getRepoTokenWeightedTimeToMaturity(offer.repoToken, offerAmount); + cumulativeOfferAmount += offerAmount; + + current = _termAuctionList.nodes[current].next; + } + } + + function _getCumulativeOfferDataCompletedAuctions( + ITermDiscountRateAdapter discountRateAdapter, + uint256 purchaseTokenPrecision + ) internal view returns (uint256 cumulativeWeightedTimeToMaturity, uint256 cumulativeOfferAmount) { + + bytes32 current = _termAuctionList.head; + + while (current != TermAuctionList.NULL_NODE) { + PendingOffer storage offer = _termAuctionList.offers[current]; + uint256 offerAmount = RepoTokenUtils.getNormalizedRepoTokenAmount( + offer.repoToken, + ITermRepoToken(offer.repoToken).balanceOf(address(this)), + purchaseTokenPrecision, + discountRateAdapter.repoRedemptionHaircut(offer.repoToken) + ); + if (offerAmount > 0) { + cumulativeWeightedTimeToMaturity += RepoTokenList.getRepoTokenWeightedTimeToMaturity(offer.repoToken, offerAmount); + cumulativeOfferAmount += offerAmount; + } + + current = _termAuctionList.nodes[current].next; + } + } + + function _getGroupedOfferTimeAndAmount( + ITermDiscountRateAdapter discountRateAdapter, + uint256 purchaseTokenPrecision + ) internal view returns (uint256 cumulativeWeightedTimeToMaturity, uint256 cumulativeOfferAmount) { + + bytes32 current = _termAuctionList.head; + + address previous = address(0); + + while (current != TermAuctionList.NULL_NODE) { + PendingOffer storage offer = _termAuctionList.offers[current]; + uint256 offerAmount; + + if (address(offer.termAuction) != previous) { + offerAmount = RepoTokenUtils.getNormalizedRepoTokenAmount( + offer.repoToken, + ITermRepoToken(offer.repoToken).balanceOf(address(this)), + purchaseTokenPrecision, + discountRateAdapter.repoRedemptionHaircut(offer.repoToken) + ); + if (offerAmount > 0) { + cumulativeWeightedTimeToMaturity += RepoTokenList.getRepoTokenWeightedTimeToMaturity(offer.repoToken, offerAmount); + cumulativeOfferAmount += offerAmount; + } + } + + previous = address(offer.termAuction); + current = _termAuctionList.nodes[current].next; + } + } + + function _filterCompletedAuctionsGetTotalValue() internal returns (uint256 totalValue) { + bytes32 current = _termAuctionList.head; + bytes32 prev = current; + + while (current != TermAuctionList.NULL_NODE) { + bytes32 next = _termAuctionList.nodes[current].next; + + PendingOffer storage offer = _termAuctionList.offers[current]; + + if (!offer.termAuction.auctionCompleted()) { + totalValue += TermAuctionOfferLocker(address(offer.offerLocker)).lockedOfferAmount(current); + + // Update the list to remove the current node + delete _termAuctionList.nodes[current]; + delete _termAuctionList.offers[current]; + if (current == _termAuctionList.head) { + _termAuctionList.head = next; + } + else { + _termAuctionList.nodes[prev].next = next; + current = prev; + } + } + prev = current; + current = next; + } + } + + function _getTotalValueCompletedAuctions( + ITermDiscountRateAdapter discountRateAdapter, + uint256 purchaseTokenPrecision + ) internal view returns (uint256 totalValue) { + + bytes32 current = _termAuctionList.head; + + while (current != TermAuctionList.NULL_NODE) { + PendingOffer storage offer = _termAuctionList.offers[current]; + uint256 repoTokenAmountInBaseAssetPrecision = RepoTokenUtils.getNormalizedRepoTokenAmount( + offer.repoToken, + ITermRepoToken(offer.repoToken).balanceOf(address(this)), + purchaseTokenPrecision, + discountRateAdapter.repoRedemptionHaircut(offer.repoToken) + ); + totalValue += RepoTokenUtils.calculatePresentValue( + repoTokenAmountInBaseAssetPrecision, + purchaseTokenPrecision, + RepoTokenList.getRepoTokenMaturity(offer.repoToken), + discountRateAdapter.getDiscountRate(offer.repoToken) + ); + + current = _termAuctionList.nodes[current].next; + } + } + + /** + * Assume or assert that the offers in the list are sorted by auction. + */ + function _establishSortedByAuctionId(Mode mode) internal view { + bytes32 previous = TermAuctionList.NULL_NODE; + bytes32 current = _termAuctionList.head; + + while (current != TermAuctionList.NULL_NODE) { + if (previous != TermAuctionList.NULL_NODE) { + address previousAuction = _getAuction(previous); + address currentAuction = _getAuction(current); + _establish(mode, previousAuction <= currentAuction); + } + + previous = current; + current = _termAuctionList.nodes[current].next; + } + } + + /** + * Assume or assert that there are no duplicate offers in the list. + */ + function _establishNoDuplicateOffers(Mode mode) internal view { + bytes32 current = _termAuctionList.head; + + while (current != TermAuctionList.NULL_NODE) { + bytes32 other = _termAuctionList.nodes[current].next; + + while (other != TermAuctionList.NULL_NODE) { + _establish(mode, current != other); + other = _termAuctionList.nodes[other].next; + } + + current = _termAuctionList.nodes[current].next; + } + } + + /** + * Assume or assert that there are no completed auctions in the list. + */ + function _establishNoCompletedOrCancelledAuctions(Mode mode) internal view { + bytes32 current = _termAuctionList.head; + + while (current != TermAuctionList.NULL_NODE) { + PendingOffer storage offer = _termAuctionList.offers[current]; + _establish(mode, !offer.termAuction.auctionCompleted()); + _establish(mode, !offer.termAuction.auctionCancelledForWithdrawal()); + + current = _termAuctionList.nodes[current].next; + } + } + + /** + * Assume or assert that all offer amounts are > 0. + */ + function _establishPositiveOfferAmounts(Mode mode) internal view { + bytes32 current = _termAuctionList.head; + + while (current != TermAuctionList.NULL_NODE) { + PendingOffer storage offer = _termAuctionList.offers[current]; + _establish(mode, 0 < offer.offerAmount); + + current = _termAuctionList.nodes[current].next; + } + } + + /** + * Assume or assert that the offer amounts recorded in the list are the same + * as the offer amounts in the offer locker. + */ + function _establishOfferAmountMatchesAmountLocked(Mode mode, bytes32 offerId) internal view { + bytes32 current = _termAuctionList.head; + + while (current != TermAuctionList.NULL_NODE) { + if(offerId == 0 || offerId != current) { + PendingOffer storage offer = _termAuctionList.offers[current]; + uint256 offerAmount = TermAuctionOfferLocker(address(offer.offerLocker)).lockedOfferAmount(current); + _establish(mode, offer.offerAmount == offerAmount); + } + + current = _termAuctionList.nodes[current].next; + } + } + + /** + * Count the number of offers in the list. + * + * Note that this function guarantees the following postconditions: + * - The head of the list is NULL_NODE iff the count is 0. + * - If the count is N, the Nth node in the list is followed by NULL_NODE. + */ + function _countOffersInList() internal view returns (uint256) { + uint256 count = 0; + bytes32 current = _termAuctionList.head; + + while (current != TermAuctionList.NULL_NODE) { + ++count; + current = _termAuctionList.nodes[current].next; + } + + return count; + } + + /** + * Return true if the given offer id is in the list, and false otherwise. + */ + function _offerInList(bytes32 offerId) internal view returns (bool) { + bytes32 current = _termAuctionList.head; + + while (current != TermAuctionList.NULL_NODE) { + if (current == offerId) { + return true; + } + + current = _termAuctionList.nodes[current].next; + } + + return false; + } + + /** + * Assume that the address doesn't overlap with any preexisting addresses. + * This is necessary in order to use cheatcodes on a symbolic address that + * change its code or storage. + */ + function _assumeNewAddress(address freshAddress) internal view { + vm.assume(10 <= uint160(freshAddress)); + + vm.assume(freshAddress != address(this)); + vm.assume(freshAddress != address(vm)); + vm.assume(freshAddress != address(kevm)); + + vm.assume(freshAddress != address(_referenceAuction)); + + bytes32 current = _termAuctionList.head; + + while (current != TermAuctionList.NULL_NODE) { + PendingOffer storage offer = _termAuctionList.offers[current]; + (,, address termRepoServicer, address termRepoCollateralManager) = + ITermRepoToken(offer.repoToken).config(); + + vm.assume(freshAddress != offer.repoToken); + vm.assume(freshAddress != address(offer.termAuction)); + vm.assume(freshAddress != address(offer.offerLocker)); + vm.assume(freshAddress != termRepoServicer); + vm.assume(freshAddress != termRepoCollateralManager); + + current = _termAuctionList.nodes[current].next; + } + } + + + function _termAuctionListToArray(uint256 length) internal view returns (bytes32[] memory offerIds) { + bytes32 current = _termAuctionList.head; + uint256 i; + offerIds = new bytes32[](length); + + while (current != TermAuctionList.NULL_NODE) { + offerIds[i++] = current; + current = _termAuctionList.nodes[current].next; + } + } + + function _establishInsertListPreservation(bytes32 newOfferId, bytes32[] memory offerIds, uint256 offerIdsCount) internal view { + bytes32 current = _termAuctionList.head; + uint256 i = 0; + + if(newOfferId != bytes32(0)) { + + while (current != TermAuctionList.NULL_NODE && i < offerIdsCount) { + if(current != offerIds[i]) { + assert (current == newOfferId); + current = _termAuctionList.nodes[current].next; + break; + } + i++; + current = _termAuctionList.nodes[current].next; + } + + if (current != TermAuctionList.NULL_NODE && i == offerIdsCount) { + assert (current == newOfferId); + } + } + + while (current != TermAuctionList.NULL_NODE && i < offerIdsCount) { + assert(current == offerIds[i++]); + current = _termAuctionList.nodes[current].next; + } + } + + function _establishRemoveListPreservation(bytes32[] memory offerIds, uint256 offerIdsCount) internal view { + bytes32 current = _termAuctionList.head; + uint256 i = 0; + + while (current != TermAuctionList.NULL_NODE && i < offerIdsCount) { + if(current == offerIds[i++]) { + current = _termAuctionList.nodes[current].next; + } + } + + assert(current == TermAuctionList.NULL_NODE); + } + + /** + * Configure the model of the OfferLocker for every offer in the list to + * follow the assumption that unlockOffers will not revert. + */ + function _guaranteeUnlockAlwaysSucceeds() internal { + bytes32 current = _termAuctionList.head; + + while (current != TermAuctionList.NULL_NODE) { + PendingOffer storage offer = _termAuctionList.offers[current]; + TermAuctionOfferLocker offerLocker = + TermAuctionOfferLocker(address(offer.offerLocker)); + + offerLocker.guaranteeUnlockAlwaysSucceeds(); + + current = _termAuctionList.nodes[current].next; + } + } +} + diff --git a/src/test/kontrol/TermAuctionOfferLocker.sol b/src/test/kontrol/TermAuctionOfferLocker.sol index 0b5fb078..04bc52f9 100644 --- a/src/test/kontrol/TermAuctionOfferLocker.sol +++ b/src/test/kontrol/TermAuctionOfferLocker.sol @@ -16,7 +16,7 @@ contract TermAuctionOfferLocker is ITermAuctionOfferLocker, KontrolTest { return uint256(keccak256(abi.encodePacked(uint256(offerId), uint256(lockedOffersSlot)))); } - function initializeSymbolic(address termRepoServicer) public { + function initializeSymbolic(address termReposervicer) public { kevm.symbolicStorage(address(this)); // Clear slot which holds two contract fields uint256 repoServicerAndUnlockSlot; @@ -25,7 +25,7 @@ contract TermAuctionOfferLocker is ITermAuctionOfferLocker, KontrolTest { sstore(lockedOffersSlot.slot, _lockedOffers.slot) } _storeUInt256(address(this), repoServicerAndUnlockSlot, 0); - _termRepoServicer = termRepoServicer; + _termRepoServicer = termReposervicer; _unlockAlwaysSucceeds = false; } @@ -33,15 +33,6 @@ contract TermAuctionOfferLocker is ITermAuctionOfferLocker, KontrolTest { TermAuctionOffer storage offer = _lockedOffers[offerId]; offer.amount = freshUInt256(); vm.assume(offer.amount < ETH_UPPER_BOUND); - - uint256 _purchaseToken = uint160(kevm.freshAddress()); - uint256 _isRevealed = uint96(kevm.freshBool()); - bytes memory offerLastSlotAbi = abi.encodePacked(uint96(_isRevealed), uint160(_purchaseToken)); - bytes32 offerLastSlot; - assembly { - offerLastSlot := mload(add(offerLastSlotAbi, 0x20)) - } - _storeBytes32(address(this), lockedOfferSlot(offerId) + 5, offerLastSlot); } function lockedOfferAmount(bytes32 id) public view returns (uint256) { @@ -86,10 +77,9 @@ contract TermAuctionOfferLocker is ITermAuctionOfferLocker, KontrolTest { function lockOffers( TermAuctionOfferSubmission[] calldata offerSubmissions - ) external returns (bytes32[] memory) { - kevm.symbolicStorage(address(this)); + ) external view returns (bytes32[] memory) { - uint256 length = freshUInt256(); + uint256 length = offerSubmissions.length; bytes32[] memory offers = new bytes32[](length); for (uint256 i = 0; i < length; ++i) { @@ -105,7 +95,8 @@ contract TermAuctionOfferLocker is ITermAuctionOfferLocker, KontrolTest { require(kevm.freshBool() != 0); } - kevm.symbolicStorage(_termRepoServicer); - kevm.symbolicStorage(address(this)); + for (uint256 i = 0; i < offerIds.length; ++i) { + delete(_lockedOffers[offerIds[i]]); + } } } diff --git a/src/test/kontrol/TermDiscountRateAdapter.sol b/src/test/kontrol/TermDiscountRateAdapter.sol index ed1036c0..60831a83 100644 --- a/src/test/kontrol/TermDiscountRateAdapter.sol +++ b/src/test/kontrol/TermDiscountRateAdapter.sol @@ -14,9 +14,9 @@ contract TermDiscountRateAdapter is ITermDiscountRateAdapter, KontrolTest { } function initializeSymbolicParamsFor(address repoToken) public { - uint256 repoRedemptionHaircut = freshUInt256(); - vm.assume(repoRedemptionHaircut <= 1e18); - _repoRedemptionHaircut[repoToken] = repoRedemptionHaircut; + uint256 repoRedemptionhaircut = freshUInt256(); + vm.assume(repoRedemptionhaircut <= 1e18); + _repoRedemptionHaircut[repoToken] = repoRedemptionhaircut; uint256 discountRate = freshUInt256(); vm.assume(discountRate < ETH_UPPER_BOUND); diff --git a/src/test/kontrol/TermRepoServicer.sol b/src/test/kontrol/TermRepoServicer.sol index d2855fe2..235ecfe9 100644 --- a/src/test/kontrol/TermRepoServicer.sol +++ b/src/test/kontrol/TermRepoServicer.sol @@ -7,7 +7,7 @@ contract TermRepoServicer is ITermRepoServicer, KontrolTest { address _termRepoToken; bool _redeemAlwaysSucceeds; - function initializeSymbolic(address termRepoToken) public { + function initializeSymbolic(address termRepotoken) public { kevm.symbolicStorage(address(this)); // Clear slot which holds two contract fields uint256 repoTokenAndRedeemSlot; @@ -15,7 +15,7 @@ contract TermRepoServicer is ITermRepoServicer, KontrolTest { repoTokenAndRedeemSlot := _termRepoToken.slot } _storeUInt256(address(this), repoTokenAndRedeemSlot, 0); - _termRepoToken = termRepoToken; + _termRepoToken = termRepotoken; _redeemAlwaysSucceeds = false; } @@ -31,9 +31,6 @@ contract TermRepoServicer is ITermRepoServicer, KontrolTest { if (!_redeemAlwaysSucceeds) { require(kevm.freshBool() != 0); } - - kevm.symbolicStorage(_termRepoToken); - kevm.symbolicStorage(address(this)); } function termRepoToken() external view returns (address) {