Cannot test simplifications with ML connectives

[PetarMax]

K Version

$ kompile --version

K version:    v5.3.82-4-g7171a25cd
Build date:   Fri Jun 24 15:50:36 BST 2022

Description

kore-exec throws error when attempting to test a simplification that uses ML connectives (e.g. #Equals instead of ==Int).

Input Files

ml-conn.k:

module ML-CONN-SYNTAX
    imports INT-SYNTAX
    imports ML-SYNTAX

    syntax Int ::= #foo (Int , Int) [function, no-evaluators]
endmodule

module ML-CONN
    imports ML-CONN-SYNTAX
    imports INT

    configuration
      <k> #Top </k>

    rule { A #Equals #foo(B, C) } => { A *Int B #Equals B +Int C } [simplification] 
endmodule

ml-conn-test.k:

requires "ml-conn.k"

module ML-CONN-TEST
    imports ML-CONN

    claim <k> { A #Equals #foo(B, C) } => { A *Int B #Equals B +Int C } ... </k>
endmodule

Reproduction Steps

kompile --backend haskell ml-conn.k
kprove ml-conn-test.k   

Output:

kore-exec: [105397] Error (ErrorException):
    The check implication step expects the configuration term to be function-like.
      Configuration term:
        /* D Sfa */
        Lbl'-LT-'generatedTop'-GT-'{}(
            /* D Sfa */
            Lbl'-LT-'k'-GT-'{}(
                /* D Sfa */
                kseq{}(
                    /* D Sfa */ \top{SortKItem{}}(),
                    /* Fl Fn D Sfa */ ConfigVar'Unds'DotVar1:SortK{}
                )
            ),
            /* Fl Fn D Sfa */
            Lbl'-LT-'generatedCounter'-GT-'{}(
                /* Fl Fn D Sfa */ ConfigVar'Unds'DotVar2:SortInt{}
            )
        )
    CallStack (from HasCallStack):
      error, called at src/Kore/Reachability/Claim.hs:499:9 in kore-0.60.0.0-AfDbhwdKwsp4a4wsGSYVve:Kore.Reachability.Claim
      assertFunctionLikeConfiguration, called at src/Kore/Reachability/Claim.hs:607:13 in kore-0.60.0.0-AfDbhwdKwsp4a4wsGSYVve:Kore.Reachability.Claim
Created bug report: kore-exec.tar.gz
  <k>
    #Top ~> _DotVar1 ~> .
  </k>
#And
  {
    B +Int C
  #Equals
    A *Int B
  }

Bug report: kore-exec.tar.gz

Expected Behavior

Claim passing, with the <k>-cell holding the rhs of the simplification in the final configuration.

[ana-pantilie]

This should be supported once https://github.com/runtimeverification/k/issues/2491 is done.

[goodlyrottenapple]

@goodlyrottenapple @ana-pantilie add a note on the possible ambiguity of => in a claim, i.e. it could be an implication or a reachability, which desugar into different things in kore. Is this a potential issue?

[ana-pantilie]

@goodlyrottenapple @radumereuta The frontend needs to apply the same kinds of constraints to these non-reachability claims it does to simplification rules. What is not allowed in simplification rules, shouldn't be allowed in non-reachability claims. I would assume that ambiguity isn't an issue in this case, right?

Also, I don't like "non-reachability" as a name, @JKTKops suggested "equational claims", which I think is good?

[goodlyrottenapple]

@ana-pantilie Would they use = instead of =>? With calling them equational, we imply they are symmetric (which in theory they are) but I'm assuming we want to use them directionally in other claims as rule ... [simplification]?

[ana-pantilie]

Simplification rules currently use =>, so I'm guessing that we'd want to preserve that in the claims as well.

[ana-pantilie]

Duplicate of #3010.