Skip to content

Commit c2969a6

Browse files
committed
feat: add asset balance check to round-trip properties
1 parent 6641fa2 commit c2969a6

File tree

1 file changed

+19
-8
lines changed

1 file changed

+19
-8
lines changed

ERC4626.prop.sol

Lines changed: 19 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -245,8 +245,19 @@ abstract contract ERC4626Prop is Test {
245245
// round trip properties
246246
//
247247

248+
modifier checkNoFreeProfit(address caller) {
249+
uint256 assetsBefore = _getTotalAssets(caller);
250+
_;
251+
uint256 assetsAfter = _getTotalAssets(caller);
252+
assertApproxLeAbs(assetsAfter, assetsBefore, _delta_);
253+
}
254+
255+
function _getTotalAssets(address account) internal returns (uint256) {
256+
return vault_convertToAssets(IERC20(_vault_).balanceOf(account)) + IERC20(_underlying_).balanceOf(account);
257+
}
258+
248259
// redeem(deposit(a)) <= a
249-
function prop_RT_deposit_redeem(address caller, uint assets) public {
260+
function prop_RT_deposit_redeem(address caller, uint assets) public checkNoFreeProfit(caller) {
250261
if (!_vaultMayBeEmpty) vm.assume(IERC20(_vault_).totalSupply() > 0);
251262
vm.prank(caller); uint shares = vault_deposit(assets, caller);
252263
vm.prank(caller); uint assets2 = vault_redeem(shares, caller, caller);
@@ -256,15 +267,15 @@ abstract contract ERC4626Prop is Test {
256267
// s = deposit(a)
257268
// s' = withdraw(a)
258269
// s' >= s
259-
function prop_RT_deposit_withdraw(address caller, uint assets) public {
270+
function prop_RT_deposit_withdraw(address caller, uint assets) public checkNoFreeProfit(caller) {
260271
if (!_vaultMayBeEmpty) vm.assume(IERC20(_vault_).totalSupply() > 0);
261272
vm.prank(caller); uint shares1 = vault_deposit(assets, caller);
262273
vm.prank(caller); uint shares2 = vault_withdraw(assets, caller, caller);
263274
assertApproxGeAbs(shares2, shares1, _delta_);
264275
}
265276

266277
// deposit(redeem(s)) <= s
267-
function prop_RT_redeem_deposit(address caller, uint shares) public {
278+
function prop_RT_redeem_deposit(address caller, uint shares) public checkNoFreeProfit(caller) {
268279
vm.prank(caller); uint assets = vault_redeem(shares, caller, caller);
269280
if (!_vaultMayBeEmpty) vm.assume(IERC20(_vault_).totalSupply() > 0);
270281
vm.prank(caller); uint shares2 = vault_deposit(assets, caller);
@@ -274,15 +285,15 @@ abstract contract ERC4626Prop is Test {
274285
// a = redeem(s)
275286
// a' = mint(s)
276287
// a' >= a
277-
function prop_RT_redeem_mint(address caller, uint shares) public {
288+
function prop_RT_redeem_mint(address caller, uint shares) public checkNoFreeProfit(caller) {
278289
vm.prank(caller); uint assets1 = vault_redeem(shares, caller, caller);
279290
if (!_vaultMayBeEmpty) vm.assume(IERC20(_vault_).totalSupply() > 0);
280291
vm.prank(caller); uint assets2 = vault_mint(shares, caller);
281292
assertApproxGeAbs(assets2, assets1, _delta_);
282293
}
283294

284295
// withdraw(mint(s)) >= s
285-
function prop_RT_mint_withdraw(address caller, uint shares) public {
296+
function prop_RT_mint_withdraw(address caller, uint shares) public checkNoFreeProfit(caller) {
286297
if (!_vaultMayBeEmpty) vm.assume(IERC20(_vault_).totalSupply() > 0);
287298
vm.prank(caller); uint assets = vault_mint(shares, caller);
288299
vm.prank(caller); uint shares2 = vault_withdraw(assets, caller, caller);
@@ -292,15 +303,15 @@ abstract contract ERC4626Prop is Test {
292303
// a = mint(s)
293304
// a' = redeem(s)
294305
// a' <= a
295-
function prop_RT_mint_redeem(address caller, uint shares) public {
306+
function prop_RT_mint_redeem(address caller, uint shares) public checkNoFreeProfit(caller) {
296307
if (!_vaultMayBeEmpty) vm.assume(IERC20(_vault_).totalSupply() > 0);
297308
vm.prank(caller); uint assets1 = vault_mint(shares, caller);
298309
vm.prank(caller); uint assets2 = vault_redeem(shares, caller, caller);
299310
assertApproxLeAbs(assets2, assets1, _delta_);
300311
}
301312

302313
// mint(withdraw(a)) >= a
303-
function prop_RT_withdraw_mint(address caller, uint assets) public {
314+
function prop_RT_withdraw_mint(address caller, uint assets) public checkNoFreeProfit(caller) {
304315
vm.prank(caller); uint shares = vault_withdraw(assets, caller, caller);
305316
if (!_vaultMayBeEmpty) vm.assume(IERC20(_vault_).totalSupply() > 0);
306317
vm.prank(caller); uint assets2 = vault_mint(shares, caller);
@@ -310,7 +321,7 @@ abstract contract ERC4626Prop is Test {
310321
// s = withdraw(a)
311322
// s' = deposit(a)
312323
// s' <= s
313-
function prop_RT_withdraw_deposit(address caller, uint assets) public {
324+
function prop_RT_withdraw_deposit(address caller, uint assets) public checkNoFreeProfit(caller) {
314325
vm.prank(caller); uint shares1 = vault_withdraw(assets, caller, caller);
315326
if (!_vaultMayBeEmpty) vm.assume(IERC20(_vault_).totalSupply() > 0);
316327
vm.prank(caller); uint shares2 = vault_deposit(assets, caller);

0 commit comments

Comments
 (0)