Rules that involves external contract interactions keep time out

I am verifying a function which calls 4 external contracts, and I have mocked the 4 external contracts and linked them, but the verification keeps time-out. I’ve adjusted the --smt_timeout param to be 1750, which is about 30 minutes, but it still times out. The function is not that complicated, it calculates a net asset by subtracting total debt from total asset. The function interacts with Euler protocol, and I’ve mocked DToken and Etoken with a simple implementation. The asset is Wrapped stETH, and I’ve mocked WstETH and StETH.
What can I do to solve this time-out issue? I don’t want a rule to run hours.

Could you attach the report link and if possible the code? repo?

The report is here
The repo is still private.
I can paste some code snippet.
The function we are verifying is the inherited withdraw function in ERC4626

    function withdraw(
        uint256 assets,
        address receiver,
        address owner
    ) public virtual returns (uint256 shares) {
        shares = previewWithdraw(assets); // No need to check for rounding error, previewWithdraw rounds up.

        if (msg.sender != owner) {
            uint256 allowed = allowance[owner][msg.sender]; // Saves gas for limited approvals.

            if (allowed != type(uint256).max) allowance[owner][msg.sender] = allowed - shares;
        }

        beforeWithdraw(assets, shares);

        _burn(owner, shares);

        emit Withdraw(msg.sender, receiver, owner, assets, shares);

        asset.safeTransfer(receiver, assets);
    }

The beforeWithdraw virtual function is overridden in the code below

// SPDX-License-Identifier: AGPL-3.0-only
pragma solidity ^0.8.13;

import {ERC20} from "solmate/tokens/ERC20.sol";
import {SafeTransferLib} from "solmate/utils/SafeTransferLib.sol";
import {FixedPointMathLib} from "solmate/utils/FixedPointMathLib.sol";
import {WETH} from "solmate/tokens/WETH.sol";
import {sc4626} from "../../src/sc4626.sol";
import {IEulerDToken} from "../../src/interfaces/euler/IEulerDToken.sol";
import {IEulerEToken} from "../../src/interfaces/euler/IEulerEToken.sol";
import {ICurvePool} from "../../src/interfaces/curve/ICurvePool.sol";
import {ILido} from "../../src/interfaces/lido/ILido.sol";
import {IwstETH} from "../../src/interfaces/lido/IwstETH.sol";
import {IMarkets} from "../../src/interfaces/euler/IMarkets.sol";
import {AggregatorV3Interface} from "../../src/interfaces/chainlink/AggregatorV3Interface.sol";
import {IVault} from "../../src/interfaces/balancer/IVault.sol";
import {IFlashLoanRecipient} from "../../src/interfaces/balancer/IFlashLoanRecipient.sol";

error InvalidTargetLtv();
error InvalidMaxLtv();
error InvalidFlashLoanCaller();
error InvalidSlippageTolerance();
error AdminZeroAddress();

