Kore: semantics of injections (and the attribute `sortInjection`)

Read docs/kore-syntax.md and inspect the frontend behavior that emits the INJ module. Resolve the proposed semantics for inj and sortInjection before changing the syntax and frontend; done requires an agreed design and consistent documentation and implementation.

TL;DR: I think that In Kore, inj should be considered a built-in operator instead of a sort-overloaded symbol. This would simplify the semantics of Kore a lot, and most likely simplify the backends also a bit.

Proposal

Currently, subsorting in Kore is done by means of the sort-overloaded symbol inj{From, To} that has to be declared in the *.kore file, like this:

symbol inj{From, To}(From) : To [sortInjection{}()]

typically in an INJ module:

 module INJ 
     symbol inj{From, To}(From) : To [sortInjection{}()]
     axiom {S1, S2, S3, R} \equals{S3, R}(inj{S2, S3}(inj{S1, S2}(T:S1)), inj{S1, S3}(T:S1)) [simplification{}()]
endmodule
[]

From a language-design perspective, this has some drawbacks:

1. The declaration depends on the sortInjection attribute, which has very tricky semantics. First, it is not clear what concrete symbols it actually defines (does it declare the symbol inj{A,B} if A,B are unrelated sorts - for example, Int and List?). Second, the interpretation of the symbols is very hard to specify, especially in the presence of “diamond sub-sorting” (e.g., if A < B,C < D, where < denotes subsorting, what is the relation between inj{A, D}(a), inj{B,D}(inj{A, B}(a)), and inj{C,D}(inj{A, C}(a)). This unnecessarily complicates the precise documentation of Kore, let alone formal semantics.
2. It lowers the abstraction level of Kore from order-sorted to multi-sorted, by requiring that what is essentially an upcasting operator is always interpreted as a matching logic symbol. (The other option, interpreting the upcasting operator as an identity function on metalevel, would be more straightforward when documenting/formalizing Kore.)
3. It is not clearly specified what should happen in the presence of multiple symbols with the sortInjection attribute.
4. It requires the “user” (be it the frontend or whoever writes the test cases for backends) to always include the same piece of Kore code again and again.
5. It is the only situation in Kore where we need sort-parametric symbols. (I am not sure if that is really the case, please correct me if I am wrong here.)

I will explain these issues in more detail below. Now, as a remedy, it would suffice if we:

1. Didn’t emit the INJ module (containing the declaration of the inj symbol) in the frontend
2. Formally, in the syntax of Kore, we would add upcast-pattern and simplified application-pattern as follows;

<pattern>
  ::= <variable-pattern>
    | <matching-logic-pattern>
    | <upcast-pattern>                       //< NEW
    | <application-pattern>
    | <string-literal>

<application-pattern> ::=
    <symbol-identifier> "{" "}" "(" <patterns> ")"        //< no sorts parameters

<upcast-pattern> ::=
    "inj" "{" <sort> "," <sort> "}" "(" <pattern> ")"    //< exactly two sort parameters and one pattern

That way, generators of Kore terms do not even need to change unless they rely on sort-parametric symbols other than "inj".

Technical details

The ideal, simple semantics of Kore (after applying the proposed changes)

We would have order-sorted signatures and order-sorted models. In the model, there would be a bunch of carrier sets similarly as in a many-sorted case; however, unlike in the many-sorted case, the carrier sets would be ordered by set inclusion in the same way the sorts are ordered by the subsort relation. The inj operator would be part of the logic and would be interpreted as identity. And there would be no sortInjection attribute.

Less convenient options for the semantics of the current Kore

I can give semantics to the Kore even in the presence of the inj-as-symbol; however, it would be much more messy and I am afraid that nobody would like it and nobody would want to read it. So here are a few options.

1. Require that each *.kore starts with the INJ module verbatim:

 module INJ 
     symbol inj{From, To}(From) : To [sortInjection{}()]
     axiom {S1, S2, S3, R} \equals{S3, R}(inj{S2, S3}(inj{S1, S2}(T:S1)), inj{S1, S3}(T:S1)) [simplification{}()]
endmodule
[]

which has no influence on the interpretation of the rest of the file, and every other module must import INJ, and prohibit the use of the sortInjection after that. And then use the ideas from the "ideal, simple semantics of Kore" from the above section for the interpretation of the rest of the file.

2. Say that the sortInjection attribute is allowed only on symbol declarations, in which case it means that the symbol inj is not really a symbol but an upcasting operator - and proceed as in the ideal case.

3. Make the symbol declaration always declare a symbol, or a symbol family if it is parameterized, but if the sortInjection attribute is present on a symbol declaration with two sort parameters, then the symbol family is not indexed by all pairs of sorts, but only of such pairs which are in the subsorting relation. Also, make sure that the symbols that are declared have the correct interpretation: they are used to build something-like-new-terms, with something-like-no-junk-no-confusion properties, except that if there are multiple paths between the upper and lower sort, then some sharing has to happen. (I am not precise here because being precise is too complex - which is the point I am making.) As a concrete example, consider sorts A,B,C,D with A < B, A < C, B < D, and C < D. That is a valid (although nonlinear) ordering. The interpretation of the symbol inj has to ensure that inj{B, D}(inj{A,B}(x)) == inj{C, D}(inj{A,C}(x)) and at the same time inj{B, D}(x) <> y whenever y is pure D - that is, if y is not the result of casting something else to y. And this would have to be specified generally in the documentation of Kore, which is probably doable, but maybe not really readable.

4. Make the symbol declaration always declare a symbol (or a symbol family) with no exceptions, and use the sortInjection attribute to specify only the interpretation of the declared symbols. In particular, injections outside the subsorting relation would be interpreted as bottom / empty set. However, then the backends cannot complain when the user uses seemingly incorrect injections because they would actually be correct - just empty. And the interpretation of the "good" symbols would be as in the previous point.

In the cases (2), (3), and (4) what would happen if (a) no such declaration is present, or (b) there are two symbols with the sortInjection attribute?

Maybe there are some other options that I left unexplored; feel free to comment on them, too.

Resolution

If the proposal does not get accepted, I would most likely choose the option (2) from the less-than-ideal list.