Certora

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;
     }
@@ -62,6 +68,13 @@ contract BridgeHarness is Bridge {
      ************************/
     /* Wrapper functions allow calling internal functions from within the spec */
 
+    function listEqualLength(
+        address[] calldata l1Tokens,
+        uint256[] calldata l2Tokens
+    ) external returns (bool) {
+        return l1Tokens.length == l2Tokens.length;
+    }
+
     // A wrapper function for _dynamicToStaticAmount
     function _dynamicToStaticAmount_Wrapper(
         uint256 amount,
@@ -95,7 +108,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 +171,36 @@ 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);
-    }    
+    }
+
+    function Cairo_isValidL2Address(uint256 l2Bridge) public returns (bool) {
+        return Cairo.isValidL2Address(l2Bridge);
+    }
+
+    function approvedL1TokensLength() public returns (uint256) {
+        return _approvedL1Tokens.length;
+    }
 }

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 \
@@ -25,10 +30,10 @@ certoraRun certora/harness/BridgeHarness.sol \
         --optimistic_loop \
         --loop_iter 3 \
         --send_only \
-        --rule sanity \
         --rule_sanity \
         --cloud \
-        --msg "AAVE S-Net"
+        $RULE \
+        --msg "AAVE S-Net $1 $2"
 
 # 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.