A Specification of KORE

[gtrepta]

The current state of documentation for the semantics of KORE seems to be a scattering of .md files and code/comments in the Haskell/LLVM backends and the Java frontend.

A monolithic specification of KORE could make a common reference point for backend/frontend implementations, ML/Proof Object generation, and make change proposals easier to define (such as those in #3306).

The best place to start pulling from might be the docs folder in the Haskell backend.

[ana-pantilie]

I agree, we definitely need to create a formal document for Kore's semantics. As far as I know, there is unfortunately a lot of hidden complexity behind generating Kore which is buried deep within https://github.com/runtimeverification/k/blob/master/kernel/src/main/java/org/kframework/backend/kore/ModuleToKORE.java.

Maybe it would be easier to first simplify the language and reimplement ModuleToKore in a more principled way. @radumereuta, what are your thoughts?

[amelieled]

What's about this document: https://hal.inria.fr/hal-03895834/?

(chapter 3)

[radumereuta]

ModuleToKORE.java is very large for a few reasons:

• we generate text. That is verbose.
• we generate the kore for both llvm and haskell backends. A bunch of ifs.
• lots of corner cases.

One way I can think of making this step more principled is to decouple the text generation from the transformation front-end data structures to KORE. That means we will have to implement and maintain a KORE representation in the front end.

Maybe that can make the complex transformation more compact and readable, but it's going to make it harder to interleave comments. We use those a lot to keep track of sources.

[Baltoli]

I'd be in favour of a reworking of ModuleToKore, and a better spec for the Kore language in principle, but I guess it's not a super pressing issue unless we're planning to make further changes to the Kore encoding of K definitions (#3306?). There are at least four versions of the Kore data structures being implicitly referenced that I know off the top of my head:

• LLVM backend's AST library + parser (@Scott-Guest identified some inconsistency between the docs + implementation there this week) + bonus binary encoding for Kore terms
• The Pyk data structures
• Text generation in ModuleToKore
• Haskell backend
• ??? more

[ehildenb]

We can start by isolating Chapter 3 of Amelie's paper above, into two new pages on the website:

• Semantics of K
  • Kompile pipeline
  • Translation to Kore

[ehildenb]

@amelieled find out if it's OK to reuse the latex of your paper, and if so let's isolate it and upload it here so we can include it on the website as the first working draft.

[Baltoli]

@Scott-Guest has compiled an excellent summary of the de facto support for rewrite rule formats in the LLVM backend https://github.com/runtimeverification/llvm-backend/pull/745#issuecomment-1520794550; we should ensure that this remains in sync with any de jure specification of the KORE language.

A parallel version appears here in the pattern-matching scala code: https://github.com/runtimeverification/llvm-backend/blob/master/matching/src/main/scala/org/kframework/backend/llvm/matching/Parser.scala

Will also be useful for changes like the last step of https://github.com/runtimeverification/k/issues/3035, where we plan to be removing an old rewrite format.