CompoundMath's fixed-point arithmetics known limitations

[Rubilmax]

Given the following operations from CompoundMath:

function mul(uint256 x, uint256 y) internal pure returns (uint256) {
    return (x * y) / 1e18;
}

function div(uint256 x, uint256 y) internal pure returns (uint256) {
    return ((1e18 * x * 1e18) / y) / 1e18;
}

The following theorem does not hold: $\forall x,y, \forall \mu,\nu, (x.mul(\mu) + y.mul(\nu)).div(\mu + \nu) = x.mul(\mu.div(\mu + \nu)) + y.mul(\nu.div(\mu + \nu))$

for values: $x < 10^{18}, \mu < 10^{18 - \log10(x)}$ and $y < 10^{18}, \nu < 10^{18 - \log10(y)}$

Proof

Because $x \times \mu < 10^{18}$ and $y \times \nu < 10^{18}$ which leads the operation mul to truncate to 0

This issue leads rounding errors with values: $x < 10^{18}, \mu < 10^{18}, \log10(x \times \mu) \geqslant 18$ or $y < 10^{18}, \nu < 10^{18}, \log10(y \times \nu) \geqslant 18$ [needs a proof]

But the theorem (at least) holds for values: $\mu \geqslant 10^{18}$ and $y \geqslant 10^{18}$

[Rubilmax]

Here is a failing test case:

function testMath() public {
    uint256 q1 = 643480029;
    uint256 q2 = 643480029;

    uint256 f1 = 1;
    uint256 f2 = 1010000000;
    uint256 total = f1 + f2;

    uint256 actual = (q1.mul(f1) + q2.mul(f2)).div(total);
    uint256 expected = q1.mul(f1.div(total)) + q2.mul(f2.div(total));

    assertApproxEqAbs(actual, expected, 0);
}

with output:

Expected: 643480028
Actual: 0
Delta: 643480020

i.e. 100% error

[MerlinEgalite]

Should we keep it live @Rubilmax perhaps we can create a discussion instead of an issue?

[Rubilmax]

I think that having it as an issue is already almost useless and that discussions are even less seen ; whereas this is something one should be aware when using compMul/compDiv. I'd rather have it at the end of the README or another similar ISSUES.md file

[MerlinEgalite]

Don't bother with that any solution is fine (even keeping the issue)