Broken Invariants Repro.MD

This is a list of repro for breaking specific invariant checks

The goal of this is to help you setup the system in interesting states

Check this quick video if you don't what we're talking about:

https://drive.google.com/file/d/1JyNQPdtKkE1ifDO7rwsgWv6fStiwnkpl/view?usp=share_link

L-15

Desynch of Grace Period

This was explained as Known Issues

-> If no synching of Grace Period -> Then the logic fails

Impact is: Instant Liquidations if RM is exited but nobody disarms the grace period

/// @dev Debunk false positives for L-15
    ///     These will happen because of the desynch if nobody calls, it is what it is
    function testL15Debunk() public {
        openCdp(67534042799335353648407647554112468697195277953615236438520200454730440793371, 8);
        openCdp(
            115792089237316195423570985008687907853269984665640564039457584007913129639931,
            1000000000000000900
        );
        setPrice(1324275793822189518402623021008446576244702559577);
        setEthPerShare(
            48542174391735010270995007834653745032392815149632706327135797120960854131722
        );
        setEthPerShare(40);
        partialLiquidate(
            48286268184227095156290128211489441036242155783962558196294945633758974303757,
            115792089237316195423570985008687907853269984665640564039457574007913129639736
        );
        _before(bytes32(0));
        setPrice(115792089237316195423570985007766067547234912789326764283000208828074618977599);
        _after(bytes32(0));
        _before(bytes32(0));
        redeemCollateral(
            999999999999999999,
            55466683072102056944478843133004903753885086444364839670214645639376128222361,
            68,
            26404592988528753382516565589028978384076848812021257892050088220355054183615
        );
        _after(bytes32(0));

        if (!vars.isRecoveryModeBefore && vars.isRecoveryModeAfter) {
            t(
                !vars.lastGracePeriodStartTimestampIsSetBefore &&
                    vars.lastGracePeriodStartTimestampIsSetAfter,
                L_15
            );
        }
    }

L-12

If all CDPs are below 110 MCR

You can liquidate the one with the highest MCR

Breaking the invariant

This scenario is a failure scenario

And impact is non-existant, the behaviour is valid

/// @dev Debunk false positives for L-12
    ///     These will happen exclusively if all CDPs are Underwater, and instead of liquidating the riskiest, the one above is liquidated
    function testL12Debunk() public {
        openCdp(92917081472816941941184964779154375129173708512214393931667457813751914161634, 20);
        openCdp(
            14357740897988057106500935390524526462940912496206879728999588820331360643957,
            1000000000000000256
        );
        openCdp(
            14357740897988057106500935390524526462940912496206879728999588820331360643957,
            1000000000000000256
        );
        setPrice(74629061016018350331730450585755319739830762911693635404016285330120218663634);
        setEthPerShare(
            69007891472983439489040112860682059911742470146824120203672378698503585549508
        );
        withdrawColl(
            2000000,
            49955707469362902507454157299064623548400035506668976771172421598874183583296
        );
        setPrice(0);
        closeCdp(79284842807605095858149520102903844594789751342105937047923718189601373042235);
        setEthPerShare(0);
        setPrice(3);
        bytes32 cdpId = _getRandomCdp(
            115792089237316195423570985008193886025822902127156998188347748450894401986382
        );

        console2.log("vars.newTcrBefore", vars.newTcrBefore);
        console2.log("vars.newTcrAfter", vars.newTcrAfter);

        uint256 newIcr;
        bytes32 currentCdp = sortedCdps.getFirst();

        while (currentCdp != bytes32(0)) {
            console2.log("ICR ICR", crLens.quoteRealICR(currentCdp));
            currentCdp = sortedCdps.getNext(currentCdp);
        }

        _before(cdpId);
        liquidate(115792089237316195423570985008193886025822902127156998188347748450894401986382);
        _after(cdpId);

        // If every CDP is liquidatable
        // Then you liquidate the 2nd
        // And break the invariant

        if (
            vars.newIcrBefore >= cdpManager.LICR() // 103% else liquidating locks in bad debt
        ) {
            // https://github.com/Badger-Finance/ebtc-fuzz-review/issues/5
            gte(vars.newTcrAfter, vars.newTcrBefore, L_12);
        }
    }

F-01

0 > 0 check

Maybe: lidofinance/lido-dao#796

Root: Unclear

Impact: Seems to have 1 wei of loss

/// @dev Known bug from stETH transfer, causing 1 share to be lost in the transfer
    function testF01Debunk() public {
        openCdp(0,1);
        setEthPerShare(0);
        openCdp(0,1);
        redeemCollateral(1967126592928475763945305251,165779958852053,214901877426779915,0);
        vm.stopPrank();
        setGovernanceParameters(13047726864602929199140172729873978268677412001741944068694426645973,1);
    }

General-08

See discussion: ebtc-protocol/ebtc#698

    /// @dev Breaks General 08 due to 1 wei of rounding error in redistribution
    function testGeneral08Debunk() public {
        openCdp(0,1);
        openCdp(0,131136193055529856);
        setEthPerShare(0);
        setEthPerShare(0);
        liquidate(1028258791029385401);
        openCdp(0,1);
        closeCdp(0);

        console2.log("activePool.getSystemCollShares()", activePool.getSystemCollShares());
        console2.log("activePool.getSystemDebt()", activePool.getSystemDebt());

        assertTrue(invariant_GENERAL_08(cdpManager, sortedCdps, priceFeedMock, collateral), "G-08");
    }