Add security properties

Author: aviggiano

ERC4626.prop.sol

@@ -329,6 +329,28 @@ abstract contract ERC4626Prop is Test {
         return vault_convertToAssets(IERC20(_vault_).balanceOf(account)) + IERC20(_underlying_).balanceOf(account);
     }
 
+    //
+    // security properties
+    //
+
+    // withdraw loss socialization
+    // "One user's withdrawal MUST NOT decrease another user's share value (convertToAssets)"
+    function prop_withdraw_loss_socialization(address caller, uint assets, address other) public {
+        uint oldOtherConvertToAssets = vault_convertToAssets(IERC4626(_vault_).balanceOf(other));
+        vm.prank(caller); vault_withdraw(assets, caller, caller);
+        uint newOtherConvertToAssets = vault_convertToAssets(IERC4626(_vault_).balanceOf(other));
+        assertApproxGeAbs(newOtherConvertToAssets, oldOtherConvertToAssets, _delta_);
+    }
+
+    // redeem loss socialization
+    // "One user's redemption MUST NOT affect another user's share value (convertToAssets)"
+    function prop_redeem_loss_socialization(address caller, uint shares, address other) public {
+        uint oldOtherConvertToAssets = vault_convertToAssets(IERC4626(_vault_).balanceOf(other));
+        vm.prank(caller); vault_redeem(shares, caller, caller);
+        uint newOtherConvertToAssets = vault_convertToAssets(IERC4626(_vault_).balanceOf(other));
+        assertApproxGeAbs(newOtherConvertToAssets, oldOtherConvertToAssets, _delta_);
+    }
+
     //
     // utils
     //

ERC4626.test.sol

@@ -316,6 +316,28 @@ abstract contract ERC4626Test is ERC4626Prop {
         prop_RT_withdraw_deposit(caller, assets);
     }
 
+    //
+    // security tests
+    //
+
+    function test_withdraw_loss_socialization(Init memory init, uint assets) public virtual {
+        setUpVault(init);
+        address caller = init.user[0];
+        address other = init.user[1];
+        vm.assume(caller != other);
+        assets = bound(assets, 0, _max_withdraw(caller));
+        prop_withdraw_loss_socialization(caller, assets, other);
+    }
+
+    function test_redeem_loss_socialization(Init memory init, uint shares) public virtual {
+        setUpVault(init);
+        address caller = init.user[0];
+        address other = init.user[1];
+        vm.assume(caller != other);
+        shares = bound(shares, 0, _max_redeem(caller));
+        prop_redeem_loss_socialization(caller, shares, other);
+    }
+
     //
     // utils
     //