Generate equations for `==K`

[goodlyrottenapple]

We have recently noticed that both the haskell backend and llvm backend hook the ==K symbol directly (LLVM) or rewrite to #Equals (haskell backend), both of which are internal simplification/evaluation strategies which are opaque to the user (i.e. the question of why some ... ==K ... term was simplified to something else cannot be traced easily in the haskell backend, because we simplified to { ... #Equals ... } and afterwards, no kore rules were applied because the internal logic of #Equals was used). In booster, we are trying to minimise the amount of built in behaviour and it would make sense for the backend to use generated equations for ==K, rather than rely on a builtin simplifier. Would it be possible to generate rules for ==K or is there some inherent limitation that would prevent us form doing this?

[Baltoli]

To check my understanding of what you're looking for, you'd want to generate the following rules for every constructor c with arity n:

syntax SomeSort ::= c(S_1, ..., S_n)

rule c(a_1, ..., a_n) ==K c(a'_1, ..., a'_n) => true
  requires a_1 ==K a'_1 andBool ... andBool a_n ==K a'_n
rule c(a_1, ..., a_n) ==K _Other => false [owise]

[goodlyrottenapple]

yes, although a better version might be

rule c(a_1, ..., a_n) ==K c(a'_1, ..., a'_n) => a_1 ==K a'_1 andBool ... andBool a_n ==K a'_n
rule c(a_1, ..., a_n) ==K _Other => false [owise]

[Baltoli]

This is basically what the LLVM backend does internally when hooking ==K: https://github.com/runtimeverification/llvm-backend/blob/29bb01e45da52e13549f4f9a38dac91aacb6d0bd/runtime/collections/kelemle.cpp#L12; it's just an optimised native-code walk over the arguments of a constructor that dispatches to specialised implementations for hooked sorts.

[Baltoli]

I guess you would need to do a few things here to implement the change:

• Rename the ==K symbol to some internal symbol, then reinstate it to unconditionally rewrite to the hooked internal symbol.
• Add a frontend pass that instantiates the axioms above for each production in a module.
• This is a big enough change that we'd want to have pretty comprehensive benchmarking + downstream testing before committing to it.

There may also be something I'm missing as well; let's put this on the agenda for Thursday to discuss in detail.

[goodlyrottenapple]

Rename the ==K symbol to some internal symbol, then reinstate it to unconditionally rewrite to the hooked internal symbol.

Why would we need this? because of the LLVM backend? could we perhaps just add the equations to a separate symbolic module somehow?

[Baltoli]

Why would we need this?

You might not need to, I guess; my thought was to minimise the surface area of the change by adding a new customisation point but it might not be necessary on inspection. Would need to give it some more thought to say in detail.

[Baltoli]

@dwightguth mentions that to avoid a quadratic blowup in the number of equations we generate, we should take care to make sure the symbolic backend handles owise correctly.

There may have been a reason not to do this; the Maude backend went through a similar process when implementing ==K. @dwightguth will try to recall this; may have been Maude specific.

If we can do this in linear rules, it should be fine and we can try a prototype.

[Baltoli]

The Maude reason may have been that the Maude backend doesn't consider the possible values of a variable when applying an owise rule; this restriction probably doesn't apply elsewhere and so the linear-rules axiomatisation might well work.

Another issue is confluence; rules for equality need to apply on fully-simplified arguments in order for ==K to be sound.

[ehildenb]

Some thoughts:

• Only generate the axioms for when compiling the haskell backend if the Maude backend can't handle them. Or only generate them with a given flag (or be able to turn them off with a flag).
• The rules should only be for free constructors, so I don't think we need to make sure the arguments are normalized before applying them, right? Free constructors shouldn't have any equations over them (otherwise they're not free), and so it should always be safe to decompose them into equalities over the arguments.
• I don't think we need some different internal symbol, we can just use _==K_.
• The owise rule may not even be needed, since we just need it to decompose when it can. That should also avoid the problem with it picking false for things where the terms aren't already simplified. Maybe though having the owise is important for path pruning.

[dwightguth]

The maude and llvm backends should be able to handle the equations you're talking about generating, but it will certainly be less efficient than what it's currently doing, so my suggestion would be to enable them only for the backends you need them on.

I agree that the non-owise rule should be sound if generated for free constructors only, even if the arguments are not simplified. This is not true for the owise rule unless the implementation of owise simplifies its arguments previously to applying the owise rule. For example, if foo is a function that evaluates to bar, and bar is a free constructor, the owise rule above might apply and rewrite foo == bar to false, which is not sound.

Without the owise rule, two unequal terms cannot be rewritten to false without a quadratic number of axioms. If you don't care about reducing unequal terms to false, that axiom is of course not needed.

[ehildenb]

I'm pretty sure the haskell backend should not apply the owise rule unless it can definitely tell that it applies, which means that it definitely knows the non-owise cannot apply. This is different than Maude's built-in equality, for example, which relies on syntactic normal forms.

So I think for the Haskell backend at least, it should be safe to generate the owise. Either way, I believe @goodlyrottenapple is first implementing it hardcoded in the backend to test the concept and performance, then we can think about generating axioms.

[Baltoli]

... first implementing it hardcoded in the backend to test the concept and performance ...

Nice, that makes sense to me. Can discuss further this afternoon

[Baltoli]

This is not a pressing issue; the booster has implemented something morally equivalent to what we'd see if we implemented this generation of equations.

There is the possible future benefit that generating the equations would be "purer", but not a priority.