contract scWETH is sc4626, IFlashLoanRecipient {
    using SafeTransferLib for ERC20;
    using FixedPointMathLib for uint256;

    event SlippageToleranceUpdated(address indexed user, uint256 newSlippageTolerance);
    event MaxLtvUpdated(address indexed user, uint256 newMaxLtv);
    event TargetLtvRatioUpdated(address indexed user, uint256 newTargetLtv);
    event Harvest(uint256 profitSinceLastHarvest, uint256 performanceFee);

    address public EULER;

    // The Euler market contract
    IMarkets public markets;

    // Euler supply token for wstETH (ewstETH)
    IEulerEToken public eToken;

    // Euler debt token for WETH (dWETH)
    IEulerDToken public dToken;

    // Curve pool for ETH-stETH
    ICurvePool public curvePool;

    // Lido staking contract (stETH)
    ILido public stEth;

    IwstETH public wstETH;
    WETH public weth;

    // Chainlink pricefeed (stETH -> ETH)
    AggregatorV3Interface public stEThToEthPriceFeed;

    // Balancer vault for flashloans
    IVault public balancerVault;

    // total invested during last harvest/rebalance
    uint256 public totalInvested;

    // total profit generated for this vault
    uint256 public totalProfit;

    // The max loan to value(ltv) ratio for borrowing eth on euler with wsteth as collateral for the flashloan
    uint256 public maxLtv = ...;

    // the target ltv ratio at which we actually borrow (<= maxLtv)
    uint256 public targetLtv = ...;

    // slippage for curve swaps
    uint256 public slippageTolerance = 0.99e18;

    constructor(address _admin) sc4626(_admin, ERC20(address(weth)), "WETH Vault", "scWETH") {
        if (_admin == address(0)) revert AdminZeroAddress();

        ERC20(address(stEth)).safeApprove(address(wstETH), type(uint256).max);
        ERC20(address(stEth)).safeApprove(address(curvePool), type(uint256).max);
        ERC20(address(wstETH)).safeApprove(EULER, type(uint256).max);
        ERC20(address(weth)).safeApprove(EULER, type(uint256).max);
        ERC20(address(wstETH)).safeApprove(address(dToken), type(uint256).max);
        ERC20(address(wstETH)).safeApprove(address(eToken), type(uint256).max);
        // Enter the euler collateral market (collateral's address, *not* the eToken address) ,
        markets.enterMarket(0, address(wstETH));
    }

    /// @param amount : amount of asset to withdraw into the vault
    function withdrawToVault(uint256 amount) external onlyRole(KEEPER_ROLE) {
        _withdrawToVault(amount);
    }

    //////////////////// VIEW METHODS //////////////////////////

    function totalAssets() public view override returns (uint256 assets) {
        // value of the supplied collateral in eth terms using chainlink oracle
        assets = totalCollateralSupplied();

        // account for slippage losses
        assets = assets.mulWadDown(slippageTolerance);

        // add float
        assets += asset.balanceOf(address(this));

        // subtract the debt
        assets -= totalDebt();
    }

    // total wstETH supplied as collateral (in ETH terms)
    function totalCollateralSupplied() public view returns (uint256) {
        return wstEthToEth(eToken.balanceOfUnderlying(address(this)));
    }

    // total eth borrowed
    function totalDebt() public view returns (uint256) {
        return dToken.balanceOf(address(this));
    }

    // returns the net LTV at which we have borrowed till now (1e18 = 100%)
    function getLtv() public view returns (uint256 ltv) {
        uint256 collateral = totalCollateralSupplied();
        if (collateral > 0) {
            // totalDebt / totalSupplied
            ltv = totalDebt().divWadUp(collateral);
        }
    }

    //////////////////// EXTERNAL METHODS //////////////////////////

    // called after the flashLoan on _rebalancePosition
    function receiveFlashLoan(address[] memory, uint256[] memory amounts, uint256[] memory, bytes memory userData)
        external
    {
        if (msg.sender != address(balancerVault)) {
            revert InvalidFlashLoanCaller();
        }

        // the amount flashloaned
        uint256 flashLoanAmount = amounts[0];

        // decode user data
        (bool deposit, uint256 amount) = abi.decode(userData, (bool, uint256));

        amount += flashLoanAmount;

        // if flashloan received as part of a deposit
        if (deposit) {
            // unwrap eth
            weth.withdraw(amount);

            // stake to lido / eth => stETH
            stEth.submit{value: amount}(address(0x00));

            // wrap stETH
            wstETH.wrap(stEth.balanceOf(address(this)));

            // add wstETH liquidity on Euler
            eToken.deposit(0, type(uint256).max);

            // borrow enough weth from Euler to payback flashloan
            dToken.borrow(0, flashLoanAmount);
        }
        // if flashloan received as part of a withdrawal
        else {
            // repay debt + withdraw collateral
            if (flashLoanAmount >= totalDebt()) {
                dToken.repay(0, type(uint256).max);
                eToken.withdraw(0, type(uint256).max);
            } else {
                dToken.repay(0, flashLoanAmount);
                eToken.withdraw(0, _ethToWstEth(amount).divWadDown(slippageTolerance));
            }

            // unwrap wstETH
            uint256 stEthAmount = wstETH.unwrap(wstETH.balanceOf(address(this)));

            // stEth to eth
            (, int256 price,,,) = stEThToEthPriceFeed.latestRoundData();
            uint256 expected = stEthAmount.mulWadDown(uint256(price));

            // stETH to eth
            curvePool.exchange(1, 0, stEthAmount, expected.mulWadDown(slippageTolerance));

            // wrap eth
            weth.deposit{value: address(this).balance}();
        }

        // payback flashloan
        asset.safeTransfer(address(balancerVault), flashLoanAmount);
    }

    // need to be able to receive eth
    receive() external payable {}

    //////////////////// INTERNAL METHODS //////////////////////////

    function _withdrawToVault(uint256 amount) internal {
        uint256 ltv = getLtv();
        uint256 debt = totalDebt();

        uint256 flashLoanAmount = (debt - ltv.mulWadDown(amount)).divWadDown(1e18 - ltv);

        address[] memory tokens = new address[](1);
        tokens[0] = address(weth);

        uint256[] memory amounts = new uint256[](1);
        amounts[0] = flashLoanAmount;

        // take flashloan
        balancerVault.flashLoan(address(this), tokens, amounts, abi.encode(false, amount));
    }

    function beforeWithdraw(uint256 assets, uint256) internal override {
        uint256 float = asset.balanceOf(address(this));
        if (assets <= float) {
            return;
        }

        uint256 missing = assets - float;

        // needed otherwise counted as loss during harvest
        totalInvested -= missing;

        _withdrawToVault(missing);
    }
}

