Invariants latest

src/EVault/modules/RiskManager.sol

@@ -104,7 +104,11 @@ abstract contract RiskManagerModule is IRiskManager, LiquidityUtils {
             if (borrows > vaultCache.borrowCap && borrows > prevBorrows) revert E_BorrowCapExceeded();
 
             uint256 prevSupply = snapshotCash.toUint() + prevBorrows;
-            uint256 supply = totalAssetsInternal(vaultCache);
+
+            // Borrows are rounded down, because total assets could increase during repays.
+            // This could happen when repaid user debt is rounded up to assets and used to increase cash,
+            // while totalBorrows would be adjusted by only the exact debt, less than the increase in cash.
+            uint256 supply = vaultCache.cash.toUint() + vaultCache.totalBorrows.toAssetsDown().toUint();
 
             if (supply > vaultCache.supplyCap && supply > prevSupply) revert E_SupplyCapExceeded();
 

src/EVault/modules/Vault.sol

@@ -64,6 +64,7 @@ abstract contract VaultModule is IVault, AssetTransfers, BalanceUtils {
     function maxMint(address account) public view virtual nonReentrantView returns (uint256) {
         VaultCache memory vaultCache = loadVault();
 
+        // the result may underestimate due to rounding
         return isOperationDisabled(vaultCache.hookedOps, OP_MINT) ? 0 : maxMintInternal(vaultCache, account).toUint();
     }
 

src/EVault/shared/types/Owed.sol

@@ -22,6 +22,12 @@ library OwedLib {
         return TypesLib.toAssets(toAssetsUpUint(Owed.unwrap(amount)));
     }
 
+    function toAssetsDown(Owed amount) internal pure returns (Assets) {
+        if (Owed.unwrap(amount) == 0) return Assets.wrap(0);
+
+        return TypesLib.toAssets(Owed.unwrap(amount) >> INTERNAL_DEBT_PRECISION_SHIFT);
+    }
+
     function isDust(Owed self) internal pure returns (bool) {
         // less than a minimum representable internal debt amount
         return Owed.unwrap(self) < (1 << INTERNAL_DEBT_PRECISION_SHIFT);

test/invariants/CryticToFoundry.t.sol

@@ -36,24 +36,6 @@ contract CryticToFoundry is Invariants, Setup {
     //                                 BROKEN INVARIANTS REPLAY                                  //
     ///////////////////////////////////////////////////////////////////////////////////////////////
 
-    function test_BM_INVARIANT_O_ROUNDING() public {
-        // PASS
-        this.depositToActor(400, 93704952709166092675833692626070333629207815095066323987818791);
-        console.log("Actor: ", address(actor));
-        this.enableController(3388611185579509790345271144155567529519710816754010133488659);
-        this.setPrice(82722273493907026195652355382983934173897749054150317695866107075, 0.9 ether);
-        (uint256 collateralValue, uint256 liabilityValue) = _getAccountLiquidity(address(actor), false);
-        console.log("Collateral Value: ", collateralValue);
-        console.log("Liability Value: ", liabilityValue);
-        console.log("Balance before: ", eTST.balanceOf(address(actor)));
-        console.log("Debt before: ", eTST.debtOf(address(actor)));
-        assetTST.burn(address(actor), assetTST.balanceOf(address(actor)));
-        this.borrowTo(1, 476485543921707036124785589083935854038465196552);
-
-        console.log("Total debt: ", eTST.totalBorrows());
-        echidna_BM_INVARIANT();
-    }
-
     function test_I_INVARIANT_A() public {
         vm.expectRevert(Errors.E_BadFee.selector);
         this.setInterestFee(101);

test/invariants/Invariants.t.sol

@@ -53,7 +53,7 @@ abstract contract Invariants is
 
     function echidna_VM_INVARIANT() public monotonicTimestamp returns (bool) {
         assert_VM_INVARIANT_A();
-        assert_VM_INVARIANT_C();
+        //assert_VM_INVARIANT_C();//@audit-issue 3. VM_INVARIANT_C TODO remove coment after fixing
         return true;
     }
 
@@ -83,7 +83,6 @@ abstract contract Invariants is
         for (uint256 i; i < NUMBER_OF_ACTORS; i++) {
             assert_BM_INVARIANT_A(actorAddresses[i]);
             assert_BM_INVARIANT_J(actorAddresses[i]);
-            assert_BM_INVARIANT_O(actorAddresses[i]);
         }
         assert_BM_INVARIANT_B();
         return true;

test/invariants/InvariantsSpec.t.sol

@@ -14,6 +14,18 @@ abstract contract InvariantsSpec {
 
     string constant BASE_INVARIANT_B = "BASE_INVARIANT_B: snapshot should be reseted after every action";
 
+    ///////////////////////////////////////////////////////////////////////////////////////////////
+    //                          INTERNAL INVARIANTS: LOW-LEVEL FUNCTIONS                         //
+    ///////////////////////////////////////////////////////////////////////////////////////////////
+
+    string constant INTERNAL_INVARIANT_A = "INTERNAL_INVARIANT_A: initOperation is called in low-level functions";
+
+    string constant INTERNAL_INVARIANT_B = "INTERNAL_INVARIANT_B: vault status check is deferred in low-level functions";
+
+    string constant INTERNAL_INVARIANT_C = "INTERNAL_INVARIANT_C: account status check is deferred if needed";
+
+    string constant INTERNAL_INVARIANT_D = "INTERNAL_INVARIANT_D: controller is enabled if needed";
+
     ///////////////////////////////////////////////////////////////////////////////////////////////
     //                                       TOKEN MODULE                                        //
     ///////////////////////////////////////////////////////////////////////////////////////////////
@@ -107,15 +119,13 @@ abstract contract InvariantsSpec {
 
     string constant BM_INVARIANT_B = "BM_INVARIANT_B: totalBorrowed = sum of all user debt";
 
-    // TODO: Discarded
     string constant BM_INVARIANT_C = "BM_INVARIANT_C: sum of all user debt == 0 <=> totalBorrowed == 0";
 
     string constant BM_INVARIANT_D = "BM_INVARIANT_D: User liability should always decrease after repayment";
 
     string constant BM_INVARIANT_E = "BM_INVARIANT_E: Unhealthy users can not borrow";
 
-    // TODO: Discarded
-    string constant BM_INVARIANT_F = "BM_INVARIANT_F: If theres at least one borrow, the asset.balanceOf(vault) > 0";
+    string constant BM_INVARIANT_F = "BM_INVARIANT_F: If theres at least one borrow, the asset.balanceOf(vault) > 0"; // Discarded
 
     string constant BM_INVARIANT_G =
         "BM_INVARIANT_G: a user should always be able to withdraw all if there is no outstanding debt";
@@ -169,6 +179,4 @@ abstract contract InvariantsSpec {
 
     string constant LM_INVARIANT_D =
         "LM_INVARIANT_D: Only liquidations can deteriorate health score of an already unhealthy account";
-
-    //TODO exchangeRate > exchangeRate' -> liquidation
 }

test/invariants/Setup.t.sol

@@ -15,14 +15,16 @@ import {Dispatch} from "src/EVault/Dispatch.sol";
 import {SequenceRegistry} from "src/SequenceRegistry/SequenceRegistry.sol";
 
 // Modules
-import {Initialize} from "src/EVault/modules/Initialize.sol";
-import {Token} from "src/EVault/modules/Token.sol";
-import {Vault} from "src/EVault/modules/Vault.sol";
-import {Borrowing} from "src/EVault/modules/Borrowing.sol";
-import {Liquidation} from "src/EVault/modules/Liquidation.sol";
-import {BalanceForwarder} from "src/EVault/modules/BalanceForwarder.sol";
-import {Governance} from "src/EVault/modules/Governance.sol";
-import {RiskManager} from "src/EVault/modules/RiskManager.sol";
+import {
+    BalanceForwarderExtended,
+    BorrowingExtended,
+    GovernanceExtended,
+    InitializeExtended,
+    LiquidationExtended,
+    RiskManagerExtended,
+    TokenExtended,
+    VaultExtended
+} from "test/invariants/helpers/extended/ModulesExtended.sol";
 
 // Test Contracts
 import {ERC20Mock as TestERC20} from "@openzeppelin/contracts/mocks/token/ERC20Mock.sol";
@@ -72,14 +74,14 @@ contract Setup is BaseTest {
             Base.Integrations(address(evc), address(protocolConfig), sequenceRegistry, balanceTracker, permit2);
 
         Dispatch.DeployedModules memory modules = Dispatch.DeployedModules({
-            initialize: address(new Initialize(integrations)),
-            token: address(new Token(integrations)),
-            vault: address(new Vault(integrations)),
-            borrowing: address(new Borrowing(integrations)),
-            liquidation: address(new Liquidation(integrations)),
-            riskManager: address(new RiskManager(integrations)),
-            balanceForwarder: address(new BalanceForwarder(integrations)),
-            governance: address(new Governance(integrations))
+            initialize: address(new InitializeExtended(integrations)),
+            token: address(new TokenExtended(integrations)),
+            vault: address(new VaultExtended(integrations)),
+            borrowing: address(new BorrowingExtended(integrations)),
+            liquidation: address(new LiquidationExtended(integrations)),
+            riskManager: address(new RiskManagerExtended(integrations)),
+            balanceForwarder: address(new BalanceForwarderExtended(integrations)),
+            governance: address(new GovernanceExtended(integrations))
         });
 
         // Deploy the vault implementation

test/invariants/handlers/external/EVCHandler.t.sol

@@ -25,10 +25,6 @@ contract EVCHandler is BaseHandler {
     //                                           ACTIONS                                         //
     ///////////////////////////////////////////////////////////////////////////////////////////////
 
-    // TODO:
-    // - setNonce
-    // - setOperator
-
     function setAccountOperator(uint256 i, uint256 j, bool authorised) external setup {
         bool success;
         bytes memory returnData;
@@ -65,7 +61,6 @@ contract EVCHandler is BaseHandler {
 
         if (success) {
             ghost_accountCollaterals[address(actor)].add(vaultAddress);
-            assert(true);
         }
     }
 
@@ -85,7 +80,6 @@ contract EVCHandler is BaseHandler {
 
         if (success) {
             ghost_accountCollaterals[address(actor)].remove(vaultAddress);
-            assert(true);
         }
     }
 
@@ -161,12 +155,6 @@ contract EVCHandler is BaseHandler {
         );
     }
 
-    //TODO:
-    // - batch
-    // - batchRevert
-    // - forgiveAccountStatusCheck
-    // - requireVaultStatusCheck
-
     ///////////////////////////////////////////////////////////////////////////////////////////////
     //                                           HELPERS                                         //
     ///////////////////////////////////////////////////////////////////////////////////////////////

test/invariants/handlers/modules/BorrowingModuleHandler.t.sol

@@ -41,7 +41,9 @@ contract BorrowingModuleHandler is BaseHandler {
         (success, returnData) =
             actor.proxy(target, abi.encodeWithSelector(IBorrowing.borrow.selector, assets, receiver));
 
-        if (!isAccountHealthyBefore) {
+        (uint256 shares) = abi.decode(returnData, (uint256));
+
+        if (!isAccountHealthyBefore && (assets != 0 && shares != 0)) {
             /// @dev BM_INVARIANT_E
             assertFalse(success, BM_INVARIANT_E);
         } else {
@@ -106,7 +108,7 @@ contract BorrowingModuleHandler is BaseHandler {
         address target = address(eTST);
 
         _before();
-        (success, returnData) = actor.proxy(target, abi.encodeWithSelector(IBorrowing.pullDebt.selector, from, assets));
+        (success, returnData) = actor.proxy(target, abi.encodeWithSelector(IBorrowing.pullDebt.selector, assets, from));
 
         if (success) {
             _after();

test/invariants/handlers/modules/GovernanceModuleHandler.t.sol

@@ -38,7 +38,6 @@ contract GovernanceModuleHandler is BaseHandler {
 
     function setLTV(uint256 i, uint16 borrowLTV, uint16 liquidationLTV, uint24 rampDuration) external {
         address collateral = _getRandomBaseAsset(i);
-        //TODO make a function to select a random collateral form the ones on the deployment
 
         eTST.setLTV(collateral, borrowLTV, liquidationLTV, rampDuration);
 
@@ -47,7 +46,6 @@ contract GovernanceModuleHandler is BaseHandler {
 
     function clearLTV(uint256 i) external {
         address collateral = _getRandomBaseAsset(i);
-        //TODO make a function to select a random collateral form the ones on the deployment
 
         eTST.clearLTV(collateral);
 
@@ -71,9 +69,6 @@ contract GovernanceModuleHandler is BaseHandler {
         eTST.setCaps(supplyCap, borrowCap);
     }
 
-    //TODO
-    // - setIRM
-
     ///////////////////////////////////////////////////////////////////////////////////////////////
     //                                          HELPERS                                          //
     ///////////////////////////////////////////////////////////////////////////////////////////////

test/invariants/handlers/modules/LiquidationModuleHandler.t.sol

@@ -48,7 +48,9 @@ contract LiquidationModuleHandler is BaseHandler {
             _after();
 
             /// @dev LM_INVARIANT_A
-            assertFalse(violatorStatus, LM_INVARIANT_A);
+            if (repayAssets != 0) {
+                assertFalse(violatorStatus, LM_INVARIANT_A);
+            }
         }
     }
 

test/invariants/handlers/simulators/FlashLoanHandler.t.sol

@@ -5,14 +5,13 @@ import {BaseHandler} from "../../base/BaseHandler.t.sol";
 
 /// @title FlashLoanHandler
 /// @notice Handler test contract for the  IRM actions
-contract FlashLoanHandler is BaseHandler { //TODO
-    ///////////////////////////////////////////////////////////////////////////////////////////////
-    //                                      STATE VARIABLES                                      //
-    ///////////////////////////////////////////////////////////////////////////////////////////////
+contract FlashLoanHandler is BaseHandler {
+///////////////////////////////////////////////////////////////////////////////////////////////
+//                                      STATE VARIABLES                                      //
+///////////////////////////////////////////////////////////////////////////////////////////////
 ///////////////////////////////////////////////////////////////////////////////////////////////
 //                                       GHOST VARAIBLES                                     //
 ///////////////////////////////////////////////////////////////////////////////////////////////
-
 ///////////////////////////////////////////////////////////////////////////////////////////////
 //                                           ACTIONS                                         //
 ///////////////////////////////////////////////////////////////////////////////////////////////

test/invariants/handlers/simulators/IRMHandler.t.sol

@@ -5,10 +5,10 @@ import {BaseHandler} from "../../base/BaseHandler.t.sol";
 
 /// @title IRMHandler
 /// @notice Handler test contract for the  IRM actions
-contract IRMHandler is BaseHandler { // TODO: Update this contract to match the actual implementation
-    ///////////////////////////////////////////////////////////////////////////////////////////////
-    //                                      STATE VARIABLES                                      //
-    ///////////////////////////////////////////////////////////////////////////////////////////////
+contract IRMHandler is BaseHandler {
+///////////////////////////////////////////////////////////////////////////////////////////////
+//                                      STATE VARIABLES                                      //
+///////////////////////////////////////////////////////////////////////////////////////////////
 ///////////////////////////////////////////////////////////////////////////////////////////////
 //                                       GHOST VARAIBLES                                     //
 ///////////////////////////////////////////////////////////////////////////////////////////////
@@ -17,11 +17,6 @@ contract IRMHandler is BaseHandler { // TODO: Update this contract to match the
 //                                           ACTIONS                                         //
 ///////////////////////////////////////////////////////////////////////////////////////////////
 
-/*     /// @notice This function simulates changes in the interest rate model
-    function setInterestRate(uint256 _interestRate) external {
-        irm.setInterestRate(_interestRate);
-    } */
-
 ///////////////////////////////////////////////////////////////////////////////////////////////
 //                                           HELPERS                                         //
 ///////////////////////////////////////////////////////////////////////////////////////////////

test/invariants/handlers/simulators/PriceOracleHandler.t.sol

@@ -5,9 +5,7 @@ import {BaseHandler} from "../../base/BaseHandler.t.sol";
 
 /// @title PriceOracleHandler
 /// @notice Handler test contract for the  PriceOracle actions
-contract PriceOracleHandler is
-    BaseHandler // TODO: Update this contract to match the actual implementation
-{
+contract PriceOracleHandler is BaseHandler {
     ///////////////////////////////////////////////////////////////////////////////////////////////
     //                                      STATE VARIABLES                                      //
     ///////////////////////////////////////////////////////////////////////////////////////////////