Solidity's model checker basic options

[leonardoalt]

Not sure if this is wanted, but I think it would be cool to have direct access to Solidity's model checker via the Foundry options. This is basically what I'm running locally.
The options are opt-in and not there by default, so it shouldn't bother the default case and Foundry users who don't explicitly add it.

Description

This PR adds the minimum required options to foundry.toml (as opt-in) that enable Soldity's model checker.

Motivation

Solidity has a built-in model checker that can be easy to use on OSX and Linux (the latter needs z3 <=4.8.14 installed system-wide) via compiler options.

Solution

The options were added based on a subset of the tools options. For now only the essential options were added, but the rest (such as divModNoSlack and invariants) can easily be added afterwards.

This PR depends on its corresponding ethers-rs PR (gakonst/ethers-rs#1258), and the first commit here points to that PR's branch to show how the integration works, and would be removed if/when that PR is merged.

Example

The feature this PR enables is represented below.

Let src/Contract.sol be the following code, which you want to verify:

// SPDX-License-Identifier: UNLICENSED
pragma solidity ^0.8.13;

contract Contract {
	uint x;

	function inc() public {
		++x;
	}

	function inv(uint y) public view {
		require(y > 2);
		assert(x <= y);
	}
}

This is added to foundry.toml:

[default.model_checker]
contracts = { '/path/to/project/src/Contract.sol' = [ 'Contract' ] }
engine = 'chc'
timeout = 10000

Result of forge build:

[⠆] Compiling...
[⠑] Compiling 2 files with 0.8.13
[⠘] Solc 0.8.13 finished in 332.19ms
Compiler run successful (with warnings)
warning[6328]: Warning: CHC: Assertion violation happens here.
Counterexample:
x = 4
y = 3

Transaction trace:
Contract.constructor()
State: x = 0
Contract.inc()
State: x = 1
Contract.inc()
State: x = 2
Contract.inc()
State: x = 3
Contract.inc()
State: x = 4
Contract.inv(3)
  --> /path/to/project/src/Contract.sol:13:3:
   |
13 | 		assert(x <= y);
   | 		^^^^^^^^^^^^^^

[mattsse]

this looks great,

thanks for the docs!

[mattsse]

I see, will check the basepath setting and make them relative from root

[mattsse]

another way to get this supported without basePath would be updating the paths in Config::canonic_at

[leonardoalt]

Ah, the current version already works. The user just needs to add the absolute path for now, but works.

[gakonst]

LGTM - let's follow up on the absolute -> Relative paths separately - cc @mattsse

[leonardoalt]

just fixed fmt