[Certora] Spec for balance and lossIndex#534
Draft
jhoenicke wants to merge 12 commits into
Draft
Conversation
…add hashOffer,isLeaf summaries
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
2 participants
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.
Work in progress: Verification currently times out.
This adds a specification for the lossIndex. The goal is to prove that the sum of all positive balanceOfAfterSlashing is less equal to totalUnits.
We prove as invariant that
(sumof balance/user.lossIndex*PRECISION) * obligation.lossIndex <= totalUnits*PRECISIONwhere the sum only ranges over the positive balances. We keep the valuesbalance/user.lossIndexas a fixed point number in the spec with a very large PRECISION value that avoids rounding. The value is 0 if the balance is negative or the user.lossIndex is 0. Think of PRECISION as being 2^128!, a number that is divisible by any positive uint128. We leave PRECISION unspecified and only require it to be positive and divisible by the accessed user.lossIndex. So the solver can choose any positive value that is divisible by any user lossIndex it sees.There are currently timeouts related to static analysis; this is why the pull request is not ready yet.
Everything except withdraw, liquidate, and take is already verified, but these missing functions are the most important ones.