Unsatisfiable implication is returning substitution and predicate

[ehildenb]

It used to be that pyk was ignoring the value of satisfiable in the implies endpoint, but then it was fixed: https://github.com/runtimeverification/pyk/pull/216

But this is now causing problems in KEVM, because the implications that were considered successful before (because tehy had a substitution and predicate), are now being reported as unsuccessful.

Here is one such bug report: https://drive.google.com/file/d/16MrofCqXuyakhVwIq3aIciwuPv3CmLG4/view?usp=share_link

I'm pretty sure this implication does hold, so my guess is that it should just be returning satisfiable: "true" instead of false. Either that, or I need to understand why this implication doesn't hold.

In general, if satisfiable is false, then we probably should not return both a substitution and a predicate. Perhaps only a substitution, and #Bottom as the predicate makes sense though.

[ehildenb]

Before this is closed, we should make sure that https://github.com/runtimeverification/pyk/pull/229 is re-reverted.

[jberthold]

I reproduced the behaviour (satisfiable: false response) and inspected the request and response for some time, but could not find anything obviously wrong. 003-request-formatted.json 003-response-formatted.json.txt The conditions in the input and output (incl. the unifying substitution) are here in short form: conditions-from-json.txt. The code path that leads to the observed answer is taken only when a condition implication is refutable, but there is no obvious contradiction between these conditions together with the unifier.

[jberthold]

Further investigation of this implies request (incl. tracing and DebugEvaluateCondition) shows that the predicate which is later sent to the SMT solver (to refute it) contains the following:

                                        /* Spa */
                                        \not{_}(
                                            /* Sfa */
                                            \equals{SortBool{}, _}(
                                                /* T Fn D Sfa Cl */
                                                \dv{SortBool{}}("true"),
                                                /* T Fn D Sfa */
                                                Lbl'Hash'rangeUInt'LParUndsCommUndsRParUnds'WORD'Unds'Bool'Unds'Int'Unds'Int{}(
                                                    /* T Fn D Sfa Cl */
                                                    \dv{SortInt{}}("256"),
                                                    /* T Fn D Sfa Cl */
                                                    \dv{SortInt{}}("9223372036854775620")

which, in brief, is #not (#rangeUInt(256, 9223372036854775620)). This should probably be evaluated within Haskell since from the #rangeUInt definition this is clearly already false (0 <= 9223372036854775620 < 2 ^ 256). When this reaches the SMT solver, the #rangeUInt is gone and it is merely a boolean value, which could of course be assumed true by the SMT solver to satisfy the predicate as a whole.

[ana-pantilie]

@ehildenb the issue is that pyk is sending requests with Kore which has not been desugared correctly, see the definition of #rangeUInt: https://github.com/runtimeverification/evm-semantics/blob/master/include/kframework/word.md#range-of-types

[ehildenb]

Oh thank you guys for the investigation! I will try and make sure that predicates are desugared fully, and see if it's the same problem!