Error Redistribution - Manual Review

[dapp-whisperer]

See testBrokenInvariantFive in EchidnaToFoundry.t.sol

There is a big lastEBTCDebtErrorRedistribution in this example, > 1e18
(lastEBTCDebtErrorRedistribution is used to calculate the remainder error in rounding and store it for the calc)

I would assume it would never go above 1 since it's a value that once it goes above 1e18 it would be added as 1 unit of debt

This test is going to require some manual review to see if the lastEBTCDebtErrorRedistribution is correct and a reasonable finding to have occur.

[rayeaster]

@dapp-whisperer the lastEBTCDebtErrorRedistribution in this test is correct as expected. Please note that lastEBTCDebtErrorRedistribution is capped by totalStake instead of 1e18 as it is the residue from redistributed debt divided by totalStake(see _redistributeDebt() in LiquidationLibrary.sol):

        uint256 EBTCDebtNumerator = (_debt * DECIMAL_PRECISION) + lastEBTCDebtErrorRedistribution;
        ......
        uint256 EBTCDebtRewardPerUnitStaked = EBTCDebtNumerator / _totalStakes;

        lastEBTCDebtErrorRedistribution =
            EBTCDebtNumerator -
            (EBTCDebtRewardPerUnitStaked * _totalStakes);

In this particular test case, the debt to be redistributed is 73080202887917575 and totalStake is 2837658138915260125 thus the calculated error is

     EBTCDebtNumerator = 73080202887917575 * 1e18 = 73080202887917575000000000000000000
     EBTCDebtRewardPerUnitStaked = 73080202887917575000000000000000000 / 2837658138915260125 = 25753702282070398
     lastEBTCDebtErrorRedistribution  = 73080202887917575000000000000000000 - 25753702282070398 * 2837658138915260125 = 1856500538267720250 < totalStake