search

runtimeverification / k

K Framework Tools 7.0
BSD 3-Clause "New" or "Revised" License
447 stars 147 forks source link

A modern Kore for a modern K #3306

Open ana-pantilie opened 1 year ago

ana-pantilie commented 1 year ago

Motivation

During the development of the Haskell backend booster, we have been noticing that the Kore language itself is not designed to achieve our goals of fast symbolic execution, the only benefit it provides is that it is easy to parse. Many other features are actually making it harder for the backend to internalize and implement certain features (like https://github.com/runtimeverification/hs-backend-booster/issues/154). This is a proposal to start a discussion about modifying the Kore language so that it is no longer focused on matching logic but a "desugared" version of K, containing only the necessary information a backend would need to execute the semantics.

This, of course, is a very large change but we think that it can be done incrementally and in a backwards compatible fashion, by extending the original Kore language with Kore 2.0 constructs.

Priority predicates in rules (a.k.a. anti-lefts)

This was a feature added in order to facilitate the creation of proof objects inside the backend itself, while executing the semantics. We know, though, that for execution these predicates are not necessary at all, their behavior can be implemented in the backends by grouping rules by a priority number.

Rewrite rules

The left hand sides of rewrite rules have very complex encodings based on aliases, so that priority predicates can be constructed and added to their left hand sides. This provides excellent support for explicitly tracing the proof steps which are done when applying a rule, but it induces several practical limitations.

Limitations:

Proposal:

Add a new Kore construct, \\rewrites2 which would translate K in the following way (or something similar):

rule leftConfig => rightConfig requires leftCondition ensures rightCondition

=====>

axiom \\rewrites2{SortGeneratedTopCell{}}(leftCondition, leftConfig, rightCondition, rightConfig)

Function definition rules

The current encoding of function definition rules is very well documented in https://github.com/runtimeverification/haskell-backend/blob/master/design-decisions/2020-05-02-function-rules.md. Again, the priority is encoded directly into the rule, and this has proved to be problematic in regards to performance, and it still is an unfixed problem in the open source Haskell backend.

The proposal would be to just remove the priority predicate from the Kore 2.0 version of the rule.

Equational rule encodings

In K, a rule has a function symbol at the top of the left hand side it is either interpreted as a function definition rule or as a simplification rule, if it has the simplification attribute. We regard both of these as equational rules, because they affirm equalities between Kore patterns.

In both cases, they are encoded as \\implies(leftCondition, \\equals(leftTerm, \\and(rightTerm, ensuresPredicate))).

Function definition rules

In the case of function definition rules, the leftCondition contains the rule's requires predicate, the priority predicates (which we have discussed above) and a predicate which essentially constrains the arguments to the function to be interpreted in ML as singletons (this is encoded with the ML \\in).

Dealing with this encoding directly is problematic from a performance perspective. Since the goal of this encoding is to make sure that the arguments of the left hand side are defined and singular, I would argue that we should directly be trying to solve this issue, instead of encoding it into ML.

Possible solutions need to be discussed in a separate issue.

Kore 2.0 should distinguish between types of rules directly

I would go even further and suggest that instead of the ML-focused encoding for equations, we should have separate constructs for each, like there is for \\rewrites.

Suggestion:

Remove unused/inefficient axioms from Kore definitions

If one opens a definition.kore, they can notice that many axioms have been generated just for the purpose of providing a "mostly complete" ML theory. These axioms are not used in practice, and even if they are I would expect there to be better representations for the information inside them.

Subsorting

A definition.kore usually contains a large list of axioms like the following:

// generated axioms
  axiom{R} \exists{R} (Val:SortKItem{}, \equals{SortKItem{}, R} (Val:SortKItem{}, inj{SortGasUsedCell{}, SortKItem{}} (From:SortGasUsedCell{}))) [subsort{SortGasUsedCell{}, SortKItem{}}()] // subsort
  axiom{R} \exists{R} (Val:SortOpCode{}, \equals{SortOpCode{}, R} (Val:SortOpCode{}, inj{SortStackOp{}, SortOpCode{}} (From:SortStackOp{}))) [subsort{SortStackOp{}, SortOpCode{}}()] // subsort
  axiom{R} \exists{R} (Val:SortKItem{}, \equals{SortKItem{}, R} (Val:SortKItem{}, inj{SortDataCellOpt{}, SortKItem{}} (From:SortDataCellOpt{}))) [subsort{SortDataCellOpt{}, SortKItem{}}()] // subsort
  axiom{R} \exists{R} (Val:SortKItem{}, \equals{SortKItem{}, R} (Val:SortKItem{}, inj{SortAccountCell{}, SortKItem{}} (From:SortAccountCell{}))) [subsort{SortAccountCell{}, SortKItem{}}()] // subsort
  axiom{R} \exists{R} (Val:SortKItem{}, \equals{SortKItem{}, R} (Val:SortKItem{}, inj{SortOmmerBlockHeadersCell{}, SortKItem{}} (From:SortOmmerBlockHeadersCell{}))) [subsort{SortOmmerBlockHeadersCell{}, SortKItem{}}()] // subsort
...

These axioms encode subsort relations into ML. They are never applied as-is, but internalized by the backends. The frontend should provide less-clunky syntax for expressing these relations. We could also reevaluate the decision of not making Kore a language which supports subsorts directly.

No-confusion, no-junk, functional etc. axioms

Again, these are only there for ML purposes. I doubt any of the backends apply these directly, instead they use the symbol attributes to know how to deal with certain symbols.

Ceil simplification rules

I believe @virgil-serbanuta has shown how the current encoding of these is actually unsound, and he has proposed separate syntax for dealing with them. Please add your ideas here when you have a chance.

Allowing users to write ML in K

I think we have been too lenient with this, @virgil-serbanuta has again found an issue with writing predicates directly into the requires clauses of rules. I believe a larger discussion needs to be had regarding this.

Conclusion

This is an issue which I hope will start some serious discussions regarding Kore and how to provide a stable foundation for modern backends. In my opinion, if the modern backends are no longer ML-focused then neither should the language they consume be ML-focused.

My (very simplified) idea of a modern Kore language would just be a very straight-forward set of sorts, constructors, functions, rewrite rules, function definitions and simplifications together with auxiliary information like the subsorting relationship. We need to also discuss what subset of the ML language we need to express patterns.

virgil-serbanuta commented 1 year ago

Since I just watched the "Vision 2023" video form our Youtube channel, I would like to ask something about "if the modern backends are no longer ML-focused then neither should the language they consume be ML-focused" - would the ideas proposed in this issue bring us closer or further away form being able to generate actual ML proofs (and, consequently, proof certificates)?

traiansf commented 1 year ago

Since I just watched the "Vision 2023" video form our Youtube channel, I would like to ask something about "if the modern backends are no longer ML-focused then neither should the language they consume be ML-focused" - would the ideas proposed in this issue bring us closer or further away form being able to generate actual ML proofs (and, consequently, proof certificates)?

My guess is that the modern Kore (which I'll name MORE below) should be amenable to generate a mu-ML specification from its more higher level spec language, using the attributes preserved or generated by the frontend to generate the additional axioms which we're currently generating but not really checking nor using.

Anyway, speaking of rewrite rules I've always wondered why do we flatten them before sending them to the backend. Having them unflattened in MORE could help devising faster matching automatons, as we can clearly observe what changes and what not.

tothtamas28 commented 1 year ago

Can we make MORE order-sorted, i.e. get rid of sort injections? They make programmatically constructing and processing KORE patterns quite awkward. Is there a benefit on the backends for having them?

Baltoli commented 6 months ago

Moving to the backlog as we've not made any meaningful updates here in a year, but at some point we may want to revisit.