[Bug] [kompile] - Compilation fails for simplifications with #Exists on right-hand side

[PetarMax]

K Version

$ kompile --version
K version:    v5.3.98-5-g993674655
Build date:   Thu Jul 07 14:35:59 BST 2022

Description

Compilation fails for either of the following two simplification, which have the Matching-Logic #Exists on right-hand side:

rule { C #Equals { C }:>Int } => #Exists I1. { C #Equals I1:Int } [simplification]
rule { C #Equals { C }:>Int } => #Exists ?I1. { C #Equals ?I1:Int } [simplification]

Input Files

File exists-simpl.k, version 1:

module EXISTS-SIMPL-SYNTAX 
endmodule

module EXISTS-SIMPL

  rule { C #Equals { C }:>Int } => #Exists I1. { C #Equals I1:Int } [simplification, anywhere]

endmodule

File exists-simpl.k, version 2:

module EXISTS-SIMPL-SYNTAX 
endmodule

module EXISTS-SIMPL

  rule { C #Equals { C }:>Int } => #Exists ?I1. { C #Equals ?I1:Int } [simplification, anywhere]

endmodule

Reproduction Steps

Run: kompile exists-simpl.k --backend haskell

For version 1:

[Error] Compiler: Cannot encode equations with existential variables to KORE.
 If this is desired, please use #Exists with regular variables.
 Offending variables: [?I1]

For version 2:

[Error] Compiler: Found variable I1 on right hand side of rule, not bound on
left hand side. Did you mean "?I1"?
        Source(/Users/petarmax/Projects/RV/exists-simpl.k)
        Location(6,44,6,46)
        6 |       rule { C #Equals { C }:>Int } => #Exists I1. { C #Equals I1:Int }
[simplification]
```          .                                

Expected Behavior
-----------------

At least one of the two simplifications being allowed by the compiler.

[radumereuta]

Offending check is in ModuleToKORE
Is there something special about #Exists_._ that these checks should pay more attention to?

[PetarMax]

I'm not sure how to answer that. Perhaps that, unlike other ?X-type existentials, #Exists introduces the existential explicitly before using it?

[radumereuta]

I was hoping to get the opinion of @traiansf since he is the original developer of that check.
Or at least @ehildenb or @dwightguth.

[PetarMax]

Yes, definitely, I'm curious as well, I'm not quite understanding what's happening and why/why not.

[traiansf]

The rationale for disabling ? variables in equations was to prevent them being used by mistake in a function definition rule, as usually that would make the function non-functional. That is why the suggested alternative was to explicitly use #Exists instead.
Unfortunately, that conflicts with another check in CheckRHSVariables

I see, though, that CheckRHSVariables allows for the user to annotate some variables as unBound: unboundVariables. Maybe that could help? Or maybe we could automatically add the RHS-bound #Exists variables to be otherwise unbound?

[PetarMax]

My guess is that it should be fine to add explicit RHS-existentials to unboundVariables, but I don't have enough experience to properly assess and I'm not sure how big of a change that would be. Since it wasn't allowed until now, nothing should break?

[PetarMax]

Update: I've tried

rule { C:Constant #Equals { C }:>Int } => #Exists I. { C #Equals I:Int } [simplification, unboundVariables(I)]

and I get an error:

kore-exec: [1469469] Error (ErrorException):
    Could not make sort
        SortKItem{}
    match sort
        SortConstant{}
    This is a program bug!

Attaching the bug report...
kore-exec.tar.gz

[radumereuta]

Can you post the front-end input?
I'd like to have a look at the entire pipeline.

[ana-pantilie]

What's wrong with having rule lhs(X) => rhs(X, ?Y) requires req(X) ensures ens(X, ?Y) [simplification] translated to

rule \\implies(req(X), \\equals(lhs(X), \\exists(Y, \\and(rhs(X, Y), ens(X, Y))))

Ideally, we'd also support writing the ML version in K, without using that unboundVariables attribute. We should just take care to not combine ML syntax with question mark variables.

Now that we support simplification rules on other constructs like #Equals (and other ML connectives in the future), I think it would be sensible to fully support this feature. Thoughts?

[ehildenb]

I think the "free variable checker" probably has a bug. #Exists X . f(X) should not consider X to be a free variable, so the free variable on RHS checker shouldn't care about it.

[radumereuta]

The free variable checker should be aware of ML binders. #Exists and #Forall.
There might be a few things that break. We can decide what to do then.

[dwightguth]

@PetarMax is this still affecting you?