I have mocked all the external contracts such as BalancerVault, EToken, DToken, WstETH, StETH, CurvePool, etc.
I have omitted some irrelevant functions. As you can see, the beforeWithdraw function calls _withdrawToVault, which invokes balancerVault.flashLoan, and balancerVault.flashLoan function calls receiveFlashLoan, which calls functions on EToken, DToken, CurvePool, WstETH, stETH, WETH etc. A lot of external contracts are involved

Hi @fyang1024,
Is the flash loan actual implementation necessary for proving the revert statement of your rule?
What if you simply summarize the flashloan with a NONDET summary or link the balancer vault to an empty contract?

Thank you @RoyCERTORA , I’ve followed your advice to summarize flashloan with NONDET, and the rule can be verified fast, which proves that the timeout was indeed caused by the flashloan function call. However, the flashloan function is the main feature of the contract which we want to verify. Even though we can workaround like this for the reverts rule, but we cannot for other rules verifying the business logic. I’ll try to increase the timeout limit to see how long it will take.

Please let me know if there is any other option.
Thank you

I increased the --smt_timeout to 36000 (10 hours), however the verification timed out after 2 hours running. It seems the max timeout is 2 hours.

You can also try using -t, -mediumTimeout, and -depth in --settings, although its somewhat of a guessing game to figure out which parameters will help. Check out this page in the docs for more info on dealing with timeouts: Troubleshooting — Certora Prover Documentation 0.0 documentation

1 Like

Readjusting the timeouts settings could be helpful in most cases but overloading them as you’ve previously tried does lose its effect when the hard-stop (2h) limit is reached.
The more complicated approach would be summarizing some functions inside the flash loan contract.
When nonlinear mathematical calculations are involved (usually mul and div of non-constants), it is advised to replace them with more generalized functions that can return an arbitrary (but reasonable) number.
If you’re looking for violation, or convinced that there is one, you can also simplify these same calculations by assuming some variables to be constant.
Do not use this approach though if you wish to verify that rule, as it narrows down the scope and potentially can miss bugs.

1 Like

It seems to me that some changes in the Certora backend makes timeout more likely.
We have a rule which could run within time a few months ago, but now it time-out even if I set the timeout to be 1 hour.
The function the rule is verifying is here

Given the code is open source, could you please have a look to see what we can do to avoid the time-out?
Thank you

Hi @fyang1024, as I said before, could you attach the report link, please? It would be perfect if you can also find the old link so we can compare it.
and for the future, if anything is related to verification results, attaching a report is necessary.

Thank you @RedLikeRoses, I didn’t attach it because it had no information but only running time, like this one https://prover.certora.com/output/52311/9a70c1da7aeb49e6a821e04e9d2f9afa?anonymousKey=728bad6bc3216a8e141a82f16757b99171762312

I gave it another try last night, and it finished in 6918s, just within the 2 hours hard-stop.
https://prover.certora.com/output/52311/4095d993718a4157aa9d54f723f98164?anonymousKey=f685acc215c93fbb660aede99a770d668d42f54a
The full report link is Error 403, which I don’t have access
Please let me know if you get any insights from the reports

You said: “which could run within time”. within what time? was it 20 mins and now almost 2h or what?
Don’t you have the old run link to compare?

It was within the time under the default setting. The link to the report is Certora - Report, which shows it ran for 764s, which is about 10 minutes

I will pass it to devs, to see what’ve change and caused this

1 Like

@fyang1024 Please try to run the tool with --settings -adaptiveSolverConfig=false,-smt_nonLinearArithmetic=true,-t=3600,-prettifyCEX=none,-multipleCEX=none

Some explanation. By default, Certora Prover first tries to solve each single rule using a linear integer arithmetic only (LIA) encoding which overapproximate the underlying non-linear operations. If this overapproximation does not contain a violation, we know the original rule&program also does not contain a violation. In the other case, when the overapproximation contains a violation, we proceed with a precise non-linear (NIA) encoding (to make sure whether the the violation from LIA was a real counter-example or not and also to possibly find another counter-example or to show that there is no counter-example). In the case of your rule&program, the LIA encoding is useless. The flags -adaptiveSolverConfig=false,-smt_nonLinearArithmetic=true avoids using LIA and keep just NIA.

Second, when the rule is violated, we try to prettify the counter-example, i.e., find a counter-example that uses relatively small values of variables (and thus is human-readable). Unfortunately, this prettification can sometimes be very time consuming. -prettifyCEX=none,-multipleCEX=none turns off all counter-example postprocessing.

I believe our documentation includes some hints and explanations that could help you in the future. Though, still, every input is unique and hence finding the right setting of our tool can be sometimes hard (we are gradually trying to improve the default/auto configuration).

1 Like

Thank you @Jaroslav_CERTORA. I used the settings to run the integrity_of_withdraw again, and it was finished in 1091s. It did reduce the time quite a lot, though it still took 40% longer than a few months ago.

However, the verification of the function that interacts 7 external contracts still timeout. The report is here, and the spec is here, and the code is here
I described the problem here
I guess this is beyond the limit of Certora