Skip to content

Commit 4ac3de6

Browse files
mihailo-maksamihailo-maksa
committed
update asset and share solvency for triples, add triple lifecylce invariant assertions
1 parent 794e681 commit 4ac3de6

File tree

5 files changed

+403
-15
lines changed

5 files changed

+403
-15
lines changed

‎test/invariant/EthMultiVaultBasicInvariant.t.sol

Lines changed: 11 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -24,10 +24,13 @@ contract EthMultiVaultBasicInvariantTest is InvariantEthMultiVaultBase {
2424
targetContract(address(actor));
2525

2626
// selectors for actor functions
27-
bytes4[] memory selectors = new bytes4[](3);
27+
bytes4[] memory selectors = new bytes4[](6);
2828
selectors[0] = actor.createAtom.selector; // createAtom
2929
selectors[1] = actor.depositAtom.selector; // depositAtom
3030
selectors[2] = actor.redeemAtom.selector; // redeemAtom
31+
selectors[3] = actor.createTriple.selector; // createTriple
32+
selectors[4] = actor.depositTriple.selector; // depositTriple
33+
selectors[5] = actor.redeemTriple.selector; // redeemTriple
3134

3235
FuzzSelector memory fuzzSelector = FuzzSelector({addr: address(actor), selectors: selectors});
3336

@@ -39,11 +42,15 @@ contract EthMultiVaultBasicInvariantTest is InvariantEthMultiVaultBase {
3942
// assets less than or equal to eth balance
4043
invariant_ethMultiVault_asset_solvency();
4144
// shares less than or equal to assets
42-
//invariant_ethMultiVault_share_solvency();
45+
invariant_ethMultiVault_share_solvency();
46+
4347
emit log_named_uint("actor.numberOfCalls()---", actor.numberOfCalls());
4448
emit log_named_uint("actor.numberOfAtoms()---", actor.numberOfAtoms());
45-
emit log_named_uint("actor.numberOfDeposits()", actor.numberOfDeposits());
46-
emit log_named_uint("actor.numberOfRedeems()-", actor.numberOfRedeems());
49+
emit log_named_uint("actor.numberOfAtomDeposits()", actor.numberOfAtomDeposits());
50+
emit log_named_uint("actor.numberOfAtomRedeems()-", actor.numberOfAtomRedeems());
51+
emit log_named_uint("actor.numberOfTriples()---", actor.numberOfTriples());
52+
emit log_named_uint("actor.numberOfTripleDeposits()", actor.numberOfTripleDeposits());
53+
emit log_named_uint("actor.numberOfTripleRedeems()", actor.numberOfTripleRedeems());
4754
emit log_named_uint("ETHMULTIVAULT ETH BALANCE---", address(ethMultiVault).balance);
4855
}
4956
}

‎test/invariant/EthMultiVaultSingleVaultInvariant.t.sol

