From 5179b34c14b451d974b4766a7dbd68959f1b3fc3 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Tue, 26 Nov 2024 09:58:51 +0100 Subject: [PATCH] Revert "fix: wait for results in the CI" This reverts commit 60991b4fe9b240d32bb49bc05fc6dc6df4886b01. --- .github/workflows/certora.yml | 2 +- certora/specs/LiquidateBuffer.spec | 5 ++--- 2 files changed, 3 insertions(+), 4 deletions(-) diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml index 4c503fb8..9eef0744 100644 --- 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 --wait_for_results + run: certoraRun certora/confs/${{ matrix.conf }}.conf env: CERTORAKEY: ${{ secrets.CERTORAKEY }} diff --git a/certora/specs/LiquidateBuffer.spec b/certora/specs/LiquidateBuffer.spec index 33ead7f4..0259d79b 100644 --- a/certora/specs/LiquidateBuffer.spec +++ b/certora/specs/LiquidateBuffer.spec @@ -61,12 +61,11 @@ 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); - require borrowerShares * virtualTotalBorrowAssets(id) * newTotalShares * newBorrowerCollateral >= newBorrowerShares * virtualTotalBorrowShares(id) * newTotalAssets * borrowerCollateral; - assert borrowerAssets * newBorrowerCollateral >= newBorrowerAssetsDown * borrowerCollateral; + assert borrowerShares * virtualTotalBorrowAssets(id) * newTotalShares * newBorrowerCollateral >= newBorrowerShares * virtualTotalBorrowShares(id) * newTotalAssets * borrowerCollateral; + assert borrowerAssets * newBorrowerCollateral >= newBorrowerAssets * borrowerCollateral; }