CAREX-Certora - Aave Formal Verification Grant

certora/harness/BridgeHarness.sol

@@ -15,39 +15,54 @@ 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;
     }
-
-     /**
+
+    // Retrieving the UnderlyingAsset of the AToken
+    function getL2TokenOfAToken(address AToken) public view returns (uint256) {
+        return _aTokenData[AToken].l2TokenAddress;
+    }
+
+    /**
      * @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;
     }
 
+    function getRewardToken() public view returns (address) {
+        return address(_rewardToken);
+    }
+
     // Retrieving the balance of a user with respect to a given token
     function tokenBalanceOf(IERC20 token, address user)
         public
@@ -57,6 +72,19 @@ contract BridgeHarness is Bridge {
         return token.balanceOf(user);
     }
 
+    // Retrieving the balance of this with respect to a given token
+    function tokenBalanceOf(IERC20 token) public view returns (uint256) {
+        return token.balanceOf(address(this));
+    }
+
+    function getApprovedL1TokensLength()
+        external
+        view
+        returns (uint256 length)
+    {
+        length = _approvedL1Tokens.length;
+    }
+
     /************************
      *       Wrappers       *
      ************************/
@@ -95,7 +123,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 +186,28 @@ 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);
-    }    
+    }
 }

certora/scripts/runComplexity.sh

@@ -1,8 +1,9 @@
 certoraRun certora/harness/BridgeL2Harness.sol \
     --verify BridgeL2Harness:certora/specs/complexity.spec \
-    --solc solc8.10 \
     --optimistic_loop \
     --send_only \
     --rule "sanity" \
-    --staging  \
+    --cloud  \
     --msg "Bridge complexity check"
+    # --solc solc8.10 \
+

certora/scripts/verifyBridge.sh

@@ -1,3 +1,8 @@
+if [[ "$1" ]]
+then
+    RULE="--rule $1"
+fi
+
 certoraRun certora/harness/BridgeHarness.sol \
         certora/harness/BridgeL2Harness.sol \
         certora/harness/DummyERC20UnderlyingA_L1.sol \
@@ -21,14 +26,12 @@ certoraRun certora/harness/BridgeHarness.sol \
                     ATokenWithPoolB_L1:_incentivesController=IncentivesControllerMock_L1 \
                     BridgeL2Harness:BRIDGE_L1=BridgeHarness \
                     BridgeL2Harness:REW_AAVE=DummyERC20RewardToken \
-        --solc solc8.10 \
+        $RULE \
         --optimistic_loop \
         --loop_iter 3 \
         --send_only \
-        --rule sanity \
-        --rule_sanity \
         --cloud \
-        --msg "AAVE S-Net"
+        --msg "AAVE S-Net Bridge"
 
 # The first lines (#1-#11) specifies all the contracts that are being called through the BridgeHarness.sol file.
 # This is a declaration of multiple contracts for the verification context.