Lines changed: 10 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -27,9 +27,11 @@ contract EthMultiVaultSingleVaultInvariantTest is InvariantEthMultiVaultBase {
2727
targetContract(address(actor));
2828

2929
// selectors for actor functions
30-
bytes4[] memory selectors = new bytes4[](2);
30+
bytes4[] memory selectors = new bytes4[](4);
3131
selectors[0] = actor.depositAtom.selector; // depositAtom
3232
selectors[1] = actor.redeemAtom.selector; // redeemAtom
33+
selectors[2] = actor.depositTriple.selector; // depositTriple
34+
selectors[3] = actor.redeemTriple.selector; // redeemTriple
3335

3436
FuzzSelector memory fuzzSelector = FuzzSelector({addr: address(actor), selectors: selectors});
3537

@@ -40,9 +42,14 @@ contract EthMultiVaultSingleVaultInvariantTest is InvariantEthMultiVaultBase {
4042
function invariant_ethMultiVault_single() external {
4143
// assets less than or equal to eth balance
4244
invariant_ethMultiVault_asset_solvency();
45+
// shares less than or equal to assets
46+
invariant_ethMultiVault_share_solvency();
47+
4348
emit log_named_uint("actor.numberOfCalls()---", actor.numberOfCalls());
44-
emit log_named_uint("actor.numberOfDeposits()", actor.numberOfDeposits());
45-
emit log_named_uint("actor.numberOfRedeems()-", actor.numberOfRedeems());
49+
emit log_named_uint("actor.numberOfAtomDeposits()", actor.numberOfAtomDeposits());
50+
emit log_named_uint("actor.numberOfAtomRedeems()-", actor.numberOfAtomRedeems());
51+
emit log_named_uint("actor.numberOfTripleDeposits()", actor.numberOfTripleDeposits());
52+
emit log_named_uint("actor.numberOfTripleRedeems()", actor.numberOfTripleRedeems());
4653
emit log_named_uint("EthMultiVAULT ETH BALANCE---", address(ethMultiVault).balance);
4754
}
4855
}

‎test/invariant/InvariantEthMultiVaultBase.sol

Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -18,12 +18,32 @@ contract InvariantEthMultiVaultBase is EthMultiVaultBase {
1818
for (uint256 i = 1; i <= ethMultiVault.count(); i++) {
1919
totalAssetsAcrossAllVaults += super.vaultTotalAssets(i);
2020
}
21+
22+
uint256 totalAssetsAcrossAllCounterTripleVaults;
23+
uint256 counterTripleId = type(uint256).max - 1;
24+
for (uint256 i = 1; i <= ethMultiVault.count(); i++) {
25+
if (ethMultiVault.isTripleId(i)) {
26+
totalAssetsAcrossAllCounterTripleVaults += super.vaultTotalAssets(counterTripleId);
27+
counterTripleId--;
28+
}
29+
}
30+
31+
totalAssetsAcrossAllVaults += totalAssetsAcrossAllCounterTripleVaults;
32+
2133
assertLe(totalAssetsAcrossAllVaults, address(ethMultiVault).balance);
2234
}
2335

2436
function invariant_ethMultiVault_share_solvency() internal view {
2537
for (uint256 i = 1; i <= ethMultiVault.count(); i++) {
2638
assertLe(super.vaultTotalShares(i), super.vaultTotalAssets(i));
2739
}
40+
41+
uint256 counterTripleId = type(uint256).max;
42+
for (uint256 i = 1; i <= ethMultiVault.count(); i++) {
43+
if (ethMultiVault.isTripleId(i)) {
44+
assertLe(super.vaultTotalShares(counterTripleId), super.vaultTotalAssets(counterTripleId));
45+
counterTripleId--;
46+
}
47+
}
2848
}
2949
}

‎test/invariant/actors/EthMultiVaultActor.sol

