fix: lint certora files

.github/workflows/certora-stata.yml

@@ -29,7 +29,7 @@ jobs:
 
       - name: Install certora cli
         run: pip install certora-cli==7.14.2
- 
+
       - name: Install solc
         run: |
           wget https://github.com/ethereum/solidity/releases/download/v0.8.20/solc-static-linux

certora/stata/harness/StataTokenV2Harness.sol

@@ -5,81 +5,69 @@ import {IERC20} from 'openzeppelin-contracts/contracts/interfaces/IERC20.sol';
 import {StataTokenV2, IPool, IRewardsController} from 'aave-v3-periphery/contracts/static-a-token/StataTokenV2.sol';
 import {SymbolicLendingPool} from './pool/SymbolicLendingPool.sol';
 
+contract StataTokenV2Harness is StataTokenV2 {
+  address internal _reward_A;
 
+  constructor(
+    IPool pool,
+    IRewardsController rewardsController
+  ) StataTokenV2(pool, rewardsController) {}
 
-contract StataTokenV2Harness is StataTokenV2 {
-    address internal _reward_A;
+  function rate() external view returns (uint256) {
+    return _rate();
+  }
+
+  // returns the address of the i-th reward token in the reward tokens list maintained by the static aToken
+  function getRewardToken(uint256 i) external view returns (address) {
+    return rewardTokens()[i];
+  }
 
-    constructor(
-                IPool pool,
-                IRewardsController rewardsController
-    ) StataTokenV2(pool, rewardsController) {}
-
-    function rate() external view returns (uint256) {
-        return _rate();
-    }
-
-    // returns the address of the i-th reward token in the reward tokens list maintained by the static aToken
-    function getRewardToken(uint256 i) external view returns (address) {
-        return rewardTokens()[i];
-    }
-
-    // returns the length of the reward tokens list maintained by the static aToken
-    function getRewardTokensLength() external view returns (uint256) {
-        return rewardTokens().length;
-    }
+  // returns the length of the reward tokens list maintained by the static aToken
+  function getRewardTokensLength() external view returns (uint256) {
+    return rewardTokens().length;
+  }
 
-    // returns a user's reward index on last interaction for a given reward
-    // function getRewardsIndexOnLastInteraction(address user, address reward)
-    // external view returns (uint128) {
-    //     UserRewardsData memory currentUserRewardsData = _userRewardsData[user][reward];
-    //     return currentUserRewardsData.rewardsIndexOnLastInteraction;
-    // }
+  // returns a user's reward index on last interaction for a given reward
+  // function getRewardsIndexOnLastInteraction(address user, address reward)
+  // external view returns (uint128) {
+  //     UserRewardsData memory currentUserRewardsData = _userRewardsData[user][reward];
+  //     return currentUserRewardsData.rewardsIndexOnLastInteraction;
+  // }
 
-    // claims rewards for a user on the static aToken.
-    // the method builds the rewards array with a single reward and calls the internal claim function with it
-    function claimSingleRewardOnBehalf(
-        address onBehalfOf,
-        address receiver,
-        address reward
-    ) external 
-    {
-        require (reward == _reward_A);
-        address[] memory rewards = new address[](1);
-        rewards[0] = _reward_A;
+  // claims rewards for a user on the static aToken.
+  // the method builds the rewards array with a single reward and calls the internal claim function with it
+  function claimSingleRewardOnBehalf(
+    address onBehalfOf,
+    address receiver,
+    address reward
+  ) external {
+    require(reward == _reward_A);
+    address[] memory rewards = new address[](1);
+    rewards[0] = _reward_A;
 
-        // @MM - think of the best way to get rid of this require
-        require(
-            msg.sender == onBehalfOf ||
-            msg.sender == INCENTIVES_CONTROLLER.getClaimer(onBehalfOf)
-        );
-        _claimRewardsOnBehalf(onBehalfOf, receiver, rewards);
-    }
+    // @MM - think of the best way to get rid of this require
+    require(msg.sender == onBehalfOf || msg.sender == INCENTIVES_CONTROLLER.getClaimer(onBehalfOf));
+    _claimRewardsOnBehalf(onBehalfOf, receiver, rewards);
+  }
 
-    // claims rewards for a user on the static aToken.
-    // the method builds the rewards array with 2 identical rewards and calls the internal claim function with it
-    function claimDoubleRewardOnBehalfSame(
-        address onBehalfOf,
-        address receiver,
-        address reward
-    ) external 
-    {
-        require (reward == _reward_A);
-        address[] memory rewards = new address[](2);
-        rewards[0] = _reward_A;
-        rewards[1] = _reward_A;
+  // claims rewards for a user on the static aToken.
+  // the method builds the rewards array with 2 identical rewards and calls the internal claim function with it
+  function claimDoubleRewardOnBehalfSame(
+    address onBehalfOf,
+    address receiver,
+    address reward
+  ) external {
+    require(reward == _reward_A);
+    address[] memory rewards = new address[](2);
+    rewards[0] = _reward_A;
+    rewards[1] = _reward_A;
 
-        require(
-            msg.sender == onBehalfOf ||
-            msg.sender == INCENTIVES_CONTROLLER.getClaimer(onBehalfOf)
-        );
-        _claimRewardsOnBehalf(onBehalfOf, receiver, rewards);
+    require(msg.sender == onBehalfOf || msg.sender == INCENTIVES_CONTROLLER.getClaimer(onBehalfOf));
+    _claimRewardsOnBehalf(onBehalfOf, receiver, rewards);
+  }
 
-    }
-
-    // wrapper function for the erc20 _mint function. Used to reduce running times
-    function _mintWrapper(address to, uint256 amount) external {
-        _mint(to, amount);
-    }
-
+  // wrapper function for the erc20 _mint function. Used to reduce running times
+  function _mintWrapper(address to, uint256 amount) external {
+    _mint(to, amount);
+  }
 }

certora/stata/harness/pool/SymbolicLendingPool.sol

@@ -2,107 +2,88 @@ pragma solidity ^0.8.10;
 pragma experimental ABIEncoderV2;
 
 import {IERC20} from 'aave-v3-core/contracts/dependencies/openzeppelin/contracts/IERC20.sol';
-import {IAToken} from "aave-v3-core/contracts/interfaces/IAToken.sol";
+import {IAToken} from 'aave-v3-core/contracts/interfaces/IAToken.sol';
 import {DataTypes} from 'aave-v3-core/contracts/protocol/libraries/types/DataTypes.sol';
 
 contract SymbolicLendingPool {
-    // an underlying asset in the pool
-    IERC20 public underlyingToken;
-    // the aToken associated with the underlying above
-    IAToken public aToken;
-    // This index is used to convert the underlying token to its matching
-    // AToken inside the pool, and vice versa.
-    uint256 public liquidityIndex;
+  // an underlying asset in the pool
+  IERC20 public underlyingToken;
+  // the aToken associated with the underlying above
+  IAToken public aToken;
+  // This index is used to convert the underlying token to its matching
+  // AToken inside the pool, and vice versa.
+  uint256 public liquidityIndex;
 
-    /**
+  /**
      * @dev Deposits underlying token in the Atoken's contract on behalf of the user,
             and mints Atoken on behalf of the user in return.
      * @param asset The underlying sent by the user and to which Atoken shall be minted
      * @param amount The amount of underlying token sent by the user
      * @param onBehalfOf The recipient of the minted Atokens
      * @param referralCode A unique code (unused)
      **/
-    function deposit(
-        address asset,
-        uint256 amount,
-        address onBehalfOf,
-        uint16 referralCode
-    ) external {
-        require(asset == address(underlyingToken));
-        underlyingToken.transferFrom(
-            msg.sender,
-            address(aToken),
-            amount
-        );
-        aToken.mint(
-            msg.sender,
-            onBehalfOf,
-            amount,
-            liquidityIndex
-        );
-    }
+  function deposit(
+    address asset,
+    uint256 amount,
+    address onBehalfOf,
+    uint16 referralCode
+  ) external {
+    require(asset == address(underlyingToken));
+    underlyingToken.transferFrom(msg.sender, address(aToken), amount);
+    aToken.mint(msg.sender, onBehalfOf, amount, liquidityIndex);
+  }
 
-    /**
-     * @dev Burns Atokens in exchange for underlying asset
-     * @param asset The underlying asset to which the Atoken is connected
-     * @param amount The amount of underlying tokens to be burned
-     * @param to The recipient of the burned Atokens
-     * @return The `amount` of tokens withdrawn
-     **/
-    function withdraw(
-        address asset,
-        uint256 amount,
-        address to
-    ) external returns (uint256) {
-        require(asset == address(underlyingToken));
-        aToken.burn(
-            msg.sender,
-            to,
-            amount,
-            liquidityIndex
-        );
-        return amount;
-    }
+  /**
+   * @dev Burns Atokens in exchange for underlying asset
+   * @param asset The underlying asset to which the Atoken is connected
+   * @param amount The amount of underlying tokens to be burned
+   * @param to The recipient of the burned Atokens
+   * @return The `amount` of tokens withdrawn
+   **/
+  function withdraw(address asset, uint256 amount, address to) external returns (uint256) {
+    require(asset == address(underlyingToken));
+    aToken.burn(msg.sender, to, amount, liquidityIndex);
+    return amount;
+  }
 
-    /**
-     * @dev A simplification returning a constant
-     * @param asset The underlying asset to which the Atoken is connected
-     * @return liquidityIndex the `liquidityIndex` of the asset
-     **/
-    function getReserveNormalizedIncome(address asset)
-        external
-        view
-        virtual
-        returns (uint256)
-    {
-        return liquidityIndex;
-    }
+  /**
+   * @dev A simplification returning a constant
+   * @param asset The underlying asset to which the Atoken is connected
+   * @return liquidityIndex the `liquidityIndex` of the asset
+   **/
+  function getReserveNormalizedIncome(address asset) external view virtual returns (uint256) {
+    return liquidityIndex;
+  }
+
+  DataTypes.ReserveDataLegacy reserveLegacy;
+  DataTypes.ReserveData reserve;
+
+  function getReserveData(
+    address asset
+  ) external view returns (DataTypes.ReserveDataLegacy memory) {
+    DataTypes.ReserveDataLegacy memory res;
+
+    res.configuration = reserve.configuration;
+    res.liquidityIndex = reserve.liquidityIndex;
+    res.currentLiquidityRate = reserve.currentLiquidityRate;
+    res.variableBorrowIndex = reserve.variableBorrowIndex;
+    res.currentVariableBorrowRate = reserve.currentVariableBorrowRate;
+    res.currentStableBorrowRate = reserve.currentStableBorrowRate;
+    res.lastUpdateTimestamp = reserve.lastUpdateTimestamp;
+    res.id = reserve.id;
+    res.aTokenAddress = reserve.aTokenAddress;
+    res.stableDebtTokenAddress = reserve.stableDebtTokenAddress;
+    res.variableDebtTokenAddress = reserve.variableDebtTokenAddress;
+    res.interestRateStrategyAddress = reserve.interestRateStrategyAddress;
+    res.accruedToTreasury = reserve.accruedToTreasury;
+    res.unbacked = reserve.unbacked;
+    res.isolationModeTotalDebt = reserve.isolationModeTotalDebt;
+    return res;
+  }
 
-    DataTypes.ReserveDataLegacy reserveLegacy;
-    DataTypes.ReserveData reserve;
-
-    function getReserveData(address asset) external view returns (DataTypes.ReserveDataLegacy memory) {
-        DataTypes.ReserveDataLegacy memory res;
-
-        res.configuration = reserve.configuration;
-        res.liquidityIndex = reserve.liquidityIndex;
-        res.currentLiquidityRate = reserve.currentLiquidityRate;
-        res.variableBorrowIndex = reserve.variableBorrowIndex;
-        res.currentVariableBorrowRate = reserve.currentVariableBorrowRate;
-        res.currentStableBorrowRate = reserve.currentStableBorrowRate;
-        res.lastUpdateTimestamp = reserve.lastUpdateTimestamp;
-        res.id = reserve.id;
-        res.aTokenAddress = reserve.aTokenAddress;
-        res.stableDebtTokenAddress = reserve.stableDebtTokenAddress;
-        res.variableDebtTokenAddress = reserve.variableDebtTokenAddress;
-        res.interestRateStrategyAddress = reserve.interestRateStrategyAddress;
-        res.accruedToTreasury = reserve.accruedToTreasury;
-        res.unbacked = reserve.unbacked;
-        res.isolationModeTotalDebt = reserve.isolationModeTotalDebt;
-        return res;
-    }
-
-    function getReserveDataExtended(address asset) external view returns (DataTypes.ReserveData memory) {
-      return reserve;
-    }
+  function getReserveDataExtended(
+    address asset
+  ) external view returns (DataTypes.ReserveData memory) {
+    return reserve;
+  }
 }