Errors in examples/rv/MultiplierCorrectness.v

[mbty]

Most of the proofs of the lemmas defined in the file examples/rv/MultiplierCorrectness.v do not pass. I did not check them all individually, but most of them seem to be outdated. At least enq_preserves_invariant (no matching clauses for match), deq_preserves_invariant (attempt to save an incomplete proof), step_preserves_finished_invariant,step_preserves_step_invariant and step_preserves_result_finished_invariant are impacted.

This is easy to miss as no target in the Makefile checks these proofs. It might be useful to add a correctness target to give an easy way to test them, especially since this file contains the most complex examples of proofs on Kôika designs of the examples folder. Not including it by default makes sense considering that it takes some time to pass and is not always directly relevant.

For the record, my version of coq is 8.11.0.

[cpitclaudel]

Ugh! Excellent catch, thanks. We have coq-all, but it compiles all in the coq/ directory, not in the examples/ one. I will look into this. @threonorm do you know anything about these proofs? (Also cc-ing @math-fehr, who wrote them)

[cpitclaudel]

Even the coq-all target was failing because of trivial oversights. I'll look into the more serious stuff in MultiplierCorrectness soon