Added some getter functions in harness and added spec file

.zip-output-url.txt

@@ -0,0 +1 @@
+https://prover.certora.com/zipOutput/93750/b08e685d792bd8ac724f?anonymousKey=50a893fa2c61102b9eeb643083e8fa32dc092e60

certora/harness/BridgeHarness.sol

@@ -15,35 +15,41 @@ contract BridgeHarness is Bridge {
      *        Getters        *
      *************************/
 
-    function withdrawMessageStatus() external view returns (bool){
+    function withdrawMessageStatus() external view returns (bool) {
         return withdrawMessageSent;
     }
 
-    function bridgeRewardsMessageStatus() external view returns (bool){
+    function bridgeRewardsMessageStatus() external view returns (bool) {
         return bridgeRewardsMessageSent;
     }
 
     // Retrieving the UnderlyingAsset of the AToken
     function getUnderlyingAssetOfAToken(address AToken)
-    public view returns (IERC20 underlyingAsset) {
+        public
+        view
+        returns (IERC20 underlyingAsset)
+    {
         return _aTokenData[AToken].underlyingAsset;
     }
-    
-     /**
+
+    /**
      * @dev Retrieving the AToken address of an underlying asset
      * @param lendPool lending pool to search the AToken for.
      * @param asset The underlying asset to which the Atoken is connected
      * @return Atoken the `atoken` address
      **/
-    function getATokenOfUnderlyingAsset(SymbolicLendingPoolL1 lendPool, address asset)
-    public view returns (address)
-    {
+    function getATokenOfUnderlyingAsset(
+        SymbolicLendingPoolL1 lendPool,
+        address asset
+    ) public view returns (address) {
         return lendPool.underlyingtoAToken(asset);
     }
 
     // Retrieving the LendingPool of the AToken
     function getLendingPoolOfAToken(address AToken)
-    public view returns (ILendingPool lendingPool)
+        public
+        view
+        returns (ILendingPool lendingPool)
     {
         return _aTokenData[AToken].lendingPool;
     }
@@ -95,7 +101,8 @@ contract BridgeHarness is Bridge {
         uint256 l2RewardsIndex,
         uint256 l1RewardsIndex
     ) external pure returns (uint256) {
-        return super._computeRewardsDiff(amount, l2RewardsIndex, l1RewardsIndex);
+        return
+            super._computeRewardsDiff(amount, l2RewardsIndex, l1RewardsIndex);
     }
 
     /*****************************************
@@ -157,19 +164,56 @@ contract BridgeHarness is Bridge {
     ) external returns (uint256) {
         require(!withdrawMessageSent, "A message is already being consumed");
         withdrawMessageSent = true;
-        BRIDGE_L2.initiateWithdraw(asset, amount, msg.sender, to, toUnderlyingAsset);
+        BRIDGE_L2.initiateWithdraw(
+            asset,
+            amount,
+            msg.sender,
+            to,
+            toUnderlyingAsset
+        );
         withdrawMessageSent = false;
         return amount;
     }
 
     function bridgeRewards_L2(address recipient, uint256 amount) external {
-        require(!bridgeRewardsMessageSent, "A message is already being consumed");
+        require(
+            !bridgeRewardsMessageSent,
+            "A message is already being consumed"
+        );
         bridgeRewardsMessageSent = true;
         BRIDGE_L2.bridgeRewards(recipient, msg.sender, amount);
         bridgeRewardsMessageSent = false;
     }
 
     function claimRewardsStatic_L2(address staticAToken) external {
         BRIDGE_L2.claimRewards(msg.sender, staticAToken);
-    }    
+    }
+
+    // get the staticAToken balance of a user
+    function getStaticATokenBalance(address asset, address user)
+        external
+        view
+        returns (uint256)
+    {
+        return BRIDGE_L2.getStaticATokenBalance(asset, user);
+    }
+
+    // get the length of _approvedl1Tokens array
+    function getApprovedTokensArrayLength() external view returns (uint256) {
+        return _approvedL1Tokens.length;
+    }
+
+    //get Reward balance
+    function getRewardBalance(address user) external view returns (uint256) {
+        return _rewardToken.balanceOf(user);
+    }
+
+    // get l2 token address
+    function getL2TokenAddress(address l1Atoken)
+        external
+        view
+        returns (address)
+    {
+        return address(uint160(_aTokenData[l1Atoken].l2TokenAddress));
+    }
 }

certora/harness/BridgeL2Harness.sol

@@ -12,36 +12,44 @@ contract BridgeL2Harness is IBridge_L2 {
     uint256 public l2RewardsIndex;
     IERC20_Extended public REW_AAVE;
 
-    modifier onlyL1Bridge()
-    {
-        require (msg.sender == address(BRIDGE_L1), "only owner can access");
+    modifier onlyL1Bridge() {
+        require(msg.sender == address(BRIDGE_L1), "only owner can access");
         _;
-    } 
+    }
 
     /**
      * @dev Sets the `l2RewardsIndex`
      * @param value the value to be assigned to `l2RewardsIndex`
      **/
-    function l2RewardsIndexSetter(uint256 value) external onlyL1Bridge{
+    function l2RewardsIndexSetter(uint256 value) external onlyL1Bridge {
         l2RewardsIndex = value;
     }
 
-
     /**
      * @dev retrieves the address of the StaticAToken on L2
      * @param AToken address of AToken on L1
      **/
     function getStaticATokenAddress(address AToken)
-    public view returns(address) {
+        public
+        view
+        returns (address)
+    {
         return AtokenToStaticAToken_L2[AToken];
     }
 
-
-    function getRewTokenAddress() external view returns(address) {
+    function getStaticATokenBalance(address asset, address user)
+        external
+        view
+        returns (uint256)
+    {
+        return IStaticAToken(AtokenToStaticAToken_L2[asset]).balanceOf(user);
+    }
+
+    function getRewTokenAddress() external view returns (address) {
         return address(REW_AAVE);
     }
 
-    function address2uint256(address add) external pure returns(uint256){
+    function address2uint256(address add) external pure returns (uint256) {
         return uint256(uint160(add));
     }
 
@@ -75,12 +83,9 @@ contract BridgeL2Harness is IBridge_L2 {
         uint256 amount,
         address caller,
         address to,
-        bool toUnderlyingAsset)
-        external onlyL1Bridge {
-        IERC20_Extended(AtokenToStaticAToken_L2[asset]).burn(
-            caller,
-            amount
-        );
+        bool toUnderlyingAsset
+    ) external onlyL1Bridge {
+        IERC20_Extended(AtokenToStaticAToken_L2[asset]).burn(caller, amount);
 
         BRIDGE_L1.withdraw(
             asset,
@@ -97,14 +102,17 @@ contract BridgeL2Harness is IBridge_L2 {
      * @param recipient The L1 user address that withdraws the reward
      * @param amount The amount of reward token desired to be withdrawn
      **/
-    function bridgeRewards(address recipient, address caller, uint256 amount) 
-    external onlyL1Bridge{
-        IERC20_Extended(REW_AAVE).transferFrom(caller, address(BRIDGE_L1), amount);
-        BRIDGE_L1.receiveRewards(
-            uint256(uint160(caller)),
-            recipient,
+    function bridgeRewards(
+        address recipient,
+        address caller,
+        uint256 amount
+    ) external onlyL1Bridge {
+        IERC20_Extended(REW_AAVE).transferFrom(
+            caller,
+            address(BRIDGE_L1),
             amount
         );
+        BRIDGE_L1.receiveRewards(uint256(uint160(caller)), recipient, amount);
     }
 
     /**
@@ -114,7 +122,9 @@ contract BridgeL2Harness is IBridge_L2 {
      * @param staticAToken The staticAToken address
      **/
     function claimRewards(address caller, address staticAToken)
-    external onlyL1Bridge{
+        external
+        onlyL1Bridge
+    {
         uint256 amount = IStaticAToken(staticAToken).claimRewards(caller);
         IERC20_Extended(REW_AAVE).mint(caller, amount);
     }

certora/harness/IBridge_L2.sol

@@ -15,11 +15,21 @@ interface IBridge_L2 {
         uint256 amount,
         address caller,
         address to,
-        bool toUnderlyingAsset) external;
+        bool toUnderlyingAsset
+    ) external;
 
-    function getRewTokenAddress() external view returns(address);
+    function getRewTokenAddress() external view returns (address);
 
-    function bridgeRewards(address recipient, address caller, uint256 amount) external;
+    function bridgeRewards(
+        address recipient,
+        address caller,
+        uint256 amount
+    ) external;
 
     function claimRewards(address recipient, address staticAToken) external;
+
+    function getStaticATokenBalance(address asset, address user)
+        external
+        view
+        returns (uint256);
 }

certora/scripts/verifyBridge.sh

@@ -21,11 +21,9 @@ certoraRun certora/harness/BridgeHarness.sol \
                     ATokenWithPoolB_L1:_incentivesController=IncentivesControllerMock_L1 \
                     BridgeL2Harness:BRIDGE_L1=BridgeHarness \
                     BridgeL2Harness:REW_AAVE=DummyERC20RewardToken \
-        --solc solc8.10 \
         --optimistic_loop \
         --loop_iter 3 \
         --send_only \
-        --rule sanity \
         --rule_sanity \
         --cloud \
         --msg "AAVE S-Net"