Automatically verifying the correctness of simplification rules.

[Stevengre]

Situation

Currently, we assume that simplification rules are correct, but that may not always be the case.

Expected

Given a simplification rule, we should be able to automatically check if it is correct or not.

Algorithm

A rule in the form of:

rule LHS => RHS requires PREV ensure POST

should be translated into the following SMT:

NOT(PREV -> (LHS == RHS) -> POST)

If there is no solution, then the simplification rule is proven to be correct.

[ehildenb]

We did try this before: #1664

It actually didn't work very well, for the reasons that @PetarMax pointed out on Slack. Basically, most of the functions are uninpretpreted, so Z3 can't do much with them.

We are soon going to make a LEAN4 backend for K, and I think we will have a better chance of verifying simplification lemmas using that.

[Stevengre]

I’m very excited about this backend and hope it will be actively maintained. I also hope to have the time and opportunity to contribute to it.