From 802e6cb2c605d633a1ce9916a892252f5076feb0 Mon Sep 17 00:00:00 2001 From: lucasmt Date: Sun, 29 Sep 2024 18:48:46 -0500 Subject: [PATCH 01/16] Add tests for getCumulativeData and getPresentValue functions --- src/test/kontrol/RepoTokenListGet.t.sol | 234 ++++++++++++++++++++++ src/test/kontrol/TermAuctionListGet.t.sol | 118 +++++++++++ 2 files changed, 352 insertions(+) create mode 100644 src/test/kontrol/RepoTokenListGet.t.sol create mode 100644 src/test/kontrol/TermAuctionListGet.t.sol diff --git a/src/test/kontrol/RepoTokenListGet.t.sol b/src/test/kontrol/RepoTokenListGet.t.sol new file mode 100644 index 00000000..426e813d --- /dev/null +++ b/src/test/kontrol/RepoTokenListGet.t.sol @@ -0,0 +1,234 @@ +pragma solidity 0.8.23; + +import "src/test/kontrol/RepoTokenListInvariants.t.sol"; +import "src/test/kontrol/TermDiscountRateAdapter.sol"; + +contract RepoTokenGetTest is RepoTokenListInvariantsTest { + using RepoTokenList for RepoTokenListData; + + function _initializeRepoTokenListEmpty() internal { + _repoTokenList.head = RepoTokenList.NULL_NODE; + } + + 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); + } + + /** + * 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.initializeSymbolicFor(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(); + assert(currentMaturity > block.timestamp); + 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; + } + } + + function testGetCumulativeData( + address repoToken, + uint256 repoTokenAmount, + uint256 purchaseTokenPrecision + ) external { + // Initialize RepoTokenList of arbitrary size + kevm.symbolicStorage(address(this)); + _initializeRepoTokenList(); + + // Assume relevant invariants + _establishNoMaturedTokens(Mode.Assume); + _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); + + // Simplified calculation in the case no tokens have matured + ( + uint256 cumulativeWeightedTimeToMaturityNotMatured, + uint256 cumulativeRepoTokenAmountNotMatured + ) = _cumulativeRepoTokenDataNotMatured( + discountRateAdapter, + purchaseTokenPrecision + ); + + assert( + cumulativeWeightedTimeToMaturity == + cumulativeWeightedTimeToMaturityNotMatured + ); + + assert( + cumulativeRepoTokenAmount == + cumulativeRepoTokenAmountNotMatured + ); + } + + // Calculates the total present value assuming that no tokens have matured + 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(); + assert(currentMaturity > block.timestamp); + 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 testGetPresentValue( + uint256 purchaseTokenPrecision + ) external { + // Initialize RepoTokenList of arbitrary size + kevm.symbolicStorage(address(this)); + _initializeRepoTokenList(); + + // Assume relevant invariants + _establishNoMaturedTokens(Mode.Assume); + _establishPositiveBalance(Mode.Assume); + + // 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 + ); + + // Simplified calculation in the case no tokens have matured + uint256 totalPresentValueNotMatured = _totalPresentValueNotMatured( + discountRateAdapter, + purchaseTokenPrecision + ); + + assert(totalPresentValue == totalPresentValueNotMatured); + } +} diff --git a/src/test/kontrol/TermAuctionListGet.t.sol b/src/test/kontrol/TermAuctionListGet.t.sol new file mode 100644 index 00000000..2c1b998d --- /dev/null +++ b/src/test/kontrol/TermAuctionListGet.t.sol @@ -0,0 +1,118 @@ +pragma solidity 0.8.23; + +import "src/test/kontrol/TermAuctionListInvariants.t.sol"; + +contract TermAuctionListGetTest is TermAuctionListInvariantsTest { + using TermAuctionList for TermAuctionListData; + + function _initializeTermAuctionListEmpty() internal { + _termAuctionList.head = TermAuctionList.NULL_NODE; + } + + 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); + } + + function testGetCumulativeData( + address repoToken, + uint256 newOfferAmount, + uint256 purchaseTokenPrecision + ) external { + // Initialize a DiscountRateAdapter with symbolic storage + TermDiscountRateAdapter discountRateAdapter = + new TermDiscountRateAdapter(); + _initializeDiscountRateAdapter(discountRateAdapter); + + // Assume relevant invariants + _establishNoMaturedTokens(Mode.Assume); + _establishPositiveBalance(Mode.Assume); + + // 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); + + ( + uint256 cumulativeWeightedTimeToMaturity, + uint256 cumulativeOfferAmount, + bool found + ) = _termAuctionList.getCumulativeOfferData( + _repoTokenList, + ITermDiscountRateAdapter(address(discountRateAdapter)), + repoToken, + newOfferAmount, + purchaseTokenPrecision + ); + + // TODO: Add checks that calculation is correct + } + + function testGetPresentValue( + uint256 purchaseTokenPrecision, + address repoTokenToMatch + ) external { + // Initialize a DiscountRateAdapter with symbolic storage + TermDiscountRateAdapter discountRateAdapter = + new TermDiscountRateAdapter(); + _initializeDiscountRateAdapter(discountRateAdapter); + + // Assume relevant invariants + _establishNoMaturedTokens(Mode.Assume); + _establishPositiveBalance(Mode.Assume); + + // Consider only the case where we are not trying to match a token + vm.assume(repoTokenToMatch == address(0)); + vm.assume(purchaseTokenPrecision <= 18); + + uint256 totalPresentValue = _termAuctionList.getPresentValue( + _repoTokenList, + ITermDiscountRateAdapter(address(discountRateAdapter)), + purchaseTokenPrecision, + repoTokenToMatch + ); + + // TODO: Add checks that calculation is correct + } +} From acb915fedfc05dcc837c34e7ceb1adc3be92571b Mon Sep 17 00:00:00 2001 From: Lisandra Date: Mon, 21 Oct 2024 14:15:12 +0100 Subject: [PATCH 02/16] Restructured contracts --- kontrol.toml | 3 + src/test/kontrol/ListTestUtils.t.sol | 299 ++++++++++++++++++ src/test/kontrol/RepoTokenListGet.t.sol | 2 +- .../kontrol/RepoTokenListInvariants.t.sol | 145 +-------- src/test/kontrol/TermAuctionListGet.t.sol | 17 +- .../kontrol/TermAuctionListInvariants.t.sol | 131 +------- src/test/kontrol/TermAuctionOfferLocker.sol | 17 +- 7 files changed, 328 insertions(+), 286 deletions(-) create mode 100644 src/test/kontrol/ListTestUtils.t.sol diff --git a/kontrol.toml b/kontrol.toml index df91602d..3ca95b85 100644 --- a/kontrol.toml +++ b/kontrol.toml @@ -42,6 +42,7 @@ bmc-depth = 3 match-test = [ "RepoTokenListInvariantsTest.setUp", "TermAuctionListInvariantsTest.setUp", + "TermAuctionListGetTest.setUp", ] ast = true @@ -81,6 +82,8 @@ match-test = [ "TermAuctionListInvariantsTest.testInsertPendingNewOffer", "TermAuctionListInvariantsTest.testInsertPendingDuplicateOffer", "TermAuctionListInvariantsTest.testRemoveCompleted", + "TermAuctionListGetTest.testGetCumulativeDataEmpty", + "TermAuctionListGetTest.testGetPresentValueEmpty", ] ast = true diff --git a/src/test/kontrol/ListTestUtils.t.sol b/src/test/kontrol/ListTestUtils.t.sol new file mode 100644 index 00000000..c29dfb86 --- /dev/null +++ b/src/test/kontrol/ListTestUtils.t.sol @@ -0,0 +1,299 @@ +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 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; + } + } +} + +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 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); + } + + /** + * 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 _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; + } + } + +} + diff --git a/src/test/kontrol/RepoTokenListGet.t.sol b/src/test/kontrol/RepoTokenListGet.t.sol index 426e813d..06a7037d 100644 --- a/src/test/kontrol/RepoTokenListGet.t.sol +++ b/src/test/kontrol/RepoTokenListGet.t.sol @@ -64,7 +64,7 @@ contract RepoTokenGetTest is RepoTokenListInvariantsTest { address current = _repoTokenList.head; while (current != RepoTokenList.NULL_NODE) { - discountRateAdapter.initializeSymbolicFor(current); + discountRateAdapter.initializeSymbolicParamsFor(current); current = _repoTokenList.nodes[current].next; } diff --git a/src/test/kontrol/RepoTokenListInvariants.t.sol b/src/test/kontrol/RepoTokenListInvariants.t.sol index c243a85c..f98607a8 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/ListTestUtils.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,146 +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. * diff --git a/src/test/kontrol/TermAuctionListGet.t.sol b/src/test/kontrol/TermAuctionListGet.t.sol index 2c1b998d..d6377fd2 100644 --- a/src/test/kontrol/TermAuctionListGet.t.sol +++ b/src/test/kontrol/TermAuctionListGet.t.sol @@ -1,9 +1,22 @@ pragma solidity 0.8.23; -import "src/test/kontrol/TermAuctionListInvariants.t.sol"; +import "src/test/kontrol/TermAuction.sol"; +import "src/test/kontrol/ListTestUtils.t.sol"; -contract TermAuctionListGetTest is TermAuctionListInvariantsTest { +contract TermAuctionListGetTest is RepoTokenListTest, TermAuctionListTest { using TermAuctionList for TermAuctionListData; + using RepoTokenList for RepoTokenListData; + + function setUp() public { + // Make storage of this contract completely symbolic + kevm.symbolicStorage(address(this)); + // Initialize RepoTokenList of arbitrary size + _initializeRepoTokenList(); + setReferenceAuction(); + + // Initialize TermAuctionList of arbitrary size + _initializeTermAuctionList(); + } function _initializeTermAuctionListEmpty() internal { _termAuctionList.head = TermAuctionList.NULL_NODE; diff --git a/src/test/kontrol/TermAuctionListInvariants.t.sol b/src/test/kontrol/TermAuctionListInvariants.t.sol index ecca714c..e1389591 100644 --- a/src/test/kontrol/TermAuctionListInvariants.t.sol +++ b/src/test/kontrol/TermAuctionListInvariants.t.sol @@ -14,137 +14,20 @@ import "src/test/kontrol/TermAuction.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. */ @@ -400,14 +283,6 @@ contract TermAuctionListInvariantsTest is KontrolTest { 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). @@ -589,6 +464,8 @@ 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(); diff --git a/src/test/kontrol/TermAuctionOfferLocker.sol b/src/test/kontrol/TermAuctionOfferLocker.sol index 0b5fb078..4d0990a6 100644 --- a/src/test/kontrol/TermAuctionOfferLocker.sol +++ b/src/test/kontrol/TermAuctionOfferLocker.sol @@ -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) { @@ -87,9 +78,8 @@ contract TermAuctionOfferLocker is ITermAuctionOfferLocker, KontrolTest { function lockOffers( TermAuctionOfferSubmission[] calldata offerSubmissions ) external returns (bytes32[] memory) { - kevm.symbolicStorage(address(this)); - 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]]); + } } } From 0b391425f59dd77175592faa2c639b05a79ebbd0 Mon Sep 17 00:00:00 2001 From: Petar Maksimovic Date: Mon, 21 Oct 2024 14:20:33 +0100 Subject: [PATCH 03/16] adding fine-grained slot update functions --- src/test/kontrol/KontrolTest.sol | 64 ++++++++++++++++++++++++++++---- 1 file changed, 56 insertions(+), 8 deletions(-) diff --git a/src/test/kontrol/KontrolTest.sol b/src/test/kontrol/KontrolTest.sol index 1cb57cba..d8622efe 100644 --- a/src/test/kontrol/KontrolTest.sol +++ b/src/test/kontrol/KontrolTest.sol @@ -35,24 +35,72 @@ 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 { From 4c08fcc9cfb0f11c843c19161af32f9439c8592d Mon Sep 17 00:00:00 2001 From: Lisandra Date: Tue, 22 Oct 2024 11:41:55 +0100 Subject: [PATCH 04/16] Added test getCumulativeOfferDataNoCompletedAuctions --- src/test/kontrol/TermAuctionListGet.t.sol | 92 ++++++++++++++++++++++- 1 file changed, 91 insertions(+), 1 deletion(-) diff --git a/src/test/kontrol/TermAuctionListGet.t.sol b/src/test/kontrol/TermAuctionListGet.t.sol index d6377fd2..4749f8b8 100644 --- a/src/test/kontrol/TermAuctionListGet.t.sol +++ b/src/test/kontrol/TermAuctionListGet.t.sol @@ -11,7 +11,7 @@ contract TermAuctionListGetTest is RepoTokenListTest, TermAuctionListTest { // Make storage of this contract completely symbolic kevm.symbolicStorage(address(this)); // Initialize RepoTokenList of arbitrary size - _initializeRepoTokenList(); + //_initializeRepoTokenList(); setReferenceAuction(); // Initialize TermAuctionList of arbitrary size @@ -68,6 +68,96 @@ contract TermAuctionListGetTest is RepoTokenListTest, TermAuctionListTest { assert(totalPresentValue == 0); } + /** + * Assume or assert that there are no completed auctions in the list. + */ + function _establishNoCompletedAuctions(Mode mode) internal { + 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; + } + } + + function getCumulativeOfferDataNoCompletedAuctions( + RepoTokenListData storage repoTokenListData, + ITermDiscountRateAdapter discountRateAdapter, + address repoToken, + uint256 newOfferAmount, + uint256 purchaseTokenPrecision + ) 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; + } + } + + /* 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(); + _initializeDiscountRateAdapter(discountRateAdapter); + + _establishNoCompletedAuctions(Mode.Assume); + + 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 + ) = getCumulativeOfferDataNoCompletedAuctions( + _repoTokenList, + ITermDiscountRateAdapter(address(discountRateAdapter)), + repoToken, + newOfferAmount, + purchaseTokenPrecision + ); + + assert(cumulativeWeightedTimeToMaturity == cumulativeWeightedTimeToMaturityNoCompletedAuctions); + assert(cumulativeOfferAmount == cumulativeOfferAmountNoCompletedAuctions); + assert(found == foundNoCompletedAuctions); + + } + function testGetCumulativeData( address repoToken, uint256 newOfferAmount, From 5dfed779c88a98bb74bd3245c980168d74a9608c Mon Sep 17 00:00:00 2001 From: Lisandra Date: Tue, 22 Oct 2024 14:48:45 +0100 Subject: [PATCH 05/16] Updated comment --- src/RepoTokenList.sol | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/RepoTokenList.sol b/src/RepoTokenList.sol index 5d87fb4a..48c83f3f 100644 --- a/src/RepoTokenList.sol +++ b/src/RepoTokenList.sol @@ -409,7 +409,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; From 3e7d8235a58c2ab81de7c306221f5108cb541a3d Mon Sep 17 00:00:00 2001 From: Lisandra Date: Tue, 22 Oct 2024 14:50:35 +0100 Subject: [PATCH 06/16] Wip --- kontrol.toml | 21 +++--- src/test/kontrol/ListTestUtils.t.sol | 16 +++++ src/test/kontrol/TermAuctionListGet.t.sol | 86 ++++++++++++++++++++++- 3 files changed, 110 insertions(+), 13 deletions(-) diff --git a/kontrol.toml b/kontrol.toml index 3ca95b85..ba46cf86 100644 --- a/kontrol.toml +++ b/kontrol.toml @@ -40,8 +40,8 @@ auto_abstract = true run-constructor = false bmc-depth = 3 match-test = [ - "RepoTokenListInvariantsTest.setUp", - "TermAuctionListInvariantsTest.setUp", + #"RepoTokenListInvariantsTest.setUp", + #"TermAuctionListInvariantsTest.setUp", "TermAuctionListGetTest.setUp", ] ast = true @@ -76,14 +76,15 @@ break-on-cheatcodes = false auto_abstract = true run-constructor = false match-test = [ - "RepoTokenListInvariantsTest.testInsertSortedNewToken", - "RepoTokenListInvariantsTest.testInsertSortedDuplicateToken", - "RepoTokenListInvariantsTest.testRemoveAndRedeemMaturedTokens", - "TermAuctionListInvariantsTest.testInsertPendingNewOffer", - "TermAuctionListInvariantsTest.testInsertPendingDuplicateOffer", - "TermAuctionListInvariantsTest.testRemoveCompleted", - "TermAuctionListGetTest.testGetCumulativeDataEmpty", - "TermAuctionListGetTest.testGetPresentValueEmpty", + #"RepoTokenListInvariantsTest.testInsertSortedNewToken", + #"RepoTokenListInvariantsTest.testInsertSortedDuplicateToken", + #"RepoTokenListInvariantsTest.testRemoveAndRedeemMaturedTokens", + #"TermAuctionListInvariantsTest.testInsertPendingNewOffer", + #"TermAuctionListInvariantsTest.testInsertPendingDuplicateOffer", + #"TermAuctionListInvariantsTest.testRemoveCompleted", + #"TermAuctionListGetTest.testGetCumulativeDataEmpty", + #"TermAuctionListGetTest.testGetPresentValueEmpty", + "TermAuctionListGetTest.testGetCumulativeDataNoCompletedAuctions", ] ast = true diff --git a/src/test/kontrol/ListTestUtils.t.sol b/src/test/kontrol/ListTestUtils.t.sol index c29dfb86..383b384c 100644 --- a/src/test/kontrol/ListTestUtils.t.sol +++ b/src/test/kontrol/ListTestUtils.t.sol @@ -295,5 +295,21 @@ contract TermAuctionListTest is KontrolTest { } } + /** + * Assume that all RepoTokens in the PendingOffers have no discount rate + * set in the RepoTokenList. + */ + function _assumeNoDiscountRatesSet() 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); + + current = _termAuctionList.nodes[current].next; + } + } + } diff --git a/src/test/kontrol/TermAuctionListGet.t.sol b/src/test/kontrol/TermAuctionListGet.t.sol index 4749f8b8..69edc522 100644 --- a/src/test/kontrol/TermAuctionListGet.t.sol +++ b/src/test/kontrol/TermAuctionListGet.t.sol @@ -12,8 +12,8 @@ contract TermAuctionListGetTest is RepoTokenListTest, TermAuctionListTest { kevm.symbolicStorage(address(this)); // Initialize RepoTokenList of arbitrary size //_initializeRepoTokenList(); - setReferenceAuction(); + setReferenceAuction(); // Initialize TermAuctionList of arbitrary size _initializeTermAuctionList(); } @@ -82,7 +82,39 @@ contract TermAuctionListGetTest is RepoTokenListTest, TermAuctionListTest { } } - function getCumulativeOfferDataNoCompletedAuctions( + /** + * Assume or assert that all auctions in the list are completed. + */ + function _establishCompletedAuctions(Mode mode) internal { + 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 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 = _termAuctionList.head; + + while (current != RepoTokenList.NULL_NODE) { + PendingOffer storage offer = _termAuctionList.offers[current]; + uint256 currentMaturity = _getRepoTokenMaturity(offer.repoToken); + + _establish(mode, block.timestamp < currentMaturity); + + current = _termAuctionList.nodes[current].next; + } + } + + + function getCumulativeOfferTimeAndAmount( RepoTokenListData storage repoTokenListData, ITermDiscountRateAdapter discountRateAdapter, address repoToken, @@ -144,7 +176,55 @@ contract TermAuctionListGetTest is RepoTokenListTest, TermAuctionListTest { uint256 cumulativeWeightedTimeToMaturityNoCompletedAuctions, uint256 cumulativeOfferAmountNoCompletedAuctions, bool foundNoCompletedAuctions - ) = getCumulativeOfferDataNoCompletedAuctions( + ) = getCumulativeOfferTimeAndAmount( + _repoTokenList, + ITermDiscountRateAdapter(address(discountRateAdapter)), + repoToken, + newOfferAmount, + purchaseTokenPrecision + ); + + 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(); + _initializeDiscountRateAdapter(discountRateAdapter); + + _establishCompletedAuctions(Mode.Assume); + + 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( _repoTokenList, ITermDiscountRateAdapter(address(discountRateAdapter)), repoToken, From 0e74dd7f8806fc80f638fcb1cdc0d98ff0f15010 Mon Sep 17 00:00:00 2001 From: Lisandra Date: Tue, 22 Oct 2024 15:17:37 +0100 Subject: [PATCH 07/16] Added new test testGetCumulativeDataCompletedAuctions --- src/test/kontrol/ListTestUtils.t.sol | 16 ----- src/test/kontrol/TermAuctionListGet.t.sol | 82 ++++++++++++++++------- 2 files changed, 58 insertions(+), 40 deletions(-) diff --git a/src/test/kontrol/ListTestUtils.t.sol b/src/test/kontrol/ListTestUtils.t.sol index 383b384c..c29dfb86 100644 --- a/src/test/kontrol/ListTestUtils.t.sol +++ b/src/test/kontrol/ListTestUtils.t.sol @@ -295,21 +295,5 @@ contract TermAuctionListTest is KontrolTest { } } - /** - * Assume that all RepoTokens in the PendingOffers have no discount rate - * set in the RepoTokenList. - */ - function _assumeNoDiscountRatesSet() 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); - - current = _termAuctionList.nodes[current].next; - } - } - } diff --git a/src/test/kontrol/TermAuctionListGet.t.sol b/src/test/kontrol/TermAuctionListGet.t.sol index 69edc522..f9168fa1 100644 --- a/src/test/kontrol/TermAuctionListGet.t.sol +++ b/src/test/kontrol/TermAuctionListGet.t.sol @@ -96,23 +96,6 @@ contract TermAuctionListGetTest is RepoTokenListTest, TermAuctionListTest { } } - /** - * 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 = _termAuctionList.head; - - while (current != RepoTokenList.NULL_NODE) { - PendingOffer storage offer = _termAuctionList.offers[current]; - uint256 currentMaturity = _getRepoTokenMaturity(offer.repoToken); - - _establish(mode, block.timestamp < currentMaturity); - - current = _termAuctionList.nodes[current].next; - } - } - function getCumulativeOfferTimeAndAmount( RepoTokenListData storage repoTokenListData, @@ -142,6 +125,38 @@ contract TermAuctionListGetTest is RepoTokenListTest, TermAuctionListTest { } } + function getGroupedOfferTimeAndAmount( + RepoTokenListData storage repoTokenListData, + ITermDiscountRateAdapter discountRateAdapter, + address repoToken, + uint256 newOfferAmount, + uint256 purchaseTokenPrecision + ) internal view returns (uint256 cumulativeWeightedTimeToMaturity, uint256 cumulativeOfferAmount, bool found) { + + 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) + ); + cumulativeWeightedTimeToMaturity += RepoTokenList.getRepoTokenWeightedTimeToMaturity(offer.repoToken, offerAmount); + cumulativeOfferAmount += offerAmount; + } + + previous = address(offer.termAuction); + current = _termAuctionList.nodes[current].next; + } + } + /* If there are no completed auctions in the list then getCumulativeOfferData should return the sum of the amount in the lockedOffer for all offers */ @@ -190,6 +205,22 @@ contract TermAuctionListGetTest is RepoTokenListTest, TermAuctionListTest { } + /** + * Assume that all RepoTokens in the PendingOffers have no discount rate + * set in the RepoTokenList. + */ + function _assumeNoDiscountRatesSet() 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); + + current = _termAuctionList.nodes[current].next; + } + } + /* If there are no completed auctions in the list then getCumulativeOfferData should return the sum of the amount in the lockedOffer for all offers */ @@ -204,7 +235,10 @@ contract TermAuctionListGetTest is RepoTokenListTest, TermAuctionListTest { _initializeDiscountRateAdapter(discountRateAdapter); _establishCompletedAuctions(Mode.Assume); + _assumeNoDiscountRatesSet(); + // 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); @@ -221,10 +255,10 @@ contract TermAuctionListGetTest is RepoTokenListTest, TermAuctionListTest { ); ( - uint256 cumulativeWeightedTimeToMaturityNoCompletedAuctions, - uint256 cumulativeOfferAmountNoCompletedAuctions, - bool foundNoCompletedAuctions - ) = getCumulativeOfferTimeAndAmount( + uint256 cumulativeWeightedTimeToMaturityCompletedAuctions, + uint256 cumulativeOfferAmountCompletedAuctions, + bool foundCompletedAuctions + ) = getGroupedOfferTimeAndAmount( _repoTokenList, ITermDiscountRateAdapter(address(discountRateAdapter)), repoToken, @@ -232,9 +266,9 @@ contract TermAuctionListGetTest is RepoTokenListTest, TermAuctionListTest { purchaseTokenPrecision ); - assert(cumulativeWeightedTimeToMaturity == cumulativeWeightedTimeToMaturityNoCompletedAuctions); - assert(cumulativeOfferAmount == cumulativeOfferAmountNoCompletedAuctions); - assert(found == foundNoCompletedAuctions); + assert(cumulativeWeightedTimeToMaturity == cumulativeWeightedTimeToMaturityCompletedAuctions); + assert(cumulativeOfferAmount == cumulativeOfferAmountCompletedAuctions); + assert(found == foundCompletedAuctions); } From e78c81d394452f714c66ca6078e467b4f1397898 Mon Sep 17 00:00:00 2001 From: Lisandra Date: Wed, 23 Oct 2024 11:25:25 +0100 Subject: [PATCH 08/16] Removed unused variable --- src/TermAuctionList.sol | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/TermAuctionList.sol b/src/TermAuctionList.sol index 8da98509..555f8ecb 100644 --- a/src/TermAuctionList.sol +++ b/src/TermAuctionList.sol @@ -175,7 +175,6 @@ library TermAuctionList { uint256 offerAmount = offer.offerLocker.lockedOffer(current).amount; bool removeNode; - bool insertRepoToken; if (offer.termAuction.auctionCompleted()) { // If auction is completed and closed, mark for removal and prepare to insert repo token @@ -343,7 +342,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( From 4c0a615482785cdc65d46bb4e1e18abcac5f3fb8 Mon Sep 17 00:00:00 2001 From: Lisandra Date: Wed, 23 Oct 2024 16:26:52 +0100 Subject: [PATCH 09/16] Proof for testGetCumulativeOfferData passing --- kontrol.toml | 7 +- src/test/kontrol/TermAuctionListGet.t.sol | 287 ++++++++++++++++++++-- 2 files changed, 273 insertions(+), 21 deletions(-) diff --git a/kontrol.toml b/kontrol.toml index ba46cf86..072d36e7 100644 --- a/kontrol.toml +++ b/kontrol.toml @@ -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", @@ -84,7 +84,10 @@ match-test = [ #"TermAuctionListInvariantsTest.testRemoveCompleted", #"TermAuctionListGetTest.testGetCumulativeDataEmpty", #"TermAuctionListGetTest.testGetPresentValueEmpty", - "TermAuctionListGetTest.testGetCumulativeDataNoCompletedAuctions", + "TermAuctionListGetTest.testGetCumulativeOfferData", + #"TermAuctionListGetTest.testGetCumulativeDataNoCompletedAuctions", + "TermAuctionListGetTest.testGetCumulativeDataCompletedAuctions", + "TermAuctionListGetTest.testGetPresentTotalValue", ] ast = true diff --git a/src/test/kontrol/TermAuctionListGet.t.sol b/src/test/kontrol/TermAuctionListGet.t.sol index f9168fa1..c0434d18 100644 --- a/src/test/kontrol/TermAuctionListGet.t.sol +++ b/src/test/kontrol/TermAuctionListGet.t.sol @@ -3,6 +3,8 @@ pragma solidity 0.8.23; import "src/test/kontrol/TermAuction.sol"; import "src/test/kontrol/ListTestUtils.t.sol"; + + contract TermAuctionListGetTest is RepoTokenListTest, TermAuctionListTest { using TermAuctionList for TermAuctionListData; using RepoTokenList for RepoTokenListData; @@ -96,6 +98,142 @@ contract TermAuctionListGetTest is RepoTokenListTest, TermAuctionListTest { } } + /** + * There are no matured tokens in the offers list + */ + function _assumeNonMaturedRepoTokens() internal { + 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 { + 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; + } + } + + + /** + * Assume or assert that the offer amounts in the offer locker for each offer in the list + * is equal to 0 + */ + function _establishOfferAmountLockedZero(Mode mode) internal { + bytes32 current = _termAuctionList.head; + + while (current != TermAuctionList.NULL_NODE) { + PendingOffer storage offer = _termAuctionList.offers[current]; + uint256 offerAmount = TermAuctionOfferLocker(address(offer.offerLocker)).lockedOfferAmount(current); + _establish(mode, offer.offerAmount == 0); + + 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 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 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( RepoTokenListData storage repoTokenListData, @@ -125,11 +263,34 @@ contract TermAuctionListGetTest is RepoTokenListTest, TermAuctionListTest { } } + function _getCumulativeOfferDataCompletedAuctions( + 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 = 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( - RepoTokenListData storage repoTokenListData, ITermDiscountRateAdapter discountRateAdapter, - address repoToken, - uint256 newOfferAmount, uint256 purchaseTokenPrecision ) internal view returns (uint256 cumulativeWeightedTimeToMaturity, uint256 cumulativeOfferAmount, bool found) { @@ -148,8 +309,10 @@ contract TermAuctionListGetTest is RepoTokenListTest, TermAuctionListTest { purchaseTokenPrecision, discountRateAdapter.repoRedemptionHaircut(offer.repoToken) ); - cumulativeWeightedTimeToMaturity += RepoTokenList.getRepoTokenWeightedTimeToMaturity(offer.repoToken, offerAmount); - cumulativeOfferAmount += offerAmount; + if (offerAmount > 0) { + cumulativeWeightedTimeToMaturity += RepoTokenList.getRepoTokenWeightedTimeToMaturity(offer.repoToken, offerAmount); + cumulativeOfferAmount += offerAmount; + } } previous = address(offer.termAuction); @@ -235,6 +398,7 @@ contract TermAuctionListGetTest is RepoTokenListTest, TermAuctionListTest { _initializeDiscountRateAdapter(discountRateAdapter); _establishCompletedAuctions(Mode.Assume); + _assumeOfferAmountLocked(); _assumeNoDiscountRatesSet(); // Consider only the case where we are not trying to match a token @@ -259,10 +423,7 @@ contract TermAuctionListGetTest is RepoTokenListTest, TermAuctionListTest { uint256 cumulativeOfferAmountCompletedAuctions, bool foundCompletedAuctions ) = getGroupedOfferTimeAndAmount( - _repoTokenList, ITermDiscountRateAdapter(address(discountRateAdapter)), - repoToken, - newOfferAmount, purchaseTokenPrecision ); @@ -272,7 +433,21 @@ contract TermAuctionListGetTest is RepoTokenListTest, TermAuctionListTest { } - function testGetCumulativeData( + function _assumeRedemptionValueAndBalancePositive() internal { + 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 testGetCumulativeOfferData( address repoToken, uint256 newOfferAmount, uint256 purchaseTokenPrecision @@ -282,14 +457,15 @@ contract TermAuctionListGetTest is RepoTokenListTest, TermAuctionListTest { new TermDiscountRateAdapter(); _initializeDiscountRateAdapter(discountRateAdapter); - // Assume relevant invariants - _establishNoMaturedTokens(Mode.Assume); - _establishPositiveBalance(Mode.Assume); + _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, @@ -303,10 +479,80 @@ contract TermAuctionListGetTest is RepoTokenListTest, TermAuctionListTest { purchaseTokenPrecision ); - // TODO: Add checks that calculation is correct + ( + uint256 cumulativeWeightedTimeToMaturityIncompletedAuctions, + uint256 cumulativeOfferAmountIncompletedAuctions + ) = filterCompletedAuctionsGetCumulativeOfferData(); + + filterDiscountRateSet(); + filterRepeatedAuctions(); + + ( + uint256 cumulativeWeightedTimeToMaturityCompletedAuctions, + uint256 cumulativeOfferAmountCompletedAuctions + ) = _getCumulativeOfferDataCompletedAuctions(discountRateAdapter, purchaseTokenPrecision); + + assert(cumulativeWeightedTimeToMaturity == cumulativeWeightedTimeToMaturityIncompletedAuctions + cumulativeWeightedTimeToMaturityCompletedAuctions); + assert(cumulativeOfferAmount == cumulativeOfferAmountIncompletedAuctions + cumulativeOfferAmountCompletedAuctions); } - function testGetPresentValue( + 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]; + uint256 offerAmount = TermAuctionOfferLocker(address(offer.offerLocker)).lockedOfferAmount(current); + if (!offer.termAuction.auctionCompleted()) { + totalValue += 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 _getTotalValueCompletedAuctions( + ITermDiscountRateAdapter discountRateAdapter, + uint256 purchaseTokenPrecision + ) internal view returns (uint256 totalValue) { + + bytes32 current = _termAuctionList.head; + + address previous = address(0); + + 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; + } + } + + function testGetPresentTotalValue( uint256 purchaseTokenPrecision, address repoTokenToMatch ) external { @@ -315,10 +561,6 @@ contract TermAuctionListGetTest is RepoTokenListTest, TermAuctionListTest { new TermDiscountRateAdapter(); _initializeDiscountRateAdapter(discountRateAdapter); - // Assume relevant invariants - _establishNoMaturedTokens(Mode.Assume); - _establishPositiveBalance(Mode.Assume); - // Consider only the case where we are not trying to match a token vm.assume(repoTokenToMatch == address(0)); vm.assume(purchaseTokenPrecision <= 18); @@ -330,6 +572,13 @@ contract TermAuctionListGetTest is RepoTokenListTest, TermAuctionListTest { repoTokenToMatch ); - // TODO: Add checks that calculation is correct + uint256 totalValueNonCompletedAuctions = filterCompletedAuctionsGetTotalValue(); + + filterDiscountRateSet(); + filterRepeatedAuctions(); + + uint256 totalValueCompletedAuctions = _getTotalValueCompletedAuctions(ITermDiscountRateAdapter(address(discountRateAdapter)), purchaseTokenPrecision); + + assert(totalPresentValue == totalValueNonCompletedAuctions + totalValueCompletedAuctions); } } From 5fd5bc1470628455bf715da76fabb47c98e5fa6b Mon Sep 17 00:00:00 2001 From: lisandrasilva Date: Thu, 24 Oct 2024 14:49:46 +0100 Subject: [PATCH 10/16] testGetPresentTotalValue passing --- src/test/kontrol/TermAuctionListGet.t.sol | 13 ++++++------- 1 file changed, 6 insertions(+), 7 deletions(-) diff --git a/src/test/kontrol/TermAuctionListGet.t.sol b/src/test/kontrol/TermAuctionListGet.t.sol index c0434d18..ac43b3f1 100644 --- a/src/test/kontrol/TermAuctionListGet.t.sol +++ b/src/test/kontrol/TermAuctionListGet.t.sol @@ -125,9 +125,9 @@ contract TermAuctionListGetTest is RepoTokenListTest, TermAuctionListTest { if (offer.termAuction.auctionCompleted()) { vm.assume(offerAmount == 0); } - else { - vm.assume(offerAmount > 0); - } + //else { + // vm.assume(offerAmount > 0); + //} current = _termAuctionList.nodes[current].next; } @@ -270,8 +270,6 @@ contract TermAuctionListGetTest is RepoTokenListTest, TermAuctionListTest { bytes32 current = _termAuctionList.head; - address previous = address(0); - while (current != TermAuctionList.NULL_NODE) { PendingOffer storage offer = _termAuctionList.offers[current]; uint256 offerAmount = RepoTokenUtils.getNormalizedRepoTokenAmount( @@ -531,8 +529,6 @@ contract TermAuctionListGetTest is RepoTokenListTest, TermAuctionListTest { bytes32 current = _termAuctionList.head; - address previous = address(0); - while (current != TermAuctionList.NULL_NODE) { PendingOffer storage offer = _termAuctionList.offers[current]; uint256 repoTokenAmountInBaseAssetPrecision = RepoTokenUtils.getNormalizedRepoTokenAmount( @@ -561,9 +557,12 @@ contract TermAuctionListGetTest is RepoTokenListTest, TermAuctionListTest { new TermDiscountRateAdapter(); _initializeDiscountRateAdapter(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, From 849086af12f2eab254b6ce5c338c7815a31d2b9f Mon Sep 17 00:00:00 2001 From: lisandrasilva Date: Sat, 26 Oct 2024 09:22:28 +0100 Subject: [PATCH 11/16] All properties for get functions passing --- kontrol.toml | 33 +- src/TermAuctionList.sol | 2 +- src/test/kontrol/ListTestUtils.t.sol | 299 --------- src/test/kontrol/RepoTokenListGet.t.sol | 234 ------- .../kontrol/RepoTokenListInvariants.t.sol | 235 +++---- src/test/kontrol/RepoTokenListTest.t.sol | 399 ++++++++++++ src/test/kontrol/TermAuctionListGet.t.sol | 583 ------------------ .../kontrol/TermAuctionListInvariants.t.sol | 258 +++++++- src/test/kontrol/TermAuctionListTest.t.sol | 425 +++++++++++++ 9 files changed, 1231 insertions(+), 1237 deletions(-) delete mode 100644 src/test/kontrol/ListTestUtils.t.sol delete mode 100644 src/test/kontrol/RepoTokenListGet.t.sol create mode 100644 src/test/kontrol/RepoTokenListTest.t.sol delete mode 100644 src/test/kontrol/TermAuctionListGet.t.sol create mode 100644 src/test/kontrol/TermAuctionListTest.t.sol diff --git a/kontrol.toml b/kontrol.toml index 072d36e7..946e0d9c 100644 --- a/kontrol.toml +++ b/kontrol.toml @@ -40,9 +40,8 @@ auto_abstract = true run-constructor = false bmc-depth = 2 match-test = [ - #"RepoTokenListInvariantsTest.setUp", - #"TermAuctionListInvariantsTest.setUp", - "TermAuctionListGetTest.setUp", + "RepoTokenListInvariantsTest.setUp", + "TermAuctionListInvariantsTest.setUp", ] ast = true @@ -76,18 +75,22 @@ break-on-cheatcodes = false auto_abstract = true run-constructor = false match-test = [ - #"RepoTokenListInvariantsTest.testInsertSortedNewToken", - #"RepoTokenListInvariantsTest.testInsertSortedDuplicateToken", - #"RepoTokenListInvariantsTest.testRemoveAndRedeemMaturedTokens", - #"TermAuctionListInvariantsTest.testInsertPendingNewOffer", - #"TermAuctionListInvariantsTest.testInsertPendingDuplicateOffer", - #"TermAuctionListInvariantsTest.testRemoveCompleted", - #"TermAuctionListGetTest.testGetCumulativeDataEmpty", - #"TermAuctionListGetTest.testGetPresentValueEmpty", - "TermAuctionListGetTest.testGetCumulativeOfferData", - #"TermAuctionListGetTest.testGetCumulativeDataNoCompletedAuctions", - "TermAuctionListGetTest.testGetCumulativeDataCompletedAuctions", - "TermAuctionListGetTest.testGetPresentTotalValue", + "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/TermAuctionList.sol b/src/TermAuctionList.sol index 555f8ecb..14f22c44 100644 --- a/src/TermAuctionList.sol +++ b/src/TermAuctionList.sol @@ -267,7 +267,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, diff --git a/src/test/kontrol/ListTestUtils.t.sol b/src/test/kontrol/ListTestUtils.t.sol deleted file mode 100644 index c29dfb86..00000000 --- a/src/test/kontrol/ListTestUtils.t.sol +++ /dev/null @@ -1,299 +0,0 @@ -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 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; - } - } -} - -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 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); - } - - /** - * 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 _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; - } - } - -} - diff --git a/src/test/kontrol/RepoTokenListGet.t.sol b/src/test/kontrol/RepoTokenListGet.t.sol deleted file mode 100644 index 06a7037d..00000000 --- a/src/test/kontrol/RepoTokenListGet.t.sol +++ /dev/null @@ -1,234 +0,0 @@ -pragma solidity 0.8.23; - -import "src/test/kontrol/RepoTokenListInvariants.t.sol"; -import "src/test/kontrol/TermDiscountRateAdapter.sol"; - -contract RepoTokenGetTest is RepoTokenListInvariantsTest { - using RepoTokenList for RepoTokenListData; - - function _initializeRepoTokenListEmpty() internal { - _repoTokenList.head = RepoTokenList.NULL_NODE; - } - - 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); - } - - /** - * 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(); - assert(currentMaturity > block.timestamp); - 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; - } - } - - function testGetCumulativeData( - address repoToken, - uint256 repoTokenAmount, - uint256 purchaseTokenPrecision - ) external { - // Initialize RepoTokenList of arbitrary size - kevm.symbolicStorage(address(this)); - _initializeRepoTokenList(); - - // Assume relevant invariants - _establishNoMaturedTokens(Mode.Assume); - _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); - - // Simplified calculation in the case no tokens have matured - ( - uint256 cumulativeWeightedTimeToMaturityNotMatured, - uint256 cumulativeRepoTokenAmountNotMatured - ) = _cumulativeRepoTokenDataNotMatured( - discountRateAdapter, - purchaseTokenPrecision - ); - - assert( - cumulativeWeightedTimeToMaturity == - cumulativeWeightedTimeToMaturityNotMatured - ); - - assert( - cumulativeRepoTokenAmount == - cumulativeRepoTokenAmountNotMatured - ); - } - - // Calculates the total present value assuming that no tokens have matured - 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(); - assert(currentMaturity > block.timestamp); - 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 testGetPresentValue( - uint256 purchaseTokenPrecision - ) external { - // Initialize RepoTokenList of arbitrary size - kevm.symbolicStorage(address(this)); - _initializeRepoTokenList(); - - // Assume relevant invariants - _establishNoMaturedTokens(Mode.Assume); - _establishPositiveBalance(Mode.Assume); - - // 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 - ); - - // Simplified calculation in the case no tokens have matured - uint256 totalPresentValueNotMatured = _totalPresentValueNotMatured( - discountRateAdapter, - purchaseTokenPrecision - ); - - assert(totalPresentValue == totalPresentValueNotMatured); - } -} diff --git a/src/test/kontrol/RepoTokenListInvariants.t.sol b/src/test/kontrol/RepoTokenListInvariants.t.sol index f98607a8..bef6aa32 100644 --- a/src/test/kontrol/RepoTokenListInvariants.t.sol +++ b/src/test/kontrol/RepoTokenListInvariants.t.sol @@ -8,7 +8,7 @@ import "src/RepoTokenList.sol"; import "src/test/kontrol/Constants.sol"; import "src/test/kontrol/RepoToken.sol"; -import "src/test/kontrol/ListTestUtils.t.sol"; +import "src/test/kontrol/RepoTokenListTest.t.sol"; contract RepoTokenListInvariantsTest is RepoTokenListTest { using RepoTokenList for RepoTokenListData; @@ -21,93 +21,6 @@ contract RepoTokenListInvariantsTest is RepoTokenListTest { _initializeRepoTokenList(); } - /** - * 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). @@ -195,21 +108,6 @@ contract RepoTokenListInvariantsTest is RepoTokenListTest { _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. */ @@ -245,4 +143,135 @@ contract RepoTokenListInvariantsTest is RepoTokenListTest { _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..17c49b77 --- /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 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)); + } + + 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 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; + } + } + + /** + * 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 { + 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; + } + } + + /** + * 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/TermAuctionListGet.t.sol b/src/test/kontrol/TermAuctionListGet.t.sol deleted file mode 100644 index ac43b3f1..00000000 --- a/src/test/kontrol/TermAuctionListGet.t.sol +++ /dev/null @@ -1,583 +0,0 @@ -pragma solidity 0.8.23; - -import "src/test/kontrol/TermAuction.sol"; -import "src/test/kontrol/ListTestUtils.t.sol"; - - - -contract TermAuctionListGetTest is RepoTokenListTest, TermAuctionListTest { - using TermAuctionList for TermAuctionListData; - using RepoTokenList for RepoTokenListData; - - function setUp() public { - // Make storage of this contract completely symbolic - kevm.symbolicStorage(address(this)); - // Initialize RepoTokenList of arbitrary size - //_initializeRepoTokenList(); - - setReferenceAuction(); - // Initialize TermAuctionList of arbitrary size - _initializeTermAuctionList(); - } - - function _initializeTermAuctionListEmpty() internal { - _termAuctionList.head = TermAuctionList.NULL_NODE; - } - - 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); - } - - /** - * Assume or assert that there are no completed auctions in the list. - */ - function _establishNoCompletedAuctions(Mode mode) internal { - 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 { - 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 { - 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 { - 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; - } - } - - - /** - * Assume or assert that the offer amounts in the offer locker for each offer in the list - * is equal to 0 - */ - function _establishOfferAmountLockedZero(Mode mode) internal { - bytes32 current = _termAuctionList.head; - - while (current != TermAuctionList.NULL_NODE) { - PendingOffer storage offer = _termAuctionList.offers[current]; - uint256 offerAmount = TermAuctionOfferLocker(address(offer.offerLocker)).lockedOfferAmount(current); - _establish(mode, offer.offerAmount == 0); - - 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 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 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( - RepoTokenListData storage repoTokenListData, - ITermDiscountRateAdapter discountRateAdapter, - address repoToken, - uint256 newOfferAmount, - uint256 purchaseTokenPrecision - ) 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, bool found) { - - 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; - } - } - - /* 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(); - _initializeDiscountRateAdapter(discountRateAdapter); - - _establishNoCompletedAuctions(Mode.Assume); - - 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( - _repoTokenList, - ITermDiscountRateAdapter(address(discountRateAdapter)), - repoToken, - newOfferAmount, - purchaseTokenPrecision - ); - - assert(cumulativeWeightedTimeToMaturity == cumulativeWeightedTimeToMaturityNoCompletedAuctions); - assert(cumulativeOfferAmount == cumulativeOfferAmountNoCompletedAuctions); - assert(found == foundNoCompletedAuctions); - - } - - /** - * Assume that all RepoTokens in the PendingOffers have no discount rate - * set in the RepoTokenList. - */ - function _assumeNoDiscountRatesSet() 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); - - current = _termAuctionList.nodes[current].next; - } - } - - /* 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(); - _initializeDiscountRateAdapter(discountRateAdapter); - - _establishCompletedAuctions(Mode.Assume); - _assumeOfferAmountLocked(); - _assumeNoDiscountRatesSet(); - - // 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); - - ( - uint256 cumulativeWeightedTimeToMaturity, - uint256 cumulativeOfferAmount, - bool found - ) = _termAuctionList.getCumulativeOfferData( - _repoTokenList, - ITermDiscountRateAdapter(address(discountRateAdapter)), - repoToken, - newOfferAmount, - purchaseTokenPrecision - ); - - ( - uint256 cumulativeWeightedTimeToMaturityCompletedAuctions, - uint256 cumulativeOfferAmountCompletedAuctions, - bool foundCompletedAuctions - ) = getGroupedOfferTimeAndAmount( - ITermDiscountRateAdapter(address(discountRateAdapter)), - purchaseTokenPrecision - ); - - assert(cumulativeWeightedTimeToMaturity == cumulativeWeightedTimeToMaturityCompletedAuctions); - assert(cumulativeOfferAmount == cumulativeOfferAmountCompletedAuctions); - assert(found == foundCompletedAuctions); - - } - - function _assumeRedemptionValueAndBalancePositive() internal { - 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 testGetCumulativeOfferData( - address repoToken, - uint256 newOfferAmount, - uint256 purchaseTokenPrecision - ) external { - // Initialize a DiscountRateAdapter with symbolic storage - TermDiscountRateAdapter discountRateAdapter = - new TermDiscountRateAdapter(); - _initializeDiscountRateAdapter(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 - ); - - ( - uint256 cumulativeWeightedTimeToMaturityIncompletedAuctions, - uint256 cumulativeOfferAmountIncompletedAuctions - ) = filterCompletedAuctionsGetCumulativeOfferData(); - - filterDiscountRateSet(); - filterRepeatedAuctions(); - - ( - uint256 cumulativeWeightedTimeToMaturityCompletedAuctions, - uint256 cumulativeOfferAmountCompletedAuctions - ) = _getCumulativeOfferDataCompletedAuctions(discountRateAdapter, purchaseTokenPrecision); - - assert(cumulativeWeightedTimeToMaturity == cumulativeWeightedTimeToMaturityIncompletedAuctions + cumulativeWeightedTimeToMaturityCompletedAuctions); - assert(cumulativeOfferAmount == cumulativeOfferAmountIncompletedAuctions + cumulativeOfferAmountCompletedAuctions); - } - - 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]; - uint256 offerAmount = TermAuctionOfferLocker(address(offer.offerLocker)).lockedOfferAmount(current); - if (!offer.termAuction.auctionCompleted()) { - totalValue += 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 _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; - } - } - - function testGetPresentTotalValue( - uint256 purchaseTokenPrecision, - address repoTokenToMatch - ) external { - // Initialize a DiscountRateAdapter with symbolic storage - TermDiscountRateAdapter discountRateAdapter = - new TermDiscountRateAdapter(); - _initializeDiscountRateAdapter(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/TermAuctionListInvariants.t.sol b/src/test/kontrol/TermAuctionListInvariants.t.sol index e1389591..802744ca 100644 --- a/src/test/kontrol/TermAuctionListInvariants.t.sol +++ b/src/test/kontrol/TermAuctionListInvariants.t.sol @@ -11,6 +11,7 @@ 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"; @@ -22,7 +23,7 @@ contract TermAuctionListInvariantsTest is RepoTokenListTest, TermAuctionListTest // Make storage of this contract completely symbolic kevm.symbolicStorage(address(this)); - setReferenceAuction(); + _setReferenceAuction(); // Initialize TermAuctionList of arbitrary size _initializeTermAuctionList(); @@ -469,7 +470,7 @@ contract TermAuctionListInvariantsTest is RepoTokenListTest, TermAuctionListTest // 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 @@ -514,4 +515,257 @@ contract TermAuctionListInvariantsTest is RepoTokenListTest, TermAuctionListTest _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); + + ( + uint256 cumulativeWeightedTimeToMaturity, + uint256 cumulativeOfferAmount, + bool found + ) = _termAuctionList.getCumulativeOfferData( + _repoTokenList, + ITermDiscountRateAdapter(address(discountRateAdapter)), + repoToken, + newOfferAmount, + purchaseTokenPrecision + ); + + ( + uint256 cumulativeWeightedTimeToMaturityCompletedAuctions, + uint256 cumulativeOfferAmountCompletedAuctions, + bool foundCompletedAuctions + ) = _getGroupedOfferTimeAndAmount( + ITermDiscountRateAdapter(address(discountRateAdapter)), + purchaseTokenPrecision + ); + + assert(cumulativeWeightedTimeToMaturity == cumulativeWeightedTimeToMaturityCompletedAuctions); + assert(cumulativeOfferAmount == cumulativeOfferAmountCompletedAuctions); + assert(found == foundCompletedAuctions); + + } + + 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..4a026182 --- /dev/null +++ b/src/test/kontrol/TermAuctionListTest.t.sol @@ -0,0 +1,425 @@ +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 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 { + 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 { + 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 { + 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 { + 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 { + 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, bool found) { + + 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; + } + } +} + From 64b9d7b0c41e19346a852d27a164995c4f6114b7 Mon Sep 17 00:00:00 2001 From: lisandrasilva Date: Sat, 26 Oct 2024 12:28:44 +0100 Subject: [PATCH 12/16] Fix forge build warnings --- src/test/kontrol/KontrolTest.sol | 4 ++-- src/test/kontrol/RepoToken.sol | 2 +- src/test/kontrol/RepoTokenListTest.t.sol | 18 +++++++++--------- .../kontrol/TermAuctionListInvariants.t.sol | 18 +++++++++--------- src/test/kontrol/TermAuctionListTest.t.sol | 16 ++++++++-------- src/test/kontrol/TermAuctionOfferLocker.sol | 6 +++--- src/test/kontrol/TermDiscountRateAdapter.sol | 6 +++--- src/test/kontrol/TermRepoServicer.sol | 4 ++-- 8 files changed, 37 insertions(+), 37 deletions(-) diff --git a/src/test/kontrol/KontrolTest.sol b/src/test/kontrol/KontrolTest.sol index d8622efe..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); } @@ -103,7 +103,7 @@ contract KontrolTest is Test, KontrolCheats { _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/RepoTokenListTest.t.sol b/src/test/kontrol/RepoTokenListTest.t.sol index 17c49b77..4b67d985 100644 --- a/src/test/kontrol/RepoTokenListTest.t.sol +++ b/src/test/kontrol/RepoTokenListTest.t.sol @@ -32,14 +32,14 @@ contract RepoTokenListTest is KontrolTest { /** * Return the maturity timestamp of the given RepoToken. */ - function _getRepoTokenMaturity(address repoToken) internal returns (uint256 redemptionTimestamp) { + 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 returns (uint256) { + function _getRepoTokenBalance(address repoToken) internal view returns (uint256) { return ITermRepoToken(repoToken).balanceOf(address(this)); } @@ -80,7 +80,7 @@ contract RepoTokenListTest is KontrolTest { * - 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) { + function _countNodesInList() internal view returns (uint256) { uint256 count = 0; address current = _repoTokenList.head; @@ -95,7 +95,7 @@ contract RepoTokenListTest is KontrolTest { /** * Return true if the given RepoToken is in the list, and false otherwise. */ - function _repoTokenInList(address repoToken) internal returns (bool) { + function _repoTokenInList(address repoToken) internal view returns (bool) { address current = _repoTokenList.head; while (current != RepoTokenList.NULL_NODE) { @@ -295,7 +295,7 @@ contract RepoTokenListTest is KontrolTest { /** * Assume or assert that the tokens in the list are sorted by maturity. */ - function _establishSortedByMaturity(Mode mode) internal { + function _establishSortedByMaturity(Mode mode) internal view { address previous = RepoTokenList.NULL_NODE; address current = _repoTokenList.head; @@ -314,7 +314,7 @@ contract RepoTokenListTest is KontrolTest { /** * Assume or assert that there are no duplicate tokens in the list. */ - function _establishNoDuplicateTokens(Mode mode) internal { + function _establishNoDuplicateTokens(Mode mode) internal view { address current = _repoTokenList.head; while (current != RepoTokenList.NULL_NODE) { @@ -333,7 +333,7 @@ contract RepoTokenListTest is KontrolTest { * 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 { + function _establishNoMaturedTokens(Mode mode) internal view { address current = _repoTokenList.head; while (current != RepoTokenList.NULL_NODE) { @@ -348,7 +348,7 @@ contract RepoTokenListTest is KontrolTest { /** * Assume or assert that all tokens in the list have balance > 0. */ - function _establishPositiveBalance(Mode mode) internal { + function _establishPositiveBalance(Mode mode) internal view { address current = _repoTokenList.head; while (current != RepoTokenList.NULL_NODE) { @@ -367,7 +367,7 @@ contract RepoTokenListTest is KontrolTest { * Note: This is equivalent to the above invariant if the NoMaturedTokens * invariant also holds. */ - function _establishPositiveBalanceForNonMaturedTokens(Mode mode) internal { + function _establishPositiveBalanceForNonMaturedTokens(Mode mode) internal view { address current = _repoTokenList.head; while (current != RepoTokenList.NULL_NODE) { diff --git a/src/test/kontrol/TermAuctionListInvariants.t.sol b/src/test/kontrol/TermAuctionListInvariants.t.sol index 802744ca..673188a7 100644 --- a/src/test/kontrol/TermAuctionListInvariants.t.sol +++ b/src/test/kontrol/TermAuctionListInvariants.t.sol @@ -32,7 +32,7 @@ contract TermAuctionListInvariantsTest is RepoTokenListTest, TermAuctionListTest /** * Assume or assert that the offers in the list are sorted by auction. */ - function _establishSortedByAuctionId(Mode mode) internal { + function _establishSortedByAuctionId(Mode mode) internal view { bytes32 previous = TermAuctionList.NULL_NODE; bytes32 current = _termAuctionList.head; @@ -51,7 +51,7 @@ contract TermAuctionListInvariantsTest is RepoTokenListTest, TermAuctionListTest /** * Assume or assert that there are no duplicate offers in the list. */ - function _establishNoDuplicateOffers(Mode mode) internal { + function _establishNoDuplicateOffers(Mode mode) internal view { bytes32 current = _termAuctionList.head; while (current != TermAuctionList.NULL_NODE) { @@ -69,7 +69,7 @@ contract TermAuctionListInvariantsTest is RepoTokenListTest, TermAuctionListTest /** * Assume or assert that there are no completed auctions in the list. */ - function _establishNoCompletedOrCancelledAuctions(Mode mode) internal { + function _establishNoCompletedOrCancelledAuctions(Mode mode) internal view { bytes32 current = _termAuctionList.head; while (current != TermAuctionList.NULL_NODE) { @@ -84,7 +84,7 @@ contract TermAuctionListInvariantsTest is RepoTokenListTest, TermAuctionListTest /** * Assume or assert that all offer amounts are > 0. */ - function _establishPositiveOfferAmounts(Mode mode) internal { + function _establishPositiveOfferAmounts(Mode mode) internal view { bytes32 current = _termAuctionList.head; while (current != TermAuctionList.NULL_NODE) { @@ -99,7 +99,7 @@ contract TermAuctionListInvariantsTest is RepoTokenListTest, TermAuctionListTest * 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 { + function _establishOfferAmountMatchesAmountLocked(Mode mode, bytes32 offerId) internal view { bytes32 current = _termAuctionList.head; while (current != TermAuctionList.NULL_NODE) { @@ -120,7 +120,7 @@ contract TermAuctionListInvariantsTest is RepoTokenListTest, TermAuctionListTest * - 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) { + function _countOffersInList() internal view returns (uint256) { uint256 count = 0; bytes32 current = _termAuctionList.head; @@ -135,7 +135,7 @@ contract TermAuctionListInvariantsTest is RepoTokenListTest, TermAuctionListTest /** * Return true if the given offer id is in the list, and false otherwise. */ - function _offerInList(bytes32 offerId) internal returns (bool) { + function _offerInList(bytes32 offerId) internal view returns (bool) { bytes32 current = _termAuctionList.head; while (current != TermAuctionList.NULL_NODE) { @@ -154,7 +154,7 @@ contract TermAuctionListInvariantsTest is RepoTokenListTest, TermAuctionListTest * This is necessary in order to use cheatcodes on a symbolic address that * change its code or storage. */ - function _assumeNewAddress(address freshAddress) internal { + function _assumeNewAddress(address freshAddress) internal view { vm.assume(10 <= uint160(freshAddress)); vm.assume(freshAddress != address(this)); @@ -449,7 +449,7 @@ contract TermAuctionListInvariantsTest is RepoTokenListTest, TermAuctionListTest * Assume that all RepoTokens in the PendingOffers have no discount rate * set in the RepoTokenList. */ - function _assumeNoDiscountRatesSet() internal { + function _assumeNoDiscountRatesSet() internal view { bytes32 current = _termAuctionList.head; while (current != TermAuctionList.NULL_NODE) { diff --git a/src/test/kontrol/TermAuctionListTest.t.sol b/src/test/kontrol/TermAuctionListTest.t.sol index 4a026182..1a7ac593 100644 --- a/src/test/kontrol/TermAuctionListTest.t.sol +++ b/src/test/kontrol/TermAuctionListTest.t.sol @@ -41,7 +41,7 @@ contract TermAuctionListTest is KontrolTest { /** * Set pending offer using slot manipulation directly */ - function setPendingOffer(bytes32 offerId, address repoToken, uint256 offerAmount, address auction, address offerLocker) internal { + 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); @@ -52,7 +52,7 @@ contract TermAuctionListTest is KontrolTest { /** * Return the auction for a given offer in the list. */ - function _getAuction(bytes32 offerId) internal returns(address) { + function _getAuction(bytes32 offerId) internal view returns(address) { return address(_termAuctionList.offers[offerId].termAuction); } @@ -121,7 +121,7 @@ contract TermAuctionListTest is KontrolTest { } // Build PendingOffer - setPendingOffer(current, address(repoToken), freshUInt256(), auction, address(offerLocker)); + _setPendingOffer(current, address(repoToken), freshUInt256(), auction, address(offerLocker)); previous = current; ++count; @@ -156,7 +156,7 @@ contract TermAuctionListTest is KontrolTest { /** * Assume or assert that there are no completed auctions in the list. */ - function _establishNoCompletedAuctions(Mode mode) internal { + function _establishNoCompletedAuctions(Mode mode) internal view { bytes32 current = _termAuctionList.head; while (current != TermAuctionList.NULL_NODE) { @@ -170,7 +170,7 @@ contract TermAuctionListTest is KontrolTest { /** * Assume or assert that all auctions in the list are completed. */ - function _establishCompletedAuctions(Mode mode) internal { + function _establishCompletedAuctions(Mode mode) internal view { bytes32 current = _termAuctionList.head; while (current != TermAuctionList.NULL_NODE) { @@ -184,7 +184,7 @@ contract TermAuctionListTest is KontrolTest { /** * There are no matured tokens in the offers list */ - function _assumeNonMaturedRepoTokens() internal { + function _assumeNonMaturedRepoTokens() internal view { bytes32 current = _termAuctionList.head; while (current != TermAuctionList.NULL_NODE) { @@ -199,7 +199,7 @@ contract TermAuctionListTest is KontrolTest { * 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 { + function _assumeOfferAmountLocked() internal view { bytes32 current = _termAuctionList.head; while (current != TermAuctionList.NULL_NODE) { @@ -216,7 +216,7 @@ contract TermAuctionListTest is KontrolTest { } } - function _assumeRedemptionValueAndBalancePositive() internal { + function _assumeRedemptionValueAndBalancePositive() internal view { bytes32 current = _termAuctionList.head; while (current != TermAuctionList.NULL_NODE) { diff --git a/src/test/kontrol/TermAuctionOfferLocker.sol b/src/test/kontrol/TermAuctionOfferLocker.sol index 4d0990a6..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; } @@ -77,7 +77,7 @@ contract TermAuctionOfferLocker is ITermAuctionOfferLocker, KontrolTest { function lockOffers( TermAuctionOfferSubmission[] calldata offerSubmissions - ) external returns (bytes32[] memory) { + ) external view returns (bytes32[] memory) { uint256 length = offerSubmissions.length; bytes32[] memory offers = new bytes32[](length); diff --git a/src/test/kontrol/TermDiscountRateAdapter.sol b/src/test/kontrol/TermDiscountRateAdapter.sol index 6226df6b..a8cb79af 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..cca4ae94 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; } From 40738e28c95b4dd374ce30195c460f42f9319998 Mon Sep 17 00:00:00 2001 From: lisandrasilva Date: Tue, 5 Nov 2024 13:57:37 +0000 Subject: [PATCH 13/16] Refactored --- .../kontrol/TermAuctionListInvariants.t.sol | 319 +++--------------- src/test/kontrol/TermAuctionListTest.t.sol | 221 ++++++++++++ 2 files changed, 271 insertions(+), 269 deletions(-) diff --git a/src/test/kontrol/TermAuctionListInvariants.t.sol b/src/test/kontrol/TermAuctionListInvariants.t.sol index 673188a7..75df2b47 100644 --- a/src/test/kontrol/TermAuctionListInvariants.t.sol +++ b/src/test/kontrol/TermAuctionListInvariants.t.sol @@ -29,261 +29,6 @@ contract TermAuctionListInvariantsTest is RepoTokenListTest, TermAuctionListTest _initializeTermAuctionList(); } - /** - * 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 _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); - } - /** * Test that insertPending preserves the list invariants when a new offer * is added (that was not present in the list before). @@ -428,34 +173,69 @@ contract TermAuctionListInvariantsTest is RepoTokenListTest, TermAuctionListTest } /** - * 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) { - PendingOffer storage offer = _termAuctionList.offers[current]; - TermAuctionOfferLocker offerLocker = - TermAuctionOfferLocker(address(offer.offerLocker)); + 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]; - offerLocker.guaranteeUnlockAlwaysSucceeds(); + 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; } } - /** - * Assume that all RepoTokens in the PendingOffers have no discount rate - * set in the RepoTokenList. - */ - function _assumeNoDiscountRatesSet() internal view { + function _assertRepoTokensValidate(address asset) 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); + (bool isRepoTokenValid, ) = _repoTokenList.validateRepoToken(ITermRepoToken(repoToken), asset); + assert(isRepoTokenValid); current = _termAuctionList.nodes[current].next; } @@ -629,6 +409,7 @@ contract TermAuctionListInvariantsTest is RepoTokenListTest, TermAuctionListTest vm.assume(repoToken == address(0)); vm.assume(newOfferAmount < ETH_UPPER_BOUND); vm.assume(purchaseTokenPrecision <= 18); + vm.assume(purchaseTokenPrecision > 0); ( uint256 cumulativeWeightedTimeToMaturity, diff --git a/src/test/kontrol/TermAuctionListTest.t.sol b/src/test/kontrol/TermAuctionListTest.t.sol index 1a7ac593..a7a1c422 100644 --- a/src/test/kontrol/TermAuctionListTest.t.sol +++ b/src/test/kontrol/TermAuctionListTest.t.sol @@ -421,5 +421,226 @@ contract TermAuctionListTest is KontrolTest { 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; + } + } } From 3ea823bf0ad46582e73d5c76d73d36062bf9743a Mon Sep 17 00:00:00 2001 From: lisandrasilva Date: Mon, 11 Nov 2024 14:50:35 +0000 Subject: [PATCH 14/16] Fixed testRemoveCompleted --- .../kontrol/TermAuctionListInvariants.t.sol | 17 +++++++++++++---- src/test/kontrol/TermAuctionListTest.t.sol | 2 +- src/test/kontrol/TermRepoServicer.sol | 3 --- 3 files changed, 14 insertions(+), 8 deletions(-) diff --git a/src/test/kontrol/TermAuctionListInvariants.t.sol b/src/test/kontrol/TermAuctionListInvariants.t.sol index 75df2b47..c8c8826f 100644 --- a/src/test/kontrol/TermAuctionListInvariants.t.sol +++ b/src/test/kontrol/TermAuctionListInvariants.t.sol @@ -241,6 +241,18 @@ contract TermAuctionListInvariantsTest is RepoTokenListTest, TermAuctionListTest } } + function _guaranteeRedeemOfferRepoTokenAlwaysSucceeds() internal { + bytes32 current = _termAuctionList.head; + + while (current != TermAuctionList.NULL_NODE) { + address repoToken = _termAuctionList.offers[current].repoToken; + (, , address repoServicer,) = ITermRepoToken(repoToken).config(); + TermRepoServicer(repoServicer).guaranteeRedeemAlwaysSucceeds(); + + current = _termAuctionList.nodes[current].next; + } + } + /** * Test that removeCompleted preserves the list invariants. */ @@ -425,8 +437,7 @@ contract TermAuctionListInvariantsTest is RepoTokenListTest, TermAuctionListTest ( uint256 cumulativeWeightedTimeToMaturityCompletedAuctions, - uint256 cumulativeOfferAmountCompletedAuctions, - bool foundCompletedAuctions + uint256 cumulativeOfferAmountCompletedAuctions ) = _getGroupedOfferTimeAndAmount( ITermDiscountRateAdapter(address(discountRateAdapter)), purchaseTokenPrecision @@ -434,8 +445,6 @@ contract TermAuctionListInvariantsTest is RepoTokenListTest, TermAuctionListTest assert(cumulativeWeightedTimeToMaturity == cumulativeWeightedTimeToMaturityCompletedAuctions); assert(cumulativeOfferAmount == cumulativeOfferAmountCompletedAuctions); - assert(found == foundCompletedAuctions); - } function _filterDiscountRateSet() internal { diff --git a/src/test/kontrol/TermAuctionListTest.t.sol b/src/test/kontrol/TermAuctionListTest.t.sol index a7a1c422..44661585 100644 --- a/src/test/kontrol/TermAuctionListTest.t.sol +++ b/src/test/kontrol/TermAuctionListTest.t.sol @@ -340,7 +340,7 @@ contract TermAuctionListTest is KontrolTest { function _getGroupedOfferTimeAndAmount( ITermDiscountRateAdapter discountRateAdapter, uint256 purchaseTokenPrecision - ) internal view returns (uint256 cumulativeWeightedTimeToMaturity, uint256 cumulativeOfferAmount, bool found) { + ) internal view returns (uint256 cumulativeWeightedTimeToMaturity, uint256 cumulativeOfferAmount) { bytes32 current = _termAuctionList.head; diff --git a/src/test/kontrol/TermRepoServicer.sol b/src/test/kontrol/TermRepoServicer.sol index cca4ae94..235ecfe9 100644 --- a/src/test/kontrol/TermRepoServicer.sol +++ b/src/test/kontrol/TermRepoServicer.sol @@ -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) { From 2e0a399163870913f10aa6871facc3a59aba45d7 Mon Sep 17 00:00:00 2001 From: lisandrasilva Date: Mon, 11 Nov 2024 15:08:23 +0000 Subject: [PATCH 15/16] Fixed merge --- src/RepoTokenList.sol | 6 +----- src/Strategy.sol | 8 +------- src/TermAuctionList.sol | 4 ---- 3 files changed, 2 insertions(+), 16 deletions(-) diff --git a/src/RepoTokenList.sol b/src/RepoTokenList.sol index 1795575c..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; diff --git a/src/Strategy.sol b/src/Strategy.sol index c4b7b355..b7466355 100644 --- a/src/Strategy.sol +++ b/src/Strategy.sol @@ -512,8 +512,6 @@ contract Strategy is BaseStrategy, Pausable, AccessControl { repoTokenListData, discountRateAdapter, PURCHASE_TOKEN_PRECISION, - prevTermController, - currTermController, repoToken ); } @@ -581,16 +579,12 @@ contract Strategy is BaseStrategy, Pausable, AccessControl { liquidBalance + repoTokenListData.getPresentValue( discountRateAdapter, - PURCHASE_TOKEN_PRECISION, - prevTermController, - currTermController + PURCHASE_TOKEN_PRECISION ) + termAuctionListData.getPresentValue( repoTokenListData, discountRateAdapter, PURCHASE_TOKEN_PRECISION, - prevTermController, - currTermController, address(0) ); } diff --git a/src/TermAuctionList.sol b/src/TermAuctionList.sol index c30e782e..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 From 02de256e473b8cc4386cfbae2c3a93c670e098da Mon Sep 17 00:00:00 2001 From: palinatolmach Date: Tue, 19 Nov 2024 20:33:57 +0400 Subject: [PATCH 16/16] Adjust `kontrol.toml` options for KaaS --- kontrol.toml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/kontrol.toml b/kontrol.toml index 946e0d9c..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' @@ -47,7 +47,7 @@ ast = true [prove.tests] foundry-project-root = '.' -verbose = false +verbose = true debug = false max-depth = 100000 max-iterations = 10000