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] Cannot lose position & can withdraw all #348

Merged
merged 2 commits into from
Aug 18, 2023
Merged

[Certora] Cannot lose position & can withdraw all #348

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
df8e27f
More generic rules
jhoenicke Aug 16, 2023
f3fc707
Rule for withdrawing everything
jhoenicke Aug 17, 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
162 changes: 161 additions & 1 deletion certora/specs/Blue.spec
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,16 +1,20 @@
methods {
function supply(MorphoHarness.Market, uint256, uint256, address, bytes) external;
function getVirtualTotalSupply(MorphoHarness.Id) external returns uint256 envfree;
function getVirtualTotalSupplyShares(MorphoHarness.Id) external returns uint256 envfree;
function supplyShares(MorphoHarness.Id, address user) external returns uint256 envfree;
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This line is duplicated at line 7

function totalSupply(MorphoHarness.Id) external returns uint256 envfree;
function totalBorrow(MorphoHarness.Id) external returns uint256 envfree;
function supplyShares(MorphoHarness.Id, address user) external returns uint256 envfree;
function borrowShares(MorphoHarness.Id, address user) external returns uint256 envfree;
function collateral(MorphoHarness.Id, address user) external returns uint256 envfree;
function totalSupplyShares(MorphoHarness.Id) external returns uint256 envfree;
function totalBorrowShares(MorphoHarness.Id) external returns uint256 envfree;
function fee(MorphoHarness.Id) external returns uint256 envfree;
function getMarketId(MorphoHarness.Market) external returns MorphoHarness.Id envfree;
function idToMarket(MorphoHarness.Id) external returns (address, address, address, address, uint256) envfree;
function isAuthorized(address, address) external returns bool envfree;

function isHealthy(MorphoHarness.Market, address user) external returns bool envfree;
function lastUpdate(MorphoHarness.Id) external returns uint256 envfree;
function isLltvEnabled(uint256) external returns bool envfree;
function isIrmEnabled(address) external returns bool envfree;
Expand Down Expand Up @@ -167,3 +171,159 @@ rule marketIdUnique() {
assert market1.irm == market2.irm;
assert market1.lltv == market2.lltv;
}

rule onlyUserCanAuthorizeWithoutSig(method f, calldataarg data)
filtered {
f -> !f.isView && f.selector != sig:setAuthorizationWithSig(MorphoHarness.Authorization memory, MorphoHarness.Signature calldata).selector
}
{
address user;
address someone;
env e;

require user != e.msg.sender;
bool authorizedBefore = isAuthorized(user, someone);

f(e, data);

assert isAuthorized(user, someone) == authorizedBefore;
}

rule supplyMovesTokensAndIncreasesShares() {
MorphoHarness.Market market;
uint256 assets;
uint256 shares;
uint256 suppliedAssets;
uint256 suppliedShares;
address onbehalf;
bytes data;
MorphoHarness.Id id = getMarketId(market);
env e;

require e.msg.sender != currentContract;
require lastUpdate(id) == e.block.timestamp;

mathint sharesBefore = supplyShares(id, onbehalf);
mathint balanceBefore = myBalances[market.borrowableToken];

suppliedAssets, suppliedShares = supply(e, market, assets, shares, onbehalf, data);
assert assets != 0 => suppliedAssets == assets && shares == 0;
assert assets == 0 => suppliedShares == shares && shares != 0;

mathint sharesAfter = supplyShares(id, onbehalf);
mathint balanceAfter = myBalances[market.borrowableToken];
assert sharesAfter == sharesBefore + suppliedShares;
assert balanceAfter == balanceBefore + suppliedAssets;
}

rule userCannotLoseSupplyShares(method f, calldataarg data)
filtered {
f -> !f.isView
}
{
MorphoHarness.Market market;
uint256 assets;
uint256 shares;
uint256 suppliedAssets;
uint256 suppliedShares;
address user;
MorphoHarness.Id id = getMarketId(market);
env e;

require !isAuthorized(user, e.msg.sender);
require user != e.msg.sender;

mathint sharesBefore = supplyShares(id, user);

f(e, data);

mathint sharesAfter = supplyShares(id, user);
assert sharesAfter >= sharesBefore;
}

rule userCannotGainBorrowShares(method f, calldataarg data)
filtered {
f -> !f.isView
}
{
MorphoHarness.Market market;
uint256 assets;
uint256 shares;
uint256 suppliedAssets;
uint256 suppliedShares;
address user;
MorphoHarness.Id id = getMarketId(market);
env e;

require !isAuthorized(user, e.msg.sender);
require user != e.msg.sender;

mathint sharesBefore = borrowShares(id, user);

f(e, data);

mathint sharesAfter = borrowShares(id, user);
assert sharesAfter <= sharesBefore;
}


rule userWithoutBorrowCannotLoseCollateral(method f, calldataarg data)
filtered {
f -> !f.isView
}
{
MorphoHarness.Market market;
uint256 assets;
uint256 shares;
uint256 suppliedAssets;
uint256 suppliedShares;
address user;
MorphoHarness.Id id = getMarketId(market);
env e;

require !isAuthorized(user, e.msg.sender);
require user != e.msg.sender;
require borrowShares(id, user) == 0;
mathint collateralBefore = collateral(id, user);

f(e, data);

mathint collateralAfter = collateral(id, user);
assert borrowShares(id, user) == 0;
assert collateralAfter >= collateralBefore;
}

rule noTimeTravel(method f, env e, calldataarg data) filtered {
f -> !f.isView
} {
MorphoHarness.Id id;
require lastUpdate(id) <= e.block.timestamp;
f(e, data);
assert lastUpdate(id) <= e.block.timestamp;
}

rule canWithdrawAll() {
MorphoHarness.Market market;
uint256 withdrawnAssets;
uint256 withdrawnShares;
address receiver;
env e;

MorphoHarness.Id id = getMarketId(market);
uint256 shares = supplyShares(id, e.msg.sender);

require isInitialized(id);
require e.msg.sender != 0;
require receiver != 0;
require e.msg.value == 0;
require shares > 0;
require totalBorrow(id) == 0;
require lastUpdate(id) <= e.block.timestamp;
require shares < totalSupplyShares(id);
require totalSupplyShares(id) < 10^40 && totalSupply(id) < 10^30;

withdrawnAssets, withdrawnShares = withdraw@withrevert(e, market, 0, shares, e.msg.sender, receiver);

assert withdrawnShares == shares;
assert !lastReverted, "Can withdraw all assets if nobody borrows";
}
36 changes: 34 additions & 2 deletions certora/specs/Health.spec
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,8 @@
methods {
function lastUpdate(MorphoHarness.Id) external returns uint256 envfree;
function collateral(MorphoHarness.Id, address) external returns uint256 envfree;
function isHealthy(MorphoHarness.Market, address user) external returns bool envfree;
function isAuthorized(address, address user) external returns bool envfree;
function getMarketId(MorphoHarness.Market) external returns MorphoHarness.Id envfree;
function _.price() external => mockPrice() expect uint256;
function MathLib.mulDivDown(uint256 a, uint256 b, uint256 c) internal returns uint256 => summaryMulDivDown(a,b,c);
Expand Down Expand Up @@ -32,9 +34,11 @@ function summaryMin(uint256 a, uint256 b) returns uint256 {
return a < b ? a : b;
}

rule stayHealthy(method f, env e, calldataarg data) filtered {
rule stayHealthy(method f, env e, calldataarg data)
filtered {
f -> !f.isView
} {
}
{
MorphoHarness.Market market;
MorphoHarness.Id id = getMarketId(market);
address user;
Expand All @@ -50,3 +54,31 @@ rule stayHealthy(method f, env e, calldataarg data) filtered {
bool stillHealthy = isHealthy(market, user);
assert !priceChanged => stillHealthy;
}

rule healthyUserCannotLoseCollateral(method f, calldataarg data)
filtered {
f -> !f.isView
}
{
MorphoHarness.Market market;
uint256 assets;
uint256 shares;
uint256 suppliedAssets;
uint256 suppliedShares;
address user;
MorphoHarness.Id id = getMarketId(market);
env e;

require !isAuthorized(user, e.msg.sender);
require user != e.msg.sender;
require lastUpdate(id) == e.block.timestamp;
require isHealthy(market, user);
mathint collateralBefore = collateral(id, user);
priceChanged = false;

f(e, data);

require !priceChanged;
mathint collateralAfter = collateral(id, user);
assert collateralAfter >= collateralBefore;
}