Feature Request: Automate the --link Process for Large Projects with Multiple Solidity Files

[dayday2019]

When working with large projects that involve multiple Solidity files, manually handling the --link process becomes increasingly complex and error-prone. Each file often requires careful linking to dependencies or libraries, and this manual effort scales poorly as the project grows—slowing down workflows and increasing the risk of mistakes.

Given that the source code of the projects being tested is already available, has there been any consideration for automating the --link process? Automating this step could significantly streamline testing pipelines, reduce manual overhead, and ensure consistency across different files and project scales.

Looking forward to hearing thoughts on this potential improvement!

[urikirsh]

You might want to try the --auto_dispatcher flag. It can help in large projects by automatically resolving calls where the sighash is known but the callee isn't.

It behaves as if a DISPATCHER(optimistic=true) was added for each such call, but without failing if no match is found (it falls back to havoc).

More details here:
https://docs.certora.com/en/latest/docs/prover/cli/options.html#auto-dispatcher

[dayday2019]

@urikirsh Thanks for sharing this great suggestion! It really got me thinking about streamlining the linking process, so I decided to run a small experiment to explore the feasibility.

I tested the same set of Solidity files and spec files twice: once using the --link flag, and once replacing it with the --auto_dispatcher flag. Interestingly, when using --auto_dispatcher, I encountered a lot of rule_not_vacuous warnings, which didn't appear with the --link approach.

You can check out the two execution results here for comparison:

• Result with --link: https://prover.certora.com/output/5562613/aedb33e3199349eb8dc3af8850d5771a?anonymousKey=ec61c98615c94ea29a830b0bbc48e34a66dcb800
• Result with --auto_dispatcher: https://prover.certora.com/output/5562613/f142d909c111410989e07bfa75b74317?anonymousKey=43a07af20b00efb7ae5ddcad5f434cba3d30a3cb

I’m still digging into why this discrepancy happens—whether it’s due to differences in how dependencies are resolved or how rules are validated. Would love to hear your thoughts on these results as we explore automating the linking process further!

[naftali-g]

Hi,
This is actually an interesting and a little delicate issue. What's happening is this. In the createBorrowOrder function there's the following code

        order = IOrderFactory(orderFactory).createOrder(
            loanTools,
            getLoanTools,
            takenExpireTime,
            submitProofExpireTime,
            repaidExpireTime,
            proofedDelayBlock,
            owner(),
            lockTime1,
            lockTime2
        );

        IOrder(order).createBorrowOrder(msg.sender, token, amount, durationDays, btcAddress, publicKey);

and createOrder creates a new instance of an Order via new.
So what this code does is actually over-write whatever value was in the order storage slot before.
In the link case, for various reasons, the call to createBorrowOrder is still resolved to the Order instance that you linked to, so the call is to that contract instance (as can be seen in the calltrace).
In the auto-dispatcher case, what happens is that when constructing the rule, at the location of the call to createBorrowOrder a sort of "switch-case" is inserted, where the prover switches over the actual value of order, and if it matches the address of some contract in the scene that implements that function then the function is called on that contract instance, and there's an require false in the default case. So here, because of the new the new value of order will always be an address that's different than that of all contracts in the scene (that's how we model new), we reach the default case which is as stated a require false so you get a vacuity.

In other words, in this case the behavior of the auto-dispatcher is actually the more "correct" one.

Regarding how to solve this - you could set --dynamic_bound 1 which tells the prover to actually create (at most 1) new instance of any contract if there's a new call for it. Then the switch-case will have a branch for the new instance as well and it will pass.
Another option which is simpler and probably closer to what you want (since I assume you don't really want 2 instances of the Order contract in the scene) is to summarize createOrder so that it always just returns the value of the Order instance in the scene:

using Order as order;
methods {
	function createOrder(
	        address _loanTools,
	        address _getLoanTools,
	        uint256 _takenExpireTime,
	        uint256 _submitProofExpireTime,
	        uint256 _repaidExpireTime,
	        uint256 _proofedDelayBlock,
	        address _owner,
	        uint256 _lockTime1,
	        uint256 _lockTime2
	    ) external returns(address) => order;
}

I believe the above should work for both the link and auto-dispatcher modes.

[dayday2019]

@naftali-g Hi, thanks for your previous insights! I tried enabling both --auto_dispatcher and --dynamic_bound 1 in my config file, but the result is exactly the same as when only --auto_dispatcher is enabled. You can check the output here: https://prover.certora.com/output/5562613/74e2b48219eb4a3d944c9bbc67a7675e/

Additionally, certoraRun printed a warning I can't figure out:
WARNING: 'disable_source_finders' is set to true while 'dynamic_bound' is set to 1 or higher.

The thing is, I never explicitly set disable_source_finders in my config. Here's my current conf file for reference:

{
    "contract_recursion_limit": "3",
    "coverage_info": "advanced",
    "files": [
        "contracts/LoanContract.sol:LoanContract",
        "contracts/order/OrderFactory.sol:OrderFactory",
        "contracts/orderTools/LoanTools.sol:LoanTools",
        "contracts/order/Order.sol",
        "contracts/utils/ContractConst.sol",
        "contracts/interest/Interest.sol"
    ],
    "dynamic_bound": "1",
    "auto_dispatcher": true,
    "packages_path": "node_modules",
    "msg": "test config file2",
    "optimistic_contract_recursion": true,
    "optimistic_hashing": true,
    "optimistic_loop": true,
    "process": "emv",
    "verify": "LoanContract:contracts/fv_target/PropertyAgent_report/LoanContract_LoanContract_createBorrowOrder_4_fix_round1222.spec",
    "rule_sanity": "basic"
}

I'm confused about two things:

1. Why isn't --dynamic_bound 1 taking effect? The behavior doesn't seem to change at all compared to using --auto_dispatcher alone.
2. Where is the disable_source_finders flag coming from? It's not in my config, but the warning suggests it's enabled. Could this be a default setting that's conflicting with dynamic_bound?

Any ideas on what might be going wrong here? Thanks for your help!

[naftali-g]

Ignore the warning, it's wrong.
Regarding the --dynamic_bound 1 not taking effect, I think it may be because of the of the proxy pattern you're using. The prover inlines the implementation of createBorrowOrder for the address of the newly created Order contract, but in practice the function is called on the new OrderProxy contract. I'm not sure, but maybe the --contract_extensions flag could help you here. See https://docs.certora.com/en/latest/docs/prover/cli/options.html#contract-extensions.

But the summarization option is probably simpler