AI/pseudotokens: state additional invariant tez<>0 => pseudotokens<>0 (Follow-up from "Proto/AI: pseudotokens for delegators only")
And prove it!
The following discussion from !9533 (merged) should be addressed:
-
@rafoo_ started a discussion: (+2 comments) In version 5 I have:
- done very minor changes (see the diff), and
- reworked the history.
I'm fine with everything except the following commit: f2186a2f. I think it needs at least a justification.
Basically, the assertion introduced by this commit is that if the frozen deposits (in tez) of the costakers is not null, then so are the pseudotokens. But this is far from obvious in a world full of division rounding. How confident are we that the last mutez on the costaked frozen deposits can indeed be unstaked? I guess we can argue that when the last unstake happens, we are in a situation in which a single costaker owns all the pseudotokens and there cannot be any rounding error in
pseudotokens_of
andtez_of
in this particular case contrary to the general case in which we tolerate the result to be wrong by up to one mutez or one pseudotoken.Do we really want to rely on this instead of just moving this new
assert
three lines further?