Setup router invariants

test/recon-core/CryticToFoundry.sol

@@ -12,4 +12,38 @@ contract CryticToFoundry is Test, TargetFunctions, FoundryAsserts {
     function setUp() public {
         setup();
     }
+
+    function test_router_enableLockDepositRequest_0() public {
+        deployNewTokenPoolAndTranche(213, 1109922828198508092022258837037897407096367457572502626);
+        poolManager_updateMember(104682477517645628);
+
+        router_enableLockDepositRequest(1571671511039135344726490349044916145036336035487780128226482691235730529);
+        assertTrue(invariant_RE_1());
+        poolManager_updateTranchePrice(56901525302466059, 7840914769514120);
+        router_executeLockedDepositRequest();
+        assertTrue(invariant_RE_1());
+    }
+
+    // forge test --match-test test_erc7540_6_deposit_call_target_1 -vv
+    function test_erc7540_6_deposit_call_target_1() public {
+        deployNewTokenPoolAndTranche(233, 28269320542146199253579888502169902638602973317426694748705922998786179475);
+        poolManager_updateMember(104682477517645628);
+        poolManager_updateTranchePrice(56901525302466059, 7840914769514120);
+        vault_requestDeposit(31538029450636696910582306038649448464549600365089094367785921647207723207717);
+        investmentManager_fulfillDepositRequest(
+            237784553952399504434353056688092462338, 11272134262104, 8548248478501905158605391940158212738
+        );
+        poolManager_freeze();
+        erc7540_6_deposit_call_target(72);
+    }
+
+    // forge test --match-test test_invariant_E_1_0 -vv
+    function test_invariant_E_1_0() public {
+        deployNewTokenPoolAndTranche(81, 113078215817378582107422693752520426616851634649913195634947047953023656943);
+        poolManager_updateTranchePrice(9757554087961420227, 972056852255743695);
+        restrictionManager_updateMemberBasic(1240252875855011110);
+        router_enableLockDepositRequest(16948529030864767477943060538480731523813239832281896240408330105234726880);
+        router_executeLockedDepositRequest();
+        assertTrue(invariant_E_1());
+    }
 }

test/recon-core/ERC7540Properties.sol

@@ -91,7 +91,8 @@ abstract contract ERC7540Properties is Setup, Asserts {
             return true; // Needs to be greater than 0, skip
         }
 
