5 - Dust when depositing AToken in the vault (#39)

Author: kyzia551

certora/basic/harness/DummyContract.sol

@@ -1,8 +1,7 @@
-
 contract DummyContract {
-    function havoc_all_dummy() external {
-      //        havoc_all_dummy_internal();
-    }
+  function havoc_all_dummy() external {
+    //        havoc_all_dummy_internal();
+  }
 
-    //function havoc_all_dummy_internal() internal {}
+  //function havoc_all_dummy_internal() internal {}
 }

certora/basic/harness/EModeConfigurationHarness.sol

@@ -10,21 +10,29 @@ contract EModeConfigurationHarness {
 
   function setCollateral(uint256 reserveIndex, bool enabled) public {
     DataTypes.EModeCategory memory emode_new = eModeCategory;
-    eModeCategory.collateralBitmap = EModeConfiguration.setReserveBitmapBit(emode_new.collateralBitmap, reserveIndex, enabled);
+    eModeCategory.collateralBitmap = EModeConfiguration.setReserveBitmapBit(
+      emode_new.collateralBitmap,
+      reserveIndex,
+      enabled
+    );
   }
 
   function isCollateralAsset(uint256 reserveIndex) public returns (bool) {
-    return EModeConfiguration.isReserveEnabledOnBitmap(eModeCategory.collateralBitmap, reserveIndex);
+    return
+      EModeConfiguration.isReserveEnabledOnBitmap(eModeCategory.collateralBitmap, reserveIndex);
   }
 
-
-
-  function setBorrowable(uint256 reserveIndex,bool enabled) public {
+  function setBorrowable(uint256 reserveIndex, bool enabled) public {
     DataTypes.EModeCategory memory emode_new = eModeCategory;
-    eModeCategory.borrowableBitmap = EModeConfiguration.setReserveBitmapBit(emode_new.borrowableBitmap, reserveIndex, enabled);
+    eModeCategory.borrowableBitmap = EModeConfiguration.setReserveBitmapBit(
+      emode_new.borrowableBitmap,
+      reserveIndex,
+      enabled
+    );
   }
-  
+
   function isBorrowableAsset(uint256 reserveIndex) public returns (bool) {
-    return EModeConfiguration.isReserveEnabledOnBitmap(eModeCategory.borrowableBitmap, reserveIndex);
+    return
+      EModeConfiguration.isReserveEnabledOnBitmap(eModeCategory.borrowableBitmap, reserveIndex);
   }
 }

certora/basic/harness/PoolInstanceHarness.sol

@@ -8,18 +8,18 @@ import {DataTypes} from '../munged/contracts/protocol/libraries/types/DataTypes.
 import {ReserveLogic} from '../munged/contracts/protocol/libraries/logic/ReserveLogic.sol';
 import {WadRayMath} from '../munged/contracts/protocol/libraries/math/WadRayMath.sol';
 
-import {DummyContract} from "./DummyContract.sol";
-
+import {DummyContract} from './DummyContract.sol';
 
 contract PoolInstanceHarness is PoolInstance {
   DummyContract DUMMY;
 
   constructor(IPoolAddressesProvider provider) PoolInstance(provider) {}
 
-  function cumulateToLiquidityIndex(address asset,
-                                    uint256 totalLiquidity,
-                                    uint256 amount
-                                   ) external returns (uint256) {
+  function cumulateToLiquidityIndex(
+    address asset,
+    uint256 totalLiquidity,
+    uint256 amount
+  ) external returns (uint256) {
     return ReserveLogic.cumulateToLiquidityIndex(_reserves[asset], totalLiquidity, amount);
   }
 
@@ -34,12 +34,12 @@ contract PoolInstanceHarness is PoolInstance {
   function havoc_all() public {
     DUMMY.havoc_all_dummy();
   }
-  
+
   function rayMul(uint256 a, uint256 b) external returns (uint256) {
-    return WadRayMath.rayMul(a,b);
+    return WadRayMath.rayMul(a, b);
   }
-  
+
   function rayDiv(uint256 a, uint256 b) external returns (uint256) {
-    return WadRayMath.rayDiv(a,b);
+    return WadRayMath.rayDiv(a, b);
   }
 }

certora/stata/harness/pool/SymbolicLendingPool.sol

@@ -80,7 +80,7 @@ contract SymbolicLendingPool {
     res.isolationModeTotalDebt = reserveLegacy.isolationModeTotalDebt;
     return res;
   }
-  
+
   function getReserveDataExtended(
     address asset
   ) external view returns (DataTypes.ReserveData memory) {

src/contracts/extensions/static-a-token/ERC4626StataTokenUpgradeable.sol

@@ -75,6 +75,12 @@ abstract contract ERC4626StataTokenUpgradeable is ERC4626Upgradeable, IERC4626St
 
   ///@inheritdoc IERC4626StataToken
   function depositATokens(uint256 assets, address receiver) external returns (uint256) {
+    // because aToken is rebasable, we allow user to specify more then he has to compensate growth during the tx mining
+    uint256 actualUserBalance = IERC20(aToken()).balanceOf(_msgSender());
+    if (assets > actualUserBalance) {
+      assets = actualUserBalance;
+    }
+
     uint256 shares = previewDeposit(assets);
     _deposit(_msgSender(), receiver, assets, shares, false);
 
@@ -89,14 +95,27 @@ abstract contract ERC4626StataTokenUpgradeable is ERC4626Upgradeable, IERC4626St
     SignatureParams memory sig,
     bool depositToAave
   ) external returns (uint256) {
-    IERC20Permit assetToDeposit = IERC20Permit(
-      depositToAave ? asset() : address(_getERC4626StataTokenStorage()._aToken)
-    );
+    address assetToDeposit = depositToAave ? asset() : aToken();
 
     try
-      assetToDeposit.permit(_msgSender(), address(this), assets, deadline, sig.v, sig.r, sig.s)
+      IERC20Permit(assetToDeposit).permit(
+        _msgSender(),
+        address(this),
+        assets,
+        deadline,
+        sig.v,
+        sig.r,
+        sig.s
+      )
     {} catch {}
 
+    // because aToken is rebasable, we allow user to specify more then he has to compensate growth during the tx mining
+    // to make it consistent, we keep the same behaviour for the normal underlying too
+    uint256 actualUserBalance = IERC20(assetToDeposit).balanceOf(_msgSender());
+    if (assets > actualUserBalance) {
+      assets = actualUserBalance;
+    }
+
     uint256 shares = previewDeposit(assets);
     _deposit(_msgSender(), receiver, assets, shares, depositToAave);
     return shares;