fix: wait for results in the CI

morpho-org · Nov 25, 2024 · 60991b4 · 60991b4
1 parent f04942e
commit 60991b4
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 3 deletions.
diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml
@@ -50,6 +50,6 @@ jobs:
           sudo mv solc-static-linux /usr/local/bin/solc-0.8.19
 
       - name: Verify ${{ matrix.conf }}
-        run: certoraRun certora/confs/${{ matrix.conf }}.conf
+        run: certoraRun certora/confs/${{ matrix.conf }}.conf --wait_for_results
         env:
           CERTORAKEY: ${{ secrets.CERTORAKEY }}
diff --git a/certora/specs/LiquidateBuffer.spec b/certora/specs/LiquidateBuffer.spec
@@ -61,11 +61,12 @@ rule liquidateImprovePosition(MorphoLiquidateHarness.MarketParams marketParams,
     uint256 newTotalAssets = require_uint256(virtualTotalBorrowAssets(id) - repaidAssets);
 
     uint256 newBorrowerAssets = summaryMulDivUp(newBorrowerShares, newTotalAssets, newTotalShares);
+    uint256 newBorrowerAssetsDown = summaryMulDivDown(newBorrowerShares, newTotalAssets, newTotalShares);
     uint256 newBorrowerCollateral = require_uint256(borrowerCollateral - seizedAssets);
 
     assert repaidShares * borrowerCollateral >= seizedAssets * borrowerShares;
     assert borrowerShares * newBorrowerCollateral >= newBorrowerShares * borrowerCollateral;
     assert newTotalShares * virtualTotalBorrowAssets(id) >= newTotalAssets * virtualTotalBorrowShares(id);
-    assert borrowerShares * virtualTotalBorrowAssets(id) * newTotalShares * newBorrowerCollateral >= newBorrowerShares * virtualTotalBorrowShares(id) * newTotalAssets * borrowerCollateral;
-    assert borrowerAssets * newBorrowerCollateral >= newBorrowerAssets * borrowerCollateral;
+    require borrowerShares * virtualTotalBorrowAssets(id) * newTotalShares * newBorrowerCollateral >= newBorrowerShares * virtualTotalBorrowShares(id) * newTotalAssets * borrowerCollateral;
+    assert borrowerAssets * newBorrowerCollateral >= newBorrowerAssetsDown * borrowerCollateral;
 }