Skip to content

Commit

Permalink
docs: fix spec of no borrow
Browse files Browse the repository at this point in the history
Co-authored-by: MathisGD <74971347+MathisGD@users.noreply.github.com>
Signed-off-by: Quentin Garchery <QGarchery@users.noreply.github.com>
  • Loading branch information
QGarchery and MathisGD authored Sep 30, 2024
1 parent eb6c5b6 commit 8282907
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion certora/specs/StayHealthy.spec
Original file line number Diff line number Diff line change
Expand Up @@ -111,7 +111,7 @@ rule stayHealthyLiquidateLastBorrow(env e, MorphoHarness.MarketParams marketPara

// Safe require because of the invariant sumBorrowSharesCorrect.
require borrowShares(id, user) <= totalBorrowShares(id);
// Assume that there is still some borrow on the market after liquidation.
// Assume that there is no remaining borrow on the market after liquidation.
require totalBorrowAssets(id) == 0;

bool stillHealthy = isHealthy(marketParams, user);
Expand Down

0 comments on commit 8282907

Please sign in to comment.