Polymorphic symbols not sent to solver

[daejunpark]

An infeasible stuck state contains the following, which should have been evaluated to #Bottom. Why does this happen, while z3 should be able to refute this easily?

#And
  {
    999999861 <Int #if N ==Int 5 orBool notBool N ==Int N #then 800 #else #if N ==Int 0 #then 20000 #else 5000 #fi #fi
  #Equals
    true
  }

NOTE: This is a blocking issue for https://github.com/kframework/evm-semantics/issues/858.

[daejunpark]

To reproduce:

1. run kore-repl against: https://github.com/kframework/evm-semantics/blob/kore-issue-1962/tests/specs/benchmarks/storagevar01-spec.k

2. step 1000; select 414; step; graph will show you this graph, where the node 417 is the result of applying the following rule:

   rule <k>  G:Int ~> #deductGas => #end EVMC_OUT_OF_GAS ... </k> <gas> GAVAIL </gas> requires GAVAIL <Int G

   Note that the above rule should not have been applied because GAVAIL <Int G is false in the current term.

3. konfig-n 417 prints this output, which should have been evaluated to #Bottom.

[ttuegel]

Note that the above rule should not have been applied because GAVAIL <Int G is false in the current term.

This is the real problem: the side condition was not refuted before the rule was applied. Could you please run this step of the proof with --log-entries DebugEvaluateCondition so we can see the exact condition sent to the solver?

[daejunpark]

run this step of the proof with --log-entries DebugEvaluateCondition

Do you mean run the single step from node 414 to 417 via axiom 271 (the infeasible path) inside kore-repl with log [DebugEvaluateCondition] enabled? I'll do that.

[daejunpark]

@ttuegel This log.txt is the output obtained by:

step 1000
select 414
log [DebugEvaluateCondition] file log.txt
step

Let me know if this is what you're looking for. Also, I'd appreciate it if you can tell me how to read this log. :)

[daejunpark]

@ttuegel This log is the output by log [DebugSolverSend,DebugSolverRecv,DebugEvaluateCondition] at the same step.

When I searched 999999861 in the log, I can see the following kore term (which corresponds to 999999861 <Int #if N ==Int 5 orBool notBool N ==Int N #then 800 #else #if N ==Int 0 #then 20000 #else 5000 #fi #fi, right?):

            /* Sfa */
            \equals{SortBool{}, SortGeneratedTopCell{}}(
                /* Fl Fn D Sfa */
                Lbl'Unds-LT-'Int'Unds'{}(
                    /* Fl Fn D Sfa Cl */
                    /* builtin: */ \dv{SortInt{}}("999999861"),
                    /* Fl Fn D Sfa */
                    Lbl'Hash'if'UndsHash'then'UndsHash'else'UndsHash'fi'Unds'K-EQUAL-SYNTAX'Unds'Sort'Unds'Bool'Unds'Sort'Unds'Sort{SortInt{}}(
                        /* Fl Fn D Sfa */
                        Lbl'Unds'orBool'UndsUnds'BOOL'Unds'Bool'Unds'Bool'Unds'Bool{}(
                            /* Fl Fn D Sfa */
                            Lbl'UndsEqlsEqls'Int'Unds'{}(
                                /* Fl Fn D Sfa */ VarN:SortInt{},
                                /* Fl Fn D Sfa Cl */
                                /* builtin: */ \dv{SortInt{}}("5")
                            ),
                            /* Fl Fn D Sfa */
                            LblnotBool'Unds'{}(
                                /* Fl Fn D Sfa */
                                Lbl'UndsEqlsEqls'Int'Unds'{}(
                                    /* Fl Fn D Sfa */ VarN:SortInt{},
                                    /* Fl Fn D Sfa */ VarN:SortInt{}
                                )
                            )
                        ),
                        /* Fl Fn D Sfa Cl */
                        /* builtin: */ \dv{SortInt{}}("800"),
                        /* Fl Fn D Sfa */
                        Lbl'Hash'if'UndsHash'then'UndsHash'else'UndsHash'fi'Unds'K-EQUAL-SYNTAX'Unds'Sort'Unds'Bool'Unds'Sort'Unds'Sort{SortInt{}}(
                            /* Fl Fn D Sfa */
                            Lbl'UndsEqlsEqls'Int'Unds'{}(
                                /* Fl Fn D Sfa */ VarN:SortInt{},
                                /* Fl Fn D Sfa Cl */
                                /* builtin: */ \dv{SortInt{}}("0")
                            ),
                            /* Fl Fn D Sfa Cl */
                            /* builtin: */ \dv{SortInt{}}("20000"),
                            /* Fl Fn D Sfa Cl */
                            /* builtin: */ \dv{SortInt{}}("5000")
                        )
                    )
                ),
                /* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortBool{}}("true")
            ),

and the following (part of) z3 query:

(= (< 999999861 <3> ) true )

But I cannot find the definition of <3> anywhere. It seems that the #if-#then-#else term is NOT encoded in z3. Am I right? If so, why does that happen?

[ttuegel]

But I cannot find the definition of <3> anywhere. It seems that the #if-#then-#else term is NOT encoded in z3. Am I right? If so, why does that happen?

Yes, it seems that #if _ #then _ #else _ isn't encoded for the solver. I think that this is not encoded because the Kore symbol is sort-parametric, and the encoding of such symbols is not handled in the backend, but I can't figure out why it isn't throwing an error.

[daejunpark]

@ttuegel Hmm, it is sort-parametric, but it is smt-hook'ed to ite that is polymorphic, so in this particular case, it should not be hard to encode in z3. This problem will happen for all smart contracts that update the storage. Indeed, any non-toy smart contract updates the storage. So, this is really a blocking issue.

How hard it will be to fix this? It may not need to be necessarily general for arbitrary sort-parametric symbols, but work only for this kind of specific ones that are smt-hooked to a polymorphic symbol. Or, just for this if-then-else term, which is special enough like the equality term (==K).

[ttuegel]

Indeed, the backend does not send parameterized symbols to the solver: https://runtimeverification.slack.com/archives/CC360GUTG/p1594242312276600

How hard it will be to fix this? It may not need to be necessarily general for arbitrary sort-parametric symbols, but work only for this kind of specific ones that are smt-hooked to a polymorphic symbol.

I'm not sure we can solve this for arbitrary parametric symbols because SMT-LIB doesn't allow parametric user-defined symbols at all. However, that should not be a problem for smt-hook symbols. Let me outline what I think we need to do:

1. resolveIndirectSymbolDeclaration should not resolve the argument sorts of the smt-hook symbol. The symbol is already declared outside the backend, and therefore so is its signature.
2. Alone, the change above will trigger this error. Check that this is the case!
3. SMT-LIB symbols don't have explicit sort parameters, so there is no need to send the Kore sort parameters to the solver. emptySortArgsToSmt can ignore the sort parameter list and return the representation directly, that is: make its second case the same as the first.

[daejunpark]

It makes sense that encoding arbitrary parametric symbols in SMT-LIB would be hard, but encoding smt-hook symbols would be doable. Indeed, I think the smt-hook symbol encoding process could be made straightforward, because it is the user's responsibility to use the smt-hook attribute properly. (I couldn't understand your detailed development plan, but hope that it is in the same line of thought.)

[ttuegel]

@dwightguth reported to me that this issue has resurfaced.