-
Notifications
You must be signed in to change notification settings - Fork 16
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Correct treatment of excess when burning kit #211
Conversation
src/burrow.ml
Outdated
@@ -59,13 +57,10 @@ type liquidation_result = (liquidation_type * liquidation_details) option | |||
[@@@coverage on] | |||
|
|||
let[@inline] assert_burrow_invariants (_b: burrow) : unit = | |||
assert (_b.outstanding_kit = kit_zero || _b.excess_kit = kit_zero); | |||
(* FIXME: no properties left to check *) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
🎉
…hing more reasonable)
These changes affect the API (and gas usage quite some I expect) so there's much more work to be done. In comments, in optimizations, and in triple-checking the changes.
9f6d8ae
to
dcce1cc
Compare
|
So @utdemir @dorranh, this should be ready for reviewing (@dorranh not many things changed since the last time you had a look, but you might want to skim it). The size and gas cost differences I think are good; only
I think the clarity is worth the few extra bytes/gas, especially given that that's where the bug was before. Give me a shout if you disagree and I can try and change I started working on paper to prove my postulate that Edit: Progress here: https://gist.github.com/gkaracha/6623da298944d23f5ebbd621f32b264d |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Nice! I looked through a second time, and it seems to all be in order as far as I can tell. I am a bit surprised that we didn't need to change more tests for this instead of mostly needing to just remove obsolete ones. Though I suppose that it kind of makes sense since this change is largely internal and doesn't seem to affect a given account's balance in the fa2 ledger as far as I can tell.
Right?! I thought so too and was not amused that not many tests failed. I think that the tests not failing means that our coverage could be improved. For example the changes to |
|
This PR fixes a long-standing bug around the concept of excess kit and removes the
excess_kit
field in burrows. It's still work in progress but I thought I'd open the PR early so that perhaps you could have a look too @utdemir @dorranh; the changes are rather pervasive (though necessary, I believe) and I really could use more pairs of eyes. Let me know what you think! 🙂Closes #209.
Closes #136.
Summary:
excess_kit
is removed from the representation of burrows. This means that in cases where more thanburrow.outstanding_kit
is attempted to be burned/deposited, the excess is directly credited to the burrow owner on the FA2 ledger. This applies both to explicit burns (viaburrow_burn_kit
) and implicit burns (viaburrow_return_kit_from_auction
).assert_burrow_invariants
now has no invariants to check. I've left it for the time being, but I think we can just get rid of it.burrow_burn_kit
andburrow_return_kit_from_auction
: they both need to return to the caller how much of that kit really got burned and how much did not. This is a good thing. This change allows us to remove fromparameters.circulating_kit
and theparameters.outstanding_kit
the kit that got repaid, but not the part that did not. This was the source of internalError_KitSubNegative error raised #209: previously we would erroneously try to remove all the kit we tried to burn from theparameters.outstanding_kit
, even if some of it really ended up in theexcess_kit
field. I left a big comment about what happens with each part of the kit to be burned (and a few assertions) intouch_liquidation_slice
to clarify this.parameters.outstanding_kit
), which is what internalError_KitSubNegative error raised #209 is about. I have not proven this yet, but I believe that the calculations imply thatparameters.outstanding_kit >= sum burrow_i.outstanding_kit
. If that is indeed the case, then sound burning per burrow implies sound burning for the total outstanding kit. I expect us to observe this inequality when we address Ensure parameters.oustanding_kit does not drift far from the real value #156, but I will try to prove it before merging this PR anyway.If the inequality does not hold then we can always circumvent the issue of internalError_KitSubNegative error raised #209 by a simple if-then-else: never try to burn more kit from
parameters.outstanding_kit
than there is. I don't like this catch-all because it could hide other bugs, but if the inequality above really does not hold at least this if-then-else works as an absorbing bound at 0, essentially showing that we have to burn more kit than we thought were outstanding. If anything, it reduces the discrepancy betweenparameters.outstanding_kit
andsum burrow_i.outstanding_kit
.touch_liquidation_slice
and friends take bigger parts of the state as arguments to be able to update the FA2 ledger when we give kit to the burrow owners. In general I wrote things having clarity in mind, but we have to make sure that the gas costs don't increase too much because of this before merging (if so, we have to re-uglify the code).