Invalid variable names created by internalized rules

[nwatson22]

I stumbled across a case where a Rule# prefix is seemingly being appended to the beginning of a variable name for the generatedCounter cell possibly caused by using a claim as a lemma (the last request/response in this bug report). Is this a genuine bug? See runtimeverification/pyk#959

<generatedCounter> in the response looks like this:

                  {
                     "tag":"App",
                     "name":"Lbl'-LT-'generatedCounter'-GT-'",
                     "sorts":[
                        
                     ],
                     "args":[
                        {
                           "tag":"EVar",
                           "name":"Rule#Var'QuesUnds'GENERATEDCOUNTER'Unds'CELL'Unds'6de8d71b",
                           "sort":{
                              "tag":"SortApp",
                              "name":"SortInt",
                              "args":[
                                 
                              ]
                           }
                        }
                     ]
                  }

Executing with the legacy backend yields the same variable name Var'QuesUnds'GENERATEDCOUNTER'Unds'CELL'Unds'6de8d71b without the Rule# prefix.

[goodlyrottenapple]

It appears we expect existential variables (i.e. ones that appear on the rhs of a rule but not on the lhs to be explicitly quantified with an \exists. We track these existentials and give them a fresh name when applying a rule, which obviously doesn't happen here and ends up leaking the internal name instead. I think the correct thing here would be for the booster to reject the incorrect rule and for pyk to emit the correct form of the rule?

[ehildenb]

This sounds like a bug in pyk to me? Maybe the path forward is:

• The booster should error out on this.
• Pyk should build the correct rule.

Let's merge the fix to pyk before merging the fix to booster, and don't merge booster until it's tested downstream. This could cause a merge logjam.

[nwatson22]

I think the issue is in krule_to_kore which doesn't yet support existential variables yet. I talked to @tothtamas28 about the pyk side of this, and it sounds like he's planning to expand the kore generation in a more structured way that would encompass this, so I'm thinking it's probably not useful to fix this one case by itself right now.