Feat/invariants

[alcueca]

First pass of fuzzing tests.

To run you need to install echidna and execute:

npx buidler compile && echidna-test . --contract USMFuzzingEthMgmt --config contracts/fuzzing/config.yaml 
npx buidler compile && echidna-test . --contract USMFuzzingRoundtrip --config contracts/fuzzing/config.yaml 

[alcueca]

I simplified these tests until they just track the management of Eth by the protocol, and found what could be a bug.

USM.sol takes the eth it says it takes, and returns the eth it says it returns, no surprises there.

However, it is possible to drain eth from the protocol, the sequence:

    1. testFundAndDefundEthValue(200790178637337)
    2. testFundAndDefundEthValue(100000000000001)

Doesn't guarantee that the eth balance in USM.sol after the sequence is equal or greater than the balance before the sequence. Preliminary testing shows that the loss of value might be around 1 ether.

Next steps are to build a unit test file, where that specific scenario can be reproduced and debugged.

[jacob-eliosoff]

Whoa, interesting! Off the top of my head... I have no idea what's going on here? So I guess that's pretty cool. Will look

[alexroan]

This tool looks like it's going to be really powerful for us... just need to get it to work

[alcueca]

Added a test file to debug the scenarios found by echidna:

npx buidler test test/fuzzing/11_USM_Fuzzing.test.js

With this we can get a detailed output of the scenario, and use console.log inside USM.sol to see what's going on:

    Fuzzing debugging helper
      minting and burning

          > ethIn:  200790178637337
          > fumOut: 50197544659334250
          > ethOut: 100395089318669

          > ethIn:  100000000000001
          > fumOut: 12524644398723310
          > ethOut: 100197544659335
        ✓ fund and defund round trip

I can track this to ethFromDefund, but there the math is too much for me. @jacob-eliosoff, can you pick it up?

[jacob-eliosoff]

Had a quick look... Very interesting!

Short version: It comes down to the edge case where the last FUM holder withdraws all their FUM. The simplest fix is probably to change this sketchy return 0 in debtRatio() to return type(uint).max instead:

    function debtRatio() public view returns (uint) {
        uint pool = ethPool();
        if (pool == 0) {
            return 0;   // This never really made sense...  Safer to treat an empty pool as a *high* debt ratio
        }
        return totalSupply().wadDiv(ethToUsm(pool));
    }

Long version: In the current code, if there's no USM in the pool, and the last FUM holder calls defund() to withdraw all their FUM (ie, all the FUM left in the pool), the pool ends up in a weird state where there's 0 USM, 0 FUM, but some "unclaimed" ETH (ie, the fees "paid" - left - by their defund() call). Then the next user who calls fund() gets all this unclaimed ETH, which is how they can profit as the fuzzer showed.

This is only possible because defund() checks that debtRatio() <= MAX_DEBT_RATIO, but our return 0 above means debtRatio() returns 0 when the pool is empty, which passes this test.

Changing it to return type(uint).max as I suggested above will mean that a defund() that tries to completely empty the pool will fail: the last user must leave at least a smidgen of FUM, which then owns any unclaimed ETH. I don't think this change would create any problems.

This is definitely a strong start for the fuzzer!

[jacob-eliosoff]

Having said that I won't be too surprised if my proposed change to debtRatio() instantly breaks all the tests... Let me check

[jacob-eliosoff]

Yup! Broke some stuff. Nothing serious I think... I'll follow up tomorrow.

[jacob-eliosoff]

(Feel free to toss out ideas about this stuff, the case where the user withdraws all their FUM and "unclaimed" ETH is left is an interesting one, I had thought about it. The fact is we could probably leave the behavior flagged by the fuzzer as is: I strongly doubt all FUM will ever be redeemed, and if it was and some ETH was left and someone claimed it, no real harm done.)

[jacob-eliosoff]

The return 0 -> return type(uint).max change to debtRatio() breaks test 2 in a trivially fixable way, but test 3 in a more confusing way, and console.log() is playing hard to get with me tonight. I'll take another crack tomorrowish... This should be simple!

[alcueca]

Thanks @jacob-eliosoff, that was really useful.

I can confirm that by adding a require(fum.totalSupply() >= 10**18); post-condition to the fund and defund test, so that we never defund all the FUM, the invariant holds.

