More properties for formal verification

[daejunpark]

EDIT by @QGarchery. Todo list:

• A1, stay healthy (in progress, some timeouts left after [Certora] Specification for stayHealthy #344)
• B, roundtrip properties (in progress, first steps in [Certora] Check supply followed by withdraw is not profitable #345)
• D1, interest accrual increases shares value (in progress in [Certora] Check that supply share ratio increases and borrow share ratio decreases #353)

A2 is omitted because it does not seem to hold. Path independence property are postponed to future work, and they also require accepting a small delta. D2 is already mentioned in #96, D3 is being considered as an improvement on D2.

END OF EDIT

In addition to the nice invariants in #96, these properties can be considered for formal verification:

Properties about healthiness

Property A.1
No Blue transaction, including liquidation calls, can cause a healthy position to become unhealthy. (In other words, only price changes occurring outside of Blue can result in a previously healthy position becoming unhealthy.)

For example, this property can be tested as follows:

vm.assume(_isHealthy(market, id, user));

address(blue).call(data);

assert(_isHealthy(market, id, user));

Property A.2 [Updated: 8/18]
"Partial" liquidation cannot change an unhealthy position into a healthy one, if the LTV is greater than 1 / liquidation_incentive.

For example,

vm.assume(ultimatelyInsolvent(market, id, borrower));

blue.liquidate(market, borrower, seized, data);

borrowAmount = borrowShares[id][borrower];
isHealthy = _isHealthy(market, id, borrower);

// borrowAmount > 0  implies  !isHealthy
assert(borrowAmount == 0 || !isHealthy);

where:

function ultimatelyInsolvent(Market memory market, Id id, address user) internal view returns {
    uint256 borrowed = borrowShares[id][user].toAssetsUp(totalBorrow[id], totalBorrowShares[id]);            

    uint256 collateralPrice = IOracle(market.oracle).price();
    uint256 collateralValue = collateral[id][user].mulDivDown(collateralPrice, ORACLE_PRICE_SCALE);

    uint256 incentive = UtilsLib.min(
        MAX_LIQUIDATION_INCENTIVE_FACTOR, WAD.wDivDown(WAD - LIQUIDATION_CURSOR.wMulDown(WAD - market.lltv))
    );

    return borrowed.wMulDown(incentive) > collateralValue;
}

High-level properties regarding rounding errors

Roundtrip properties

Roundtrip properties between supply() and withdraw():

• Property B.1.1: There should be no profit from supply() immediately followed by withdraw().
• Property B.1.2: There should be no profit from withdraw() immediately followed by supply().

Similarly, roundtrip properties between borrow() and repay():

• Property B.2.1: There should be no profit from borrow() immediately followed by repay().
• Property B.2.2: There should be no profit from repay() immediately followed by borrow().

For example, Property B.1.1 can be tested as follows:

Id id = market.id();

uint oldBalance = IERC20(market.borrowableAsset).balanceOf(x);
uint oldShares = blue.supplyShares(id, x);

blue.supply(market, amount, x, data);
uint shares = blue.supplyShares(id, x) - oldShares;
blue.withdraw(market, shares, x, data);

uint newBalance = IERC20(market.borrowableAsset).balanceOf(x);
assert(newBalance <= oldBalance);

Path independence properties

Property C.1
Path independence for _accrueInterests():

• Multiple interest accruals do not generate more interest than a single accrual for the same time period.

For example,

current = lastUpdate[id];
oldSupply = totalSupply[id];
vm.warp(current + x);
_accrueInterests(market, id);
vm.warp(current + x + y);
_accrueInterests(market, id);
delta1 = totalSupply[id] - oldSupply;

current = lastUpdate[id];
oldSupply = totalSupply[id];
vm.warp(current + x + y);
_accrueInterests(market, id);
delta2 = totalSupply[id] - oldSupply;

assert(delta1 <= delta2);

Property C.2
Path independence for liquidate()

• There is no benefit to making multiple liquidate() calls compared to a single liquidate() call for the same total seized amount.

For example,

oldBalance = IERC20(market.borrowableAsset).balanceOf(caller);
vm.prank(caller); blue.liquidate(market, borrower, x, data);
vm.prank(caller); blue.liquidate(market, borrower, y, data);
repaid1 = oldBalance - IERC20(market.borrowableAsset).balanceOf(caller);

oldBalance = IERC20(market.borrowableAsset).balanceOf(caller);
vm.prank(caller); blue.liquidate(market, borrower, x + y, data);
repaid2 = oldBalance - IERC20(market.borrowableAsset).balanceOf(caller);

assert(repaid1 >= repaid2);

Properties about share prices

Property D.1
The price of both supply and borrow shares do not decrease after interest accruals.

For example,

oldSupplySharePrice = toAssetsDown(1e18, totalSupply[id], totalSupplyShares[id]);
oldBorrowSharePrice = toAssetsDown(1e18, totalBorrow[id], totalBorrowShares[id]);

_accrueInterests(market, id);

newSupplySharePrice = toAssetsDown(1e18, totalSupply[id], totalSupplyShares[id]);
newBorrowSharePrice = toAssetsDown(1e18, totalBorrow[id], totalBorrowShares[id]);

assert(oldSupplySharePrice <= newSupplySharePrice);
assert(oldBorrowSharePrice <= newBorrowSharePrice);

Property D.2
More generally, the price of both supply and borrow shares do not decrease after any non-liquidation Blue transactions.

For example,

oldSupplySharePrice = toAssetsDown(1e18, totalSupply[id], totalSupplyShares[id]);
oldBorrowSharePrice = toAssetsDown(1e18, totalBorrow[id], totalBorrowShares[id]);

vm.assume(selector != blue.liquidate.selector);
address(blue).call(abi.encodePacked(selector, data));

newSupplySharePrice = toAssetsDown(1e18, totalSupply[id], totalSupplyShares[id]);
newBorrowSharePrice = toAssetsDown(1e18, totalBorrow[id], totalBorrowShares[id]);

assert(oldSupplySharePrice <= newSupplySharePrice);
assert(oldBorrowSharePrice <= newBorrowSharePrice);

Property D.3
The share prices do not decrease after liquidation, as long as it wasn't a result of bad debt.

For example,

oldSupplySharePrice = toAssetsDown(1e18, totalSupply[id], totalSupplyShares[id]);
oldBorrowSharePrice = toAssetsDown(1e18, totalBorrow[id], totalBorrowShares[id]);

blue.liquidate(market, borrower, seized, data);
vm.assume(collateral[id][borrower] > 0); // no bad debt

newSupplySharePrice = toAssetsDown(1e18, totalSupply[id], totalSupplyShares[id]);
newBorrowSharePrice = toAssetsDown(1e18, totalBorrow[id], totalBorrowShares[id]);

assert(oldSupplySharePrice <= newSupplySharePrice);
assert(oldBorrowSharePrice <= newBorrowSharePrice);

Property D.4 [Added 8/18]
The share prices do not decrease after liquidation, if the LTV is less than or equal to 1 / liquidation_incentive.

For example,

oldSupplySharePrice = toAssetsDown(1e18, totalSupply[id], totalSupplyShares[id]);
oldBorrowSharePrice = toAssetsDown(1e18, totalBorrow[id], totalBorrowShares[id]);

vm.assume(ultimatelyInsolvent(market, id, borrower) == false);  // ultimately solvent, implying no bad debt

blue.liquidate(market, borrower, seized, data);

newSupplySharePrice = toAssetsDown(1e18, totalSupply[id], totalSupplyShares[id]);
newBorrowSharePrice = toAssetsDown(1e18, totalBorrow[id], totalBorrowShares[id]);

assert(oldSupplySharePrice <= newSupplySharePrice);
assert(oldBorrowSharePrice <= newBorrowSharePrice);

where ultimatelyInsolvent() is defined in Property A.2.

[daejunpark]

Question: Property A.1 does not hold if the borrow rate is unreasonably high, or if the market has been inactive for an extended period of time. Is this intended?

[QGarchery]

Thanks a lot for the detailed invariants, this is really helpful ! I'll try to verify as much as possible :)

A.1

Question: Property A.1 does not hold if the borrow rate is unreasonably high, or if the market has been inactive for an extended period of time. Is this intended?

I think that the property holds for an atomic call because there are no accrued interests (the code snippet you wrote should work because it does not include time passing). If there can be a waiting period however, the fact that this property does not hold anymore is intended: as a borrower you should monitor your position and the potential increase of the borrow rate.

A.2

I don't think it holds, there should be some liquidations that make the position healthy. It should be the same setup as in Morpho yellow paper (see lemma 2.2.1 page 18 notably). For example, with a liquidation incentive of 1.1, a LLTV of 0.5, and a unhealthy position of 51 borrow (in value) with 100 collateral (in value), a liquidation repaying 10 (and seizing 1.1 * 10 = 11), will put that account ltv to 41 / 89 < 0.5.

C.1

I'm not sure that we necessarily want to verify that property. In particular, if we had a simple interest rate model, then compounding more often would lead to more interests accrued. It would only become problematic if the benefit of doing so makes it so the interest accrual would be called a lot, leading to gas inefficiencies overall. To mitigate that, we use an approximation of the perfect compouding model, so it should still not verify the C.1 property, but it should still be ok because it's very close.

C.2

Do we want to verify this property to make sure that liquidators do not have to call liquidate multiple times, or is there a functional correctness argument to this property ?

[daejunpark]

I think that the property holds for an atomic call because there are no accrued interests (the code snippet you wrote should work because it does not include time passing).

What do you mean by "atomic calls"? Most entrypoint calls invoke _accrueInterests() at the beginning, which may generate interest and increase totalBorrow[id], which in turn can cause _isHealthy() to become false after the call. I don't think that the example test can be passed without the assumption that the max interest is small enough, or the lastUpdate[id] is not too old.

C1 and C2

The properties stem from the specific rounding directions used in the current implementation. So I figured they might be an implicit design decision made under the hood. Please feel free to ignore them if C1 and C2 are not intended, but you may want to consider other high-level properties that imply the correctness of the specific rounding directions chosen by the implementation.

[QGarchery]

Oh ok you are right about A1, I assumed that the code snippet showed an interaction with Blue in the same transaction as another interaction (this is forge's default), and this is what I meant about "atomic calls".

C1 and C2 were not intended but they are nice properties. I think that if we get close to those properties of a few WEI (let's say because of a rounding error), then weird behaviors are not incentivized and there should be no gas waste which should be enough

[daejunpark]

A.2
I don't think it holds, there should be some liquidations that make the position healthy. It should be the same setup as in Morpho yellow paper (see lemma 2.2.1 page 18 notably).

You're right. Thanks for providing the pointer to it.

I've added the condition for Property A.2, which essentially captures Lemma 2.2.1 in the Morpho yellow paper.

I also added Property D.4, to capture the other aspect of the lemma.

The updated Property A.2, along with the newly introduced Property D.4, are provided for the sake of completeness. But I'm not very confident that they can be verified by automated provers due to the complex arithmetic involved. In that case, you may want to utilize fuzz testing as much as possible.

[QGarchery]

Thanks for the added invariants ! I think that one property that would be very interesting to prove is that the position stay healthy if it's LTV was lower than 1 / liquidation_incentive. This would ensure that our liquidation system has some breathing room to liquidate users before it leads to bad debt.

I'm closing this issue because I'm opening a general issue about formal verification to keep track of what's left to do. See #390