Merge pull request #315 from morpho-labs/certora/update-ci

[Certora] Update CI
morpho-org · Aug 16, 2023 · 7cd9d1e · 7cd9d1e
2 parents 31b9133 + e46fd73
commit 7cd9d1e
Show file tree

Hide file tree

Showing 4 changed files with 5 additions and 5 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
 }