internalError_KitSubNegative error raised

[gkaracha]

While developing #207 I came across a scenario which raises an internal error (internalError_KitSubNegative). I tried to simplify the example a bit though it probably can be simplified further. The scenario goes as follows:

1. Initial state (timestamp:0, level:0):

   last_index = 1_000_000n
   circulating = 0mukit
   outstanding = 0mukit

2. After (~seconds_passed:0 ~blocks_passed:0), create a burrow with 10_000_000mutez (1tez deposit + 9tez collateral).

   circulating = 0mukit
   outstanding = 0mukit

3. After (~seconds_passed:1181 ~blocks_passed:18), mint as much kit as possible (4_285_714mukit).

   circulating = 4_285_714mukit
   outstanding = 4_285_714mukit
   alice_addr : 4_285_714mukit

4. After (~seconds_passed:0 ~blocks_passed:0), set the last observed index to 1_357_906n

5. After (~seconds_passed:(60 * 191) ~blocks_passed:191), touch checker (last index still at 1_357_906n).

   circulating = 205_969_055mukit  -- 4_285_714mukit minted + 201_683_333 touch reward + 8mukit cfmm accrual
   outstanding = 4_285_807mukit    -- 4_285_714mukit minted scaled up (burrowing fees and/or imbalance)
   alice_addr : 205_969_047mukit  -- 4_285_714mukit minted + 201_683_333 touch reward
   checker    : 8mukit            -- accrual of burrow fees to cfmm.kit

6. After (~seconds_passed:342 ~blocks_passed:5), mark the burrow for liquidation.

   circulating = 205_969_055mukit  -- (as it was) 4_285_714mukit minted + 201_683_333 touch reward + 8mukit cfmm accrual
   outstanding = 4_285_807mukit    -- (as it was) 4_285_714mukit minted scaled up (burrowing fees and/or imbalance)
   alice_addr : 205_969_047mukit  -- (as it was) 4_285_714mukit minted + 201_683_333 touch reward
   checker    : 8mukit            -- (as it was) accrual of burrow fees to cfmm.kit

7. After (~seconds_passed:63 ~blocks_passed:1), touch checker to start an auction (last index still at 1_357_906n).

   circulating = 206_644_055mukit -- (+675_000mukit touch reward)
   outstanding = 4_285_809mukit   -- (+2mukit (burrowing fees and/or imbalance))
   alice_addr : 206_644_047mukit -- (+675_000mukit touch reward)
   checker    : 8mukit           -- (as it was) accrual of burrow fees to cfmm.kit

8. After (~seconds_passed:394 ~blocks_passed:6), place a bid of 4_285_824mukit.

   circulating = 206_644_055mukit -- (as it was)
   outstanding = 4_285_809mukit   -- (as it was)
   alice_addr : 202_358_223mukit -- (-4_285_824mukit auction bid)
   checker    : 4_285_832mukit   -- (8mukit in cfmm.kit + 4_285_824mukit auction bid)

9. If we touch checker now, what happens is that the received kit (the bid, equal to 4_285_824mukit) is subtracted (burned) from the outstanding kit (currently at 4_285_820mukit, 4mukit less than the bid) and we get a failure.

Each individual step above makes sense to me, so I am not entirely sure how to classify this error. Some thoughts:

• On one hand, I am troubled that the out-of-thin-air reward can increase the kit in circulation an arbitrary amount (that would be a specification bug,I think).
• On the other hand, I assume that the total outstanding can always be decreased due to other reasons (e.g., if the value of kit rises); the implementation should be able to deal with this (that is, never try to burn more than the total outstanding kit) (that would be an implementation bug, I think).
• On the other-other hand (:upside_down_face:) I find it weird that we can have kit in circulation without it being backed by tez. I guess the touch reward is in a way justified/backed by the gas costs paid when touching?

Any thoughts?

[gkaracha]

More thoughts on this:

I believe it's a more general issue, arising when parameters.circulating_kit exceeds parameters.outstanding_kit. We might thus be able to treat similar cases similarly.

• Small-scale: when a burrow owner wants to burn more kit than is outstanding, we store the excess into the burrow.excess_kit field. (How exactly to mark that excess kit as being in circulation is not entirely clear at the moment (see https://github.com/tezos-checker/checker/issues/136#issuecomment-856744297), but that's a separate topic.) This prevents underflows and allows us to gracefully deal with cases where either the burrow owner or a liquidation auction tries to burn more kit than is outstanding.

• Large-scale: the issue at hand. When the total parameters.circulating_kit is greater than parameters.outstanding_kit, it is possible that someone will try to burn more kit than is outstanding. After all, I think that checker should be able to deal gracefully with this case as well; the system is supposed to be able to deal with both parameters.circulating_kit <= parameters.outstanding_kit and parameters.circulating_kit > parameters.outstanding_kit.

I thought initially that perhaps burning from the total parameters.outstanding_kit the burrow.outstanding_kit when touching a slice would be sufficient to protect us from the error above, but I don't think so after all. As stated in #156, parameters.oustanding_kit can potentially drift from the real value (i.e., sum burrow_i.outstanding_kit), and we have not evaluated yet how far can that be. My expectation (given the calculations) is that

parameters.oustanding_kit >= sum burrow_i.outstanding_kit

but that remains to be seen. Hopefully #204 will help with this.

So, I think the safest option when returning a slice (or, in general, when removing kit from parameters.outstanding_kit) is to burn up to parameters.outstanding_kit, and deal with the remaining kit differently. The best way to deal with it that I can think of is to burn the excess as well (i.e., subtract it from parameters.circulating_kit). So, in short, when touching a slice:

kit_to_remove_from_outstanding = min parameters.outstanding_kit kit_from_auction
kit_to_remove_from_circulating = kit_from_auction

parameters.outstanding_kit = parameters.outstanding_kit - kit_to_remove_from_outstanding
parameters.circulating_kit = parameters.circulating_kit - kit_to_remove_from_circulating

I am not sure what this means for the system though (e.g., if it introduces the wrong incentives, or positive feedback loops).

@murbard I could use your input on this one :slightly_smiling_face:

Edit: Actually, I think that we should eliminate the concept of excess_kit as well, for the reasons I mentioned on #136. I think it's much cleaner if we just credit the burrow owner the excess kit directly.