[K-Bug] #Equals of #Equals produces invalid kore

[virgil-serbanuta]

What component is the issue in?

Front-End

Which command

• kompile
• kast
• krun
• kprove
• kprovex
• ksearch

What K Version?

v6.0.57-0-ga91e8fd25a-dirty

Operating System

Linux

K Definitions (If Possible)

module A-SYNTAX
  imports BOOL
  syntax A ::= "a" | "b"
endmodule

module A
  import A-SYNTAX
  import INT

  syntax Int ::= #bool(Bool)  [function, total]
  rule #bool(true) => 1
  rule #bool(false) => 0

  rule a => b
    requires true
        #And { { 0 #Equals #bool(B:Bool) } #Equals {false #Equals B} }
endmodule

Steps to Reproduce

$ kompile a.k --backend haskell
kore-exec: [100320] Error (ErrorVerify):
    Error:
      module 'A':
      axiom declaration:
      \rewrites (definition.kore 715:21):
      \and (definition.kore 716:12):
      \equals (definition.kore 718:28):
      \and (definition.kore 719:14):
      \equals (definition.kore 719:63):
      (definition.kore 719:58):
        Sort variable Q10 not declared.
Created bug report: kore-exec.tar.gz
[Error] Critical: Haskell backend reported errors validating compiled
definition.
Examine output to see errors.

Expected Results

The source above should just compile. If that's unfeasible, #Iff should be available (it does not show up in kast.md).

[gtrepta]

Is this another problem with the type inferencer, @radumereuta? It complains Sort variable Q10 not declared., but the generated rule has the attribute sortParams({Q10})

The kore term that gets generated:

\equals{SortBool{},SortGeneratedTopCell{}}(
    \and{SortBool{}}(                                                                                                                                                                                                                           \dv{SortBool{}}("true"),                                                                                                                                                                                                                \equals{Q10, SortBool{}}(
            \equals{SortInt{}, Q10}(
                \dv{SortInt{}}("0"),
                Lbl'Hash'bool'LParUndsRParUnds'A'Unds'Int'Unds'Bool{}(VarB:SortBool{})
            ),
            \equals{SortBool{}, Q10}(
                \dv{SortBool{}}("false"),
                VarB:SortBool{}
            )
        )
    ),
    \dv{SortBool{}}("true")
)

[radumereuta]

Ah, I missed this issue. Thank you for adding it to the board.
@virgil-serbanuta can you please add the issues you post in the K repo to the K Development board? Just to make sure we don't miss it.

@gtrepta I'm not sure. It might be an issue with ModuleToKore. This needs more investigation.

[radumereuta]

Try to fix the generated file and see if it passes.
Then we can see if we can fix it when it's being generated.

[gtrepta]

I tried changing Q10 to SortK{} and kore-exec stopped complaining about it. I wasn't able to get a full run of it though because the example produced in kore-exec.tar.gz doesn't have an argument for --pattern which kore-exec requires.

[radumereuta]

Check again when we make more progress on: #3601