Merge pull request #653 from morpho-org/refactor/improve-rounding-liq…

…uidate Rounding liquidate fix
morpho-org · Dec 20, 2023 · 5afa588 · 5afa588
2 parents e1dc2e2 + 90fb045
commit 5afa588
Show file tree

Hide file tree

Showing 12 changed files with 13 additions and 1 deletion.
diff --git a/certora/confs/AccrueInterest.conf b/certora/confs/AccrueInterest.conf
@@ -4,9 +4,11 @@
     ],
     "verify": "MorphoHarness:certora/specs/AccrueInterest.spec",
     "prover_args": [
+        "-depth 3",
         "-smt_hashingScheme plaininjectivity",
         "-mediumTimeout 30"
     ],
     "rule_sanity": "basic",
+    "server": "production",
     "msg": "Morpho Blue Accrue Interest"
 }
diff --git a/certora/confs/AssetsAccounting.conf b/certora/confs/AssetsAccounting.conf
@@ -4,5 +4,6 @@
     ],
     "verify": "MorphoHarness:certora/specs/AssetsAccounting.spec",
     "rule_sanity": "basic",
+    "server": "production",
     "msg": "Morpho Blue Assets Accounting"
 }
diff --git a/certora/confs/ConsistentState.conf b/certora/confs/ConsistentState.conf
@@ -4,5 +4,6 @@
     ],
     "verify": "MorphoHarness:certora/specs/ConsistentState.spec",
     "rule_sanity": "basic",
+    "server": "production",
     "msg": "Morpho Blue Consistent State"
 }
diff --git a/certora/confs/ExactMath.conf b/certora/confs/ExactMath.conf
@@ -8,5 +8,6 @@
         "-smt_hashingScheme plaininjectivity",
         "-mediumTimeout 30"
     ],
+    "server": "production",
     "msg": "Morpho Blue Exact Math"
 }
diff --git a/certora/confs/Health.conf b/certora/confs/Health.conf
@@ -8,5 +8,6 @@
     "prover_args": [
         "-smt_hashingScheme plaininjectivity"
     ],
+    "server": "production",
     "msg": "Morpho Blue Health"
 }
diff --git a/certora/confs/LibSummary.conf b/certora/confs/LibSummary.conf
@@ -4,5 +4,6 @@
     ],
     "verify": "MorphoHarness:certora/specs/LibSummary.spec",
     "rule_sanity": "basic",
+    "server": "production",
     "msg": "Morpho Blue Lib Summary"
 }
diff --git a/certora/confs/Liveness.conf b/certora/confs/Liveness.conf
@@ -4,5 +4,6 @@
     ],
     "verify": "MorphoInternalAccess:certora/specs/Liveness.spec",
     "rule_sanity": "basic",
+    "server": "production",
     "msg": "Morpho Blue Liveness"
 }
diff --git a/certora/confs/RatioMath.conf b/certora/confs/RatioMath.conf
@@ -9,5 +9,6 @@
         "-mediumTimeout 30",
         "-timeout 3600"
     ],
+    "server": "production",
     "msg": "Morpho Blue Ratio Math"
 }
diff --git a/certora/confs/Reentrancy.conf b/certora/confs/Reentrancy.conf
@@ -7,5 +7,6 @@
     "prover_args": [
         "-enableStorageSplitting false"
     ],
+    "server": "production",
     "msg": "Morpho Blue Reentrancy"
 }
diff --git a/certora/confs/Reverts.conf b/certora/confs/Reverts.conf
@@ -4,5 +4,6 @@
     ],
     "verify": "MorphoHarness:certora/specs/Reverts.spec",
     "rule_sanity": "basic",
+    "server": "production",
     "msg": "Morpho Blue Reverts"
 }
diff --git a/certora/confs/Transfer.conf b/certora/confs/Transfer.conf
@@ -7,5 +7,6 @@
     ],
     "verify": "TransferHarness:certora/specs/Transfer.spec",
     "rule_sanity": "basic",
+    "server": "production",
     "msg": "Morpho Blue Transfer"
 }
diff --git a/src/Morpho.sol b/src/Morpho.sol
@@ -371,7 +371,7 @@ contract Morpho is IMorphoStaticTyping {
             if (seizedAssets > 0) {
                 uint256 seizedAssetsQuoted = seizedAssets.mulDivUp(collateralPrice, ORACLE_PRICE_SCALE);
 
-                repaidShares = seizedAssetsQuoted.wDivUp(liquidationIncentiveFactor).toSharesDown(
+                repaidShares = seizedAssetsQuoted.wDivUp(liquidationIncentiveFactor).toSharesUp(
                     market[id].totalBorrowAssets, market[id].totalBorrowShares
                 );
             } else {