Improve implication endpoint in booster

[goodlyrottenapple]

The recently merged implication endpoint in the booster is very conservative atm, especially when it comes to checking implication of the predicates. The current algorithm essentially just checks if the set of consequent predicates, minus the set of antecedent predicates all evaluate to true and aborts on any unknowns. In the next iteration, we should use the SMT solver to properly check implication of all thew predicates as a whole.

[ehildenb]

First we should measure what the effect is. Over the KEVM test-suite, for all the implications we do, how many and which ones fall back? What about for Kontrol? And for Kasmer?

We shouldn't speculatively implement any reasoning, it should all be motivated by data.

[goodlyrottenapple]

Yes, this is why we didn't include it in the initial PR, the current implementation seems to be able to handle at least 80% of the cases in KEVM and Kontrol. Just putting this here to track the (in)completeness of the current booster implementation.