Speed up instance proofs of Primitives

[Columbus240]

Proofs in Minimal.v, MinimalMMIO.v and MetricMinimalMMIO.v are very slow (ordered from a little slow to very slow) and make it annoying to check whether some changes are consistent with the rest of the code.
Maybe the amount of backtracking that has to be done can be reduced. The proofs use similar code of Ltac that maybe can be put in one place (Utility/Tactics.v might be good). Separating the tactics that do a lot of backtracking like _ |- _ \/ _ => left from the ones that do very little or no backtracking might be a good idea, if it is reasonably possible. Maybe CPDT of Chlipala has some ideas.

[samuelgruetter]

You're right, these proofs should definitely be improved. One way would be to make the tactic t better/more general, but probably it would be better to define MinimalMMIO in terms of Minimal, and MetrictMinimalMMIO in terms of MinimalMMIO, and then each additional layer would only have to prove what it adds instead of the whole thing. I tried to do that about 2 times already and gave up each time because I ran out of the time I had allocated for that, and after all, it works as it is, and the ugliness is hidden behind a reasonable interface (riscv.Spec.Primitives).

But if you find a way to improve this, that'd be more than welcome!

[samuelgruetter]

While adding a parametrizable ext_spec to the instances, I also made some improvements regarding this issue:

• In 1175fb1, I changed the instance proof of MinimalMMIO to do less unfolding and use more helper lemmas instead.
• In 674cff5, I reused instance proofs from MinimalMMIO for the instance proof of MetricMinimalMMIO.

[Columbus240]

Thanks. MetricMinimalMMIO still takes about 45s to compile for me, but I think it’s faster now (didn’t measure it earlier).

[samuelgruetter]

On Coq's CI, which runs with timing enabled, it went down from 829 seconds to 71 seconds. Feel free to suggest a PR which improves it further 😉

[Columbus240]

Just wow!
I had a look at it using the profiler and didn’t find a (simple) opportunity to optimize it further.