-
Notifications
You must be signed in to change notification settings - Fork 48
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Merge pull request #623 from morpho-org/certora/assets-accounting
[Certora] Assets accounting when entering a position
- Loading branch information
Showing
8 changed files
with
165 additions
and
109 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,8 @@ | ||
| { | ||
| "files": [ | ||
| "certora/harness/MorphoHarness.sol" | ||
| ], | ||
| "verify": "MorphoHarness:certora/specs/AssetsAccounting.spec", | ||
| "rule_sanity": "basic", | ||
| "msg": "Morpho Blue Assets Accounting" | ||
| } |
This file was deleted.
Oops, something went wrong.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,126 @@ | ||
| // SPDX-License-Identifier: GPL-2.0-or-later | ||
| 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 collateral(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 lastUpdate(MorphoHarness.Id) external returns uint256 envfree; | ||
|
|
||
| function libMulDivDown(uint256, uint256, uint256) external returns uint256 envfree; | ||
| function libMulDivUp(uint256, uint256, uint256) external returns uint256 envfree; | ||
| function libId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree; | ||
| } | ||
|
|
||
| function expectedSupplyAssets(MorphoHarness.Id id, address user) returns uint256 { | ||
| uint256 userShares = supplyShares(id, user); | ||
| uint256 totalSupplyAssets = virtualTotalSupplyAssets(id); | ||
| uint256 totalSupplyShares = virtualTotalSupplyShares(id); | ||
|
|
||
| return libMulDivDown(userShares, totalSupplyAssets, totalSupplyShares); | ||
| } | ||
|
|
||
| function expectedBorrowAssets(MorphoHarness.Id id, address user) returns uint256 { | ||
| uint256 userShares = borrowShares(id, user); | ||
| uint256 totalBorrowAssets = virtualTotalBorrowAssets(id); | ||
| uint256 totalBorrowShares = virtualTotalBorrowShares(id); | ||
|
|
||
| return libMulDivUp(userShares, totalBorrowAssets, totalBorrowShares); | ||
| } | ||
|
|
||
| // Check that the assets supplied are greater than the assets owned in the end. | ||
| rule supplyAssetsAccounting(env e, MorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, bytes data) { | ||
| MorphoHarness.Id id = libId(marketParams); | ||
|
|
||
| // Assume no interest as it would increase the total supply assets. | ||
| require lastUpdate(id) == e.block.timestamp; | ||
| // Assume no supply position to begin with. | ||
| require supplyShares(id, onBehalf) == 0; | ||
|
|
||
| uint256 suppliedAssets; | ||
| suppliedAssets, _ = supply(e, marketParams, assets, shares, onBehalf, data); | ||
|
|
||
| uint256 ownedAssets = expectedSupplyAssets(id, onBehalf); | ||
|
|
||
| assert suppliedAssets >= ownedAssets; | ||
| } | ||
|
|
||
| // Check that the assets withdrawn are less than the assets owned initially. | ||
| rule withdrawAssetsAccounting(env e, MorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, address receiver) { | ||
| MorphoHarness.Id id = libId(marketParams); | ||
|
|
||
| // Assume no interest as it would increase the total supply assets. | ||
| require lastUpdate(id) == e.block.timestamp; | ||
|
|
||
| uint256 ownedAssets = expectedSupplyAssets(id, onBehalf); | ||
|
|
||
| uint256 withdrawnAssets; | ||
| withdrawnAssets, _ = withdraw(e, marketParams, assets, shares, onBehalf, receiver); | ||
|
|
||
| assert withdrawnAssets <= ownedAssets; | ||
| } | ||
|
|
||
| // Check that the assets borrowed are less than the assets owed in the end. | ||
| rule borrowAssetsAccounting(env e, MorphoHarness.MarketParams marketParams, uint256 shares, address onBehalf, address receiver) { | ||
| MorphoHarness.Id id = libId(marketParams); | ||
|
|
||
| // Assume no interest as it would increase the total borrowed assets. | ||
| require lastUpdate(id) == e.block.timestamp; | ||
| // Assume no outstanding debt to begin with. | ||
| require borrowShares(id, onBehalf) == 0; | ||
|
|
||
| // The borrow call is restricted to shares as input to make it easier on the prover. | ||
| uint256 borrowedAssets; | ||
| borrowedAssets, _ = borrow(e, marketParams, 0, shares, onBehalf, receiver); | ||
|
|
||
| uint256 owedAssets = expectedBorrowAssets(id, onBehalf); | ||
|
|
||
| assert borrowedAssets <= owedAssets; | ||
| } | ||
|
|
||
| // Check that the assets repaid are greater than the assets owed initially. | ||
| rule repayAssetsAccounting(env e, MorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, bytes data) { | ||
| MorphoHarness.Id id = libId(marketParams); | ||
|
|
||
| // Assume no interest as it would increase the total borrowed assets. | ||
| require lastUpdate(id) == e.block.timestamp; | ||
|
|
||
| uint256 owedAssets = expectedBorrowAssets(id, onBehalf); | ||
|
|
||
| uint256 repaidAssets; | ||
| repaidAssets, _ = repay(e, marketParams, assets, shares, onBehalf, data); | ||
|
|
||
| // Assume a full repay. | ||
| require borrowShares(id, onBehalf) == 0; | ||
|
|
||
| assert repaidAssets >= owedAssets; | ||
| } | ||
|
|
||
| // Check that the collateral assets supplied are greater than the assets owned in the end. | ||
| rule supplyCollateralAssetsAccounting(env e, MorphoHarness.MarketParams marketParams, uint256 suppliedAssets, address onBehalf, bytes data) { | ||
| MorphoHarness.Id id = libId(marketParams); | ||
|
|
||
| // Assume no collateral to begin with. | ||
| require collateral(id, onBehalf) == 0; | ||
|
|
||
| supplyCollateral(e, marketParams, suppliedAssets, onBehalf, data); | ||
|
|
||
| uint256 ownedAssets = collateral(id, onBehalf); | ||
|
|
||
| assert suppliedAssets == ownedAssets; | ||
| } | ||
|
|
||
| // Check that the collateral assets withdrawn are less than the assets owned initially. | ||
| rule withdrawCollateralAssetsAccounting(env e, MorphoHarness.MarketParams marketParams, uint256 withdrawnAssets, address onBehalf, address receiver) { | ||
| MorphoHarness.Id id = libId(marketParams); | ||
|
|
||
| uint256 ownedAssets = collateral(id, onBehalf); | ||
|
|
||
| withdrawCollateral(e, marketParams, withdrawnAssets, onBehalf, receiver); | ||
|
|
||
| assert withdrawnAssets <= ownedAssets; | ||
| } |
This file was deleted.
Oops, something went wrong.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.