-
Notifications
You must be signed in to change notification settings - Fork 9
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Errors in examples/rv/MultiplierCorrectness.v #7
Comments
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
added a commit
that referenced
this issue
Apr 13, 2021
I forgot to update these files when I introduced the interp_cycle APIs. Reported-by: @mbty
Even the coq-all target was failing because of trivial oversights. I'll look into the more serious stuff in MultiplierCorrectness soon |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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 leastenq_preserves_invariant
(no matching clauses for match),deq_preserves_invariant
(attempt to save an incomplete proof),step_preserves_finished_invariant
,step_preserves_step_invariant
andstep_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 theexamples
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.
The text was updated successfully, but these errors were encountered: