Merge pull request #72 from 0xIntuition/mihailo/triple-invariant-asse…

…rtions Mihailo/triple invariant assertions
0xIntuition · May 27, 2024 · 68a46c4 · 68a46c4
2 parents c65bed1 + 0c36cd7
commit 68a46c4
Show file tree

Hide file tree

Showing 5 changed files with 640 additions and 123 deletions.
diff --git a/test/invariant/EthMultiVaultBasicInvariant.t.sol b/test/invariant/EthMultiVaultBasicInvariant.t.sol
@@ -24,10 +24,13 @@ contract EthMultiVaultBasicInvariantTest is InvariantEthMultiVaultBase {
         targetContract(address(actor));
 
         // selectors for actor functions
-        bytes4[] memory selectors = new bytes4[](3);
+        bytes4[] memory selectors = new bytes4[](6);
         selectors[0] = actor.createAtom.selector; // createAtom
         selectors[1] = actor.depositAtom.selector; // depositAtom
         selectors[2] = actor.redeemAtom.selector; // redeemAtom
+        selectors[3] = actor.createTriple.selector; // createTriple
+        selectors[4] = actor.depositTriple.selector; // depositTriple
+        selectors[5] = actor.redeemTriple.selector; // redeemTriple
 
         FuzzSelector memory fuzzSelector = FuzzSelector({addr: address(actor), selectors: selectors});
 
@@ -39,11 +42,15 @@ contract EthMultiVaultBasicInvariantTest is InvariantEthMultiVaultBase {
         // assets less than or equal to eth balance
         invariant_ethMultiVault_asset_solvency();
         // shares less than or equal to assets
-        //invariant_ethMultiVault_share_solvency();
+        invariant_ethMultiVault_share_solvency();
+
         emit log_named_uint("actor.numberOfCalls()---", actor.numberOfCalls());
         emit log_named_uint("actor.numberOfAtoms()---", actor.numberOfAtoms());
-        emit log_named_uint("actor.numberOfDeposits()", actor.numberOfDeposits());
-        emit log_named_uint("actor.numberOfRedeems()-", actor.numberOfRedeems());
+        emit log_named_uint("actor.numberOfAtomDeposits()", actor.numberOfAtomDeposits());
+        emit log_named_uint("actor.numberOfAtomRedeems()-", actor.numberOfAtomRedeems());
+        emit log_named_uint("actor.numberOfTriples()---", actor.numberOfTriples());
+        emit log_named_uint("actor.numberOfTripleDeposits()", actor.numberOfTripleDeposits());
+        emit log_named_uint("actor.numberOfTripleRedeems()", actor.numberOfTripleRedeems());
         emit log_named_uint("ETHMULTIVAULT ETH BALANCE---", address(ethMultiVault).balance);
     }
 }
diff --git a/test/invariant/EthMultiVaultSingleVaultInvariant.t.sol b/test/invariant/EthMultiVaultSingleVaultInvariant.t.sol
@@ -20,16 +20,25 @@ contract EthMultiVaultSingleVaultInvariantTest is InvariantEthMultiVaultBase {
         // create single vault
         ethMultiVault.createAtom{value: 100 ether}("PEPE");
 
+        // create 2 more atoms for the triple vault
+        ethMultiVault.createAtom{value: 100 ether}("WIF");
+        ethMultiVault.createAtom{value: 100 ether}("BASE");
+
+        // create triple vault
+        ethMultiVault.createTriple{value: 100 ether}(1, 2, 3);
+
         // deploy actor
         actor = new EthMultiVaultSingleVaultActor(ethMultiVault);
 
         // target actor
         targetContract(address(actor));
 
         // selectors for actor functions
-        bytes4[] memory selectors = new bytes4[](2);
+        bytes4[] memory selectors = new bytes4[](4);
         selectors[0] = actor.depositAtom.selector; // depositAtom
         selectors[1] = actor.redeemAtom.selector; // redeemAtom
+        selectors[2] = actor.depositTriple.selector; // depositTriple
+        selectors[3] = actor.redeemTriple.selector; // redeemTriple
 
         FuzzSelector memory fuzzSelector = FuzzSelector({addr: address(actor), selectors: selectors});
 
@@ -40,9 +49,14 @@ contract EthMultiVaultSingleVaultInvariantTest is InvariantEthMultiVaultBase {
     function invariant_ethMultiVault_single() external {
         // assets less than or equal to eth balance
         invariant_ethMultiVault_asset_solvency();
+        // shares less than or equal to assets
+        invariant_ethMultiVault_share_solvency();
+
         emit log_named_uint("actor.numberOfCalls()---", actor.numberOfCalls());
-        emit log_named_uint("actor.numberOfDeposits()", actor.numberOfDeposits());
-        emit log_named_uint("actor.numberOfRedeems()-", actor.numberOfRedeems());
+        emit log_named_uint("actor.numberOfAtomDeposits()", actor.numberOfAtomDeposits());
+        emit log_named_uint("actor.numberOfAtomRedeems()-", actor.numberOfAtomRedeems());
+        emit log_named_uint("actor.numberOfTripleDeposits()", actor.numberOfTripleDeposits());
+        emit log_named_uint("actor.numberOfTripleRedeems()", actor.numberOfTripleRedeems());
         emit log_named_uint("EthMultiVAULT ETH BALANCE---", address(ethMultiVault).balance);
     }
 }
diff --git a/test/invariant/InvariantEthMultiVaultBase.sol b/test/invariant/InvariantEthMultiVaultBase.sol
@@ -18,12 +18,32 @@ contract InvariantEthMultiVaultBase is EthMultiVaultBase {
         for (uint256 i = 1; i <= ethMultiVault.count(); i++) {
             totalAssetsAcrossAllVaults += super.vaultTotalAssets(i);
         }
+
+        uint256 totalAssetsAcrossAllCounterTripleVaults;
+        uint256 counterTripleId = type(uint256).max - 1;
+        for (uint256 i = 1; i <= ethMultiVault.count(); i++) {
+            if (ethMultiVault.isTripleId(i)) {
+                totalAssetsAcrossAllCounterTripleVaults += super.vaultTotalAssets(counterTripleId);
+                counterTripleId--;
+            }
+        }
+
+        totalAssetsAcrossAllVaults += totalAssetsAcrossAllCounterTripleVaults;
+
         assertLe(totalAssetsAcrossAllVaults, address(ethMultiVault).balance);
     }
 
     function invariant_ethMultiVault_share_solvency() internal view {
         for (uint256 i = 1; i <= ethMultiVault.count(); i++) {
             assertLe(super.vaultTotalShares(i), super.vaultTotalAssets(i));
         }
+
+        uint256 counterTripleId = type(uint256).max;
+        for (uint256 i = 1; i <= ethMultiVault.count(); i++) {
+            if (ethMultiVault.isTripleId(i)) {
+                assertLe(super.vaultTotalShares(counterTripleId), super.vaultTotalAssets(counterTripleId));
+                counterTripleId--;
+            }
+        }
     }
 }