Merge pull request #100 from term-finance/runtime-fv

Merge pull request #99 from term-finance/master

kontrol.toml

@@ -1,7 +1,7 @@
 [build.default]
 foundry-project-root       = '.'
-regen                      = true
-rekompile                  = true
+regen                      = false
+rekompile                  = false
 verbose                    = false
 debug                      = false
 require                    = 'src/test/kontrol/term-lemmas.k'
@@ -38,7 +38,7 @@ break-on-basic-blocks      = false
 break-on-cheatcodes        = false
 auto_abstract              = true
 run-constructor            = false
-bmc-depth                  = 3
+bmc-depth                  = 2
 match-test                 = [
         "RepoTokenListInvariantsTest.setUp",
         "TermAuctionListInvariantsTest.setUp",
@@ -47,7 +47,7 @@ ast                        = true
 
 [prove.tests]
 foundry-project-root       = '.'
-verbose                    = false
+verbose                    = true
 debug                      = false
 max-depth                  = 100000
 max-iterations             = 10000
@@ -78,9 +78,19 @@ match-test                 = [
         "RepoTokenListInvariantsTest.testInsertSortedNewToken",
         "RepoTokenListInvariantsTest.testInsertSortedDuplicateToken",
         "RepoTokenListInvariantsTest.testRemoveAndRedeemMaturedTokens",
+        "RepoTokenListInvariantsTest.testGetCumulativeDataEmpty",
+        "RepoTokenListInvariantsTest.testGetPresentValueEmpty",
+        "RepoTokenListInvariantsTest.testGetPresentTotalValue",
+        "RepoTokenListInvariantsTest.testGetCumulativeRepoTokenData",
         "TermAuctionListInvariantsTest.testInsertPendingNewOffer",
         "TermAuctionListInvariantsTest.testInsertPendingDuplicateOffer",
         "TermAuctionListInvariantsTest.testRemoveCompleted",
+        "TermAuctionListInvariantsTest.testGetCumulativeDataEmpty",
+        "TermAuctionListInvariantsTest.testGetPresentValueEmpty",
+        "TermAuctionListInvariantsTest.testGetCumulativeDataNoCompletedAuctions",
+        "TermAuctionListInvariantsTest.testGetCumulativeDataCompletedAuctions",
+        "TermAuctionListInvariantsTest.testGetCumulativeOfferData",
+        "TermAuctionListInvariantsTest.testGetPresentTotalValue",
     ]
 ast                        = true
 

src/RepoTokenList.sol

@@ -177,17 +177,13 @@ library RepoTokenList {
      * @param listData The list data
      * @param discountRateAdapter The discount rate adapter
      * @param purchaseTokenPrecision The precision of the purchase token
-     * @param prevTermController The previous term controller
-     * @param currTermController The current term controller
      * @return totalPresentValue The total present value of the repoTokens
      * @dev  Aggregates the present value of all repoTokens in the list. 
      */
     function getPresentValue(
         RepoTokenListData storage listData, 
         ITermDiscountRateAdapter discountRateAdapter,
-        uint256 purchaseTokenPrecision,
-        ITermController prevTermController,
-        ITermController currTermController
+        uint256 purchaseTokenPrecision
     ) internal view returns (uint256 totalPresentValue) {
         // If the list is empty, return 0
         if (listData.head == NULL_NODE) return 0;
@@ -425,7 +421,7 @@ library RepoTokenList {
 
             uint256 currentMaturity = getRepoTokenMaturity(current);
 
-            // Insert repoToken before current if its maturity is less than or equal
+            // Insert repoToken before current if its maturity is less than current maturity
             if (maturityToInsert < currentMaturity) {
                 if (prev == NULL_NODE) {
                     listData.head = repoToken;

src/Strategy.sol

@@ -524,8 +524,6 @@ contract Strategy is BaseStrategy, Pausable, AccessControl {
                 repoTokenListData,
                 strategyState.discountRateAdapter,
                 PURCHASE_TOKEN_PRECISION,
-                strategyState.prevTermController,
-                strategyState.currTermController,
                 repoToken
             );
     }
@@ -582,16 +580,12 @@ contract Strategy is BaseStrategy, Pausable, AccessControl {
             liquidBalance +
             repoTokenListData.getPresentValue(
                 strategyState.discountRateAdapter,
-                PURCHASE_TOKEN_PRECISION,
-                prevTermController,
-                currTermController
+                PURCHASE_TOKEN_PRECISION
             ) +
             termAuctionListData.getPresentValue(
                 repoTokenListData,
                 strategyState.discountRateAdapter,
                 PURCHASE_TOKEN_PRECISION,
-                prevTermController,
-                currTermController,
                 address(0)
             );
     }

src/TermAuctionList.sol

@@ -242,8 +242,6 @@ library TermAuctionList {
      * @param repoTokenListData The repoToken list data
      * @param discountRateAdapter The discount rate adapter
      * @param purchaseTokenPrecision The precision of the purchase token
-     * @param prevTermController The previous term controller
-     * @param currTermController The current term controller
      * @param repoTokenToMatch The address of the repoToken to match (optional)
      * @return totalValue The total present value of the offers
      *
@@ -257,8 +255,6 @@ library TermAuctionList {
         RepoTokenListData storage repoTokenListData,
         ITermDiscountRateAdapter discountRateAdapter,
         uint256 purchaseTokenPrecision,
-        ITermController prevTermController,
-        ITermController currTermController,
         address repoTokenToMatch
     ) internal view returns (uint256 totalValue) {
         // Return 0 if the list is empty
@@ -282,7 +278,7 @@ library TermAuctionList {
             // Handle new or unseen repo tokens
             /// @dev offer processed, but auctionClosed not yet called and auction is new so repoToken not on List and wont be picked up
             /// checking repoTokendiscountRates to make sure we are not double counting on re-openings
-            if (repoTokenListData.discountRates[offer.repoToken] == 0 && offer.termAuction.auctionCompleted()) {
+            if (offer.termAuction.auctionCompleted() && repoTokenListData.discountRates[offer.repoToken] == 0) {
                 if (edgeCaseAuction != address(offer.termAuction)) {
                     uint256 repoTokenAmountInBaseAssetPrecision = RepoTokenUtils.getNormalizedRepoTokenAmount(
                         offer.repoToken,
@@ -357,7 +353,7 @@ library TermAuctionList {
                 // Handle new repo tokens or reopening auctions
                 /// @dev offer processed, but auctionClosed not yet called and auction is new so repoToken not on List and wont be picked up
                 /// checking repoTokendiscountRates to make sure we are not double counting on re-openings
-                if (repoTokenListData.discountRates[offer.repoToken] == 0 && offer.termAuction.auctionCompleted()) {
+                if (offer.termAuction.auctionCompleted() && repoTokenListData.discountRates[offer.repoToken] == 0) {
                     // use normalized repoToken amount if repoToken is not in the list
                     if (edgeCaseAuction != address(offer.termAuction)) {
                         offerAmount = RepoTokenUtils.getNormalizedRepoTokenAmount(

src/test/kontrol/KontrolTest.sol

@@ -11,7 +11,7 @@ contract KontrolTest is Test, KontrolCheats {
     // Note: 2 ** 35 takes us to year 3058
     uint256 constant timeUpperBound = 2 ** 35;
 
-    function infoAssert(bool condition, string memory message) external {
+    function infoAssert(bool condition, string memory message) external pure {
         if (!condition) {
             revert(message);
         }
@@ -35,27 +35,75 @@ contract KontrolTest is Test, KontrolCheats {
         }
     }
 
-    function _loadUInt256(address contractAddress, uint256 slot) internal view returns (uint256) {
-        return uint256(vm.load(contractAddress, bytes32(slot)));
+    function _loadData(
+        address contractAddress,
+        uint256 slot,
+        uint256 offset,
+        uint256 width
+    ) internal view returns (uint256) {
+        // `offset` and `width` must not overflow the slot
+        assert(offset + width <= 32);
+
+        // Slot read mask
+        uint256 mask;
+        unchecked {
+            mask = (2 ** (8 * width)) - 1;
+        }
+        // Value right shift
+        uint256 shift = 8 * offset;
+
+        // Current slot value
+        uint256 slotValue = uint256(vm.load(contractAddress, bytes32(slot)));
+
+        // Isolate and return data to retrieve
+        return mask & (slotValue >> shift);
     }
 
-    function _loadAddress(address contractAddress, uint256 slot) internal view returns (address) {
-        return address(uint160(uint256(vm.load(contractAddress, bytes32(slot)))));
+    function _storeData(address contractAddress, uint256 slot, uint256 offset, uint256 width, uint256 value) internal {
+        // `offset` and `width` must not overflow the slot
+        assert(offset + width <= 32);
+        // and `value` must fit into the designated part
+        assert(width == 32 || value < 2 ** (8 * width));
+
+        // Slot update mask
+        uint256 maskLeft;
+        unchecked {
+            maskLeft = ~((2 ** (8 * (offset + width))) - 1);
+        }
+        uint256 maskRight = (2 ** (8 * offset)) - 1;
+        uint256 mask = maskLeft | maskRight;
+
+        value = (2 ** (8 * offset)) * value;
+
+        // Current slot value
+        uint256 slotValue = uint256(vm.load(contractAddress, bytes32(slot)));
+        // Updated slot value
+        slotValue = value | (mask & slotValue);
+
+        vm.store(contractAddress, bytes32(slot), bytes32(slotValue));
     }
 
-    function _storeBytes32(address contractAddress, uint256 slot, bytes32 value) internal {
-        vm.store(contractAddress, bytes32(slot), value);
+    function _loadUInt256(address contractAddress, uint256 slot) internal view returns (uint256) {
+        return _loadData(contractAddress, slot, 0, 32);
+    }
+
+    function _loadAddress(address contractAddress, uint256 slot) internal view returns (address) {
+        return address(uint160(_loadData(contractAddress, slot, 0, 20)));
     }
 
     function _storeUInt256(address contractAddress, uint256 slot, uint256 value) internal {
-        vm.store(contractAddress, bytes32(slot), bytes32(value));
+        _storeData(contractAddress, slot, 0, 32, value);
     }
 
     function _storeAddress(address contractAddress, uint256 slot, address value) internal {
-        vm.store(contractAddress, bytes32(slot), bytes32(uint256(uint160(value))));
+        _storeData(contractAddress, slot, 0, 20, uint160(value));
+    }
+
+    function _storeBytes32(address contractAddress, uint256 slot, bytes32 value) internal {
+        _storeUInt256(contractAddress, slot, uint256(value));
     }
 
-    function _assumeNoOverflow(uint256 augend, uint256 addend) internal {
+    function _assumeNoOverflow(uint256 augend, uint256 addend) internal pure {
         unchecked {
             vm.assume(augend < augend + addend);
         }

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