Merge pull request #246 from pq-code-package/add_proof_guide

Add first draft of "Proof Guide" document for review.

README.md

@@ -32,9 +32,12 @@ ENVIRONMENT OR TO PROTECT ANY SENSITIVE DATA.** Once we have the first stable ve
 
 #### Verification
 
-Mostly TODO. We apply CBMC to verify the absence of UB in a few basic C routines, but the bulk of the C verification
+Mostly TODO. We apply [CBMC](https://github.com/diffblue/cbmc) to verify type-safety and the absence of
+UB in a few basic C routines, but the bulk of the C verification
 is outstanding. No formal verification has yet been applied to the backends.
 
+See the [Proof README](cbmc/proofs/README.md) and [Proof Guide](cbmc/proofs/proof_guide.md) for more details.
+
 ### Getting started
 
 ### Nix setup

cbmc/proofs/README.md

@@ -11,7 +11,8 @@ of certain classes of undefined behaviour for parts of the C-code in mlkem-nativ
 Proofs are organized by functions, with the harnesses and proofs for each function
 in a separate directory.
 
-TODO: Provide more information about CBMC and the properties it proves
+See the [Proof Guide](proof_guide.md) for a walkthrough of how to use CBMC and
+develop new proofs.
 
 # Usage
 
@@ -26,6 +27,10 @@ If `GITHUB_STEP_SUMMARY` is set, the proof summary will be appended to it.
 
 # Covered functions
 
-The following functions are currently covered:
+Each proved function has an eponymous sub-directory of its own. The shell command
 
-- `poly.c`: `poly_compress`
+```
+find . -name cbmc-proof.txt
+```
+
+yields a list of the subdirectories, and thus function names, that have a proof.