Feature: custom unification rules

[ehildenb]

I've attempted to add the following rule to a KEVM proof:

    rule [fast-unification-failure]: { <kevm> <k> K_CELL </k> ... </kevm> #Equals <kevm> <k> K_CELL' </k> ... </kevm> } => #Bottom requires K_CELL =/=K K_CELL' [simplification(20)]

I can see in definition.kore (bug report attached storagevar00-spec.tar.gz), that the rule makes it into the backend. I've also marked several other rules with labels. I'm calling the backend with export KORE_EXEC_OPTS="--debug-equation VERIFICATION.fast-unification-failure --debug-equation VERIFICATION.test1 --debug-equation VERIFICATION.test2 --debug-equation VERIFICATION.test3 --bug-report tests/specs/benchmarks/storagevar00-spec --log tests/specs/benchmarks/storagevar00-spec.debug-log --log-format oneline --log-entries DebugTransition,DebugAttemptedRewriteRules", so that we can see attempts of these equations.

In the debug log (attached storagevar00-spec.debug-log.txt), I can see that equation test1 in exercised, but simplification rule fast-unification-failure never is. I use command grep 'DebugAttemptEquation' tests/specs/benchmarks/storagevar00-spec.debug-log | cut -d ':' -f3-4 | sort -u to see this.

Can the Haskell backend try user-supplied unification rules before trying the default unification algorithm when applying semantic rules? Maybe if they are simplification(N) for N < 50 rules, or N < 25?

[ana-pantilie]

Meeting notes:

This will definitely not work like this because it's a simplification rule and it won't have the desired effect on unification.

There are two issues here:

1. we need faster unification failure (by checking the K cell first), we already have an issue for that Optimize semantic rule application #2969 and we discussed that we need to do some profiling to see if this is actually a problem, now that Dwight's unification overhaul has been merged
2. custom unification rules: how high priority is this? is it even safe to give users this feature? how would we merge this feature into our internal unification algorithm? are there any other compelling use cases for this feature?

[virgil-serbanuta]

My two cents about 2 - I think that Grigore liked this idea (well, he liked the idea of defining everything in K and having as few specialized algorithms in the backend as possible). I would think that it's hard for users without good knowledge of ML to write reasonable unification rules. I'm not sure how useful it would be right now (i.e. after Dwight's rewrite of AC unification), but in the past I wished I could write custom unification rules for maps. I guess that this would allow users to define custom data structures, though I'm not sure how often that would happen (I tried in the past to define some sort of map-like structure and making unification work was one of the hard problems, but I could solve the main issue without this custom structure, so whatever).

Anyway, if one does not take performance into account, I would guess that most unsolved unification problems just become #Equals expressions, so most unification issues should be solvable by writing custom simplification rules for #Equals.

[ehildenb]

The question here is whether the unification algorithm can take these simplification rules into account. Not sure why it would not be able to, unless it's transforming the unification problem into something that is not a { ... #Equals ... } internally when doing semantic rule unification. My impression is that the algorithm was not currently doing that, and that it is currently operating directly over an { ... #Equals ...}. Please correct me if I'm wrong.

This is a way to achieve faster rule unification failure, without having to hack it directly into the backend. So I'm proposing it as an alternative to #2969. We don't have any results there yet, so I figured to try a different approach.

I also agree with @virgil-serbanuta that this makes the "help" to the unification algorithm very explicit in K, which is really nice.

[radumereuta]

1. documentation about how the backend works
2. do we support adding custom unification rules with the current implementation, if not, how can we add it
3. do we want to add this heuristic inside the backend, or should they be provided by the user?
   Everett wants them provided by the user. Might speed up unification.