feat: ensure math is safe

.github/workflows/certora.yml

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

certora/README.md

@@ -5,7 +5,7 @@ This folder contains the [CVL](https://docs.certora.com/en/latest/docs/cvl/index
 ## 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
+### Consitent 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 operation 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/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,44 @@
+// SPDX-License-Identifier: GPL-2.0-or-later
+
+definition WAD() returns uint256 = 10^18;
+
+function summaryWMulDown(uint256 x,uint256 y) returns uint256 {
+    // Safe require because the reference implementation would revert.
+    return require_uint256((x * y)/WAD());
+}
+
+function summaryWDivUp(uint256 x,uint256 y) returns uint256 {
+    // Safe require because the reference implementation would revert.
+    return require_uint256((x * WAD() + (y-1)) / y);
+}
+
+
+// Check that LTV <= LLTV is equivalent to borrowed <= (collateralQuoted * LLTV) / WAD.
+rule borrowedLECollatQuotedTimesLLTVEqLtvLTEqLLTV {
+    uint256 borrowed;
+    uint256 collateralQuoted;
+
+    // Safe require because the implementation would revert, see rule zeroCollateralQuotedReverts.
+    require collateralQuoted > 0;
+
+    mathint ltv = summaryWDivUp(borrowed, collateralQuoted);
+
+    assert (ltv <= currentContract.LLTV) <=> borrowed <= summaryWMulDown(collateralQuoted, currentContract.LLTV);
+}
+
+// Check that substracting the PRE_LLTV to LTV wont underflow.
+rule ltvMinusPreLltvWontUnderflow {
+    uint256 borrowed;
+    uint256 collateralQuoted;
+    uint256 preLltv;
+
+    // Safe require because the implementation would revert, see rule zeroCollateralQuotedReverts.
+    require (collateralQuoted > 0);
+
+    // Safe require because the implementation would revert if borrowed threshold is not ensured.
+    uint256 borrowThreshold = summaryWMulDown(collateralQuoted, preLltv);
+    require (borrowed > borrowThreshold);
+
+    uint256 ltv = summaryWDivUp(borrowed, collateralQuoted);
+    assert ltv >= preLltv;
+}