[Bug] [kompile] - Failure to match variable in depth 2 context after substitution

K Version

$ kompile --version
K version:    5.1.152
Build date:   Mon Aug 23 13:06:14 CDT 2021

Description

In a pi calculus variant, a quoted process gets substituted for a variable. A subsequent pattern match on a depth-2 context fails.

The particular rules of interest are these: when I encounter a term in the list of terms of the form *(name), I store the name in the <derefs> section, and when I find a name that is a referenced process (a depth-1 context), I remove the ampersand and put it in the k cell.

rule
    <k> *(Nm:N) | Ts:Terms => Ts </k>
    <derefs> (Ds) => (Ds <deref> Nm </deref>) </derefs>

rule
    <deref> &(P) => . </deref>
    <k> .Terms => P </k>

The program gets stuck when I use these rules instead: when I encounter a Deref in the list of terms (which by construction can only be of the form *(name)), I store it as-is in the <derefs> section, and when I find a name that is a dereferenced referenced process (a depth-2 context), I remove both the asterisk and the ampersand and put it in the k cell.

rule
    <k> D:Deref | Ts:Terms => Ts </k>
    <derefs> (Ds) => (Ds <deref> D </deref>) </derefs>

rule
    <deref> *(&(P)) => . </deref>
    <k> .Terms => P </k>

Note that both ways of writing the rules work on lists that are parsed directly as part of the source code. The second pair only seems to fail when the list is the result of a substitution.

Working rho.k file:

require "substitution.md"

module RHO-SYNTAX
    imports DOMAINS-SYNTAX
    imports KVAR-SYNTAX

  syntax N ::= "&" "(" Terms ")"
               | KVar

  syntax Zero   ::= "Z"
  syntax In     ::= "in" "(" KVar "<-" N "." Terms ")" [binder]
  syntax Out    ::= "out" "(" N "," Terms ")"
  syntax Deref  ::= "*" "(" N ")"
  syntax Term   ::= Zero
                    | In
                    | Out
                    | Deref

  syntax Terms ::= List{Term, "|"}
  syntax Terms ::= Terms "++Terms" Terms [function, functional, left, avoid]

endmodule

module RHO
  imports RHO-SYNTAX
  imports SUBSTITUTION

  syntax KResult ::= Terms

  configuration <T>
    <zeros><zero multiplicity="*" type="Set"> . </zero></zeros>
    <ins><in multiplicity="*" type="Set"> . </in></ins>
    <outs><out multiplicity="*" type="Set"> . </out></outs>
    <derefs><deref multiplicity="*" type="Set"> . </deref></derefs>
    <k> $PGM:Terms </k> </T>

  rule (S1 | S1s) ++Terms S2s => S1 | (S1s ++Terms S2s)
  rule .Terms ++Terms S2s => S2s

  rule
    <k> Zo:Zero | Ts:Terms => Ts </k>
    <zeros> (Zs) => (Zs <zero> Zo </zero>) </zeros>

  rule
    <k> I:In | Ts:Terms => Ts </k>
    <ins> (Is) => (Is <in> I </in>) </ins>

  rule
    <k> O:Out | Ts:Terms => Ts </k>
    <outs> (Os) => (Os <out> O </out>) </outs>

  rule
    <k> *(Nm:N) | Ts:Terms => Ts </k>
    <derefs> (Ds) => (Ds <deref> Nm </deref>) </derefs>

  rule
    <zero> _:Zero => . </zero>

  rule
    <in> in (Y <- X . Ts:Terms ) => . </in>
    <out> out(X , P:Terms) => . </out>
    <k> .Terms => Ts[&(P) / Y] </k>

  rule
    <deref> &(P) => . </deref>
    <k> .Terms => P </k>

endmodule

Expected Behavior

The variable P should bind to the list of terms in the context *(&(P)).

Test programs:

test1.rho out(x, Z) | in(y <- x.*(y)) Should result in an empty derefs cell. In the non-working case, I get <deref> *(&(Z | .Terms)) </deref>. In the working case, I get an empty derefs cell.

test2.rho *(&(Z)) Should result in an empty derefs cell. In both the working and non-working cases, it does result in an empty derefs cell, suggesting that the problem only manifests when there is a substitution.

runtimeverification / llvm-backend