search

runtimeverification / haskell-backend

The symbolic execution engine powering the K Framework
BSD 3-Clause "New" or "Revised" License
210 stars 42 forks source link

Improve implication endpoint in booster #3854

Open goodlyrottenapple opened 6 months ago

goodlyrottenapple commented 6 months ago

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 commented 6 months ago

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 commented 6 months ago

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.