Kontrol property tests for RepoTokenList and TermAuctionList invariants
#47
Conversation
|
Important Review skippedAuto reviews are disabled on base/target branches other than the default branch. Please check the settings in the CodeRabbit UI or the You can disable this status message by setting the WalkthroughThe pull request introduces significant updates to the project, including the addition of a new submodule for Changes
Possibly related PRs
Poem
Thank you for using CodeRabbit. We offer it for free to the OSS community and would appreciate your support in helping us grow. If you find it useful, would you consider giving us a shout-out on your favorite social media? 🪧 TipsChatThere are 3 ways to chat with CodeRabbit:
Note: Be mindful of the bot's finite context window. It's strongly recommended to break down tasks such as reading entire modules into smaller chunks. For a focused discussion, use review comments to chat about specific files and their changes, instead of using the PR comments. CodeRabbit Commands (Invoked using PR comments)
Other keywords and placeholders
CodeRabbit Configuration File (
|
![coderabbitai[bot]](https://avatars.githubusercontent.com/in/347564?s=60&v=4){kind=small}
There was a problem hiding this comment.
Actionable comments posted: 10
🧹 Outside diff range and nitpick comments (8)
.gitmodules (1)
20-22: LGTM! Consider specifying a branch for consistency.The addition of the "kontrol-cheatcodes" submodule is correct and aligns well with the PR objectives of introducing symbolic property tests using Kontrol. The entry follows the proper format and is consistent with other submodule entries.
For consistency with some of the other submodule entries, consider specifying a branch:
[submodule "lib/kontrol-cheatcodes"] path = lib/kontrol-cheatcodes url = https://github.com/runtimeverification/kontrol-cheatcodes + branch = mainThis helps to pin the submodule to a specific branch, which can be beneficial for reproducibility and version control.
src/test/kontrol/TermRepoServicer.sol (3)
11-14: LGTM: Symbolic initialization looks correct.The
initializeSymbolicfunction correctly sets up the contract for symbolic execution by marking the contract's storage as symbolic and initializing the_termRepoTokenstate variable.Consider making this function
internalorexternalinstead ofpublicto be more explicit about its intended use in the testing environment.
35-37: LGTM:purchaseTokenfunction is well-implemented for symbolic testing.The
purchaseTokenfunction is correctly implemented as a view function. The use ofkevm.freshAddress()is appropriate for symbolic execution, allowing the simulation of different possible purchase token addresses in various test scenarios.Note that this function's implementation is identical to
termRepoLocker. While this might be intentional for testing purposes, it's worth considering if these functions should return distinct addresses in some scenarios.
1-38: Summary: Well-structured symbolic test contract with minor improvement opportunities.Overall, the
TermRepoServicercontract is well-implemented for symbolic testing purposes. It correctly uses Kontrol-specific cheatcodes and implements the required interface functions.Key points:
- The contract structure and imports are appropriate.
- Most functions are correctly implemented for symbolic testing.
- The
redeemTermRepoTokensfunction could be improved to better capture all possible states.Next steps:
- Address the suggested improvements in the
redeemTermRepoTokensfunction.- Consider adding comments to explain the purpose of using
kevm.freshAddress()intermRepoLockerandpurchaseTokenfunctions.- Implement actual token redemption logic in
redeemTermRepoTokensif required for comprehensive testing.To enhance the effectiveness of this symbolic test contract, consider adding more complex scenarios that test the interaction between different functions and state changes. This could help uncover potential edge cases or unexpected behaviors in the actual implementation.
kontrol.toml (2)
1-10: Build configuration looks good, consider verbosity setting.The [build.default] section is well-configured for a Foundry project using Kontrol. The inclusion of auxiliary lemmas and AST generation is appropriate for formal verification.
Consider setting
verbose = falsefor regular runs to reduce output, and only enable it when debugging is necessary.
12-45: Prove configuration is comprehensive, consider performance optimizations.The [prove.default] section provides a detailed configuration for the proving process, which aligns well with the PR objectives. The specified test cases for
RepoTokenListInvariantsTestare correctly included.Consider the following optimizations:
- Adjust
max-depthandmax-iterationsbased on the expected complexity of your proofs to avoid unnecessarily long-running processes.- Increase
workersif running on a multi-core system to potentially improve performance.- Consider enabling
minimize-proofs = trueto get more concise proof outputs, which can be helpful for debugging and understanding the verification process.src/RepoTokenList.sol (1)
Line range hint
1-428: Summary: Improvements toinsertSortedfunctionThe changes in this file enhance the
insertSortedfunction by:
- Properly initializing the
nextpointer when inserting into an empty list.- Modifying the insertion logic for tokens with equal maturities.
- Correctly terminating the list when inserting at the end.
These changes align with the PR objectives of maintaining list invariants and improve the overall robustness of the
RepoTokenListlibrary.However, it's crucial to verify that the change in insertion logic for equal maturities (from
<=to<) doesn't have unintended consequences in other parts of the codebase. Please review the results of the verification script and ensure that this change aligns with the expected behavior across the entire system.src/test/kontrol/term-lemmas.k (1)
47-191: Suggestion: Enhance Documentation for Complex ClaimsThe claims in the
TERM-LEMMAS-SPECmodule involve complex expressions and arithmetic operations. Providing additional comments or explanations for each claim can improve readability and maintainability.Consider adding descriptive comments above each claim to explain its purpose and any important details.
📜 Review details
Configuration used: CodeRabbit UI
Review profile: CHILL
📒 Files selected for processing (10)
- .gitmodules (1 hunks)
- kontrol.toml (1 hunks)
- lib/kontrol-cheatcodes (1 hunks)
- src/RepoTokenList.sol (3 hunks)
- src/TermAuctionList.sol (4 hunks)
- src/test/kontrol/Constants.sol (1 hunks)
- src/test/kontrol/RepoToken.sol (1 hunks)
- src/test/kontrol/RepoTokenListInvariants.t.sol (1 hunks)
- src/test/kontrol/TermRepoServicer.sol (1 hunks)
- src/test/kontrol/term-lemmas.k (1 hunks)
✅ Files skipped from review due to trivial changes (1)
- lib/kontrol-cheatcodes
🔇 Additional comments not posted (20)
src/test/kontrol/Constants.sol (2)
1-1: LGTM: Up-to-date Solidity versionThe pragma statement specifies Solidity version 0.8.23, which is current and appropriate for this project.
3-4: Verify the rationale behind the chosen upper bound valuesThe constants
ETH_UPPER_BOUNDandTIME_UPPER_BOUNDare defined with large values (2^95 and 2^35 respectively). While these seem reasonable for upper bounds in property-based testing, it's important to ensure they align with the intended use cases.
ETH_UPPER_BOUND(2^95 ≈ 3.9e28) is significantly larger than the total ETH supply. This might be intentional to account for wei values or extreme test cases.TIME_UPPER_BOUND(2^35 ≈ 34 years in seconds) seems reasonable for time-related tests, covering a wide range of scenarios.Please confirm that these values are intentionally chosen and appropriate for the Kontrol property tests being implemented.
src/test/kontrol/TermRepoServicer.sol (3)
1-8: LGTM: Contract structure and imports are appropriate.The contract structure, inheritance, and imports are well-defined for a symbolic test contract. The use of an up-to-date Solidity version (^0.8.23) is commendable.
27-29: LGTM:termRepoTokenfunction is correctly implemented.The
termRepoTokenfunction is properly implemented as a view function and correctly returns the_termRepoTokenaddress, adhering to theITermRepoServicerinterface.
31-33: LGTM:termRepoLockerfunction is well-implemented for symbolic testing.The
termRepoLockerfunction is correctly implemented as a view function. The use ofkevm.freshAddress()is appropriate for symbolic execution, allowing the simulation of different possible locker addresses in various test scenarios.kontrol.toml (2)
1-50: Well-structured Kontrol configuration for RepoTokenList invariant testing.This
kontrol.tomlfile provides a comprehensive configuration for using Kontrol to perform symbolic property tests on theRepoTokenListinvariants. The configuration is well-aligned with the PR objectives and covers all necessary aspects of the build, prove, and show processes.The file structure and settings demonstrate a good understanding of formal verification practices. With the minor optimizations suggested in the previous comments, this configuration should provide a robust foundation for verifying the
RepoTokenListinvariants.
47-50: Show configuration is basic, consider if additional settings are needed.The [show.default] section provides a minimal configuration that mirrors the basic settings from the build and prove sections.
It might be beneficial to review if there are any additional 'show' specific settings that could enhance the output or visualization of the verification results. Let's check the Kontrol documentation for any such settings:
✅ Verification successful
Show configuration is verified and sufficient.
The
[show.default]section provides a minimal configuration, and no additional 'show' specific settings were found that could enhance the output or visualization.🏁 Scripts executed
The following scripts were executed for the analysis:
Script:
#!/bin/bash # Description: Search for additional 'show' configuration options in Kontrol documentation # Test: Look for 'show' related configuration options in Kontrol documentation rg --type md -i 'show.*configuration|configuration.*show' .Length of output: 61
Script:
#!/bin/bash # Description: Search for related configuration options that might influence 'show' functionality # Look for configurations related to display, visualization, or output that could be associated with 'show' rg --type toml -i 'display|visualization|output' .Length of output: 52
Script:
#!/bin/bash # Description: Search for all occurrences of 'show.default' to understand its usage context rg --type toml 'show\.default' .Length of output: 64
src/TermAuctionList.sol (4)
106-106: Approved: Explicit NULL_NODE assignment for list integrityThe addition of
listData.nodes[offerId].next = NULL_NODE;when inserting into an empty list is a good practice. It explicitly sets thenextpointer of the new (and only) node toNULL_NODE, maintaining the integrity of the linked list structure.
123-123: Clarification needed: Change in insertion logicThe comparison operator has been changed from
<=to<in the condition for inserting a new auction offer. This modification alters the insertion logic, potentially changing the order of auction offers with the same auction address.Could you please clarify:
- Is this change intentional?
- Are auction addresses guaranteed to be unique?
- What are the implications of this change on the ordering of offers with the same auction address?
This information will help ensure that the change aligns with the intended behavior of the
insertPendingfunction.
139-139: Approved: Consistent NULL_NODE assignment for list integrityThe addition of
listData.nodes[offerId].next = NULL_NODE;when inserting a new offer at the end of the list is a good practice. It explicitly sets thenextpointer of the new last node toNULL_NODE, maintaining the integrity of the linked list structure. This change is consistent with the similar addition at the beginning of the function and ensures proper list termination.
Line range hint
1-380: Summary of TermAuctionList.sol reviewThe changes in this file generally improve the integrity of the linked list structure used for managing auction offers. Two additions explicitly set the
nextpointer toNULL_NODEwhen inserting at the beginning or end of the list, which is a good practice.However, the change in the comparison operator (from
<=to<) in theinsertPendingfunction requires clarification. This modification could potentially alter the ordering of offers with the same auction address, and its implications need to be understood and verified.Once the clarification is provided for the comparison operator change, and assuming no issues are found, the overall changes to this file appear to enhance the robustness of the linked list implementation.
src/RepoTokenList.sol (3)
387-387: LGTM: Proper initialization of thenextpointerThis change correctly initializes the
nextpointer of the newly inserted repo token toNULL_NODEwhen it becomes the head of an empty list. This ensures the list's integrity is maintained and aligns with the PR objectives of preserving list invariants.
419-419: LGTM: Proper termination of the listThis change correctly sets the
nextpointer of the newly inserted repo token toNULL_NODEwhen it's inserted at the end of the list. This ensures the list is properly terminated and maintains its integrity, aligning with the PR objectives of preserving list invariants.
403-403: LGTM: Modified insertion logic for equal maturitiesThe change from
<=to<in the insertion condition modifies the behavior for repo tokens with equal maturities. Now, a new repo token with the same maturity as an existing token will be inserted after the existing token, rather than before it. This change maintains the stability of the list by preserving the relative order of tokens with the same maturity.Please verify that this change aligns with the intended behavior and doesn't break any assumptions in other parts of the code. Run the following script to check for any potential impacts:
src/test/kontrol/RepoToken.sol (2)
18-33: Ensure symbolic variables have appropriate constraintsIn the
initializeSymbolic()function, you generate fresh symbolic variables likesenderBalance,_redemptionTimestamp, and_redemptionValue. While you assume upper bounds for these variables, consider adding constraints to prevent them from being zero or exceeding certain limits, which could lead to edge case issues or overflows during testing.
47-57: Review the use of fresh addresses inconfig()functionIn the
config()function,purchaseTokenandtermRepoCollateralManagerare set tokevm.freshAddress(). While using fresh addresses is suitable for symbolic testing, ensure that this aligns with the expected behavior and that there are no unintended side effects in the testing environment.src/test/kontrol/term-lemmas.k (4)
18-21: LGTM! Definition ofrunLemmaanddoneLemmais correctThe syntax and transformation rule for
runLemmaanddoneLemmaare well-defined and accurately implemented.
1-191: Overall ReviewThe module
TERM-LEMMASand its specifications inTERM-LEMMAS-SPECare comprehensive and add valuable lemmas for symbolic execution and formal verification. The added rules and claims enhance the reasoning capabilities of the system.
125-132: Logical Concern: Ineffective Claim in[slot-update-06]The claim
[slot-update-06]aims to compare a sliced buffer withTIMESTAMP_CELL:Int. However, the result of the#asWordand#rangefunctions may not necessarily be less than or equal toTIMESTAMP_CELL:Intwithout additional constraints.Please verify whether the claim holds under the provided requirements.
Run the following script to check if the claim is valid given the constraints:
#!/bin/bash # Description: Validate the claim `[slot-update-06]` under given conditions. # No direct commands can validate this claim, consider revisiting the mathematical logic. echo "Please review the mathematical correctness of claim [slot-update-06]."
35-38:⚠️ Potential issuePotential Logical Error: Inconsistent Condition in Rule
The rule in lines 36-38 uses the condition
orBool Y <Int Z, which differs from the original lemma where the condition isorBool Y ==Int 0. This change may alter the intended behavior of the lemma.Please verify if the condition
Y <Int Zis intentional and correct. If the goal is to handle the case whenYis zero, the condition should beY ==Int 0.Run the following script to check for similar lemmas and ensure consistency:
✅ Verification successful
Verification Successful: Condition Change is Intentional and Correct
The usage oforBool Y <Int Zin the specified rule is intentional and consistent with similar patterns in the codebase to handle specific cases involving division operations.🏁 Scripts executed
The following scripts were executed for the analysis:
Script:
#!/bin/bash # Description: Search for similar lemmas to compare conditions. rg --type k 'rule.*X ==Int.* /Word.*orBool' -A 3Length of output: 148
Script:
#!/bin/bash # Description: Search for all rules with 'orBool Y <Int Z' in their conditions. rg --type k 'rule.*orBool Y <Int Z' -A 3Length of output: 334
Script:
#!/bin/bash # Description: Search for all rules with 'orBool Y ==Int 0' in their conditions. rg --type k 'rule.*orBool Y ==Int 0' -A 3Length of output: 1552
Script:
#!/bin/bash # Description: Extract surrounding context for rules with 'orBool Y <Int Z' and 'orBool Y ==Int 0'. rg --type k -C 2 '(orBool Y <Int Z|orBool Y ==Int 0)'Length of output: 1886
lucasmt
force-pushed
the
list-invariant-tests
branch
from
61dc5d8 to
8b9ea05
Compare
lucasmt
changed the title
RepoTokenList invariantsRepoTokenList and TermAuctionList invariants
| // Create sequential addresses to ensure that list is sorted | ||
| address auction = address(uint160(1000 + count)); | ||
| // Etch the code of the auction contract into this address | ||
| vm.etch(auction, _referenceAuction.code); | ||
| TermAuction(auction).initializeSymbolic(); |
There was a problem hiding this comment.
Unfortunately, we can't make the auction addresses completely symbolic here because we need to be able to call functions in the auction contracts. So instead, we initialize sequential addresses to guarantee the sortedness of the list and etch the code of the TermAuction contract into them.
Note, however, that this means that we are not covering the cases where we have multiple offers in the list for the same auction. It would be impractical to cover all possible combinations with symbolic execution. For example, for a list with length 3 we would have 5 separate cases: all 3 offers for different auctions, 1 and 2 share an auction, 1 and 3 share an auction, 2 and 3 share an auction, all share a single auction. For length 4 this shoots up to 15.
Some options to complement this could be:
- Fuzz tests that generate different test cases with repeated auctions.
- Select a specific subset of cases and write additional symbolic tests for them.
| */ | ||
| function testRemoveCompleted(address asset) external { | ||
| // For simplicity, assume that the RepoTokenList is empty | ||
| _repoTokenList.head = RepoTokenList.NULL_NODE; |
There was a problem hiding this comment.
Since these tests focus on the invariants of the TermAuctionList, we are using an empty RepoTokenList here for simplicity, instead of initializing a general list of arbitrary size (like we do for the TermAuctionList in the setUp() function). The removeCompleted function may insert a token into this list, but the initial state of the RepoTokenList shouldn't otherwise affect the execution of the function or the TermAuctionList invariants. Note that the insertSorted function of RepoTokenList is already verified in RepoTokenListInvariants.t.sol.
| kevm.symbolicStorage(address(this)); | ||
|
|
||
| // For simplicity, choose an arbitrary number of collateral tokens | ||
| vm.assume(_collateralTokens.length == 3); |
There was a problem hiding this comment.
For simplicity, we use a fixed number of collateral tokens. We can change this to a different number if desired, and it wouldn't affect the complexity of the formal verification. But if we used a symbolic value here instead, that would considerably increase the number of branches in the symbolic execution without providing any significant extra coverage. So I don't think it's worth it.
Depends on #52.
Adds Kontrol symbolic property tests verifying that the following functions preserve the list invariants:
insertSortedandremoveAndRedeemMaturedTokens, inRepoTokenList(RepoTokenListInvariants.t.sol).insertPendingandremoveCompleted, inTermAuctionList(TermAuctionListInvariants.t.sol).Besides the test files, also includes:
kontrol-cheatcodessubmodule, which gives access to Kontrol-specific cheatcodes likesymbolicStorageandfreshUInt.term-lemmas.kwith helper lemmas for the proofs.kontrol.tomlfile with configurations to build and run the proofs.TermRepoTokenTermRepoServicerTermRepoCollateralManagerTermAuctionTermAuctionOfferLockerTermDiscountRateAdapterCounterexamples.t.sol) exercising the infinite cycle bug that was identified and fixed during formal verification.Summary by CodeRabbit
New Features
lib/kontrol-cheatcodes.kontrol.tomlfor build, prove, and show processes.RepoToken,TermRepoServicer, andRepoTokenListInvariantsTestfor improved token management and testing.Constants.sol.term-lemmas.k.Bug Fixes
RepoTokenListandTermAuctionListto ensure correct order based on maturity.Tests
RepoTokenListto verify list invariants and token management functionalities.