Computation of dependencies (related to the K prelude)

Question

I'm particularly interested to understand the K prelude (how it is structured, why its content is like that, how "kompile" calculates dependencies, etc). The main question is: what is the criterion for a hooked symbol from the K prelude to be copied into the generated Kore file?

Here some examples of potential problems:

1. The symbol andBool is copied with its associated rewrite rules, which does not seem to be the case for the symbol in_keys, which is simply copied without its rewrite rules. Other symbols seem to be useless (for the IMP semantic) but exist, with or without its rewrite rules, in the generated Kore file, such as countAllOccurrences, findChar, signExtendBitRangeInt or Float2String.

2. It seems that SortId is generated by the line syntax Id [token]. However, the lines "syntax Bool ::= "true" [token] and syntax Bool ::= "false" [token] do not generate true and false symbols. (Moreover, is it a choice that true and false are values and not constructors?)

3. The sort named SortId is not generated for the following example, whereas some generated hooked symbols depend on this sort. This problem does not exist with the IMP semantic.

module MAX-OW-SYNTAX
    imports INT
    imports BOOL
    syntax Exp ::= Int | "(" Exp ")" [bracket]
                 | "max" Exp Exp
endmodule
        
module MAX-OW
    imports MAX-OW-SYNTAX
    syntax KResult ::= Int
        
    rule max X Y => Y requires X <Int Y
    rule max X _ => X [owise]
endmodule

4. Is it correct that the K prelude is implemented in each language of each backend, and that an implementation in the Kore language is available in the K prelude? Do you have the necessary interface to implement for a new backend? (For instance, Bag is obsolete, but not Set, List and Map, but I don't know the list of set operators, map operators, etc. that the new backend must provide.)

5. Is there a reason why andThenBool and andBool have the same semantics once implemented in the Kore syntax (Booleans module)?

6. Where are the rewrite rules defined for ==Bool, used in the definition of =/=Bool (Booleans module)?

Answer 1

The best reference point for the K internals is the User Manual, along with the K source for the prelude. To respond to your specific questions as best as I can:

1. in_keys only has simplification rules that apply on symbolic backends. These will not apply on concrete backends, and so those backends use the hooked implementation MAP.in_keys. Some functions (such as andBool) can be implemented both in K and as an efficient backend hook. For example, on the K LLVM backend, andBool is implemented by code generation. If a backend didn't support that hook, the (relatively) inefficient K rewriting implementation would be used.
2. The Id sort is built in for convenience. It represents program identifiers.
3. You haven't imported DOMAINS in this example. Doing so will pull in the Id sort and related rewrites.
4. Very roughly, and largely for internal purposes. Do you have a hypothetical K backend in mind, or is there a way in which the LLVM / Haskell backends provided by K are inadequate for your specific use case?
5. andThenBool is required to short-circuit its arguments; andBool is permitted to short-circuit, but may evaluate both arguments strictly. An implementation that makes both perform short-circuiting is valid.
6. ==Bool is implemented only in terms of a hook. In domains.md, you can see the hook(BOOL.eq) attribute that indicates how ==Bool is implemented.

Do let us know if you have further questions, or would like help implementing a specific semantics in K.