Skip to content

Commit 9f80ff1

Browse files
QGarcheryQGarchery
authored
Merge pull request #607 from morpho-org/certora/mutant-12
[Certora] mutant 12
2 parents 434df02 + 166ea99 commit 9f80ff1

File tree

10 files changed

+57
-27
lines changed

10 files changed

+57
-27
lines changed

‎certora/specs/AccrueInterest.spec

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,12 @@
11
// SPDX-License-Identifier: GPL-2.0-or-later
22
methods {
33
function extSloads(bytes32[]) external returns bytes32[] => NONDET DELETE;
4+
5+
function maxFee() external returns uint256 envfree;
6+
47
function MathLib.mulDivDown(uint256 a, uint256 b, uint256 c) internal returns uint256 => ghostMulDivDown(a,b,c);
58
function MathLib.mulDivUp(uint256 a, uint256 b, uint256 c) internal returns uint256 => ghostMulDivUp(a,b,c);
69
function MathLib.wTaylorCompounded(uint256 a, uint256 b) internal returns uint256 => ghostTaylorCompounded(a, b);
7-
810
// We assume here that all external functions will not access storage, since we cannot show commutativity otherwise.
911
// We also need to assume that the price and borrow rate return always the same value (and do not depend on msg.origin), so we use ghost functions for them.
1012
function _.borrowRate(MorphoHarness.MarketParams marketParams, MorphoHarness.Market market) external with (env e) => ghostBorrowRate(marketParams.irm, e.block.timestamp) expect uint256;
@@ -16,8 +18,6 @@ methods {
1618
function _.onMorphoSupply(uint256, bytes) external => NONDET;
1719
function _.onMorphoSupplyCollateral(uint256, bytes) external => NONDET;
1820
function _.onMorphoFlashLoan(uint256, bytes) external => NONDET;
19-
20-
function maxFee() external returns uint256 envfree;
2121
}
2222

2323
ghost ghostMulDivUp(uint256, uint256, uint256) returns uint256;

‎certora/specs/ConsistentState.spec

Lines changed: 9 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -1,25 +1,25 @@
11
// SPDX-License-Identifier: GPL-2.0-or-later
22
methods {
33
function extSloads(bytes32[]) external returns bytes32[] => NONDET DELETE;
4+
5+
function supplyShares(MorphoHarness.Id, address) external returns uint256 envfree;
6+
function borrowShares(MorphoHarness.Id, address) external returns uint256 envfree;
7+
function collateral(MorphoHarness.Id, address) external returns uint256 envfree;
48
function totalSupplyAssets(MorphoHarness.Id) external returns uint256 envfree;
59
function totalSupplyShares(MorphoHarness.Id) external returns uint256 envfree;
610
function totalBorrowAssets(MorphoHarness.Id) external returns uint256 envfree;
711
function totalBorrowShares(MorphoHarness.Id) external returns uint256 envfree;
8-
function supplyShares(MorphoHarness.Id, address) external returns uint256 envfree;
9-
function borrowShares(MorphoHarness.Id, address) external returns uint256 envfree;
10-
function collateral(MorphoHarness.Id, address) external returns uint256 envfree;
1112
function fee(MorphoHarness.Id) external returns uint256 envfree;
1213
function lastUpdate(MorphoHarness.Id) external returns uint256 envfree;
13-
function libId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree;
14-
15-
function isAuthorized(address, address) external returns bool envfree;
16-
function isLltvEnabled(uint256) external returns bool envfree;
1714
function isIrmEnabled(address) external returns bool envfree;
18-
19-
function _.borrowRate(MorphoHarness.MarketParams, MorphoHarness.Market) external => HAVOC_ECF;
15+
function isLltvEnabled(uint256) external returns bool envfree;
16+
function isAuthorized(address, address) external returns bool envfree;
2017

2118
function maxFee() external returns uint256 envfree;
2219
function wad() external returns uint256 envfree;
20+
function libId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree;
21+
22+
function _.borrowRate(MorphoHarness.MarketParams, MorphoHarness.Market) external => HAVOC_ECF;
2323

2424
function SafeTransferLib.safeTransfer(address token, address to, uint256 value) internal => summarySafeTransferFrom(token, currentContract, to, value);
2525
function SafeTransferLib.safeTransferFrom(address token, address from, address to, uint256 value) internal => summarySafeTransferFrom(token, from, to, value);

‎certora/specs/ExactMath.spec

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,21 +1,22 @@
11
// SPDX-License-Identifier: GPL-2.0-or-later
22
methods {
33
function extSloads(bytes32[]) external returns bytes32[] => NONDET DELETE;
4-
function libId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree;
4+
55
function virtualTotalSupplyAssets(MorphoHarness.Id) external returns uint256 envfree;
66
function virtualTotalSupplyShares(MorphoHarness.Id) external returns uint256 envfree;
77
function virtualTotalBorrowAssets(MorphoHarness.Id) external returns uint256 envfree;
88
function virtualTotalBorrowShares(MorphoHarness.Id) external returns uint256 envfree;
99
function fee(MorphoHarness.Id) external returns uint256 envfree;
1010
function lastUpdate(MorphoHarness.Id) external returns uint256 envfree;
1111

12+
function maxFee() external returns uint256 envfree;
13+
function libId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree;
14+
1215
function MathLib.mulDivDown(uint256 a, uint256 b, uint256 c) internal returns uint256 => summaryMulDivDown(a,b,c);
1316
function MathLib.mulDivUp(uint256 a, uint256 b, uint256 c) internal returns uint256 => summaryMulDivUp(a,b,c);
1417
function SafeTransferLib.safeTransfer(address token, address to, uint256 value) internal => NONDET;
1518
function SafeTransferLib.safeTransferFrom(address token, address from, address to, uint256 value) internal => NONDET;
1619
function _.onMorphoSupply(uint256 assets, bytes data) external => HAVOC_ECF;
17-
18-
function maxFee() external returns uint256 envfree;
1920
}
2021

2122
function summaryMulDivUp(uint256 x, uint256 y, uint256 d) returns uint256 {

‎certora/specs/ExitLiquidity.spec

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,14 +1,14 @@
11
// SPDX-License-Identifier: GPL-2.0-or-later
22
methods {
33
function extSloads(bytes32[]) external returns bytes32[] => NONDET DELETE;
4+
45
function supplyShares(MorphoHarness.Id, address) external returns uint256 envfree;
56
function borrowShares(MorphoHarness.Id, address) external returns uint256 envfree;
67
function collateral(MorphoHarness.Id, address) external returns uint256 envfree;
78
function virtualTotalSupplyAssets(MorphoHarness.Id) external returns uint256 envfree;
89
function virtualTotalSupplyShares(MorphoHarness.Id) external returns uint256 envfree;
910
function virtualTotalBorrowAssets(MorphoHarness.Id) external returns uint256 envfree;
1011
function virtualTotalBorrowShares(MorphoHarness.Id) external returns uint256 envfree;
11-
1212
function lastUpdate(MorphoHarness.Id) external returns uint256 envfree;
1313

1414
function libMulDivDown(uint256, uint256, uint256) external returns uint256 envfree;

‎certora/specs/Health.spec

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,13 +1,15 @@
11
// SPDX-License-Identifier: GPL-2.0-or-later
22
methods {
33
function extSloads(bytes32[]) external returns bytes32[] => NONDET DELETE;
4-
function lastUpdate(MorphoHarness.Id) external returns uint256 envfree;
4+
55
function totalBorrowShares(MorphoHarness.Id) external returns uint256 envfree;
6+
function lastUpdate(MorphoHarness.Id) external returns uint256 envfree;
67
function borrowShares(MorphoHarness.Id, address) external returns uint256 envfree;
78
function collateral(MorphoHarness.Id, address) external returns uint256 envfree;
8-
function isHealthy(MorphoHarness.MarketParams, address user) external returns bool envfree;
99
function isAuthorized(address, address user) external returns bool envfree;
10+
1011
function libId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree;
12+
function isHealthy(MorphoHarness.MarketParams, address user) external returns bool envfree;
1113

1214
function _.price() external => mockPrice() expect uint256;
1315
function MathLib.mulDivDown(uint256 a, uint256 b, uint256 c) internal returns uint256 => summaryMulDivDown(a,b,c);

‎certora/specs/LibSummary.spec

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,7 @@
11
// SPDX-License-Identifier: GPL-2.0-or-later
22
methods {
33
function extSloads(bytes32[]) external returns bytes32[] => NONDET DELETE;
4+
45
function libMulDivUp(uint256, uint256, uint256) external returns uint256 envfree;
56
function libMulDivDown(uint256, uint256, uint256) external returns uint256 envfree;
67
function libId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree;

‎certora/specs/Liveness.spec

Lines changed: 18 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,15 +1,18 @@
11
// SPDX-License-Identifier: GPL-2.0-or-later
22
methods {
33
function extSloads(bytes32[]) external returns bytes32[] => NONDET DELETE;
4+
function supplyShares(MorphoInternalAccess.Id, address) external returns uint256 envfree;
5+
function borrowShares(MorphoInternalAccess.Id, address) external returns uint256 envfree;
6+
function collateral(MorphoInternalAccess.Id, address) external returns uint256 envfree;
47
function totalSupplyAssets(MorphoInternalAccess.Id) external returns uint256 envfree;
58
function totalSupplyShares(MorphoInternalAccess.Id) external returns uint256 envfree;
69
function totalBorrowAssets(MorphoInternalAccess.Id) external returns uint256 envfree;
710
function totalBorrowShares(MorphoInternalAccess.Id) external returns uint256 envfree;
8-
function supplyShares(MorphoInternalAccess.Id, address) external returns uint256 envfree;
9-
function borrowShares(MorphoInternalAccess.Id, address) external returns uint256 envfree;
10-
function collateral(MorphoInternalAccess.Id, address) external returns uint256 envfree;
1111
function fee(MorphoInternalAccess.Id) external returns uint256 envfree;
1212
function lastUpdate(MorphoInternalAccess.Id) external returns uint256 envfree;
13+
function nonce(address) external returns uint256 envfree;
14+
function isAuthorized(address, address) external returns bool envfree;
15+
1316
function libId(MorphoInternalAccess.MarketParams) external returns MorphoInternalAccess.Id envfree;
1417
function refId(MorphoInternalAccess.MarketParams) external returns MorphoInternalAccess.Id envfree;
1518

@@ -290,6 +293,18 @@ rule liquidateChangesTokens(env e, MorphoInternalAccess.MarketParams marketParam
290293
assert liquidityAfter == liquidityBefore + min(repaidAssets, borrowLoanAssetsBefore);
291294
}
292295

296+
// Check that nonce and authorization are properly updated with calling setAuthorizationWithSig.
297+
rule setAuthorizationWithSigChangesNonceAndAuthorizes(env e, MorphoInternalAccess.Authorization authorization, MorphoInternalAccess.Signature signature) {
298+
mathint nonceBefore = nonce(authorization.authorizer);
299+
300+
setAuthorizationWithSig(e, authorization, signature);
301+
302+
mathint nonceAfter = nonce(authorization.authorizer);
303+
304+
assert nonceAfter == nonceBefore + 1;
305+
assert isAuthorized(authorization.authorizer, authorization.authorized) == authorization.isAuthorized;
306+
}
307+
293308
// Check that one can always repay the debt in full.
294309
rule canRepayAll(env e, MorphoInternalAccess.MarketParams marketParams, uint256 shares, bytes data) {
295310
MorphoInternalAccess.Id id = libId(marketParams);

‎certora/specs/RatioMath.spec

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,21 +1,22 @@
11
// SPDX-License-Identifier: GPL-2.0-or-later
22
methods {
33
function extSloads(bytes32[]) external returns bytes32[] => NONDET DELETE;
4-
function libId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree;
54
function virtualTotalSupplyAssets(MorphoHarness.Id) external returns uint256 envfree;
65
function virtualTotalSupplyShares(MorphoHarness.Id) external returns uint256 envfree;
76
function virtualTotalBorrowAssets(MorphoHarness.Id) external returns uint256 envfree;
87
function virtualTotalBorrowShares(MorphoHarness.Id) external returns uint256 envfree;
98
function fee(MorphoHarness.Id) external returns uint256 envfree;
109
function lastUpdate(MorphoHarness.Id) external returns uint256 envfree;
1110

11+
function maxFee() external returns uint256 envfree;
12+
function libId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree;
13+
1214
function MathLib.mulDivDown(uint256 a, uint256 b, uint256 c) internal returns uint256 => summaryMulDivDown(a,b,c);
1315
function MathLib.mulDivUp(uint256 a, uint256 b, uint256 c) internal returns uint256 => summaryMulDivUp(a,b,c);
1416
function MathLib.wTaylorCompounded(uint256, uint256) internal returns uint256 => NONDET;
1517

1618
function _.borrowRate(MorphoHarness.MarketParams, MorphoHarness.Market) external => HAVOC_ECF;
1719

18-
function maxFee() external returns uint256 envfree;
1920
}
2021

2122
invariant feeInRange(MorphoHarness.Id id)

‎certora/specs/Reentrancy.spec

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,7 @@
11
// SPDX-License-Identifier: GPL-2.0-or-later
22
methods {
33
function extSloads(bytes32[]) external returns bytes32[] => NONDET DELETE;
4+
45
function _.borrowRate(MorphoHarness.MarketParams marketParams, MorphoHarness.Market) external => summaryBorrowRate() expect uint256;
56
}
67

‎certora/specs/Reverts.spec

Lines changed: 13 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,19 +1,21 @@
11
// SPDX-License-Identifier: GPL-2.0-or-later
22
methods {
33
function extSloads(bytes32[]) external returns bytes32[] => NONDET DELETE;
4+
45
function owner() external returns address envfree;
6+
function feeRecipient() external returns address envfree;
57
function totalSupplyAssets(MorphoHarness.Id) external returns uint256 envfree;
68
function totalBorrowAssets(MorphoHarness.Id) external returns uint256 envfree;
79
function totalSupplyShares(MorphoHarness.Id) external returns uint256 envfree;
810
function totalBorrowShares(MorphoHarness.Id) external returns uint256 envfree;
911
function lastUpdate(MorphoHarness.Id) external returns uint256 envfree;
10-
11-
function feeRecipient() external returns address envfree;
12-
function isLltvEnabled(uint256) external returns bool envfree;
1312
function isIrmEnabled(address) external returns bool envfree;
13+
function isLltvEnabled(uint256) external returns bool envfree;
1414
function isAuthorized(address, address) external returns bool envfree;
15+
function nonce(address) external returns uint256 envfree;
1516

1617
function libId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree;
18+
1719
function maxFee() external returns uint256 envfree;
1820
function wad() external returns uint256 envfree;
1921
}
@@ -156,12 +158,19 @@ rule withdrawCollateralInputValidation(env e, MorphoHarness.MarketParams marketP
156158
assert assets == 0 || onBehalf == 0 => lastReverted;
157159
}
158160

159-
// Check that liqudiate reverts when its inputs are not validated.
161+
// Check that liquidate reverts when its inputs are not validated.
160162
rule liquidateInputValidation(env e, MorphoHarness.MarketParams marketParams, address borrower, uint256 seizedAssets, uint256 repaidShares, bytes data) {
161163
liquidate@withrevert(e, marketParams, borrower, seizedAssets, repaidShares, data);
162164
assert !exactlyOneZero(seizedAssets, repaidShares) => lastReverted;
163165
}
164166

167+
// Check that setAuthorizationWithSig reverts when its inputs are not validated.
168+
rule setAuthorizationWithSigInputValidation(env e, MorphoHarness.Authorization authorization, MorphoHarness.Signature signature) {
169+
uint256 nonceBefore = nonce(authorization.authorizer);
170+
setAuthorizationWithSig@withrevert(e, authorization, signature);
171+
assert e.block.timestamp > authorization.deadline || authorization.nonce != nonceBefore => lastReverted;
172+
}
173+
165174
// Check that accrueInterest reverts when its inputs are not validated.
166175
rule accrueInterestInputValidation(env e, MorphoHarness.MarketParams marketParams) {
167176
uint256 lastUpdate = lastUpdate(libId(marketParams));

0 commit comments

Comments
 (0)