[RFC] Added findInputs function and checkAssertionsOrStop

[gustavo-grieco]

Description

I´m requesting comments and feedback regarding adding a findInputs function, which mirrors verify but instead focus on finding inputs given a postcondition.

There a few small changes and comments to discuss:

• I needed to use my own fetcher instead of selecting a particular RPC, so modified the input type. Perhaps we can do the same with verify to make it a bit more abstract.
• I reused the VeriOpts type for the options, but perhaps we should create another type or change the name to be more generic (e.g. "ExploreOpt"?)
• I added a variation of checkAssertions to allow to find inputs that are changing the state (to enhance the exploration of the fuzzer).
• I´m not sure if this function can benefit from Haskell lazyness but it can be a good idea to investigate a bit more. In theory, it should be possible to stop the exploration when an input was found, even if it is still exploring, simplifying or flattening. This is particularly interesting if you are looking for assertion failures, once you found one, you can just stop the exploration.
• In the near future, this function also receive a list of PCs or events collected in each path so it can select or avoid exploring certain paths.

Checklist

• tested locally
• added automated tests
• updated the docs
• updated the changelog

[msooseth]

Do I understand that this is basically tailored to find specific (set of) postcondition(s)? If so, then I think this could be very useful in some scenarios. Of course one could express these postconditions as asserts in the actual code. However, this could allow us to move towards a form of analysis where there are a number of predefined "bad states" that we want all contracts to avoid, such as e.g. funds being locked up. Then we could query that via this system as a postcondition. Although currently that would not be possible.