Speed up instance proofs of `Primitives` about riscv-coq HOT 5 CLOSED

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!

from riscv-coq.

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.

from riscv-coq.

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

from riscv-coq.

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 😉

from riscv-coq.

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

from riscv-coq.