Counter examples in Solidity

[RaoulSchaffranek]

It would be very cool if Kontrol could generate executable counter-examples. Here is a small example:

function prove_foo(uint256 bar) {
    assert(bar != 0xC0FFEE);
}

Kontrol fails and gives us a counter-example with bar = 0xC0FFEE. It would be even nicer if Kontrol could generate an executable unit test like this:

function prove_foo_1() {
    prove_foo(0xC0FFEE);
}

If we can make the generated test fully concrete and self-contained, it would make an excellent entry point for Simbolik, and it can be easily added as a regression test to CI.

[palinatolmach]

Agreed, thanks @RaoulSchaffranek! It would also make it easier to integrate Kontrol with third-party tools like https://getrecon.xyz/.

The only challenge I see is related to mapping Kontrol cheatcodes to Foundry (there're not many incompatible ones now, and we can come up with translation rules) and, mainly, concretizing/setting up symbolic storage — right now, we don't concretize the storage entries.