From 3e4f205bd468f42907c2557b3ba1d2eff9051347 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Wed, 22 Nov 2023 17:45:52 +0100 Subject: [PATCH 1/2] refactor: roundtrip with arbitrary amounts --- certora/specs/ExactMath.spec | 57 ++++++++++++++++++------------------ certora/specs/Liveness.spec | 12 +++----- 2 files changed, 32 insertions(+), 37 deletions(-) diff --git a/certora/specs/ExactMath.spec b/certora/specs/ExactMath.spec index 5f92dac3d..e0e00369d 100644 --- a/certora/specs/ExactMath.spec +++ b/certora/specs/ExactMath.spec @@ -2,6 +2,8 @@ methods { function extSloads(bytes32[]) external returns bytes32[] => NONDET DELETE; + function supplyShares(MorphoHarness.Id, address) external returns uint256 envfree; + function borrowShares(MorphoHarness.Id, address) external returns uint256 envfree; function virtualTotalSupplyAssets(MorphoHarness.Id) external returns uint256 envfree; function virtualTotalSupplyShares(MorphoHarness.Id) external returns uint256 envfree; function virtualTotalBorrowAssets(MorphoHarness.Id) external returns uint256 envfree; @@ -31,7 +33,7 @@ function summaryMulDivDown(uint256 x, uint256 y, uint256 d) returns uint256 { // Check that when not accruing interest, and when repaying all, the borrow ratio is at least reset to the initial ratio. // More details on the purpose of this rule in RatioMath.spec. -rule repayAllResetsBorrowRatio(env e, MorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onbehalf, bytes data) { +rule repayAllResetsBorrowRatio(env e, MorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, bytes data) { MorphoHarness.Id id = libId(marketParams); // Safe require because this invariant is checked in ConsistentState.spec require fee(id) <= maxFee(); @@ -43,7 +45,7 @@ rule repayAllResetsBorrowRatio(env e, MorphoHarness.MarketParams marketParams, u require lastUpdate(id) == e.block.timestamp; mathint repaidAssets; - repaidAssets, _ = repay(e, marketParams, assets, shares, onbehalf, data); + repaidAssets, _ = repay(e, marketParams, assets, shares, onBehalf, data); // Check the case where the market is fully repaid. require repaidAssets >= assetsBefore; @@ -59,63 +61,60 @@ rule repayAllResetsBorrowRatio(env e, MorphoHarness.MarketParams marketParams, u rule supplyWithdraw() { MorphoHarness.MarketParams marketParams; MorphoHarness.Id id = libId(marketParams); - uint256 assets; - uint256 shares; - address onbehalf; - address receiver; - bytes data; env e1; env e2; + address onBehalf; - // Assume that interactions to happen at the same block. + // Assume that interactions happen at the same block. require e1.block.timestamp == e2.block.timestamp; + // Assume that the user starts without any supply position. + require supplyShares(id, onBehalf) == 0; // Safe require because timestamps cannot realistically be that large. require e1.block.timestamp < 2^128; + uint256 supplyAssets; uint256 supplyShares; bytes data; uint256 suppliedAssets; uint256 suppliedShares; - suppliedAssets, suppliedShares = supply(e1, marketParams, assets, shares, onbehalf, data); + suppliedAssets, suppliedShares = supply(e1, marketParams, supplyAssets, supplyShares, onBehalf, data); // Hints for the prover. assert suppliedAssets * (virtualTotalSupplyShares(id) - suppliedShares) >= suppliedShares * (virtualTotalSupplyAssets(id) - suppliedAssets); assert suppliedAssets * virtualTotalSupplyShares(id) >= suppliedShares * virtualTotalSupplyAssets(id); + uint256 withdrawAssets; uint256 withdrawShares; address receiver; uint256 withdrawnAssets; - uint256 withdrawnShares; - withdrawnAssets, withdrawnShares = withdraw(e2, marketParams, 0, suppliedShares, onbehalf, receiver); + withdrawnAssets, _ = withdraw(e2, marketParams, withdrawAssets, withdrawShares, onBehalf, receiver); - assert withdrawnShares == suppliedShares; assert withdrawnAssets <= suppliedAssets; } -// There should be no profit from withdraw followed immediately by supply. -rule withdrawSupply() { +// There should be no profit from borrow followed immediately by repay. +rule borrowRepay() { MorphoHarness.MarketParams marketParams; MorphoHarness.Id id = libId(marketParams); - uint256 assets; - uint256 shares; - address onbehalf; - address receiver; - bytes data; + address onBehalf; env e1; env e2; - // Assume interactions to happen at the same block. + // Assume interactions happen at the same block. require e1.block.timestamp == e2.block.timestamp; + // Assume that the user starts without any borrow position. + require borrowShares(id, onBehalf) == 0; // Safe require because timestamps cannot realistically be that large. require e1.block.timestamp < 2^128; - uint256 withdrawnAssets; - uint256 withdrawnShares; - withdrawnAssets, withdrawnShares = withdraw(e2, marketParams, assets, shares, onbehalf, receiver); + uint256 borrowAssets; uint256 borrowShares; address receiver; + uint256 borrowedAssets; + uint256 borrowedShares; + borrowedAssets, borrowedShares = borrow(e2, marketParams, borrowAssets, borrowShares, onBehalf, receiver); // Hints for the prover. - assert withdrawnAssets * (virtualTotalSupplyShares(id) + withdrawnShares) <= withdrawnShares * (virtualTotalSupplyAssets(id) + withdrawnAssets); - assert withdrawnAssets * virtualTotalSupplyShares(id) <= withdrawnShares * virtualTotalSupplyAssets(id); + assert borrowedAssets * (virtualTotalBorrowShares(id) - borrowedShares) <= borrowedShares * (virtualTotalBorrowAssets(id) - borrowedAssets); + assert borrowedAssets * virtualTotalBorrowShares(id) <= borrowedShares * virtualTotalBorrowAssets(id); - uint256 suppliedAssets; - uint256 suppliedShares; - suppliedAssets, suppliedShares = supply(e1, marketParams, withdrawnAssets, 0, onbehalf, data); + uint256 repayAssets; uint256 repayShares; bytes data; + uint256 repaidAssets; + repaidAssets, _ = repay(e1, marketParams, repayAssets, repayShares, onBehalf, data); - assert suppliedAssets == withdrawnAssets && withdrawnShares >= suppliedShares; + assert borrowedAssets <= repaidAssets; } diff --git a/certora/specs/Liveness.spec b/certora/specs/Liveness.spec index 0c3fb3130..7d66662ad 100644 --- a/certora/specs/Liveness.spec +++ b/certora/specs/Liveness.spec @@ -98,8 +98,7 @@ rule supplyChangesTokensAndShares(env e, MorphoInternalAccess.MarketParams marke // Check that you can supply non-zero tokens by passing shares. rule canSupplyByPassingShares(env e, MorphoInternalAccess.MarketParams marketParams, uint256 shares, address onBehalf, bytes data) { uint256 suppliedAssets; - uint256 suppliedShares; - suppliedAssets, suppliedShares = supply(e, marketParams, 0, shares, onBehalf, data); + suppliedAssets, _ = supply(e, marketParams, 0, shares, onBehalf, data); satisfy suppliedAssets != 0; } @@ -135,8 +134,7 @@ rule withdrawChangesTokensAndShares(env e, MorphoInternalAccess.MarketParams mar // Check that you can withdraw non-zero tokens by passing shares. rule canWithdrawByPassingShares(env e, MorphoInternalAccess.MarketParams marketParams, uint256 shares, address onBehalf, address receiver) { uint256 withdrawnAssets; - uint256 withdrawnShares; - withdrawnAssets, withdrawnShares = withdraw(e, marketParams, 0, shares, onBehalf, receiver); + withdrawnAssets, _ = withdraw(e, marketParams, 0, shares, onBehalf, receiver); satisfy withdrawnAssets != 0; } @@ -172,8 +170,7 @@ rule borrowChangesTokensAndShares(env e, MorphoInternalAccess.MarketParams marke // Check that you can borrow non-zero tokens by passing shares. rule canBorrowByPassingShares(env e, MorphoInternalAccess.MarketParams marketParams, uint256 shares, address onBehalf, address receiver) { uint256 borrowedAssets; - uint256 borrowedShares; - borrowedAssets, borrowedShares = borrow(e, marketParams, 0, shares, onBehalf, receiver); + borrowedAssets, _ = borrow(e, marketParams, 0, shares, onBehalf, receiver); satisfy borrowedAssets != 0; } @@ -212,8 +209,7 @@ rule repayChangesTokensAndShares(env e, MorphoInternalAccess.MarketParams market // Check that you can repay non-zero tokens by passing shares. rule canRepayByPassingShares(env e, MorphoInternalAccess.MarketParams marketParams, uint256 shares, address onBehalf, bytes data) { uint256 repaidAssets; - uint256 repaidShares; - repaidAssets, repaidShares = repay(e, marketParams, 0, shares, onBehalf, data); + repaidAssets, _ = repay(e, marketParams, 0, shares, onBehalf, data); satisfy repaidAssets != 0; } From 83f692f3092957906f2608e55d62b98d75a7c711 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Thu, 30 Nov 2023 15:46:52 +0100 Subject: [PATCH 2/2] fix: rules specification --- certora/specs/ExactMath.spec | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/certora/specs/ExactMath.spec b/certora/specs/ExactMath.spec index e0e00369d..d25465c25 100644 --- a/certora/specs/ExactMath.spec +++ b/certora/specs/ExactMath.spec @@ -2,14 +2,15 @@ methods { function extSloads(bytes32[]) external returns bytes32[] => NONDET DELETE; + function feeRecipient() external returns address envfree; function supplyShares(MorphoHarness.Id, address) external returns uint256 envfree; function borrowShares(MorphoHarness.Id, address) external returns uint256 envfree; function virtualTotalSupplyAssets(MorphoHarness.Id) external returns uint256 envfree; function virtualTotalSupplyShares(MorphoHarness.Id) external returns uint256 envfree; function virtualTotalBorrowAssets(MorphoHarness.Id) external returns uint256 envfree; function virtualTotalBorrowShares(MorphoHarness.Id) external returns uint256 envfree; - function fee(MorphoHarness.Id) external returns uint256 envfree; function lastUpdate(MorphoHarness.Id) external returns uint256 envfree; + function fee(MorphoHarness.Id) external returns uint256 envfree; function maxFee() external returns uint256 envfree; function libId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree; @@ -69,6 +70,8 @@ rule supplyWithdraw() { require e1.block.timestamp == e2.block.timestamp; // Assume that the user starts without any supply position. require supplyShares(id, onBehalf) == 0; + // Assume that the user is not the fee recipient, otherwise the gain can come from the fee. + require onBehalf != feeRecipient(); // Safe require because timestamps cannot realistically be that large. require e1.block.timestamp < 2^128; @@ -88,7 +91,7 @@ rule supplyWithdraw() { assert withdrawnAssets <= suppliedAssets; } -// There should be no profit from borrow followed immediately by repay. +// There should be no profit from borrow followed immediately by repaying all. rule borrowRepay() { MorphoHarness.MarketParams marketParams; MorphoHarness.Id id = libId(marketParams); @@ -112,9 +115,9 @@ rule borrowRepay() { assert borrowedAssets * (virtualTotalBorrowShares(id) - borrowedShares) <= borrowedShares * (virtualTotalBorrowAssets(id) - borrowedAssets); assert borrowedAssets * virtualTotalBorrowShares(id) <= borrowedShares * virtualTotalBorrowAssets(id); - uint256 repayAssets; uint256 repayShares; bytes data; + bytes data; uint256 repaidAssets; - repaidAssets, _ = repay(e1, marketParams, repayAssets, repayShares, onBehalf, data); + repaidAssets, _ = repay(e1, marketParams, 0, borrowedShares, onBehalf, data); assert borrowedAssets <= repaidAssets; }