Add first draft of "Proof Guide" document for review. #246
Conversation
|
I think this should also be reviewed by someone who does not know CBMC. @mkannwischer What about you? I imagine you don't have time until November? |
rod-chapman
force-pushed
the
add_proof_guide
branch
from
97f0cd8 to
2ea6f60
Compare
rod-chapman
force-pushed
the
add_proof_guide
branch
from
2ea6f60 to
7fc1030
Compare
hanno-becker
force-pushed
the
add_proof_guide
branch
from
ff8a577 to
6530579
Compare
hanno-becker
force-pushed
the
add_proof_guide
branch
from
6530579 to
2accf06
Compare
rod-chapman
force-pushed
the
add_proof_guide
branch
from
2accf06 to
43c426d
Compare
rod-chapman
force-pushed
the
add_proof_guide
branch
from
3f558ad to
d8b8e30
Compare
rod-chapman
force-pushed
the
add_proof_guide
branch
2 times, most recently
from
2604f23 to
f7da28a
Compare
There was a problem hiding this comment.
Thanks @rod-chapman - this is excellent.
Let's merge this after some very minor edits.
Sorry for the the long delay - I wanted to take the time and write my first proof at the same time. I just added a proof for poly_tomont in #307 .
rod-chapman
force-pushed
the
add_proof_guide
branch
from
f7da28a to
eefc04a
Compare
rod-chapman
force-pushed
the
add_proof_guide
branch
from
430f2b8 to
4462500
Compare
|
High-level comment: should there be any links towards more-general CBMC training (like https://model-checking.github.io/cbmc-training/)? |
|
Most of that existing training material talks about using CBMC in "bounded model checking" mode, rather than "deductive sound contract-based proof" mode. I think pushing readers towards the former will cause confusion... |
rod-chapman
force-pushed
the
add_proof_guide
branch
from
b76acf0 to
5896b3c
Compare
rod-chapman
force-pushed
the
add_proof_guide
branch
2 times, most recently
from
6638384 to
150efc7
Compare
There was a problem hiding this comment.
@rod-chapman Can you wrap this up, by rebasing and cleaning up the history and addressing whatever comments, if any, are still outstanding? The PR has been open for too long, let's get it in.
rod-chapman
force-pushed
the
add_proof_guide
branch
3 times, most recently
from
ee6444a to
7ad2e5f
Compare
|
Rebased and squashed. Ready to approve and merge. |
rod-chapman
force-pushed
the
add_proof_guide
branch
2 times, most recently
from
b216f5d to
c18d4b3
Compare
There was a problem hiding this comment.
@rod-chapman Can you change all occurrences of mlkem-c-aarch64 to mlkem-native?
rod-chapman
force-pushed
the
add_proof_guide
branch
from
82dcea8 to
6f5e75c
Compare
mkannwischer
force-pushed
the
add_proof_guide
branch
from
6f5e75c to
92da76d
Compare
There was a problem hiding this comment.
Thanks @rod-chapman for writing this up and for taking our comments into account!
LGTM now!
If we later want to extend it, we can always have another PR.
This PR add a guide to proof using CBMC for the mlkem-native project in cbmc/proofs/proof_guide.md The document contains: * Onboarding and installation guide for CBMC * Common proof "patterns" * Advice on writing loop invariants and contracts * A step-by-step guide to producing a new proof of a C function * A worked example of the above process. Signed-off-by: Rod Chapman <[email protected]>
mkannwischer
force-pushed
the
add_proof_guide
branch
from
92da76d to
15c9d20
Compare
This PR adds a "Cookbook" for how to develop and run CBMC proofs for the C code in this repo.
The guide uses the proof of poly_tobytes() as an example, so PR #235 should be reviewed and merged first.