-        try IERC7540Vault(erc7540Target).deposit(maxDep + amt, actor) {
+        try IERC7540Vault(erc7540Target).deposit(maxDep + amt, actor) returns (uint256 shares) {
+            if (shares == 0) return true;
             return false;
         } catch {
             // We want this to be hit
@@ -163,7 +164,8 @@ abstract contract ERC7540Properties is Setup, Asserts {
             return true; // Needs to be greater than 0
         }
 
-        try IERC7540Vault(erc7540Target).redeem(maxDep + amt, actor, actor) {
+        try IERC7540Vault(erc7540Target).redeem(maxDep + amt, actor, actor) returns (uint256 assets) {
+            if (assets == 0) return true;
             return false;
         } catch {
             // We want this to be hit

test/recon-core/Properties.sol

@@ -271,7 +271,7 @@ abstract contract Properties is Setup, Asserts, ERC7540CentrifugeProperties {
             /// @audit Minted by Asset Payouts by Investors
             == (
                 mintedByCurrencyPayout[address(token)] + sumOfDepositRequests[address(token)]
-                    + sumOfTransfersIn[address(token)]
+                    + sumOfTransfersIn[address(token)] + sumOfExecutedLockedDepositRequests[address(token)]
                 // Minus Claimed Redemptions and TransfersOut
                 - sumOfClaimedRedemptions[address(token)] - sumOfClaimedDepositCancelations[address(token)]
                     - sumOfTransfersOut[address(token)]
@@ -382,4 +382,55 @@ abstract contract Properties is Setup, Asserts, ERC7540CentrifugeProperties {
         emit DebugWithString("acc - balOfEscrow", balOfEscrow < acc ? acc - balOfEscrow : 0);
         return acc <= balOfEscrow; // Ensure bal of escrow is sufficient to fulfill requests
     }
+
+    // Router Escrow
+
+    /**
+     * The balance of currencies in RouterEscrow is
+     *     sum of locked deposit requests
+     *     minus sum of unlock deposit requests
+     *     minus sum of executed deposit requests
+     *
+     *     NOTE: Ignores donations
+     */
+    function invariant_RE_1() public returns (bool) {
+        if (address(routerEscrow) == address(0)) {
+            return true;
+        }
+        if (address(token) == address(0)) {
+            return true;
+        }
+
+        unchecked {
+            return token.balanceOf(address(routerEscrow))
+                == (
+                    sumOfLockedDepositRequests[address(token)] - sumOfUnlockedDepositRequests[address(token)]
+                        - sumOfExecutedLockedDepositRequests[address(token)]
+                );
+        }
+    }
+
+    // CentrifugeRouter
+
+    /**
+     * The sum of unlocked deposit requests must be less than the sum of locked deposit requests
+     */
+    function invariant_CR_1() public returns (bool) {
+        if (address(routerEscrow) == address(0)) {
+            return true;
+        }
+
+        return sumOfUnlockedDepositRequests[address(token)] <= sumOfLockedDepositRequests[address(token)];
+    }
+
+    /**
+     * The sum of executed deposit requests must be less than the sum of locked deposit requests
+     */
+    function invariant_CR_2() public returns (bool) {
+        if (address(routerEscrow) == address(0)) {
+            return true;
+        }
+
+        return sumOfExecutedLockedDepositRequests[address(token)] <= sumOfLockedDepositRequests[address(token)];
+    }
 }

test/recon-core/Setup.sol

@@ -8,6 +8,7 @@ import {PoolManager} from "src/PoolManager.sol";
 import {ERC7540Vault} from "src/ERC7540Vault.sol";
 import {Root} from "src/Root.sol";
 import {Tranche} from "src/token/Tranche.sol";
+import {CentrifugeRouter} from "src/CentrifugeRouter.sol";
 
 import {ERC7540VaultFactory} from "src/factories/ERC7540VaultFactory.sol";
 import {TrancheFactory} from "src/factories/TrancheFactory.sol";
@@ -28,8 +29,10 @@ abstract contract Setup is BaseSetup, SharedStorage {
 
     // Handled //
     Escrow public escrow; // NOTE: Restriction Manager will query it
+    Escrow public routerEscrow;
     InvestmentManager investmentManager;
     PoolManager poolManager;
+    CentrifugeRouter router;
 
     // TODO: CYCLE / Make it work for variable values
     ERC7540Vault vault;
@@ -59,17 +62,19 @@ abstract contract Setup is BaseSetup, SharedStorage {
         centrifugeChain = address(this);
 
         // Dependencies
-        vaultFactory = new ERC7540VaultFactory(address(this));
-        trancheFactory = new TrancheFactory(address(this), address(this));
         escrow = new Escrow(address(address(this)));
+        routerEscrow = new Escrow(address(address(this)));
         root = new Root(address(escrow), 48 hours, address(this));
+        vaultFactory = new ERC7540VaultFactory(address(root));
+        trancheFactory = new TrancheFactory(address(root), address(this));
         restrictionManager = new RestrictionManager(address(root), address(this));
 
-        root.endorse(address(escrow));
-
         poolManager = new PoolManager(address(escrow), address(vaultFactory), address(trancheFactory));
         poolManager.file("gateway", address(this));
 
+        // Setup router
+        router = new CentrifugeRouter(address(routerEscrow), address(this), address(poolManager));
+
         investmentManager = new InvestmentManager(address(root), address(escrow));
 
         investmentManager.file("gateway", address(this));
@@ -83,6 +88,10 @@ abstract contract Setup is BaseSetup, SharedStorage {
         // Setup Escrow Permissions
         escrow.rely(address(investmentManager));
         escrow.rely(address(poolManager));
+        routerEscrow.rely(address(router));
+
+        root.endorse(address(router));
+        root.endorse(address(escrow));
 
         // Permissions on factories
         vaultFactory.rely(address(poolManager));
@@ -151,4 +160,12 @@ abstract contract Setup is BaseSetup, SharedStorage {
 
         return (depositPrice, redeemPrice);
     }
+
+    /// @dev Get the balance of the current token and actor
+    function _getTokenAndBalanceForVault() internal view returns (uint256) {
+        // Token
+        uint256 amt = token.balanceOf(actor);
+
+        return amt;
+    }
 }

test/recon-core/SharedStorage.sol

@@ -32,7 +32,7 @@ abstract contract SharedStorage {
     // Should we also enforce the exact balance check on asset / shares?
     // TODO: This is broken rn
     // Liquidity Pool functions
-    bool RECON_EXACT_BAL_CHECK = false;
+    bool RECON_EXACT_BAL_CHECK = true;
 
     /// === INTERNAL COUNTERS === ///
     // Currency ID = Currency Length
@@ -178,4 +178,10 @@ abstract contract SharedStorage {
     // System will enter an inconsistent state
     mapping(address => mapping(address => uint256)) requestDepositAssets;
     mapping(address => mapping(address => uint256)) requestRedeemShares;
+
+    // === invariant_RE_1 === //
+    // Indexed by Currency
+    mapping(address => uint256) sumOfLockedDepositRequests;
+    mapping(address => uint256) sumOfUnlockedDepositRequests;
+    mapping(address => uint256) sumOfExecutedLockedDepositRequests;
 }

test/recon-core/TargetFunctions.sol

@@ -17,6 +17,7 @@ import {RestrictionManagerFunctions} from "./targets/RestrictionManagerFunctions
 import {VaultFunctions} from "./targets/VaultFunctions.sol";
 import {PoolManagerFunctions} from "./targets/PoolManagerFunctions.sol";
 import {VaultCallbacks} from "./targets/VaultCallbacks.sol";
+import {RouterFunctions} from "./targets/RouterFunctions.sol";
 
 abstract contract TargetFunctions is
     BaseTargetFunctions,
@@ -26,7 +27,8 @@ abstract contract TargetFunctions is
     RestrictionManagerFunctions,
     VaultFunctions,
     PoolManagerFunctions,
-    VaultCallbacks
+    VaultCallbacks,
+    RouterFunctions
 {
     /**
      * TODO: Port Over tranche, liquidity pool stuff

test/recon-core/targets/RouterFunctions.sol

@@ -0,0 +1,158 @@
+// SPDX-License-Identifier: AGPL-3.0-only
+pragma solidity 0.8.26;
+
+// Recon Deps
+import {BaseTargetFunctions} from "@chimera/BaseTargetFunctions.sol";
+import {Properties} from "../Properties.sol";
+import {vm} from "@chimera/Hevm.sol";
+
+// Dependencies
+import {ERC20} from "src/token/ERC20.sol";
+import {ERC7540Vault} from "src/ERC7540Vault.sol";
+
+/**
+ * A collection of handlers that interact with the Centrifuge Router
+ */
+abstract contract RouterFunctions is BaseTargetFunctions, Properties {
+    // === Enable lock deposit request === //
+    function router_enableLockDepositRequest(uint256 assets) public {
+        assets = between(assets, 0, _getTokenAndBalanceForVault());
+
+        token.approve(address(router), assets);
+
+        // B4 Balances
+        uint256 balanceB4 = token.balanceOf(actor);
+        uint256 balanceOfRouterEscrowB4 = token.balanceOf(address(routerEscrow));
+
+        bool hasReverted;
+        try router.enableLockDepositRequest(address(vault), assets) {
+            sumOfLockedDepositRequests[address(token)] += assets;
+        } catch {
+            hasReverted = true;
+        }
+
+        // After Balances and Checks
+        uint256 balanceAfter = token.balanceOf(actor);
+        uint256 balanceOfRouterEscrowAfter = token.balanceOf(address(routerEscrow));
+
+        // NOTE: We only enforce the check if the tx didn't revert
+        if (!hasReverted) {
+            // Extra check
+            // NOTE: Unchecked so we get broken property and debug faster
+            uint256 deltaUser = balanceB4 - balanceAfter;
+            uint256 deltaRouterEscrow = balanceOfRouterEscrowAfter - balanceOfRouterEscrowB4;
+
+            if (RECON_EXACT_BAL_CHECK) {
+                eq(deltaUser, assets, "Router-x");
+            }
+
+            eq(deltaUser, deltaRouterEscrow, "Router-x");
+        }
+    }
+
+    // === Lock deposit request === //
+    // TODO
+
+    // === Executed locked deposit request === //
+    function router_unlockDepositRequest() public {
+        uint256 balanceB4 = token.balanceOf(actor);
+        uint256 balanceOfRouterEscrowB4 = token.balanceOf(address(routerEscrow));
+        uint256 lockedRequestB4 = router.lockedRequests(actor, address(vault));
+
+        bool hasReverted;
+        try router.unlockDepositRequest(address(vault), actor) {
+            sumOfUnlockedDepositRequests[address(token)] += lockedRequestB4;
+        } catch {
+            hasReverted = true;
+        }
+
+        // After Balances and Checks
+        uint256 balanceAfter = token.balanceOf(actor);
+        uint256 balanceOfRouterEscrowAfter = token.balanceOf(address(routerEscrow));
+        uint256 lockedRequestAfter = router.lockedRequests(actor, address(vault));
+
+        // NOTE: We only enforce the check if the tx didn't revert
+        if (!hasReverted) {
+            uint256 deltaUser = balanceB4 - balanceAfter;
+            uint256 deltaRouterEscrow = balanceOfRouterEscrowAfter - balanceOfRouterEscrowB4;
+
+            if (RECON_EXACT_BAL_CHECK) {
+                eq(deltaUser, lockedRequestB4, "Router-x");
+            }
+
+            eq(deltaRouterEscrow, lockedRequestB4, "Router-x");
+            eq(lockedRequestAfter, 0, "Router-x");
+        }
+    }
+
+    // === Executed locked deposit request === //
+    function router_executeLockedDepositRequest() public {
+        uint256 balanceOfEscrowB4 = token.balanceOf(address(escrow));
+        uint256 balanceOfRouterEscrowB4 = token.balanceOf(address(routerEscrow));
+        uint256 lockedRequestB4 = router.lockedRequests(actor, address(vault));
+
+        bool hasReverted;
+        try router.executeLockedDepositRequest(address(vault), actor, 0) {
+            sumOfExecutedLockedDepositRequests[address(token)] += lockedRequestB4;
+        } catch {
+            hasReverted = true;
+        }
+
+        if (!poolManager.isAllowedAsset(poolId, address(token))) {
+            // TODO: Ensure this works via actor switch
+            t(hasReverted, "Router-x Must Revert");
+        }
+
+        // After Balances and Checks
+        uint256 balanceOfEscrowAfter = token.balanceOf(address(escrow));
+        uint256 balanceOfRouterEscrowAfter = token.balanceOf(address(routerEscrow));
+        uint256 lockedRequestAfter = router.lockedRequests(actor, address(vault));
+
+        // NOTE: We only enforce the check if the tx didn't revert
+        if (!hasReverted) {
+            uint256 deltaEscrow = balanceOfEscrowAfter - balanceOfEscrowB4;
+            uint256 deltaRouterEscrow = balanceOfRouterEscrowB4 - balanceOfRouterEscrowAfter;
+
+            eq(deltaEscrow, lockedRequestB4, "Router-x");
+            eq(deltaRouterEscrow, lockedRequestB4, "Router-x");
+            eq(lockedRequestAfter, 0, "Router-x");
+        }
+    }
+
+    // TODO: once we have multi actor support, include receiver != controller case
+    function router_claimDeposit(address sender) public {
+        // Bal b4
+        uint256 trancheUserB4 = trancheToken.balanceOf(actor);
+        uint256 trancheEscrowB4 = trancheToken.balanceOf(address(escrow));
+        uint256 shares = vault.maxMint(address(actor));
+
+        bool hasReverted;
+        vm.prank(sender);
+        try router.claimDeposit(address(vault), address(actor), address(actor)) {
+            // Processed Deposit | E-2 | Global-1
+            sumOfClaimedDeposits[address(trancheToken)] += shares;
+        } catch {
+            hasReverted = true;
+        }
+
+        if (!router.isEnabled(address(vault), address(actor)) && address(actor) != sender) {
+            t(hasReverted, "Router-x Must Revert");
+        }
+
+        // Bal after
+        uint256 trancheUserAfter = trancheToken.balanceOf(actor);
+        uint256 trancheEscrowAfter = trancheToken.balanceOf(address(escrow));
+
+        // NOTE: We only enforce the check if the tx didn't revert
+        if (!hasReverted) {
+            unchecked {
+                uint256 deltaUser = trancheUserAfter - trancheUserB4; // B4 - after -> They pay
+                uint256 deltaEscrow = trancheEscrowB4 - trancheEscrowAfter; // After - B4 -> They gain
+                emit DebugNumber(deltaUser);
+                emit DebugNumber(deltaEscrow);
+
+                eq(deltaUser, deltaEscrow, "Router-x");
+            }
+        }
+    }
+}