Booster RPC server deficiency related to isX sort predicates #4132
Description
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.