Conversation
Contributor
There was a problem hiding this comment.
🟡 Changes recommended
Several newly added invariants in XLS-0066 contradict existing specified state changes (and contain an internal definition inconsistency), which would mis-specify normative behavior.
Once you've addressed the issues Copilot identified, you can request another Copilot review.
Pull request overview
This PR strengthens the normative “Invariants” sections in the lending and vault XLS documents, aiming to make ledger-impact constraints explicit for broker deletion, loan lifecycle operations, and vault deletion.
Changes:
- Adds invariants for
LoanBrokerDelete,LoanSet,LoanDelete,LoanManage, andLoanPayin XLS-0066 (replacing severalTBDplaceholders). - Adds an explicit invariant in XLS-0065 requiring
VaultDeleteto delete the vault referenced by the transaction.
File summaries
| File | Description |
|---|---|
| XLS-0066-lending-protocol/README.md | Adds/expands invariants for multiple lending transactions (broker deletion, loan create/delete/manage/pay). |
| XLS-0065-single-asset-vault/README.md | Adds an explicit invariant tying VaultDelete to the VaultID in the transaction. |
Review details
Suppressed comments (1)
XLS-0066-lending-protocol/README.md:1229
- This invariant says
LoanBroker.DebtTotalmust be unchanged, but the defined state changes allow settingLoanBroker.DebtTotal = 0whenLoanBroker.OwnerCount == 0to forgive rounding dust (3.9.4 step 5). The invariant should allow that explicit adjustment.
- The transaction must change nothing else: `Vault.AssetsTotal`, `Vault.AssetsAvailable`, `Vault.LossUnrealized`, the Vault pseudo-account balance, `LoanBroker.DebtTotal`, `LoanBroker.CoverAvailable` and the LoanBroker pseudo-account balance all unchanged.
- Files reviewed: 2/2 changed files
- Comments generated: 2
- Review effort level: Lite
💡 Configure MCP servers for context-aware, tailored reviews. Learn more in the docs.
|
|
||
| - If `LoanBroker.OwnerCount = 0` the `DirectoryNode` will have at most one node (the root), which will only hold entries for `RippleState` or `MPToken` objects. | ||
| - The transaction must not touch any `Loan`. | ||
| - `LoanBroker.DebtTotal` and `LoanBroker.CoverAvailable` must both be zero when the `LoanBroker` is deleted. |
| #### 3.10.6 Invariants | ||
|
|
||
| **TBD** | ||
| This section uses `DefaultAmount` and `DefaultCovered` as computed in section 3.10.5, both taken from the pre-transaction state; for a cash-basis Vault, `DefaultAmount = Loan.PrincipalOutstanding`. Equalities on IOU amounts are evaluated as a single rounded residual with a tolerance of one unit at the comparison scale; XRP and MPT amounts compare exactly. |
This branch has not been deployed
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
High Level Overview of Change
Context of Change
Type of Change