Merge branch 'main' into certora/supply-cap

README.md

@@ -6,7 +6,7 @@ MetaMorpho is a protocol for noncustodial risk management on top of [Morpho Blue
 It enables anyone to create a vault depositing liquidity into multiple Morpho Blue markets.
 It offers a seamless experience similar to Aave and Compound.
 
-Users of MetaMorpho are liquidity providers that want to earn from borrowing interest without having to actively manage the risk of their position.
+Users of MetaMorpho are liquidity providers who want to earn from borrowing interest without having to actively manage the risk of their position.
 The active management of the deposited assets is the responsibility of a set of different roles (owner, curator and allocators).
 These roles are primarily responsible for enabling and disabling markets on Morpho Blue and managing the allocation of users’ funds.
 
@@ -182,6 +182,50 @@ If one of the allocators starts setting the withdraw queue and/or supply queue t
 
 ## Getting Started
 
+### Package installation
+
+```bash
+npm install @morpho-org/metamorpho
+```
+
+```bash
+yarn add @morpho-org/metamorpho
+```
+
+### Usage
+
+Bundle a supply cap raise and a reallocation to the market:
+
+```typescript
+import { MetaMorphoAction } from "@morpho-org/metamorpho";
+
+const marketParams1 = {
+  collateralToken: "0x...",
+  loanToken: "0x...",
+  irm: "0x...",
+  oracle: "0x...",
+  lltv: 86_0000000000000000n,
+};
+
+const marketParams2 = {
+  collateralToken: "0x...",
+  loanToken: marketParams1.loanToken,
+  irm: "0x...",
+  oracle: "0x...",
+  lltv: 96_5000000000000000n,
+};
+
+await metamorpho.connect(curator).multicall([
+  MetaMorphoAction.acceptCap(marketParams2),
+  MetaMorphoAction.reallocate([
+    { marketParams: marketParams1, assets: 600_000000000000000000n },
+    { marketParams: marketParams2, assets: 100_000000000000000000n },
+  ]),
+]);
+```
+
+## Development
+
 Install dependencies: `yarn`
 
 Run forge tests: `yarn test:forge`

certora/README.md

@@ -26,7 +26,7 @@ certoraRun certora/confs/Range.conf --rule timelockInRange
 # High-level description
 
 A MetaMorpho vault is an ERC4626 vault that defines a list of Morpho Blue markets to allocate its funds.
-See [`README.md`](../README.md) for a in depth description of MetaMorpho.
+See [`README.md`](../README.md) for an in depth description of MetaMorpho.
 
 ## ERC20 tokens and transfers
 
@@ -38,7 +38,7 @@ The verification is done for the most common ERC20 implementations, for which we
 
 - [ERC20Standard](dispatch/ERC20Standard.sol) which respects the standard and reverts in case of insufficient funds or in case of insufficient allowance.
 - [ERC20NoRevert](dispatch/ERC20NoRevert.sol) which respects the standard but does not revert (and returns false instead).
-- [ERC20USDT](dispatch/ERC20USDT.sol) which does not strictly respects the standard because it omits the return value of the `transfer` and `transferFrom` functions.
+- [ERC20USDT](dispatch/ERC20USDT.sol) which does not strictly respect the standard because it omits the return value of the `transfer` and `transferFrom` functions.
 
 ## Roles
 
@@ -90,7 +90,7 @@ Note also that these properties are ensured to always hold, because the contract
 
 ### Consistent asset
 
-For deposit and withdraw, it is checked that markets have a the same loan token as the loan token of the vault.
+For deposit and withdraw, it is checked that markets have the same loan token as the loan token of the vault.
 We say that such market has a consistent asset.
 The following function defined in [`ConsistentState.spec`](specs/ConsistentState.spec) is verified to always return `true` and contributes to verifying the property above.
 
@@ -120,7 +120,7 @@ function isInWithdrawQueueIsEnabled(uint256 i) returns bool {
 }
 ```
 
-Thorough the code of MetaMorpho, this enabled flag is checked to be set to true, which is an efficient check that does not require to go through the whole withdraw queue.
+Throughout the code of MetaMorpho, this enabled flag is checked to be set to true, which is an efficient check that does not require to go through the whole withdraw queue.
 This check also ensures that such markets have some properties, since verifying those are necessary to be added to the withdraw queue.
 For example, markets added to the withdraw queue necessarily have a consistent asset.
 
@@ -143,11 +143,11 @@ rule newSupplyQueueEnsuresPositiveCap(env e, MetaMorphoHarness.Id[] newSupplyQue
 
 The previous rule ensures that when setting a new supply queue, each market has a positive supply cap.
 Markets can have a positive supply cap only if they are created on Morpho Blue.
-We can prove then that each market of the supply queue has been created on Morpho, because if a market has ben created it cannot be "destroyed" later.
+We can prove then that each market of the supply queue has been created on Morpho, because if a market has been created it cannot be "destroyed" later.
 
 ## Liveness
 
-The liveness properties ensures that some crucial actions cannot be blocked.
+The liveness properties ensure that some crucial actions cannot be blocked.
 It is notably useful to show that in case of an emergency, it is still possible to make salvaging transactions.
 The `canPauseSupply` rule in [`Liveness.spec`](specs/Liveness.spec) shows that it is always possible to prevent new deposits.
 This is done by first setting the supply queue as the empty queue and checking that it does not revert:

certora/confs/ConsistentState.conf

@@ -10,11 +10,7 @@
     "verify": "MetaMorphoHarness:certora/specs/ConsistentState.spec",
     "loop_iter": "2",
     "optimistic_loop": true,
-    "prover_args": [
-        "-depth 3",
-        "-mediumTimeout 20",
-        "-timeout 300",
-    ],
+    "smt_timeout": "600",
     "rule_sanity": "basic",
     "server": "production",
     "msg": "MetaMorpho Consistent State"

certora/confs/Enabled.conf

@@ -11,7 +11,9 @@
         "-depth 3",
         "-mediumTimeout 20",
         "-timeout 1000",
+        "-smt_easy_LIA true",
     ],
+    "smt_timeout": "7000",
     "rule_sanity": "basic",
     "server": "production",
     "msg": "MetaMorpho Enabled"

certora/confs/Liveness.conf

@@ -16,10 +16,9 @@
     "loop_iter": "2",
     "optimistic_loop": true,
     "prover_args": [
-        "-depth 3",
-        "-mediumTimeout 20",
-        "-timeout 120",
+        "-smt_easy_LIA true",
     ],
+    "smt_timeout": "7000",
     "rule_sanity": "basic",
     "server": "production",
     "msg": "MetaMorpho Liveness"

certora/confs/Range.conf

@@ -7,9 +7,11 @@
     "loop_iter": "2",
     "optimistic_loop": true,
     "prover_args": [
-        "-depth 3",
-        "-mediumTimeout 20",
+        "-depth 0",
         "-timeout 300",
+        "-smt_nonLinearArithmetic true",
+        "-adaptiveSolverConfig false",
+        "-solvers [z3:def{randomSeed=1},z3:def{randomSeed=2},z3:def{randomSeed=3},z3:def{randomSeed=4},z3:def{randomSeed=5},z3:def{randomSeed=6},z3:def{randomSeed=7},z3:def{randomSeed=8},z3:def{randomSeed=9},z3:def{randomSeed=10}]",
     ],
     "rule_sanity": "basic",
     "server": "production",

certora/specs/ConsistentState.spec

@@ -11,7 +11,7 @@ methods {
     function Util.withdrawnAssets(address, MetaMorphoHarness.Id, uint256, uint256) external returns (uint256) envfree;
 }
 
-// Check that fee cannot accrue to an unset fee recipient.
+// Check that the fee cannot accrue to an unset fee recipient.
 invariant noFeeToUnsetFeeRecipient()
     feeRecipient() == 0 => fee() == 0;
 

certora/specs/LastUpdated.spec

@@ -19,10 +19,10 @@ function hasGuardianRole(address user) returns bool {
     return user == owner() || user == guardian();
 }
 
-// Check that any market with positive cap is created on Morpho Blue.
+// Check that any market with a positive cap is created on Morpho Blue.
 // The corresponding invariant is difficult to verify because it requires to check properties on MetaMorpho and on Blue at the same time:
 // - on MetaMorpho, that it holds when the cap is positive for the first time
-// - on Blue, that a created market always has positive last update
+// - on Blue, that a created market always has a positive last update
 function hasPositiveSupplyCapIsUpdated(MetaMorphoHarness.Id id) returns bool {
     return config_(id).cap > 0 => Morpho.lastUpdate(id) > 0;
 }

certora/specs/Roles.spec

@@ -13,7 +13,7 @@ methods {
     function guardian() external returns(address) envfree;
     function isAllocator(address target) external returns(bool) envfree;
 
-    // Sumarize Morpho external calls, as they don't depend on the authorization system of MetaMorpho.
+    // Summarize Morpho external calls, as they don't depend on the authorization system of MetaMorpho.
     function _.idToMarketParams(MetaMorphoHarness.Id) external => CONSTANT;
     function _.supplyShares(MetaMorphoHarness.Id, address) external => CONSTANT;
     function _.accrueInterest(MetaMorphoHarness.MarketParams) external => CONSTANT;

certora/specs/Timelock.spec

@@ -97,7 +97,7 @@ rule capIncreaseTime(env e_next, method f, calldataarg args) {
     f(e_next, args);
 
     if (e_next.block.timestamp < nextTime)  {
-        // Check that cap cannot increase.
+        // Check that the cap cannot increase.
         assert config_(id).cap <= prevCap;
         // Increasing nextCapIncreaseTime with an interaction;
         assert nextCapIncreaseTime(e_next, id) >= nextCapIncreaseTimeBeforeInteraction;

package.json

@@ -2,7 +2,7 @@
   "name": "@morpho-org/metamorpho",
   "description": "MetaMorpho multicall encoder",
   "license": "GPL-2.0-or-later",
-  "version": "1.0.0",
+  "version": "1.1.0",
   "main": "lib/index.js",
   "bin": "lib/cli.js",
   "files": [