Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[Certora] mutant 3 #616

Merged
merged 3 commits into from
Nov 24, 2023
Merged

[Certora] mutant 3 #616

Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
744d0ff
test: mutant 3
QGarchery Nov 22, 2023
5753c9f
feat: can use shares properties
QGarchery Nov 23, 2023
87d55a6
Revert "test: mutant 3"
QGarchery Nov 24, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
36 changes: 36 additions & 0 deletions certora/specs/Liveness.spec
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -85,6 +85,15 @@ rule supplyChangesTokensAndShares(env e, MorphoInternalAccess.MarketParams marke
assert balanceAfter == balanceBefore + suppliedAssets;
}

// Check that you can supply non-zero tokens by passing shares.
rule canSupplyByPassingShares(env e, MorphoInternalAccess.MarketParams marketParams, uint256 shares, address onBehalf, bytes data) {
uint256 suppliedAssets;
uint256 suppliedShares;
suppliedAssets, suppliedShares = supply(e, marketParams, 0, shares, onBehalf, data);

satisfy suppliedAssets != 0;
}

// Check that tokens and shares are properly accounted following a withdraw.
rule withdrawChangesTokensAndShares(env e, MorphoInternalAccess.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, address receiver) {
MorphoInternalAccess.Id id = libId(marketParams);
Expand All @@ -110,6 +119,15 @@ rule withdrawChangesTokensAndShares(env e, MorphoInternalAccess.MarketParams mar
assert balanceAfter == balanceBefore - withdrawnAssets;
}

// Check that you can withdraw non-zero tokens by passing shares.
rule canWithdrawByPassingShares(env e, MorphoInternalAccess.MarketParams marketParams, uint256 shares, address onBehalf, address receiver) {
uint256 withdrawnAssets;
uint256 withdrawnShares;
withdrawnAssets, withdrawnShares = withdraw(e, marketParams, 0, shares, onBehalf, receiver);

satisfy withdrawnAssets != 0;
}

// Check that tokens and shares are properly accounted following a borrow.
rule borrowChangesTokensAndShares(env e, MorphoInternalAccess.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, address receiver) {
MorphoInternalAccess.Id id = libId(marketParams);
Expand All @@ -135,6 +153,15 @@ rule borrowChangesTokensAndShares(env e, MorphoInternalAccess.MarketParams marke
assert balanceAfter == balanceBefore - borrowedAssets;
}

// Check that you can borrow non-zero tokens by passing shares.
rule canBorrowByPassingShares(env e, MorphoInternalAccess.MarketParams marketParams, uint256 shares, address onBehalf, address receiver) {
uint256 borrowedAssets;
uint256 borrowedShares;
borrowedAssets, borrowedShares = borrow(e, marketParams, 0, shares, onBehalf, receiver);

satisfy borrowedAssets != 0;
}

// Check that tokens and shares are properly accounted following a repay.
rule repayChangesTokensAndShares(env e, MorphoInternalAccess.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, bytes data) {
MorphoInternalAccess.Id id = libId(marketParams);
Expand All @@ -160,6 +187,15 @@ rule repayChangesTokensAndShares(env e, MorphoInternalAccess.MarketParams market
assert balanceAfter == balanceBefore + repaidAssets;
}

// Check that you can repay non-zero tokens by passing shares.
rule canRepayByPassingShares(env e, MorphoInternalAccess.MarketParams marketParams, uint256 shares, address onBehalf, bytes data) {
uint256 repaidAssets;
uint256 repaidShares;
repaidAssets, repaidShares = repay(e, marketParams, 0, shares, onBehalf, data);

satisfy repaidAssets != 0;
}

// Check that tokens and balances are properly accounted following a supplyCollateral.
rule supplyCollateralChangesTokensAndBalance(env e, MorphoInternalAccess.MarketParams marketParams, uint256 assets, address onBehalf, bytes data) {
MorphoInternalAccess.Id id = libId(marketParams);
Expand Down