Merge pull request #47 from runtimeverification/list-invariant-tests

Kontrol property tests for `RepoTokenList` and `TermAuctionList` invariants

.gitmodules

@@ -17,6 +17,9 @@
 [submodule "lib/openzeppelin-contracts-upgradeable"]
 	path = lib/openzeppelin-contracts-upgradeable
 	url = https://github.com/OpenZeppelin/openzeppelin-contracts-upgradeable
+[submodule "lib/kontrol-cheatcodes"]
+	path = lib/kontrol-cheatcodes
+	url = https://github.com/runtimeverification/kontrol-cheatcodes
 [submodule "lib/yearn-vaults-v3"]
 	path = lib/yearn-vaults-v3
 	url = https://github.com/yearn/yearn-vaults-v3.git

kontrol.toml

@@ -0,0 +1,88 @@
+[build.default]
+foundry-project-root       = '.'
+regen                      = true
+rekompile                  = true
+verbose                    = false
+debug                      = false
+require                    = 'src/test/kontrol/term-lemmas.k'
+module-import              = 'RepoTokenListInvariantsTest:TERM-LEMMAS'
+ast                        = true
+auxiliary-lemmas           = true
+
+[prove.setup]
+foundry-project-root       = '.'
+verbose                    = false
+debug                      = false
+max-depth                  = 100000
+max-iterations             = 10000
+reinit                     = false
+cse                        = false
+workers                    = 1
+max-frontier-parallel      = 6
+maintenance-rate           = 24
+assume-defined             = true
+no-log-rewrites            = true
+kore-rpc-command           = 'kore-rpc-booster --no-post-exec-simplify'
+failure-information        = true
+counterexample-information = true
+minimize-proofs            = false
+fail-fast                  = true
+smt-timeout                = 16000
+smt-retry-limit            = 0
+break-every-step           = false
+break-on-jumpi             = false
+break-on-calls             = false
+break-on-storage           = false
+break-on-basic-blocks      = false
+break-on-cheatcodes        = false
+auto_abstract              = true
+run-constructor            = false
+bmc-depth                  = 3
+match-test                 = [
+        "RepoTokenListInvariantsTest.setUp",
+        "TermAuctionListInvariantsTest.setUp",
+    ]
+ast                        = true
+
+[prove.tests]
+foundry-project-root       = '.'
+verbose                    = false
+debug                      = false
+max-depth                  = 100000
+max-iterations             = 10000
+reinit                     = false
+cse                        = false
+workers                    = 1
+max-frontier-parallel      = 6
+maintenance-rate           = 24
+assume-defined             = true
+no-log-rewrites            = true
+kore-rpc-command           = 'kore-rpc-booster --no-post-exec-simplify'
+failure-information        = true
+counterexample-information = true
+minimize-proofs            = false
+fail-fast                  = true
+smt-timeout                = 16000
+smt-retry-limit            = 0
+break-every-step           = false
+break-on-jumpi             = false
+break-on-calls             = false
+break-on-storage           = false
+break-on-basic-blocks      = false
+break-on-cheatcodes        = false
+auto_abstract              = true
+run-constructor            = false
+match-test                 = [
+        "RepoTokenListInvariantsTest.testInsertSortedNewToken",
+        "RepoTokenListInvariantsTest.testInsertSortedDuplicateToken",
+        "RepoTokenListInvariantsTest.testRemoveAndRedeemMaturedTokens",
+        "TermAuctionListInvariantsTest.testInsertPendingNewOffer",
+        "TermAuctionListInvariantsTest.testInsertPendingDuplicateOffer",
+        "TermAuctionListInvariantsTest.testRemoveCompleted",
+    ]
+ast                        = true
+
+[show.default]
+foundry-project-root       = '.'
+verbose                    = true
+debug                      = false

src/RepoTokenList.sol

@@ -243,7 +243,7 @@ library RepoTokenList {
         address prev = current;
         while (current != NULL_NODE) {
             address next;
-            if (getRepoTokenMaturity(current) < block.timestamp) {
+            if (getRepoTokenMaturity(current) <= block.timestamp) {
                 bool removeMaturedToken;
                 uint256 repoTokenBalance = ITermRepoToken(current).balanceOf(address(this));
 
@@ -337,6 +337,7 @@ library RepoTokenList {
      * @param repoToken The repoToken to validate and insert
      * @param discountRateAdapter The discount rate adapter
      * @param asset The address of the base asset
+     * @return validRepoToken Whether the repoToken is valid
      * @return discountRate The discount rate to be applied to the validated repoToken 
      * @return redemptionTimestamp The redemption timestamp of the validated repoToken     
      */
@@ -345,14 +346,14 @@ library RepoTokenList {
         ITermRepoToken repoToken,
         ITermDiscountRateAdapter discountRateAdapter,
         address asset
-    ) internal returns (uint256 discountRate, uint256 redemptionTimestamp) {
+    ) internal returns (bool validRepoToken, uint256 discountRate, uint256 redemptionTimestamp) {
         discountRate = listData.discountRates[address(repoToken)];
         if (discountRate != INVALID_AUCTION_RATE) {
             (redemptionTimestamp, , ,) = repoToken.config();
 
             // skip matured repoTokens
             if (redemptionTimestamp < block.timestamp) {
-                revert InvalidRepoToken(address(repoToken));
+                return (false, discountRate, redemptionTimestamp); //revert InvalidRepoToken(address(repoToken));
             }
 
             uint256 oracleRate = discountRateAdapter.getDiscountRate(address(repoToken));
@@ -368,11 +369,13 @@ library RepoTokenList {
 
             (isRepoTokenValid, redemptionTimestamp) = validateRepoToken(listData, repoToken, asset);
             if (!isRepoTokenValid) {
-                revert InvalidRepoToken(address(repoToken));
+                return (false, discountRate, redemptionTimestamp);
             }
             insertSorted(listData, address(repoToken));
             listData.discountRates[address(repoToken)] = discountRate;
         }
+
+        return (true, discountRate, redemptionTimestamp);
     }
 
     /**
@@ -394,6 +397,8 @@ library RepoTokenList {
             return;
         }
 
+        uint256 maturityToInsert = getRepoTokenMaturity(repoToken);
+
         address prev;
         while (current != NULL_NODE) {
 
@@ -403,7 +408,6 @@ library RepoTokenList {
             }
 
             uint256 currentMaturity = getRepoTokenMaturity(current);
-            uint256 maturityToInsert = getRepoTokenMaturity(repoToken);
 
             // Insert repoToken before current if its maturity is less than or equal
             if (maturityToInsert < currentMaturity) {

src/Strategy.sol

@@ -999,13 +999,17 @@ contract Strategy is BaseStrategy, Pausable, ReentrancyGuard {
         }
 
         // Validate and insert the repoToken into the list, retrieve auction rate and redemption timestamp
-        (, uint256 redemptionTimestamp) = repoTokenListData
+        (bool isRepoTokenValid , , uint256 redemptionTimestamp) = repoTokenListData
             .validateAndInsertRepoToken(
                 ITermRepoToken(repoToken),
                 discountRateAdapter,
                 address(asset)
             );
 
+        if (!isRepoTokenValid) {
+                revert RepoTokenList.InvalidRepoToken(repoToken);
+        }
+
         // Sweep assets and redeem repoTokens, if needed
         _redeemRepoTokens(0);