search

runtimeverification / kontrol

BSD 3-Clause "New" or "Revised" License
55 stars 9 forks source link

Counter examples in Solidity #886

Open RaoulSchaffranek opened 4 days ago

RaoulSchaffranek commented 4 days ago

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 commented 2 days ago

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.