Skip to content

Commit

Permalink
chore: one assert
Browse files Browse the repository at this point in the history
  • Loading branch information
QGarchery committed Dec 12, 2024
1 parent 914c244 commit 47d7558
Showing 1 changed file with 1 addition and 2 deletions.
3 changes: 1 addition & 2 deletions certora/specs/LiquidateBuffer.spec
Original file line number Diff line number Diff line change
Expand Up @@ -34,12 +34,11 @@ rule liquidateImprovePosition(env e, MorphoHarness.MarketParams marketParams, ad
uint256 repaidAssets;
(seizedAssets, repaidAssets) = liquidate(e, marketParams, borrower, seizedAssetsInput, repaidSharesInput, data);


uint256 newBorrowerShares = borrowShares(id, borrower);
uint256 repaidShares = assert_uint256(borrowerShares - newBorrowerShares);

require !priceChanged;
assert collateral(id, borrower) != 0;
require collateral(id, borrower) != 0;
assert repaidShares * borrowerCollateral >= seizedAssets * borrowerShares;
// assert borrowerShares * newBorrowerCollateral >= newBorrowerShares * borrowerCollateral;
// assert newTotalShares * OldVirtualTotalBorrowAssets >= newTotalAssets * OldVirtualTotalBorrowShares;
Expand Down

0 comments on commit 47d7558

Please sign in to comment.