runtimeverification / kontrol

BSD 3-Clause "New" or "Revised" License
48 stars 5 forks source link

Slowdown detected for new versions of forge-std #534

Open anvacaru opened 5 months ago

anvacaru commented 5 months ago

Our current test-suite uses a hardcoded version of forge-std linked here, tagged by the hash 75f1746. After updating to the latest version, it seems that there is a ~72% slowdown.

To check this, I've used the project that gets created with kontrol init, but I've tweaked the test below to use assert instead of assertEq.

    function test_Increment() public {
        counter.increment();
        assert(counter.number() == 1);
    }

Using the master branch of kontrol (v0.1.256), I've ran the test with both forge-std libraries. forge-std version: "1.8.1": 55s forge-std version: "1.6.0": 32s

I have the bug-report tar for the proof that has the slowdown (we-transfer link here as the file has 155 MB)

anvacaru commented 1 month ago

I investigated a bit the CounterTest example using the "old" v1.6.0 version of forge-std that we are using in our test project and the latest one, v1.9.2:

In addition to this, I ran a setUp and a proof from the ongoing engagement and the times are:

At this point, I think this is just an overhead caused by the codebase changes in forge-std. I'm not sure why the kore server start takes longer; one educated guess is that it is because of the library's larger codebase.

The Solidity files that are part of the lib are

./src/interfaces/IERC4626.sol
./src/interfaces/IERC165.sol
./src/interfaces/IERC721.sol
./src/interfaces/IERC1155.sol
./src/interfaces/IERC20.sol
./src/interfaces/IMulticall3.sol
./src/StdInvariant.sol
./src/StdJson.sol
./src/console.sol
./src/Base.sol
./src/StdStorage.sol
./src/StdChains.sol
./src/Vm.sol
./src/StdMath.sol
./src/StdAssertions.sol
./src/StdStyle.sol
./src/StdError.sol
./src/StdUtils.sol
./src/StdCheats.sol
./src/StdToml.sol
./src/Script.sol
./src/console2.sol
./src/safeconsole.sol
./src/mocks/MockERC721.sol
./src/mocks/MockERC20.sol
./src/Test.sol
./test/StdMath.t.sol
./test/StdChains.t.sol
./test/StdToml.t.sol
./test/StdStorage.t.sol
./test/Vm.t.sol
./test/StdJson.t.sol
./test/StdAssertions.t.sol
./test/StdCheats.t.sol
./test/compilation/CompilationScript.sol
./test/compilation/CompilationTestBase.sol
./test/compilation/CompilationTest.sol
./test/compilation/CompilationScriptBase.sol
./test/mocks/MockERC20.t.sol
./test/mocks/MockERC721.t.sol
./test/StdError.t.sol
./test/StdUtils.t.sol
./test/StdStyle.t.sol

One suggestion that @PetarMax had was to add a new flag for kontrol build to ignore certain .sol files such as ./test/*, ./mocks/*, ./src/console2.sol, ./src/StdChains.sol from the build process.

PetarMax commented 1 month ago

On the other hand, the overhead seems to be constant (~1 minute), however, so we could live with it?

palinatolmach commented 1 month ago

Thanks @anvacaru! Agreed, I think, to start with, we can just bump the version and maybe slightly increase the CI timeout, as @anvacaru suggested. Maybe we can check with the backend team on what can make the server start slower?

But, separately, ignoring files from seemingly irrelevant folders might still be useful (e.g., I was also wondering whether we can automatically skip files from lib/x/test, since they tend get large for some projects but are usually not used directly).

PetarMax commented 1 month ago

While we're on the timeout increase topic, could we increase the SMT timeout to, say, 60 seconds, and check if that's what is causing the ever-present flakiness? :)