From faafe0f3b1aa7f3980e32ec562b1c8241ad4138e Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Fri, 5 Jul 2024 10:52:13 +0200 Subject: [PATCH 01/14] feat: add healthy liquidate general rule --- certora/specs/Health.spec | 48 +++++++++++++++++++++++++++++++++++++++ 1 file changed, 48 insertions(+) diff --git a/certora/specs/Health.spec b/certora/specs/Health.spec index cd4cca94..93fc894b 100644 --- a/certora/specs/Health.spec +++ b/certora/specs/Health.spec @@ -2,7 +2,10 @@ methods { function extSloads(bytes32[]) external returns bytes32[] => NONDET DELETE; + function totalBorrowAssets(MorphoHarness.Id) external returns uint256 envfree; function totalBorrowShares(MorphoHarness.Id) external returns uint256 envfree; + function virtualTotalBorrowAssets(MorphoHarness.Id) external returns uint256 envfree; + function virtualTotalBorrowShares(MorphoHarness.Id) external returns uint256 envfree; function lastUpdate(MorphoHarness.Id) external returns uint256 envfree; function borrowShares(MorphoHarness.Id, address) external returns uint256 envfree; function collateral(MorphoHarness.Id, address) external returns uint256 envfree; @@ -75,6 +78,51 @@ filtered { assert !priceChanged => stillHealthy; } +rule stayHealthy_liquidate(env e) +{ + MorphoHarness.MarketParams marketParams; + MorphoHarness.Id id = libId(marketParams); + address user; + + // Assume that the position is healthy before the interaction. + require isHealthy(marketParams, user); + uint256 debtSharesBefore = borrowShares(id, user); + uint256 debtAssetsBefore = summaryMulDivUp(debtSharesBefore, virtualTotalBorrowAssets(id), virtualTotalBorrowShares(id)); + // Safe require because of the invariants onlyEnabledLltv and lltvSmallerThanWad in ConsistentState.spec. + require marketParams.lltv < 10^18; + // Assumption to ensure that no interest is accumulated. + require lastUpdate(id) == e.block.timestamp; + + priceChanged = false; + + MorphoHarness.MarketParams marketParams2; + address borrower; + uint256 seizedAssets; + uint256 repaidShares; + bytes data; + require marketParams2 == marketParams; + + liquidate(e, marketParams2, borrower, seizedAssets, 0, data); + require !priceChanged; + // Safe require because of the invariant sumBorrowSharesCorrect. + require borrowShares(id, user) <= totalBorrowShares(id); + + // the case where not everything was repaid + require totalBorrowAssets(id) > 0; + // user has collateral left + require collateral(id, borrower) > 0; + + assert user != borrower; + assert debtSharesBefore == borrowShares(id, user); + assert debtAssetsBefore >= summaryMulDivUp(debtSharesBefore, virtualTotalBorrowAssets(id), virtualTotalBorrowShares(id)); + + bool stillHealthy = isHealthy(marketParams, user); + require !priceChanged; + + // assert !priceChanged => stillHealthy; + assert stillHealthy; +} + // Check that users cannot lose collateral by unauthorized parties except in case of an unhealthy position. rule healthyUserCannotLoseCollateral(env e, method f, calldataarg data) filtered { f -> !f.isView } From 4263c9b1976c06489f53ea49b7142170c0135b6e Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Fri, 5 Jul 2024 10:53:55 +0200 Subject: [PATCH 02/14] chore: switch to certora-cli-beta --- .github/workflows/certora.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml index e0931e6e..2ddf7e09 100644 --- a/.github/workflows/certora.yml +++ b/.github/workflows/certora.yml @@ -39,7 +39,7 @@ jobs: python-version: ">=3.9" - name: Install certora - run: pip install certora-cli + run: pip install certora-cli-beta - name: Install solc run: | From d1e81edbf6adfd542a983d7010cb34328a5e91ee Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Fri, 5 Jul 2024 11:36:37 +0200 Subject: [PATCH 03/14] style: refactor stay healthy liquidate --- certora/specs/Health.spec | 28 ++++++++++------------------ 1 file changed, 10 insertions(+), 18 deletions(-) diff --git a/certora/specs/Health.spec b/certora/specs/Health.spec index 93fc894b..83fe5722 100644 --- a/certora/specs/Health.spec +++ b/certora/specs/Health.spec @@ -78,9 +78,12 @@ filtered { assert !priceChanged => stillHealthy; } -rule stayHealthy_liquidate(env e) -{ - MorphoHarness.MarketParams marketParams; +// The general case of liquidate for the stayHealthy rule +// - the user checked is not the borrower, +// - the market of the liquidation is the market of the user, +// - there is still some borrow on the market after liquidation, +// - there was no bad debt realization. +rule stayHealthyLiquidate(env e, MorphoHarness.MarketParams marketParams, address borrower, uint256 seizedAssets, bytes data) { MorphoHarness.Id id = libId(marketParams); address user; @@ -94,22 +97,14 @@ rule stayHealthy_liquidate(env e) require lastUpdate(id) == e.block.timestamp; priceChanged = false; - - MorphoHarness.MarketParams marketParams2; - address borrower; - uint256 seizedAssets; - uint256 repaidShares; - bytes data; - require marketParams2 == marketParams; - - liquidate(e, marketParams2, borrower, seizedAssets, 0, data); + liquidate(e, marketParams, borrower, seizedAssets, 0, data); require !priceChanged; + // Safe require because of the invariant sumBorrowSharesCorrect. require borrowShares(id, user) <= totalBorrowShares(id); - - // the case where not everything was repaid + // Handle the case where not everything was repaid. require totalBorrowAssets(id) > 0; - // user has collateral left + // Handle the case where the user has some collateral left. require collateral(id, borrower) > 0; assert user != borrower; @@ -117,9 +112,6 @@ rule stayHealthy_liquidate(env e) assert debtAssetsBefore >= summaryMulDivUp(debtSharesBefore, virtualTotalBorrowAssets(id), virtualTotalBorrowShares(id)); bool stillHealthy = isHealthy(marketParams, user); - require !priceChanged; - - // assert !priceChanged => stillHealthy; assert stillHealthy; } From 9aeb49f1dcab15dc1de448feb6100fdea13c0f1d Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Wed, 14 Aug 2024 13:11:27 +0200 Subject: [PATCH 04/14] chore: switch back to certora-cli --- .github/workflows/certora.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml index 2ddf7e09..e0931e6e 100644 --- a/.github/workflows/certora.yml +++ b/.github/workflows/certora.yml @@ -39,7 +39,7 @@ jobs: python-version: ">=3.9" - name: Install certora - run: pip install certora-cli-beta + run: pip install certora-cli - name: Install solc run: | From 91e6bebc948e3841d80fe92b9f2eeccebec9f568 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Wed, 28 Aug 2024 17:32:27 +0200 Subject: [PATCH 05/14] fix: ensure price not changed by view functions --- certora/specs/Health.spec | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/certora/specs/Health.spec b/certora/specs/Health.spec index 83fe5722..fa88cc68 100644 --- a/certora/specs/Health.spec +++ b/certora/specs/Health.spec @@ -87,6 +87,7 @@ rule stayHealthyLiquidate(env e, MorphoHarness.MarketParams marketParams, addres MorphoHarness.Id id = libId(marketParams); address user; + priceChanged = false; // Assume that the position is healthy before the interaction. require isHealthy(marketParams, user); uint256 debtSharesBefore = borrowShares(id, user); @@ -96,9 +97,7 @@ rule stayHealthyLiquidate(env e, MorphoHarness.MarketParams marketParams, addres // Assumption to ensure that no interest is accumulated. require lastUpdate(id) == e.block.timestamp; - priceChanged = false; liquidate(e, marketParams, borrower, seizedAssets, 0, data); - require !priceChanged; // Safe require because of the invariant sumBorrowSharesCorrect. require borrowShares(id, user) <= totalBorrowShares(id); @@ -112,6 +111,7 @@ rule stayHealthyLiquidate(env e, MorphoHarness.MarketParams marketParams, addres assert debtAssetsBefore >= summaryMulDivUp(debtSharesBefore, virtualTotalBorrowAssets(id), virtualTotalBorrowShares(id)); bool stillHealthy = isHealthy(marketParams, user); + require !priceChanged; assert stillHealthy; } From b48561465aab8357020c669911fe692ef9bb5c0b Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Wed, 28 Aug 2024 17:48:28 +0200 Subject: [PATCH 06/14] fix: price did not change after liquidate --- certora/specs/Health.spec | 1 + 1 file changed, 1 insertion(+) diff --git a/certora/specs/Health.spec b/certora/specs/Health.spec index fa88cc68..02e5f4b7 100644 --- a/certora/specs/Health.spec +++ b/certora/specs/Health.spec @@ -98,6 +98,7 @@ rule stayHealthyLiquidate(env e, MorphoHarness.MarketParams marketParams, addres require lastUpdate(id) == e.block.timestamp; liquidate(e, marketParams, borrower, seizedAssets, 0, data); + require !priceChanged; // Safe require because of the invariant sumBorrowSharesCorrect. require borrowShares(id, user) <= totalBorrowShares(id); From 1cc0444b53af812609261ab39057f31b96c8dc99 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Thu, 26 Sep 2024 17:02:50 +0200 Subject: [PATCH 07/14] refactor: remove unnecessary require --- certora/specs/Health.spec | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/certora/specs/Health.spec b/certora/specs/Health.spec index 02e5f4b7..5e706d38 100644 --- a/certora/specs/Health.spec +++ b/certora/specs/Health.spec @@ -82,12 +82,11 @@ filtered { // - the user checked is not the borrower, // - the market of the liquidation is the market of the user, // - there is still some borrow on the market after liquidation, -// - there was no bad debt realization. +// - there was no bad debt realization (without this the rule times out). rule stayHealthyLiquidate(env e, MorphoHarness.MarketParams marketParams, address borrower, uint256 seizedAssets, bytes data) { MorphoHarness.Id id = libId(marketParams); address user; - priceChanged = false; // Assume that the position is healthy before the interaction. require isHealthy(marketParams, user); uint256 debtSharesBefore = borrowShares(id, user); From a5efbc2ed25df71bd3c3582c5873666d6950fac1 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Thu, 26 Sep 2024 17:21:56 +0200 Subject: [PATCH 08/14] docs: comment stayHealthyLiquidate --- certora/specs/Health.spec | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/certora/specs/Health.spec b/certora/specs/Health.spec index 5e706d38..58b4e4ce 100644 --- a/certora/specs/Health.spec +++ b/certora/specs/Health.spec @@ -78,11 +78,10 @@ filtered { assert !priceChanged => stillHealthy; } -// The general case of liquidate for the stayHealthy rule -// - the user checked is not the borrower, +// The liquidate case for the stayHealthy rule, assuming no bad debt realization, otherwise it times out. +// This particular rule makes the following assumptions: // - the market of the liquidation is the market of the user, -// - there is still some borrow on the market after liquidation, -// - there was no bad debt realization (without this the rule times out). +// - there is still some borrow on the market after liquidation. rule stayHealthyLiquidate(env e, MorphoHarness.MarketParams marketParams, address borrower, uint256 seizedAssets, bytes data) { MorphoHarness.Id id = libId(marketParams); address user; From beea950ecbbc23d300214bd8ad502381a1db880e Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Thu, 26 Sep 2024 18:06:34 +0200 Subject: [PATCH 09/14] feat: stay healthy liquidate with different markets --- certora/specs/Health.spec | 35 +++++++++++++++++++++++++++++++---- 1 file changed, 31 insertions(+), 4 deletions(-) diff --git a/certora/specs/Health.spec b/certora/specs/Health.spec index 58b4e4ce..3ff23803 100644 --- a/certora/specs/Health.spec +++ b/certora/specs/Health.spec @@ -80,14 +80,15 @@ filtered { // The liquidate case for the stayHealthy rule, assuming no bad debt realization, otherwise it times out. // This particular rule makes the following assumptions: -// - the market of the liquidation is the market of the user, +// - the market of the liquidation is the market of the user, see the *DifferentMarkets rule // - there is still some borrow on the market after liquidation. rule stayHealthyLiquidate(env e, MorphoHarness.MarketParams marketParams, address borrower, uint256 seizedAssets, bytes data) { MorphoHarness.Id id = libId(marketParams); address user; - // Assume that the position is healthy before the interaction. + // Assume the invariant initially. require isHealthy(marketParams, user); + uint256 debtSharesBefore = borrowShares(id, user); uint256 debtAssetsBefore = summaryMulDivUp(debtSharesBefore, virtualTotalBorrowAssets(id), virtualTotalBorrowShares(id)); // Safe require because of the invariants onlyEnabledLltv and lltvSmallerThanWad in ConsistentState.spec. @@ -100,9 +101,9 @@ rule stayHealthyLiquidate(env e, MorphoHarness.MarketParams marketParams, addres // Safe require because of the invariant sumBorrowSharesCorrect. require borrowShares(id, user) <= totalBorrowShares(id); - // Handle the case where not everything was repaid. + // Assume that there is still some borrow on the market after liquidation. require totalBorrowAssets(id) > 0; - // Handle the case where the user has some collateral left. + // Assume no bad debt realization. require collateral(id, borrower) > 0; assert user != borrower; @@ -114,6 +115,32 @@ rule stayHealthyLiquidate(env e, MorphoHarness.MarketParams marketParams, addres assert stillHealthy; } +rule stayHealthyLiquidateDifferentMarkets(env e, MorphoHarness.MarketParams marketParams, address borrower, uint256 seizedAssets, bytes data) { + MorphoHarness.Id id = libId(marketParams); + address user; + MorphoHarness.MarketParams liquidationMarketParams; + + // Assume the invariant initially. + require isHealthy(marketParams, user); + + // Safe require because of the invariants onlyEnabledLltv and lltvSmallerThanWad in ConsistentState.spec. + require marketParams.lltv < 10^18; + // Assumption to ensure that no interest is accumulated. + require lastUpdate(id) == e.block.timestamp; + // Assume that the liquidation is on a different market. + require liquidationMarketParams != marketParams; + + liquidate(e, liquidationMarketParams, borrower, seizedAssets, 0, data); + require !priceChanged; + + // Safe require because of the invariant sumBorrowSharesCorrect. + require borrowShares(id, user) <= totalBorrowShares(id); + + bool stillHealthy = isHealthy(marketParams, user); + require !priceChanged; + assert stillHealthy; +} + // Check that users cannot lose collateral by unauthorized parties except in case of an unhealthy position. rule healthyUserCannotLoseCollateral(env e, method f, calldataarg data) filtered { f -> !f.isView } From 3b9eb66094d699813bf7335c484f7c22e9cd1f34 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Mon, 30 Sep 2024 11:35:44 +0200 Subject: [PATCH 10/14] feat: split stay healthy rules --- .github/workflows/certora.yml | 1 + certora/confs/AccrueInterest.conf | 2 +- certora/confs/StayHealthy.conf | 18 ++++++ certora/specs/Health.spec | 92 ------------------------------- certora/specs/StayHealthy.spec | 0 5 files changed, 20 insertions(+), 93 deletions(-) create mode 100644 certora/confs/StayHealthy.conf create mode 100644 certora/specs/StayHealthy.spec diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml index e0931e6e..87a17a69 100644 --- a/.github/workflows/certora.yml +++ b/.github/workflows/certora.yml @@ -26,6 +26,7 @@ jobs: - Liveness - Reentrancy - Reverts + - StayHealthy - Transfer steps: diff --git a/certora/confs/AccrueInterest.conf b/certora/confs/AccrueInterest.conf index b5adb6ad..80570064 100644 --- a/certora/confs/AccrueInterest.conf +++ b/certora/confs/AccrueInterest.conf @@ -6,8 +6,8 @@ "verify": "MorphoHarness:certora/specs/AccrueInterest.spec", "prover_args": [ "-depth 3", - "-smt_hashingScheme plaininjectivity", "-mediumTimeout 30", + "-smt_hashingScheme plaininjectivity", ], "rule_sanity": "basic", "server": "production", diff --git a/certora/confs/StayHealthy.conf b/certora/confs/StayHealthy.conf new file mode 100644 index 00000000..567f70d4 --- /dev/null +++ b/certora/confs/StayHealthy.conf @@ -0,0 +1,18 @@ +{ + "files": [ + "certora/harness/MorphoHarness.sol", + "src/mocks/OracleMock.sol", + ], + "msg": "Morpho Blue Stay Healthy", + "process": "emv", + "prover_args": [ + "-depth 5", + "-mediumTimeout 5", + "-timeout 3600", + "-smt_hashingScheme plaininjectivity" + ], + "rule_sanity": "basic", + "server": "production", + "solc": "solc-0.8.19", + "verify": "MorphoHarness:certora/specs/StayHealthy.spec" +} diff --git a/certora/specs/Health.spec b/certora/specs/Health.spec index 3ff23803..6f2d395e 100644 --- a/certora/specs/Health.spec +++ b/certora/specs/Health.spec @@ -49,98 +49,6 @@ function summaryMin(uint256 a, uint256 b) returns uint256 { return a < b ? a : b; } -// Check that without accruing interest, no interaction can put an healthy account into an unhealthy one. -// The liquidate function times out in this rule, but has been checked separately. -rule stayHealthy(env e, method f, calldataarg data) -filtered { - f -> !f.isView && - f.selector != sig:liquidate(MorphoHarness.MarketParams, address, uint256, uint256, bytes).selector -} -{ - MorphoHarness.MarketParams marketParams; - MorphoHarness.Id id = libId(marketParams); - address user; - - // Assume that the position is healthy before the interaction. - require isHealthy(marketParams, user); - // Safe require because of the invariants onlyEnabledLltv and lltvSmallerThanWad in ConsistentState.spec. - require marketParams.lltv < 10^18; - // Assumption to ensure that no interest is accumulated. - require lastUpdate(id) == e.block.timestamp; - - priceChanged = false; - f(e, data); - - // Safe require because of the invariant sumBorrowSharesCorrect. - require borrowShares(id, user) <= totalBorrowShares(id); - - bool stillHealthy = isHealthy(marketParams, user); - assert !priceChanged => stillHealthy; -} - -// The liquidate case for the stayHealthy rule, assuming no bad debt realization, otherwise it times out. -// This particular rule makes the following assumptions: -// - the market of the liquidation is the market of the user, see the *DifferentMarkets rule -// - there is still some borrow on the market after liquidation. -rule stayHealthyLiquidate(env e, MorphoHarness.MarketParams marketParams, address borrower, uint256 seizedAssets, bytes data) { - MorphoHarness.Id id = libId(marketParams); - address user; - - // Assume the invariant initially. - require isHealthy(marketParams, user); - - uint256 debtSharesBefore = borrowShares(id, user); - uint256 debtAssetsBefore = summaryMulDivUp(debtSharesBefore, virtualTotalBorrowAssets(id), virtualTotalBorrowShares(id)); - // Safe require because of the invariants onlyEnabledLltv and lltvSmallerThanWad in ConsistentState.spec. - require marketParams.lltv < 10^18; - // Assumption to ensure that no interest is accumulated. - require lastUpdate(id) == e.block.timestamp; - - liquidate(e, marketParams, borrower, seizedAssets, 0, data); - require !priceChanged; - - // Safe require because of the invariant sumBorrowSharesCorrect. - require borrowShares(id, user) <= totalBorrowShares(id); - // Assume that there is still some borrow on the market after liquidation. - require totalBorrowAssets(id) > 0; - // Assume no bad debt realization. - require collateral(id, borrower) > 0; - - assert user != borrower; - assert debtSharesBefore == borrowShares(id, user); - assert debtAssetsBefore >= summaryMulDivUp(debtSharesBefore, virtualTotalBorrowAssets(id), virtualTotalBorrowShares(id)); - - bool stillHealthy = isHealthy(marketParams, user); - require !priceChanged; - assert stillHealthy; -} - -rule stayHealthyLiquidateDifferentMarkets(env e, MorphoHarness.MarketParams marketParams, address borrower, uint256 seizedAssets, bytes data) { - MorphoHarness.Id id = libId(marketParams); - address user; - MorphoHarness.MarketParams liquidationMarketParams; - - // Assume the invariant initially. - require isHealthy(marketParams, user); - - // Safe require because of the invariants onlyEnabledLltv and lltvSmallerThanWad in ConsistentState.spec. - require marketParams.lltv < 10^18; - // Assumption to ensure that no interest is accumulated. - require lastUpdate(id) == e.block.timestamp; - // Assume that the liquidation is on a different market. - require liquidationMarketParams != marketParams; - - liquidate(e, liquidationMarketParams, borrower, seizedAssets, 0, data); - require !priceChanged; - - // Safe require because of the invariant sumBorrowSharesCorrect. - require borrowShares(id, user) <= totalBorrowShares(id); - - bool stillHealthy = isHealthy(marketParams, user); - require !priceChanged; - assert stillHealthy; -} - // Check that users cannot lose collateral by unauthorized parties except in case of an unhealthy position. rule healthyUserCannotLoseCollateral(env e, method f, calldataarg data) filtered { f -> !f.isView } diff --git a/certora/specs/StayHealthy.spec b/certora/specs/StayHealthy.spec new file mode 100644 index 00000000..e69de29b From bbb4ccafad2ca652df70c5ac096bdc7aa01380d5 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Mon, 30 Sep 2024 11:37:30 +0200 Subject: [PATCH 11/14] chore: add StayHealthy spec --- certora/specs/StayHealthy.spec | 121 +++++++++++++++++++++++++++++++++ 1 file changed, 121 insertions(+) diff --git a/certora/specs/StayHealthy.spec b/certora/specs/StayHealthy.spec index e69de29b..840ed26d 100644 --- a/certora/specs/StayHealthy.spec +++ b/certora/specs/StayHealthy.spec @@ -0,0 +1,121 @@ +// SPDX-License-Identifier: GPL-2.0-or-later +import "Health.spec"; + +// Check that without accruing interest, no interaction can put an healthy account into an unhealthy one. +// The liquidate function times out in this rule, but has been checked separately. +rule stayHealthy(env e, method f, calldataarg data) +filtered { + f -> !f.isView && + f.selector != sig:liquidate(MorphoHarness.MarketParams, address, uint256, uint256, bytes).selector +} +{ + MorphoHarness.MarketParams marketParams; + MorphoHarness.Id id = libId(marketParams); + address user; + + // Assume that the position is healthy before the interaction. + require isHealthy(marketParams, user); + // Safe require because of the invariants onlyEnabledLltv and lltvSmallerThanWad in ConsistentState.spec. + require marketParams.lltv < 10^18; + // Assumption to ensure that no interest is accumulated. + require lastUpdate(id) == e.block.timestamp; + + priceChanged = false; + f(e, data); + + // Safe require because of the invariant sumBorrowSharesCorrect. + require borrowShares(id, user) <= totalBorrowShares(id); + + bool stillHealthy = isHealthy(marketParams, user); + assert !priceChanged => stillHealthy; +} + +// The liquidate case for the stayHealthy rule, assuming no bad debt realization, otherwise it times out. +// This particular rule makes the following assumptions: +// - the market of the liquidation is the market of the user, see the *DifferentMarkets rule, +// - there is still some borrow on the market after liquidation, see the *LastBorrow rule. +rule stayHealthyLiquidate(env e, MorphoHarness.MarketParams marketParams, address borrower, uint256 seizedAssets, bytes data) { + MorphoHarness.Id id = libId(marketParams); + address user; + + // Assume the invariant initially. + require isHealthy(marketParams, user); + + uint256 debtSharesBefore = borrowShares(id, user); + uint256 debtAssetsBefore = summaryMulDivUp(debtSharesBefore, virtualTotalBorrowAssets(id), virtualTotalBorrowShares(id)); + // Safe require because of the invariants onlyEnabledLltv and lltvSmallerThanWad in ConsistentState.spec. + require marketParams.lltv < 10^18; + // Assumption to ensure that no interest is accumulated. + require lastUpdate(id) == e.block.timestamp; + + liquidate(e, marketParams, borrower, seizedAssets, 0, data); + require !priceChanged; + + // Safe require because of the invariant sumBorrowSharesCorrect. + require borrowShares(id, user) <= totalBorrowShares(id); + // Assume that there is still some borrow on the market after liquidation. + require totalBorrowAssets(id) > 0; + // Assume no bad debt realization. + require collateral(id, borrower) > 0; + + assert user != borrower; + assert debtSharesBefore == borrowShares(id, user); + assert debtAssetsBefore >= summaryMulDivUp(debtSharesBefore, virtualTotalBorrowAssets(id), virtualTotalBorrowShares(id)); + + bool stillHealthy = isHealthy(marketParams, user); + require !priceChanged; + assert stillHealthy; +} + +rule stayHealthyLiquidateDifferentMarkets(env e, MorphoHarness.MarketParams marketParams, address borrower, uint256 seizedAssets, bytes data) { + MorphoHarness.Id id = libId(marketParams); + address user; + MorphoHarness.MarketParams liquidationMarketParams; + + // Assume the invariant initially. + require isHealthy(marketParams, user); + + // Safe require because of the invariants onlyEnabledLltv and lltvSmallerThanWad in ConsistentState.spec. + require marketParams.lltv < 10^18; + // Assumption to ensure that no interest is accumulated. + require lastUpdate(id) == e.block.timestamp; + // Assume that the liquidation is on a different market. + require liquidationMarketParams != marketParams; + + liquidate(e, liquidationMarketParams, borrower, seizedAssets, 0, data); + require !priceChanged; + + // Safe require because of the invariant sumBorrowSharesCorrect. + require borrowShares(id, user) <= totalBorrowShares(id); + + bool stillHealthy = isHealthy(marketParams, user); + require !priceChanged; + assert stillHealthy; +} + +rule stayHealthyLiquidateLastBorrow(env e, MorphoHarness.MarketParams marketParams, address borrower, uint256 seizedAssets, bytes data) { + MorphoHarness.Id id = libId(marketParams); + address user; + + // Assume the invariant initially. + require isHealthy(marketParams, user); + + uint256 debtSharesBefore = borrowShares(id, user); + uint256 debtAssetsBefore = summaryMulDivUp(debtSharesBefore, virtualTotalBorrowAssets(id), virtualTotalBorrowShares(id)); + // Safe require because of the invariants onlyEnabledLltv and lltvSmallerThanWad in ConsistentState.spec. + require marketParams.lltv < 10^18; + // Assumption to ensure that no interest is accumulated. + require lastUpdate(id) == e.block.timestamp; + + liquidate(e, marketParams, borrower, seizedAssets, 0, data); + require !priceChanged; + + // Safe require because of the invariant sumBorrowSharesCorrect. + require borrowShares(id, user) <= totalBorrowShares(id); + // Assume that there is still some borrow on the market after liquidation. + require totalBorrowAssets(id) == 0; + + bool stillHealthy = isHealthy(marketParams, user); + require !priceChanged; + assert stillHealthy; +} From eb6c5b613e70d32f502a69d7535adcef2513db45 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Mon, 30 Sep 2024 16:07:35 +0200 Subject: [PATCH 12/14] docs: adapt README --- certora/README.md | 3 ++- certora/specs/StayHealthy.spec | 1 - 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/certora/README.md b/certora/README.md index 12cc0fd8..cbd2b424 100644 --- a/certora/README.md +++ b/certora/README.md @@ -250,12 +250,13 @@ The [`certora/specs`](specs) folder contains the following files: - [`ExactMath.spec`](specs/ExactMath.spec) checks precise properties when taking into account exact multiplication and division. Notably, this file specifies that using supply and withdraw in the same block cannot yield more funds than at the start. - [`Health.spec`](specs/Health.spec) checks properties about the health of the positions. - Notably, functions cannot render an account unhealthy, and debt positions always have some collateral (thanks to the bad debt realization mechanism). + Notably, debt positions always have some collateral thanks to the bad debt realization mechanism. - [`LibSummary.spec`](specs/LibSummary.spec) checks the summarization of the library functions that are used in other specification files. - [`Liveness.spec`](specs/Liveness.spec) checks that main functions change the owner of funds and the amount of shares as expected, and that it's always possible to exit a position. - [`ExchangeRate.spec`](specs/ExchangeRate.spec) checks that the exchange rate between shares and assets evolves predictably over time. - [`Reentrancy.spec`](specs/Reentrancy.spec) checks that the contract is immune to a particular class of reentrancy issues. - [`Reverts.spec`](specs/Reverts.spec) checks the condition for reverts and that inputs are correctly validated. +- [`StayHealthy.spec`](specs/Health.spec) checks that functions cannot render an account unhealthy. - [`Transfer.spec`](specs/Transfer.spec) checks the summarization of the safe transfer library functions that are used in other specification files. The [`certora/confs`](confs) folder contains a configuration file for each corresponding specification file. diff --git a/certora/specs/StayHealthy.spec b/certora/specs/StayHealthy.spec index 840ed26d..9a8357e2 100644 --- a/certora/specs/StayHealthy.spec +++ b/certora/specs/StayHealthy.spec @@ -20,7 +20,6 @@ filtered { // Assumption to ensure that no interest is accumulated. require lastUpdate(id) == e.block.timestamp; - priceChanged = false; f(e, data); // Safe require because of the invariant sumBorrowSharesCorrect. From 82829078b1dfeb9ac4b56860cfffbe38f485da07 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Mon, 30 Sep 2024 16:11:35 +0200 Subject: [PATCH 13/14] docs: fix spec of no borrow Co-authored-by: MathisGD <74971347+MathisGD@users.noreply.github.com> Signed-off-by: Quentin Garchery --- certora/specs/StayHealthy.spec | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/certora/specs/StayHealthy.spec b/certora/specs/StayHealthy.spec index 9a8357e2..b4d8d85a 100644 --- a/certora/specs/StayHealthy.spec +++ b/certora/specs/StayHealthy.spec @@ -111,7 +111,7 @@ rule stayHealthyLiquidateLastBorrow(env e, MorphoHarness.MarketParams marketPara // Safe require because of the invariant sumBorrowSharesCorrect. require borrowShares(id, user) <= totalBorrowShares(id); - // Assume that there is still some borrow on the market after liquidation. + // Assume that there is no remaining borrow on the market after liquidation. require totalBorrowAssets(id) == 0; bool stillHealthy = isHealthy(marketParams, user); From 90c3c8e4ccb69c8b0ad9eda5143e81620f2ead96 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Mon, 30 Sep 2024 16:13:06 +0200 Subject: [PATCH 14/14] chore: remove unnecessary variable definition Co-authored-by: MathisGD <74971347+MathisGD@users.noreply.github.com> Signed-off-by: Quentin Garchery --- certora/specs/StayHealthy.spec | 2 -- 1 file changed, 2 deletions(-) diff --git a/certora/specs/StayHealthy.spec b/certora/specs/StayHealthy.spec index b4d8d85a..c92ea00e 100644 --- a/certora/specs/StayHealthy.spec +++ b/certora/specs/StayHealthy.spec @@ -99,8 +99,6 @@ rule stayHealthyLiquidateLastBorrow(env e, MorphoHarness.MarketParams marketPara // Assume the invariant initially. require isHealthy(marketParams, user); - uint256 debtSharesBefore = borrowShares(id, user); - uint256 debtAssetsBefore = summaryMulDivUp(debtSharesBefore, virtualTotalBorrowAssets(id), virtualTotalBorrowShares(id)); // Safe require because of the invariants onlyEnabledLltv and lltvSmallerThanWad in ConsistentState.spec. require marketParams.lltv < 10^18; // Assumption to ensure that no interest is accumulated.