Gg/request redeem router target (#416)

* Router request redeem target function implementation * Improve invariant expectation for tranche token * A new fix of the invariant
centrifuge · Oct 3, 2024 · a2212cd · a2212cd
1 parent 1fa9b61
commit a2212cd
Show file tree

Hide file tree

Showing 3 changed files with 42 additions and 2 deletions.
diff --git a/test/recon-core/Properties.sol b/test/recon-core/Properties.sol
@@ -302,8 +302,8 @@ abstract contract Properties is Setup, Asserts, ERC7540CentrifugeProperties {
             return trancheToken.balanceOf(address(escrow))
                 == (
                     sumOfFullfilledDeposits[address(trancheToken)] + sumOfRedeemRequests[address(trancheToken)]
-                        - sumOfClaimedDeposits[address(trancheToken)] - sumOfClaimedRedeemCancelations[address(trancheToken)]
-                        - sumOfClaimedRequests[address(trancheToken)]
+                        + sumOfRedeemRequestsRouter[address(trancheToken)] - sumOfClaimedDeposits[address(trancheToken)]
+                        - sumOfClaimedRedeemCancelations[address(trancheToken)] - sumOfClaimedRequests[address(trancheToken)]
                 );
         }
     }

diff --git a/test/recon-core/SharedStorage.sol b/test/recon-core/SharedStorage.sol
@@ -186,4 +186,5 @@ abstract contract SharedStorage {
     mapping(address => uint256) sumOfExecutedLockedDepositRequests;
     // stores request data coming through the router
     mapping(address => uint256) sumOfDepositRequestsRouter;
+    mapping(address => uint256) sumOfRedeemRequestsRouter;
 }
diff --git a/test/recon-core/targets/RouterFunctions.sol b/test/recon-core/targets/RouterFunctions.sol
@@ -176,6 +176,45 @@ abstract contract RouterFunctions is BaseTargetFunctions, Properties {
         }
     }
 
+    function router_requestRedeem(uint256 shares) public {
+        address owner = actor;
+        address controller = actor;
+
+        uint256 balanceOfEscrowB4 = trancheToken.balanceOf(address(escrow));
+        uint256 balanceOfRouterEscrowB4 = trancheToken.balanceOf(address(routerEscrow));
+        uint256 balanceOfOwnerB4 = trancheToken.balanceOf(owner);
+        shares = between(shares, 0, balanceOfOwnerB4);
+
+        bool hasReverted;
+
+        trancheToken.approve(address(vault), shares);
+
+        try router.requestRedeem(address(vault), shares, controller, owner, 0) {
+            sumOfRedeemRequestsRouter[address(trancheToken)] += shares;
+            requestRedeemShares[actor][address(trancheToken)] += shares;
+        } catch {
+            hasReverted = true;
+        }
+        if (restrictionManager.isFrozen(address(trancheToken), controller)) {
+            t(hasReverted, "Router-Redeem-Frozen Must Revert");
+        }
+        // After Balances and Checks
+        uint256 balanceOfEscrowAfter = trancheToken.balanceOf(address(escrow));
+        uint256 balanceOfOwnerAfter = trancheToken.balanceOf(owner);
+        uint256 balanceOfRouterEscrowAfter = trancheToken.balanceOf(address(routerEscrow));
+
+        // NOTE: We only enforce the check if the tx didn't revert
+        if (!hasReverted) {
+            uint256 deltaEscrow = balanceOfEscrowAfter - balanceOfEscrowB4;
+            uint256 deltaOwner = balanceOfOwnerB4 - balanceOfOwnerAfter;
+            uint256 deltaRouterEscrow = balanceOfRouterEscrowB4 - balanceOfRouterEscrowAfter;
+
+            eq(deltaEscrow, shares, "Router-x");
+            eq(deltaOwner, shares, "Router-x");
+            eq(deltaRouterEscrow, 0, "Router-x");
+        }
+    }
+
     // TODO: once we have multi actor support, include receiver != controller case
     function router_claimDeposit(address sender) public {
         // Bal b4