k: [Bug] [kprovex] - Fails with cryptic error message when backend fails

K Version

Tell us what version of K you are using.

Example:

+ kompile --version
K version:    v5.1.208-2-g264c3af2b2
Build date:   Fri Oct 01 16:39:34 UTC 2021

Description

Running kprove where the LHS of the <k> cell looks like claim <k> (SOMETHING ~> _ => .) ... </k> causes a cryptic failure in the frontend with the backends output.

Input Files

File: test.k:

requires "domains.md"

module TEST
    imports MAP
    imports BOOL

    syntax Foo ::= "a" | "b" | "c"
 // ------------------------------
    rule <k> a => b ... </k>

endmodule

module TEST-SPEC
    imports TEST

    claim <k> (a ~> _ => .) ... </k>
 
endmodule

Reproduction Steps:

Run kompile:

+ kompile --main-module TEST --backend haskell test.k
[Warning] Compiler: Could not find main syntax module with name TEST-SYNTAX in
definition.  Use --syntax-module to specify one. Using TEST as default.

Run kprovex:

+ kprovex test.k --spec-module TEST-SPEC --debug
kore-exec: [221324] Warning (WarnStuckClaimState):
    (InfoReachability) while checking the implication:
    The proof has reached the final configuration, but the claimed implication is not valid. Location: /home/dev/src/k/test.k:16:11-16:37
java.util.NoSuchElementException: key not found: append
        at scala.collection.MapLike.default(MapLike.scala:232)
        at scala.collection.MapLike.default$(MapLike.scala:231)
        at scala.collection.AbstractMap.default(Map.scala:59)
        at scala.collection.MapLike.apply(MapLike.scala:141)
        at scala.collection.MapLike.apply$(MapLike.scala:140)
        at scala.collection.AbstractMap.apply(Map.scala:59)
        at org.kframework.unparser.KPrint$2.apply(KPrint.java:302)
        at org.kframework.unparser.KPrint$2.apply(KPrint.java:296)
        at org.kframework.kore.KTransformer.apply(transformers.scala:11)
        at org.kframework.kore.KTransformer.apply$(transformers.scala:10)
        at org.kframework.kore.AbstractKTransformer.apply(transformers.scala:123)
        at org.kframework.kore.TransformK.apply(TransformK.java:76)
        at org.kframework.kore.TransformK.apply(TransformK.java:15)
        at org.kframework.kore.KTransformer.apply(transformers.scala:15)
        at org.kframework.kore.KTransformer.apply$(transformers.scala:10)
        at org.kframework.kore.AbstractKTransformer.apply(transformers.scala:123)
        at org.kframework.kore.TransformK.apply(TransformK.java:23)
        at org.kframework.unparser.KPrint$2.apply(KPrint.java:314)
        at org.kframework.unparser.KPrint$2.apply(KPrint.java:296)
        at org.kframework.kore.KTransformer.apply(transformers.scala:11)
        at org.kframework.kore.KTransformer.apply$(transformers.scala:10)
        at org.kframework.kore.AbstractKTransformer.apply(transformers.scala:123)
        at org.kframework.kore.TransformK.apply(TransformK.java:23)
        at org.kframework.unparser.KPrint$2.apply(KPrint.java:314)
        at org.kframework.unparser.KPrint$2.apply(KPrint.java:296)
        at org.kframework.kore.KTransformer.apply(transformers.scala:11)
        at org.kframework.kore.KTransformer.apply$(transformers.scala:10)
        at org.kframework.kore.AbstractKTransformer.apply(transformers.scala:123)
        at org.kframework.unparser.KPrint$2.apply(KPrint.java:307)
        at org.kframework.unparser.KPrint$2.apply(KPrint.java:296)
        at org.kframework.kore.KTransformer.apply(transformers.scala:11)
        at org.kframework.kore.KTransformer.apply$(transformers.scala:10)
        at org.kframework.kore.AbstractKTransformer.apply(transformers.scala:123)
        at org.kframework.unparser.KPrint.sortCollections(KPrint.java:316)
        at org.kframework.unparser.KPrint.abstractTerm(KPrint.java:199)
        at org.kframework.unparser.KPrint.prettyPrint(KPrint.java:122)
        at org.kframework.unparser.KPrint.prettyPrint(KPrint.java:114)
        at org.kframework.unparser.KPrint.prettyPrint(KPrint.java:110)
        at org.kframework.kprovex.KProve.run(KProve.java:90)
        at org.kframework.kprovex.KProveFrontEnd.run(KProveFrontEnd.java:58)
        at org.kframework.main.FrontEnd.main(FrontEnd.java:57)
        at org.kframework.main.Main.runApplication(Main.java:118)
        at org.kframework.main.Main.runApplication(Main.java:108)
        at org.kframework.main.Main.main(Main.java:56)
[Error] Internal: Uncaught exception thrown of type NoSuchElementException
(NoSuchElementException: key not found: append)

This is happenning in the sort collections pass in the term printing it looks like: https://github.com/kframework/k/blob/master/kernel/src/main/java/org/kframework/unparser/KPrint.java#L302. Indeed, if I add --no-sort-collections, to kprovex, the error changes to a different location (in KOREToTreeNodes).

Expected Behavior

Either this should be an error in the original proof (maybe there is something weird happenning with parsing I don’t understand?), or we should be able to handle this case and get a counterexample state.