Lines changed: 236 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -18,8 +18,11 @@ contract EthMultiVaultActor is Test, EthMultiVaultHelpers {
1818
// ghost variables
1919
uint256 public numberOfCalls;
2020
uint256 public numberOfAtoms;
21-
uint256 public numberOfDeposits;
22-
uint256 public numberOfRedeems;
21+
uint256 public numberOfAtomDeposits;
22+
uint256 public numberOfAtomRedeems;
23+
uint256 public numberOfTriples;
24+
uint256 public numberOfTripleDeposits;
25+
uint256 public numberOfTripleRedeems;
2326

2427
modifier useActor(uint256 actorIndexSeed) {
2528
currentActor = actors[bound(actorIndexSeed, 0, actors.length - 1)];
@@ -124,7 +127,7 @@ contract EthMultiVaultActor is Test, EthMultiVaultHelpers {
124127
uint256 actorIndexSeed
125128
) public useActor(actorIndexSeed) returns (uint256) {
126129
numberOfCalls++;
127-
numberOfDeposits++;
130+
numberOfAtomDeposits++;
128131
emit log_named_uint(
129132
"==================================== ACTOR depositAtom ====================================", 6000000009
130133
);
@@ -210,7 +213,7 @@ contract EthMultiVaultActor is Test, EthMultiVaultHelpers {
210213
uint256 actorIndexSeed
211214
) public useActor(actorIndexSeed) returns (uint256) {
212215
numberOfCalls++;
213-
numberOfRedeems++;
216+
numberOfAtomRedeems++;
214217
emit log_named_uint(
215218
"==================================== ACTOR redeemAtom START ====================================",
216219
6000000009
@@ -287,5 +290,234 @@ contract EthMultiVaultActor is Test, EthMultiVaultHelpers {
287290
return assetsForReceiver;
288291
}
289292

293+
function createTriple(
294+
uint256 _subjectId,
295+
uint256 _predicateId,
296+
uint256 _objectId,
297+
uint256 msgValue,
298+
uint256 actorIndexSeed
299+
) public useActor(actorIndexSeed) returns (uint256) {
300+
numberOfCalls++;
301+
numberOfTriples++;
302+
emit log_named_uint(
303+
"==================================== ACTOR createTriple START ====================================",
304+
6000000009
305+
);
306+
emit log_named_address("currentActor-----", currentActor);
307+
emit log_named_uint("currentActor.balance", currentActor.balance);
308+
emit log_named_uint("msgValue------------", msgValue);
309+
if (currentActor.balance < getAtomCost()) {
310+
vm.deal(currentActor, 1 ether);
311+
}
312+
if (msgValue < getAtomCost()) {
313+
msgValue = getAtomCost();
314+
}
315+
if (msgValue > currentActor.balance) {
316+
if (msgValue > 1 ether) {
317+
vm.deal(currentActor, 1 ether);
318+
msgValue = 1 ether;
319+
} else {
320+
vm.deal(currentActor, msgValue);
321+
}
322+
}
323+
emit log_named_uint("msg.sender.balance Right before create", currentActor.balance);
324+
emit log_named_address("msg.sender-----", currentActor);
325+
326+
uint256 totalAssetsBefore = vaultTotalAssets(ethMultiVault.count() + 1);
327+
uint256 totalSharesBefore = vaultTotalShares(ethMultiVault.count() + 1);
328+
329+
uint256 protocolVaultBalanceBefore = address(getProtocolVault()).balance;
330+
331+
// create atom
332+
uint256 id = actEthMultiVault.createTriple{value: msgValue}(_subjectId, _predicateId, _objectId);
333+
assertEq(id, actEthMultiVault.count());
334+
335+
checkDepositOnAtomVaultCreation(id, msgValue, totalAssetsBefore, totalSharesBefore);
336+
337+
uint256 userDeposit = msgValue - getAtomCost();
338+
339+
checkProtocolVaultBalanceOnVaultCreation(id, userDeposit, protocolVaultBalanceBefore);
340+
341+
// logs
342+
emit log_named_uint(
343+
"------------------------------------ POST STATE ------------------------------------------", 6000000009
344+
);
345+
emit log_named_uint("msg.sender.balance", currentActor.balance);
346+
emit log_named_uint("vaultTotalShares--", getVaultTotalAssets(id));
347+
emit log_named_uint("vaultTAssets------", getVaultTotalShares(id));
348+
emit log_named_uint(
349+
"==================================== ACTOR createTriple END ====================================", id
350+
);
351+
return id;
352+
}
353+
354+
function depositTriple(address _receiver, uint256 _vaultId, uint256 msgValue, uint256 actorIndexSeed)
355+
public
356+
useActor(actorIndexSeed)
357+
returns (uint256)
358+
{
359+
numberOfCalls++;
360+
numberOfTripleDeposits++;
361+
emit log_named_uint(
362+
"==================================== ACTOR depositTriple ====================================", 6000000009
363+
);
364+
emit log_named_address("currentActor-----", currentActor);
365+
emit log_named_uint("currentActor.balance", currentActor.balance);
366+
emit log_named_uint("msgValue------------", msgValue);
367+
// bound _receiver to msg.sender always
368+
_receiver = currentActor;
369+
uint256 shares;
370+
// if no atom exist yet, create and deposit on one
371+
if (actEthMultiVault.count() == 0) {
372+
vm.deal(currentActor, getAtomCost());
373+
_vaultId = actEthMultiVault.createTriple{value: getAtomCost()}(1, 2, 3);
374+
emit log_named_uint("vaultTotalAssets----", getVaultTotalShares(_vaultId));
375+
emit log_named_uint("vaultTotalShares----", getVaultTotalAssets(_vaultId));
376+
emit log_named_uint("vaultBalanceOf------", getVaultBalanceForAddress(_vaultId, currentActor));
377+
msgValue = bound(msgValue, getMinDeposit(), 10 ether);
378+
vm.deal(currentActor, msgValue);
379+
emit log_named_uint("|||||||||||||||||||||||||||||||||||BRANCH 1|||||||||||||||||||||||||||||||||||", 1);
380+
381+
uint256 totalAssetsBefore = vaultTotalAssets(_vaultId);
382+
uint256 totalSharesBefore = vaultTotalShares(_vaultId);
383+
384+
uint256 protocolVaultBalanceBefore = address(getProtocolVault()).balance;
385+
386+
shares = actEthMultiVault.depositTriple{value: msgValue}(_receiver, _vaultId);
387+
388+
checkDepositIntoVault(
389+
msgValue - getProtocolFeeAmount(msgValue, _vaultId), _vaultId, totalAssetsBefore, totalSharesBefore
390+
);
391+
392+
checkProtocolVaultBalance(_vaultId, msgValue, protocolVaultBalanceBefore);
393+
} else {
394+
// deposit on existing vault
395+
// bound _vaultId between 1 and count()
396+
if (_vaultId == 0 || _vaultId > actEthMultiVault.count()) {
397+
_vaultId = bound(_vaultId, 1, actEthMultiVault.count());
398+
}
399+
emit log_named_uint("vaultTotalAssets----", getVaultTotalShares(_vaultId));
400+
emit log_named_uint("vaultTotalShares----", getVaultTotalAssets(_vaultId));
401+
emit log_named_uint("vaultBalanceOf------", getVaultBalanceForAddress(_vaultId, currentActor));
402+
// bound msgValue to between minDeposit and 10 ether
403+
msgValue = bound(msgValue, getAtomCost(), 10 ether);
404+
vm.deal(currentActor, msgValue);
405+
emit log_named_uint("|||||||||||||||||||||||||||||||||||BRANCH 2|||||||||||||||||||||||||||||||||||", 2);
406+
407+
uint256 totalAssetsBefore = vaultTotalAssets(_vaultId);
408+
uint256 totalSharesBefore = vaultTotalShares(_vaultId);
409+
410+
uint256 protocolVaultBalanceBefore = address(getProtocolVault()).balance;
411+
412+
shares = actEthMultiVault.depositTriple{value: msgValue}(_receiver, _vaultId);
413+
414+
checkDepositIntoVault(
415+
msgValue - getProtocolFeeAmount(msgValue, _vaultId), _vaultId, totalAssetsBefore, totalSharesBefore
416+
);
417+
418+
checkProtocolVaultBalance(_vaultId, msgValue, protocolVaultBalanceBefore);
419+
}
420+
// deposit triple
421+
emit log_named_uint("balance currentActor", currentActor.balance);
422+
emit log_named_uint("balance EthMultiVaultbal-", address(actEthMultiVault).balance);
423+
emit log_named_uint("balance this--------", address(this).balance);
424+
// logs
425+
emit log_named_uint(
426+
"------------------------------------ POST STATE -------------------------------------------", 6000000009
427+
);
428+
emit log_named_uint("vaultTotalShares----", getVaultTotalAssets(_vaultId));
429+
emit log_named_uint("vaultTAssets--------", getVaultTotalShares(_vaultId));
430+
emit log_named_uint("vaultBalanceOf------", getVaultBalanceForAddress(_vaultId, currentActor));
431+
emit log_named_uint(
432+
"==================================== ACTOR depositTriple ====================================", shares
433+
);
434+
return shares;
435+
}
436+
437+
function redeemTriple(
438+
uint256 _shares2Redeem,
439+
address _receiver,
440+
uint256 _vaultId,
441+
uint256 msgValue,
442+
uint256 actorIndexSeed
443+
) public useActor(actorIndexSeed) returns (uint256) {
444+
numberOfCalls++;
445+
numberOfTripleRedeems++;
446+
emit log_named_uint(
447+
"==================================== ACTOR redeemTriple START ====================================",
448+
6000000009
449+
);
450+
emit log_named_address("currentActor-----", currentActor);
451+
emit log_named_uint("currentActor.balance", currentActor.balance);
452+
emit log_named_uint("msgValue------------", msgValue);
453+
// if no atom vaults exist create one and deposit on it
454+
if (actEthMultiVault.count() == 0) {
455+
vm.deal(currentActor, getAtomCost());
456+
_vaultId = actEthMultiVault.createTriple{value: getAtomCost()}(1, 2, 3);
457+
msgValue = bound(msgValue, getMinDeposit(), 10 ether);
458+
vm.deal(currentActor, msgValue);
459+
emit log_named_uint("|||||||||||||||||||||||||||||||||||BRANCH 1|||||||||||||||||||||||||||||||||||", 1);
460+
_shares2Redeem = actEthMultiVault.depositTriple{value: msgValue}(currentActor, 1);
461+
} else {
462+
// vault exists
463+
// bound _vaultId between 1 and count()
464+
if (_vaultId == 0 || _vaultId > actEthMultiVault.count()) {
465+
_vaultId = bound(_vaultId, 1, actEthMultiVault.count());
466+
}
467+
// if vault balance of the selected vault is 0, deposit minDeposit
468+
if (getVaultBalanceForAddress(_vaultId, currentActor) == 0) {
469+
vm.deal(currentActor, 10 ether);
470+
emit log_named_uint("vaultTShares--", getVaultTotalAssets(_vaultId));
471+
emit log_named_uint("vaultTAssets--", getVaultTotalShares(_vaultId));
472+
emit log_named_uint("vaultBalanceOf", getVaultBalanceForAddress(_vaultId, currentActor));
473+
msgValue = bound(msgValue, getAtomCost(), 10 ether);
474+
emit log_named_uint("REEEE getVaultTotalAssets(_vaultId)", getVaultTotalAssets(_vaultId));
475+
emit log_named_uint("REEEE getVaultTotalShares(_vaultId)", getVaultTotalShares(_vaultId));
476+
emit log_named_uint("|||||||||||||||||||||||||||||||BRANCH 2||||||||||||||||||||||||||||||||||||", 2);
477+
_shares2Redeem = actEthMultiVault.depositTriple{value: msgValue}(currentActor, _vaultId);
478+
emit log_named_uint("_shares2Redeem", _shares2Redeem);
479+
} else {
480+
emit log_named_uint("|||||||||||||||||||||||||||||||BRANCH 3||||||||||||||||||||||||||||||||||||", 3);
481+
// bound _shares2Redeem to between 1 and vaultBalanceOf
482+
_shares2Redeem = bound(_shares2Redeem, 1, getVaultBalanceForAddress(_vaultId, currentActor));
483+
emit log_named_uint("_shares2Redeem", _shares2Redeem);
484+
}
485+
}
486+
// use the redeemer as the receiver always
487+
_receiver = currentActor;
488+
489+
emit log_named_uint("before vaultTotalShares--", getVaultTotalAssets(_vaultId));
490+
emit log_named_uint("before vaultTAssets------", getVaultTotalShares(_vaultId));
491+
emit log_named_uint("before vaultBalanceOf----", getVaultBalanceForAddress(_vaultId, currentActor));
492+
493+
// snapshots before redeem
494+
uint256 protocolVaultBalanceBefore = address(getProtocolVault()).balance;
495+
uint256 userSharesBeforeRedeem = getSharesInVault(_vaultId, _receiver);
496+
uint256 userBalanceBeforeRedeem = address(_receiver).balance;
497+
498+
uint256 assetsForReceiverBeforeFees = getAssetsForReceiverBeforeFees(userSharesBeforeRedeem, _vaultId);
499+
500+
// redeem atom
501+
uint256 assetsForReceiver = actEthMultiVault.redeemTriple(_shares2Redeem, _receiver, _vaultId);
502+
503+
checkProtocolVaultBalance(_vaultId, assetsForReceiverBeforeFees, protocolVaultBalanceBefore);
504+
505+
assertEq(getSharesInVault(_vaultId, _receiver), userSharesBeforeRedeem - _shares2Redeem);
506+
assertEq(address(_receiver).balance - userBalanceBeforeRedeem, assetsForReceiver);
507+
508+
// logs
509+
emit log_named_uint(
510+
"------------------------------------ POST STATE -------------------------------------------", 6000000009
511+
);
512+
emit log_named_uint("vaultTotalShares--", getVaultTotalAssets(_vaultId));
513+
emit log_named_uint("vaultTAssets------", getVaultTotalShares(_vaultId));
514+
emit log_named_uint("vaultBalanceOf----", getVaultBalanceForAddress(_vaultId, currentActor));
515+
emit log_named_uint(
516+
"==================================== ACTOR redeemTriple END ====================================",
517+
assetsForReceiver
518+
);
519+
return assetsForReceiver;
520+
}
521+
290522
receive() external payable {}
291523
}

0 commit comments

Comments
 (0)