search

mit-plv / bedrock2

A work-in-progress language and compiler for verified low-level programming
http://adam.chlipala.net/papers/LightbulbPLDI21/
MIT License
297 stars 45 forks source link

Add proof for isSquare program correctness #335

Closed leognon closed 1 year ago

leognon commented 1 year ago

I have completed the proof that the sample isSquare program is correct. The proof is a bit tedious and has some long lemmas, so let me know if there are any improvements I should make.

DIJamner commented 1 year ago

I can understand why isSquare and the Examples section started out in this file, but we should move them into a separate file from the notation definitions and their dedicated tests.

DIJamner commented 1 year ago

I agree that the situation with the long lemmas should be able to be improved. However, I think once we've addressed Andres' comments and separated isSquare and the rest into another file, we should merge this, and we can leave improving the proofs to a future PR. I'll take a more detailed look at the proofs early next week to give you some feedback and suggestions.

leognon commented 1 year ago

I have moved the examples to a separate file (for now I've just called it SamplePrograms.v) and fixed some of the suggestions you've given. Is there anything else that should be changed?