[Certora] Verif math is safe

.github/workflows/certora.yml

@@ -22,6 +22,7 @@ jobs:
           - Liveness
           - Reentrancy
           - Reverts
+          - SafeMath
 
     steps:
       - uses: actions/checkout@v4

certora/README.md

@@ -1,11 +1,11 @@
-# Pre-liquidation Contract Formal Verification
+# Pre-liquidation contract formal verification
 
 This folder contains the [CVL](https://docs.certora.com/en/latest/docs/cvl/index.html) specification and verification setup for the [PreLiquidation](../src/PreLiquidation.sol) contract.
 
-## Getting Started
+## Getting started
 
 This project depends on two different versions of [Solidity](https://soliditylang.org/) which are required for running the verification.
-The compiler binaries should be available under the following path names:
+The compiler binaries should be available in the paths:
 
 - `solc-0.8.19` for the solidity compiler version `0.8.19`, which is used for `Morpho`;
 - `solc-0.8.27` for the solidity compiler version `0.8.27`, which is used for `PreLiquidation`.
@@ -26,18 +26,22 @@ This is checked in [`Reentrancy.spec`](specs/Reentrancy.spec).
 
 This is checked in [`Immutability.spec`](specs/Immutability.spec).
 
-## Reverts
+### Reverts
 
 This is checked in [`Reverts.spec`](specs/Reverts.spec) and [`MarketExists.spec`](specs/MarketExists.spec)
 
-# Consitent Instantiation
+### Consistent instantiation
 
 This is checked in [`ConsistentInstantiation.spec`](specs/ConsistentInstantiation.spec).
 
 ### Liveness properties
 
 This is checked in [`Liveness.spec`](specs/Liveness.spec).
 
+### Safe math
+
+This is checked in [`SafeMath.spec`](specs/SafeMath.spec).
+
 ## Verification architecture
 
 ### Folders and file structure
@@ -48,14 +52,10 @@ The [`certora/specs`](specs) folder contains the following files:
 - [`Immutability.spec`](specs/Immutability.spec) checks that PreLiquidation contract is immutable because it doesn't perform any delegate call;
 - [`Liveness.spec`](specs/Liveness.spec) ensure that expected computations will always be performed.
   For instance, pre-liquidations will always trigger a repay operation.
-  We also check that pre-liquidation can successfully be performed by passing shares to be repaid instead of the collateral ammount to be seized.
+  We also check that pre-liquidation can successfully be performed by passing shares to be repaid instead of the collateral amount to be seized.
 - [`Reverts.spec`](specs/Reverts.spec) checks the conditions for reverts and that inputs are correctly validated.
 - [`ConsistentInstantiation.spec`](specs/ConsistentInstantiation.spec) checks the conditions for reverts are met in PreLiquidation constructor.
-- [`MarketExists.spec`](specs/MarketExists.spec) checks that PreLiquidations can be instanciated only if the target market exists.
+- [`MarketExists.spec`](specs/MarketExists.spec) checks that PreLiquidations can be instantiated only if the target market exists;
+- [`SafeMath.spec`](specs/SafeMath.spec) checks that PreLiquidations mathematical operations are safe.
 
 The [`certora/confs`](confs) folder contains a configuration file for each corresponding specification file.
-
-## TODO
-
-- [ ] Provide an overview of the specification.
-- [ ] Update the verification architecture.

certora/confs/ConsistentInstantiation.conf

@@ -2,28 +2,30 @@
   "files": [
     "src/PreLiquidation.sol",
     "lib/morpho-blue/certora/harness/MorphoHarness.sol",
-    "lib/morpho-blue/certora/harness/Util.sol",
+    "lib/morpho-blue/certora/harness/Util.sol"
   ],
   "link": [
-    "PreLiquidation:MORPHO=MorphoHarness",
+    "PreLiquidation:MORPHO=MorphoHarness"
   ],
-  "parametric_contracts" : ["PreLiquidation"],
-  "solc_optimize" : "99999",
-  "solc_via_ir" : true,
+  "parametric_contracts": [
+    "PreLiquidation"
+  ],
+  "solc_optimize": "99999",
+  "solc_via_ir": true,
   "solc_map": {
     "MorphoHarness": "solc-0.8.19",
     "Util": "solc-0.8.19",
-    "PreLiquidation": "solc-0.8.27",
+    "PreLiquidation": "solc-0.8.27"
   },
   "verify": "PreLiquidation:certora/specs/ConsistentInstantiation.spec",
   "prover_args": [
     "-depth 5",
     "-mediumTimeout 5",
     "-timeout 3600",
     "-smt_nonLinearArithmetic true",
-    "-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:lia2]",
+    "-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:lia2]"
   ],
   "rule_sanity": "basic",
   "server": "production",
-  "msg": "PreLiquidation ConsistentInstantiation",
+  "msg": "PreLiquidation ConsistentInstantiation"
 }

certora/confs/MarketExists.conf

@@ -1,17 +1,19 @@
 {
   "files": [
     "src/PreLiquidation.sol",
-    "lib/morpho-blue/src/Morpho.sol",
+    "lib/morpho-blue/src/Morpho.sol"
   ],
   "link": [
     "PreLiquidation:MORPHO=Morpho"
   ],
-  "parametric_contracts" : ["Morpho"],
-  "solc_optimize" : "99999",
-  "solc_via_ir" : true,
+  "parametric_contracts": [
+    "Morpho"
+  ],
+  "solc_optimize": "99999",
+  "solc_via_ir": true,
   "solc_map": {
     "Morpho": "solc-0.8.19",
-    "PreLiquidation": "solc-0.8.27",
+    "PreLiquidation": "solc-0.8.27"
   },
   "verify": "PreLiquidation:certora/specs/MarketExists.spec",
   "prover_args": [

certora/confs/Reverts.conf

@@ -2,29 +2,30 @@
   "files": [
     "src/PreLiquidation.sol",
     "lib/morpho-blue/certora/harness/MorphoHarness.sol",
-    "lib/morpho-blue/certora/harness/Util.sol",
+    "lib/morpho-blue/certora/harness/Util.sol"
   ],
   "link": [
-    "PreLiquidation:MORPHO=MorphoHarness",
+    "PreLiquidation:MORPHO=MorphoHarness"
   ],
-  "parametric_contracts" : ["PreLiquidation"],
-  "solc_optimize" : "99999",
-  "solc_via_ir" : true,
+  "parametric_contracts": [
+    "PreLiquidation"
+  ],
+  "solc_optimize": "99999",
+  "solc_via_ir": true,
   "solc_map": {
     "PreLiquidation": "solc-0.8.27",
     "MorphoHarness": "solc-0.8.19",
-    "Util": "solc-0.8.19",
+    "Util": "solc-0.8.19"
   },
   "verify": "PreLiquidation:certora/specs/Reverts.spec",
   "prover_args": [
     "-depth 5",
     "-mediumTimeout 40",
     "-timeout 3600",
     "-smt_nonLinearArithmetic true",
-    "-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:lia2]",
-
+    "-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:lia2]"
   ],
   "rule_sanity": "basic",
   "server": "production",
-  "msg": "PreLiquidation Reverts",
+  "msg": "PreLiquidation Reverts"
 }

certora/confs/SafeMath.conf

@@ -0,0 +1,11 @@
+{
+  "files": [
+    "src/PreLiquidation.sol"
+  ],
+  "solc_via_ir": true,
+  "solc": "solc-0.8.27",
+  "verify": "PreLiquidation:certora/specs/SafeMath.spec",
+  "rule_sanity": "basic",
+  "server": "production",
+  "msg": "PreLiquidation Safe Maths"
+}

certora/specs/SafeMath.spec

@@ -0,0 +1,40 @@
+// SPDX-License-Identifier: GPL-2.0-or-later
+
+definition WAD() returns mathint = 10^18;
+
+function summaryWMulDown(mathint x,mathint y) returns mathint {
+    return (x * y) / WAD();
+}
+
+function summaryWDivUp(mathint x,mathint y) returns mathint {
+    return (x * WAD() + (y-1)) / y;
+}
+
+
+// Check that LTV <= LLTV is equivalent to borrowed <= (collateralQuoted * LLTV) / WAD.
+rule ltvAgainstLltvEquivalentCheck {
+    uint256 borrowed;
+    uint256 collateralQuoted;
+    uint256 lltv;
+
+    // Safe require because the implementation would revert, see rule zeroCollateralQuotedReverts.
+    require collateralQuoted > 0;
+
+    mathint ltv = summaryWDivUp(borrowed, collateralQuoted);
+
+    assert ltv <= lltv <=> borrowed <= summaryWMulDown(collateralQuoted, lltv);
+}
+
+// Check that substracting the PRE_LLTV to LTV wont underflow.
+rule ltvAgainstPreLltvEquivalentCheck {
+    uint256 borrowed;
+    uint256 collateralQuoted;
+    uint256 preLltv;
+
+    // Safe require because the implementation would revert, see rule zeroCollateralQuotedReverts.
+    require (collateralQuoted > 0);
+
+    mathint ltv = summaryWDivUp(borrowed, collateralQuoted);
+
+    assert ltv > preLltv <=> borrowed > summaryWMulDown(collateralQuoted, preLltv);
+}