Skip to content

Commit

Permalink
Merge pull request #619 from morpho-org/certora/refactor-exact-math
Browse files Browse the repository at this point in the history 
[Certora] Refactor ExactMath
  • Loading branch information
@QGarchery
QGarchery authored Dec 1, 2023
2 parents 2d5a8f6 + 83f692f commit 3646c4d
Show file tree
Hide file tree
Showing 2 changed files with 36 additions and 38 deletions.
62 changes: 32 additions & 30 deletions certora/specs/ExactMath.spec
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,12 +2,15 @@
methods {
function extSloads(bytes32[]) external returns bytes32[] => NONDET DELETE;

function feeRecipient() external returns address envfree;
function supplyShares(MorphoHarness.Id, address) external returns uint256 envfree;
function borrowShares(MorphoHarness.Id, address) external returns uint256 envfree;
function virtualTotalSupplyAssets(MorphoHarness.Id) external returns uint256 envfree;
function virtualTotalSupplyShares(MorphoHarness.Id) external returns uint256 envfree;
function virtualTotalBorrowAssets(MorphoHarness.Id) external returns uint256 envfree;
function virtualTotalBorrowShares(MorphoHarness.Id) external returns uint256 envfree;
function fee(MorphoHarness.Id) external returns uint256 envfree;
function lastUpdate(MorphoHarness.Id) external returns uint256 envfree;
function fee(MorphoHarness.Id) external returns uint256 envfree;

function maxFee() external returns uint256 envfree;
function libId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree;
Expand All @@ -31,7 +34,7 @@ function summaryMulDivDown(uint256 x, uint256 y, uint256 d) returns uint256 {

// Check that when not accruing interest, and when repaying all, the borrow ratio is at least reset to the initial ratio.
// More details on the purpose of this rule in RatioMath.spec.
rule repayAllResetsBorrowRatio(env e, MorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onbehalf, bytes data) {
rule repayAllResetsBorrowRatio(env e, MorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, bytes data) {
MorphoHarness.Id id = libId(marketParams);
// Safe require because this invariant is checked in ConsistentState.spec
require fee(id) <= maxFee();
Expand All @@ -43,7 +46,7 @@ rule repayAllResetsBorrowRatio(env e, MorphoHarness.MarketParams marketParams, u
require lastUpdate(id) == e.block.timestamp;

mathint repaidAssets;
repaidAssets, _ = repay(e, marketParams, assets, shares, onbehalf, data);
repaidAssets, _ = repay(e, marketParams, assets, shares, onBehalf, data);

// Check the case where the market is fully repaid.
require repaidAssets >= assetsBefore;
Expand All @@ -59,63 +62,62 @@ rule repayAllResetsBorrowRatio(env e, MorphoHarness.MarketParams marketParams, u
rule supplyWithdraw() {
MorphoHarness.MarketParams marketParams;
MorphoHarness.Id id = libId(marketParams);
uint256 assets;
uint256 shares;
address onbehalf;
address receiver;
bytes data;
env e1;
env e2;
address onBehalf;

// Assume that interactions to happen at the same block.
// Assume that interactions happen at the same block.
require e1.block.timestamp == e2.block.timestamp;
// Assume that the user starts without any supply position.
require supplyShares(id, onBehalf) == 0;
// Assume that the user is not the fee recipient, otherwise the gain can come from the fee.
require onBehalf != feeRecipient();
// Safe require because timestamps cannot realistically be that large.
require e1.block.timestamp < 2^128;

uint256 supplyAssets; uint256 supplyShares; bytes data;
uint256 suppliedAssets;
uint256 suppliedShares;
suppliedAssets, suppliedShares = supply(e1, marketParams, assets, shares, onbehalf, data);
suppliedAssets, suppliedShares = supply(e1, marketParams, supplyAssets, supplyShares, onBehalf, data);

// Hints for the prover.
assert suppliedAssets * (virtualTotalSupplyShares(id) - suppliedShares) >= suppliedShares * (virtualTotalSupplyAssets(id) - suppliedAssets);
assert suppliedAssets * virtualTotalSupplyShares(id) >= suppliedShares * virtualTotalSupplyAssets(id);

uint256 withdrawAssets; uint256 withdrawShares; address receiver;
uint256 withdrawnAssets;
uint256 withdrawnShares;
withdrawnAssets, withdrawnShares = withdraw(e2, marketParams, 0, suppliedShares, onbehalf, receiver);
withdrawnAssets, _ = withdraw(e2, marketParams, withdrawAssets, withdrawShares, onBehalf, receiver);

assert withdrawnShares == suppliedShares;
assert withdrawnAssets <= suppliedAssets;
}

// There should be no profit from withdraw followed immediately by supply.
rule withdrawSupply() {
// There should be no profit from borrow followed immediately by repaying all.
rule borrowRepay() {
MorphoHarness.MarketParams marketParams;
MorphoHarness.Id id = libId(marketParams);
uint256 assets;
uint256 shares;
address onbehalf;
address receiver;
bytes data;
address onBehalf;
env e1;
env e2;

// Assume interactions to happen at the same block.
// Assume interactions happen at the same block.
require e1.block.timestamp == e2.block.timestamp;
// Assume that the user starts without any borrow position.
require borrowShares(id, onBehalf) == 0;
// Safe require because timestamps cannot realistically be that large.
require e1.block.timestamp < 2^128;

uint256 withdrawnAssets;
uint256 withdrawnShares;
withdrawnAssets, withdrawnShares = withdraw(e2, marketParams, assets, shares, onbehalf, receiver);
uint256 borrowAssets; uint256 borrowShares; address receiver;
uint256 borrowedAssets;
uint256 borrowedShares;
borrowedAssets, borrowedShares = borrow(e2, marketParams, borrowAssets, borrowShares, onBehalf, receiver);

// Hints for the prover.
assert withdrawnAssets * (virtualTotalSupplyShares(id) + withdrawnShares) <= withdrawnShares * (virtualTotalSupplyAssets(id) + withdrawnAssets);
assert withdrawnAssets * virtualTotalSupplyShares(id) <= withdrawnShares * virtualTotalSupplyAssets(id);
assert borrowedAssets * (virtualTotalBorrowShares(id) - borrowedShares) <= borrowedShares * (virtualTotalBorrowAssets(id) - borrowedAssets);
assert borrowedAssets * virtualTotalBorrowShares(id) <= borrowedShares * virtualTotalBorrowAssets(id);

uint256 suppliedAssets;
uint256 suppliedShares;
suppliedAssets, suppliedShares = supply(e1, marketParams, withdrawnAssets, 0, onbehalf, data);
bytes data;
uint256 repaidAssets;
repaidAssets, _ = repay(e1, marketParams, 0, borrowedShares, onBehalf, data);

assert suppliedAssets == withdrawnAssets && withdrawnShares >= suppliedShares;
assert borrowedAssets <= repaidAssets;
}
12 changes: 4 additions & 8 deletions certora/specs/Liveness.spec
View file
Original file line number Diff line number Diff line change
Expand Up @@ -96,8 +96,7 @@ rule supplyChangesTokensAndShares(env e, MorphoInternalAccess.MarketParams marke
// 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);
suppliedAssets, _ = supply(e, marketParams, 0, shares, onBehalf, data);

satisfy suppliedAssets != 0;
}
Expand Down Expand Up @@ -133,8 +132,7 @@ rule withdrawChangesTokensAndShares(env e, MorphoInternalAccess.MarketParams mar
// 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);
withdrawnAssets, _ = withdraw(e, marketParams, 0, shares, onBehalf, receiver);

satisfy withdrawnAssets != 0;
}
Expand Down Expand Up @@ -170,8 +168,7 @@ rule borrowChangesTokensAndShares(env e, MorphoInternalAccess.MarketParams marke
// 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);
borrowedAssets, _ = borrow(e, marketParams, 0, shares, onBehalf, receiver);

satisfy borrowedAssets != 0;
}
Expand Down Expand Up @@ -210,8 +207,7 @@ rule repayChangesTokensAndShares(env e, MorphoInternalAccess.MarketParams market
// 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);
repaidAssets, _ = repay(e, marketParams, 0, shares, onBehalf, data);

satisfy repaidAssets != 0;
}
Expand Down

0 comments on commit 3646c4d

Please sign in to comment.