[alcueca]

I split and simplified those fuzzing tests, to make them crystal clear.

I'm not too worried if after burning all FUM someone refloats the contracts and gets a little bonus, tbh. If it has an easy fix then let's do it, for robustness, otherwise we can let it be.

I'm more interested on other invariant testing, such as managing the ethBuffer and the sliding prices. Let's merge this PR and work on those.

Also @jacob-eliosoff, any properties of the system that you can think of in terms of invariants, please let me know and I'll implement them. This is fun.

[jacob-eliosoff]

I can confirm that by adding a require(fum.totalSupply() >= 10**18); post-condition to the fund and defund test, so that we never defund all the FUM, the invariant holds.

This was my original thought too (well, I had > 0), but even cleaner is to fix debtRatio()'s handling of the empty-pool case so we don't need this extra check. I'm still puzzled my type(uint).max doesn't work - maybe it's overflowing somehow. Making debtRatio() return MAX_DEBT_RATIO does work and avoids the extra check - I suggest we do that.

In general I think it's cleaner to return numbers that avoid error scenarios, than to add explicit requires for those scenarios - less code and more importantly, we could be missing the same check in other places.

[jacob-eliosoff]

I will spend some time today thinking of more invariants!

[alcueca]

Unfortunately, debtRatio returning MAX_DEBT_RATIO when the pool is zero still breaks the invariant:

    testFundAndDefundEthValue(12)
    testFundAndDefundEthValue(1)

I'm not sure if there is a fix for this. I think that you would need the fumPrice to be WAD, meaning that it should converge to USD/ETH. However this can't be because we have sliding prices that are calculated on the fum supply before the fund, and they would need to be calculated on the fum supply after the fund.

That might even be reasonable, to calculate prices on the resulting balances, what do you think?

[jacob-eliosoff]

Fascinating! I'll have to dig in a bit.

[jacob-eliosoff]

OK, we were looking at the right edge case (user withdraws last remaining FUM), but I had made TWO simple mistakes in my reasoning here:

1. Most basically - making debtRatio() return MAX_DEBT_RATIO rather than 0 doesn't help, because the require() in question (at the end of defund()) checks debtRatio() <= MAX_DEBT_RATIO. Note the <= 🙄 So to make any difference it would need to return MAX_DEBT_RATIO + 1 or something.
2. But also - the special case in debtRatio() is if the (ETH) pool is empty, and the whole problem with the case the fuzzer flagged is that the pool is not empty! What's empty is the FUM supply.

So I think we should add back the explicit require(FUM.totalSupply() > 0) (or whatever) I told you to take out. And we can remove the change to debtRatio() and keep it returning 0.

See my commit I just pushed - please retry the fuzzer...

Sorry for the silly mistakes above! Let's see what my next one is...

[jacob-eliosoff]

Btw my latest commit here breaks the fuzzing test: by design, since that test fund()s and then defund()s the full amount of FUM created, which my commit now disallows.

[alcueca]

Different approach, instead of disallowing retrieving the last FUM wei, which is rude, we just mint one wei FUM on deployment and lock it away.

One less external contract call in the code :D

[jacob-eliosoff]

The 1 wei thing is clever, but it could have weird effects: if all that's left in the pool is 10 ETH and 1e-18 FUM, then the implied FUM price is 1 FUM = 10^19 ETH... And then next time a user passes ETH to fund(), they'd be getting back incredibly tiny fractions of a FUM.

I think the big picture here is these are edge cases that are extremely unlikely to happen and basically harmless if they do, so we should just keep the code maximally simple:

• No fum.totalSupply() > 0 check. If someday (against all expectations) all FUM is withdrawn and the next funder gets a windfall, so be it.
• No explicit "Fund before minting" check (saves another external call in mint()). mint() before fund() fails anyway with a div by 0: I added a test.
• Make the fuzzer do a fund() call before fuzzing, since this is the realistic environment anyway (nonzero FUM). I added this to the fuzzer.

But if any of this seems worse to you feel free to add back your change!

[alcueca]

That's not the fuzzer (it's a helper to debug the scenarios found by the fuzzer), this is the fuzzer.

I agree that the edge case is rare and harmless, I'm more than happy to just document and accept it.