Evaluation & Quality

contract MarketTest is Test {
    Morpho morpho;
    address USER = makeAddr("user");

    function setUp() public {
        morpho = new Morpho(OWNER);
    }

    function test_supply_mintsExpectedShares() public {
        deal(address(loanToken), USER, 100e18);
        vm.prank(USER);
        loanToken.approve(address(morpho), type(uint256).max);
        vm.prank(USER);
        uint256 shares = morpho.supply(marketParams, 100e18, 0, USER, "");
        assertEq(shares, 100e18 * morpho.SHARES_OFFSET());
    }

    function test_supply_revertsOnZero() public {
        vm.expectRevert(ErrorsLib.ZeroAssets.selector);
        morpho.supply(marketParams, 0, 0, USER, "");
    }
}

forge test --match-contract MarketTest -vvv
forge test --fork-url $MAINNET_RPC --fork-block-number 19000000 --match-test test_realIntegration
forge coverage --report lcov

contract LendingHandler is Test {
    Morpho morpho;
    address[] internal actors;

    function supply(uint256 actorSeed, uint256 assets) external {
        assets = bound(assets, 1, 1e24);
        address actor = actors[actorSeed % actors.length];
        deal(address(loanToken), actor, assets);
        vm.startPrank(actor);
        loanToken.approve(address(morpho), assets);
        morpho.supply(marketParams, assets, 0, actor, "");
        vm.stopPrank();
        ghost_totalSupplied += assets;
    }

    uint256 public ghost_totalSupplied;
}

contract LendingInvariantTest is Test {
    LendingHandler handler;

    function setUp() public {
        handler = new LendingHandler();
        targetContract(address(handler));
        bytes4[] memory selectors = new bytes4[](3);
        selectors[0] = LendingHandler.supply.selector;
        selectors[1] = LendingHandler.borrow.selector;
        selectors[2] = LendingHandler.repay.selector;
        targetSelector(FuzzSelector(address(handler), selectors));
    }

    /// @dev Bookkeeping: total supplied equals sum of users' shares × price.
    function invariant_supplyAccounting() public view {
        Market memory m = morpho.market(id);
        assertGe(m.totalSupplyAssets, m.totalBorrowAssets);
    }

    /// @dev Solvency: no position is borrowing more than allowed.
    function invariant_allPositionsHealthy() public view {
        for (uint256 i; i < handler.actorCount(); ++i) {
            assertTrue(morpho.isHealthy(marketParams, handler.actor(i)));
        }
    }
}

contract LendingFuzz {
    Morpho morpho;

    function echidna_supplyGeBorrow() public view returns (bool) {
        Market memory m = morpho.market(id);
        return m.totalSupplyAssets >= m.totalBorrowAssets;
    }

    function echidna_noUnhealthyAfterAccrual() public returns (bool) {
        morpho.accrueInterest(marketParams);
        for (uint256 i; i < actors.length; ++i) {
            if (!morpho.isHealthy(marketParams, actors[i])) {
                // Healthy now? Maybe it became unhealthy passively from accrual — that's fine.
                // But this assertion catches "no one became unhealthy due to a state change".
            }
        }
        return true;
    }
}

echidna . --contract LendingFuzz --config echidna.yaml
medusa fuzz --config medusa.json

// A symbolic test using Halmos. svm.createUint(...) is symbolic.
function check_supplyMintsConsistentShares(uint256 assets, uint256 totalAssets, uint256 totalShares) public {
    vm.assume(totalAssets > 0 && totalShares > 0);
    vm.assume(assets <= type(uint128).max);

    uint256 sharesOut = assets * totalShares / totalAssets;
    uint256 assetsBack = sharesOut * totalAssets / totalShares;
    assert(assetsBack <= assets);   // round-trip never gains assets
}

halmos --contract LendingSymbolicTest --function check_supplyMintsConsistentShares

// Conceptual CVL — not Solidity
methods {
    function supply(address, uint256, uint256, address, bytes) external returns (uint256, uint256);
    function totalSupplyAssets() external returns (uint256) envfree;
    function totalSupplyShares() external returns (uint256) envfree;
}

invariant supplySharesNonZeroIffAssets()
    totalSupplyShares() == 0 <=> totalSupplyAssets() == 0;

rule supplyIncreasesAssets(env e, uint256 amount, address user) {
    uint256 before = totalSupplyAssets();
    supply(e, amount, 0, user, "");
    uint256 after = totalSupplyAssets();
    assert after >= before;
}

parametric rule noOpDoesNotChangeShares(method f) {
    uint256 before = totalSupplyShares();
    env e; calldataarg args;
    f(e, args);
    uint256 after = totalSupplyShares();
    // shares only change on supply/withdraw/etc — check the diff is expected
}

function test_irm_atKink() public {
    // U = OPTIMAL_U should give exactly BASE + SLOPE_1
    uint256 r = irm.borrowRate(OPTIMAL_U);
    assertEq(r, BASE_RATE + SLOPE_1);
}

function test_irm_justAboveKink() public {
    uint256 r = irm.borrowRate(OPTIMAL_U + 1);
    // Slope2 is steep — small step above kink should produce
    // significant rate jump but not overflow.
    assertGt(r, BASE_RATE + SLOPE_1);
    assertLt(r, MAX_BORROW_RATE);
}

function testFuzz_wadMulInverse(uint256 a, uint256 b) public {
    a = bound(a, 1, 1e36);
    b = bound(b, 1, 1e36);
    uint256 product = a.wadMul(b);
    uint256 back = product.wadDiv(b);
    assertApproxEqAbs(back, a, 1);   // off by at most 1 wei
}