From e46fd7392bb5b8c39833360cac65c8fe94e86d07 Mon Sep 17 00:00:00 2001
From: Quentin Garchery <garchery.quentin@gmail.com>
Date: Tue, 15 Aug 2023 13:31:52 +0200
Subject: [PATCH] chore: add blue ratio math summary to CI

---
 .github/workflows/certora.yml          | 1 +
 certora/scripts/verifyBlueRatioMath.sh | 1 -
 certora/specs/Blue.spec                | 4 ++--
 certora/specs/BlueRatioMath.spec       | 4 ++--
 4 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml
index f43d9489f..ddced1d4d 100644
--- a/.github/workflows/certora.yml
+++ b/.github/workflows/certora.yml
@@ -42,3 +42,4 @@ jobs:
       matrix:
         script:
           - verifyBlue.sh
+          - verifyBlueRatioMathSummary.sh
diff --git a/certora/scripts/verifyBlueRatioMath.sh b/certora/scripts/verifyBlueRatioMath.sh
index c8cbf3987..088b34380 100755
--- a/certora/scripts/verifyBlueRatioMath.sh
+++ b/certora/scripts/verifyBlueRatioMath.sh
@@ -5,5 +5,4 @@ certoraRun \
     --verify MorphoHarness:certora/specs/BlueRatioMath.spec \
     --solc_allow_path src \
     --msg "Morpho Ratio Math" \
-    --send_only \
     "$@"
diff --git a/certora/specs/Blue.spec b/certora/specs/Blue.spec
index e45806fb1..ca5681e5d 100644
--- a/certora/specs/Blue.spec
+++ b/certora/specs/Blue.spec
@@ -150,10 +150,10 @@ rule supplyRevertZero(MorphoHarness.Market market) {
     assert lastReverted;
 }
 
-invariant invOnlyEnabledLltv(MorphoHarness.Market market)
+invariant onlyEnabledLltv(MorphoHarness.Market market)
     isInitialized(getMarketId(market)) => isLltvEnabled(market.lltv);
 
-invariant invOnlyEnabledIrm(MorphoHarness.Market market)
+invariant onlyEnabledIrm(MorphoHarness.Market market)
     isInitialized(getMarketId(market)) => isIrmEnabled(market.irm);
 
 rule marketIdUnique() {
diff --git a/certora/specs/BlueRatioMath.spec b/certora/specs/BlueRatioMath.spec
index ea5a48cb1..8461f973e 100644
--- a/certora/specs/BlueRatioMath.spec
+++ b/certora/specs/BlueRatioMath.spec
@@ -16,7 +16,7 @@ definition MAX_FEE() returns mathint = 10^18 * 25/100;
 
 invariant feeInRange(MorphoHarness.Id id)
     to_mathint(fee(id)) <= MAX_FEE();
- 
+
 /* This is a simple overapproximative summary, stating that it rounds in the right direction.
  * The summary is checked by the specification in BlueRatioMathSummary.spec.
  */
@@ -35,7 +35,7 @@ function summaryMulDivDown(uint256 x, uint256 y, uint256 d) returns uint256 {
     return result;
 }
 
-rule onlyLiquidateCanDecreasesRatio(method f) 
+rule onlyLiquidateCanDecreasesRatio(method f)
 filtered {
     f -> f.selector != sig:liquidate(MorphoHarness.Market, address, uint256, bytes).selector
 }