debunk: g-08 due to ghost debt

[GalloDaSballo]

Shows how 1 wei of ghost debt messes up the invariant

Would like advice @rayeaster @dapp-whisperer

[GalloDaSballo]

We can obviously ack and be done, but we should figure out why this is happening

[rayeaster]

@GalloDaSballo IMO this is similar to previous General-08 break:

• There is a 1 wei difference between the sum of all CDP debts and the debt accounting in activePool after liquidation at step 5 due to rounding issue and is tracked by global variable lastEBTCDebtErrorRedistribution in CdpManagerStorage

• And the debt number is so small (1 wei or 2 wei) thus the TCR comparison exceeds the expected tolerance limit:

2420000000000000022(coll) * 74280000000000000 (price) / 1 (debt) vs
2420000000000000022(coll) * 74280000000000000 (price) / 2 (debt)

The recommendation still holds for this sequence: "It might make sense for the invariant to compare the sum(cdpDebt) & activePool.getSystemDebt() directly. Similar for sum(cdpColl) & activePool.getSystemCollShares()"

[GalloDaSballo]

• lastEBTCDebtErrorRedistribution

Can you explain to me this:

• Will the pendingEBTC debt be redistributed in the future, or is it forever stuck?

If it will be redistributed, what's the simplest example of it happening?

[rayeaster]

• lastEBTCDebtErrorRedistribution

Can you explain to me this:

• Will the pendingEBTC debt be redistributed in the future, or is it forever stuck?

If it will be redistributed, what's the simplest example of it happening?

it will be used in next liquidation with bad-debt as the redistributed debt is added by the accumulated error

The simplest example is to have another liquidation that cause bad-debt then the error will be used to calculate new redistributed debt per stake unit

[GalloDaSballo]

@dapp-whisperer I would merge as part of acknowledge broken invariants cases