Booster RPC server deficiency related to `isX` sort predicates

[jberthold]

When the booster RPC server evaluates function nests in side conditions that involve sort predicates (isX for a sort X), nested function calls are not evaluated further. This can lead to wrong rewriting results.

The K module below rewrites from Run(I:Int) to Done(I) if lookup(Wrap(I)) is of sort Value.
The lookup function evaluates to a call of lookup0 after unwrapping the Wrap(I:Int), and lookup0(42) is Integer(42).

module TEST
  imports BOOL
  imports INT

  // sorts involved
  syntax Evaluation ::= Value | Stuff
  syntax Value ::= Integer ( Int ) [symbol(Integer)]
  syntax Stuff ::= Stuff()         [symbol(Stuff)]
  syntax Wrap ::= Wrap ( Int )     [symbol(Wrap)]

  // lookup function, two-stage
  // upper level, dispatching
  syntax Evaluation ::= lookup ( Wrap ) [function, total, symbol(lookup), no-evaluators]
  //        The no-evaluators here leads to the HS backend evaluating it  ^^^^^^^^^^^^^
  rule [dispatch]: lookup(Wrap(N)) => lookup0(N) requires N %Int 1 ==Int 0

  syntax Evaluation ::= lookup0 ( Int ) [function, total, symbol(lookup0)]
  // ----------------------------------------------------
  rule [notfound]: lookup0(_N) => Stuff() [owise]
  rule [target]:   lookup0(42) => Integer(42)

  // test harness
  syntax KItem ::= Run ( Int )    [symbol(Run)]
                 | Done ( Value ) [symbol(Done)]
                 | Fail ( Int )   [symbol(Fail)]

  rule [run-done]: Run(I) => Done(Integer(I)) requires isValue( lookup(Wrap(I)) )
  rule [run-fail]: Run(I) => Fail(I) [owise]

endmodule

When evaluating Run(42), the result should be Done(42) because lookup(Wrap(42)) =eval=> lookup0(42) =eval=> Integer(42). However, when running the evaluation as an RPC request, it results in Fail(42).

jost@freshcode-1:scratch/not-a-value-or-what$ kore-rpc-booster test-kompiled/definition.kore  --module TEST &
[1] 53145
[proxy] Loading definition from test-kompiled/definition.kore, main module "TEST"
jost@freshcode-1:scratch/not-a-value-or-what$ [kore][info] Reading the input file TimeSpec {sec = 0, nsec = 385027}
[kore][info] Parsing the file TimeSpec {sec = 0, nsec = 145}
[kore][info] Verifying the definition TimeSpec {sec = 0, nsec = 150}
[kore][info] Executing TimeSpec {sec = 0, nsec = 28584657}
[kore][info] Reading the input file TimeSpec {sec = 0, nsec = 404938}
[kore][info] Parsing the file TimeSpec {sec = 0, nsec = 113}
[kore][info] Verifying the definition TimeSpec {sec = 0, nsec = 148}
[proxy] Starting RPC server
jost@freshcode-1:scratch/not-a-value-or-what$
jost@freshcode-1:scratch/not-a-value-or-what$ kore-rpc-client execute run-42.json | jq .result.state.term | haskell-backend/.build/kore/bin/pretty test-kompiled/definition.kore /dev/stdin
[Info] Preparing request data
[Info] Sending request run-42.json...
[proxy] Processing request 1
[Info] Response received.
[Info] Round trip time for request 'run-42.json' was 199.082375 ms

Pretty-printing pattern:
<generatedTop>(<k>(kseq(Fail("42"), dotk)), <generatedCounter>("0"))
Bool predicates: -
Ceil predicates: -
Substitution:

jost@freshcode-1:scratch/not-a-value-or-what$ fg
kore-rpc-booster test-kompiled/definition.kore --module TEST
^C[proxy] Server shutting down
jost@freshcode-1:scratch/not-a-value-or-what$ krun -cPGM="Run(42)"
<k>
  Done ( Integer ( 42 ) ) ~> .K
</k>

krun evaluates it correctly, the problem is in the booster evaluation.
The root cause of the problem is that booster's matching algorithm finds the function call has supersort Evaluation > Value, and booster prematurely discards the equation that could match after evaluation, concluding isValue(lookup0(42)) => false.