Further review comments and clarifications.

1. Correct typos and grammar errors
2. Add explanatory comment on IS_FRESH()
3. Add comment on use of contracts vs inlining for proof
4. Recommends using $(nproc) to set processor cores when running all proofs.
5. Add comment explaining meaning of ARRAY_IN_BOUNDS macro.
6. Note that i >= 0 invariant is not strictly required for unsigned i.

Signed-off-by: Rod Chapman <[email protected]>

cbmc/proofs/proof_guide.md

@@ -15,7 +15,7 @@ This document uses the abbreviated forms of the CBMC contracts defined by macros
 
 1. A function should contain at most one outermost loop statement. If the function you're trying to prove has more than one outermost loop, then re-factor it into two or more functions.
 
-2. The one outermost loop statement should be _final_ statement before the function returns. Don't have complicated code _after_ the loop body.
+2. The one outermost loop statement should be the _final_ statement before the function returns. Don't have complicated code _after_ the loop body.
 
 ### For loops
 
@@ -60,13 +60,15 @@ ASSIGNS(OBJECT_WHOLE(dst));
 // clang-format on
 ```
 
+The `IS_FRESH(dst,len)` in the precondition means that the pointer value `dst` is not `NULL` and is pointing to at least `len` bytes of data. The `ASSIGNS` contract (in this case) means that when the function returns, it promises to have updated the whole object pointed to by dst - in this case `len` bytes of data.
+
 The body:
 
 ```
 void zero_array_ts (uint8_t *dst, int len)
 {
     for (int i = 0; i < len; i++)
-    // clang-format off
+        // clang-format off
     ASSIGNS(i, OBJECT_WHOLE(dst))
     INVARIANT(i >= 0 && i <= len)
     DECREASES(len - i)
@@ -118,7 +120,7 @@ void zero_array_correct (uint8_t *dst, int len)
 Rules of thumb:
 1. Don't overload your program variables with quantified variables inside your FORALL contracts. It get confusing if you do.
 2. The type of the quanitified variable is _signed_ "int". This is important.
-3. The path in the program from the loop-invariant, through the final loop exit test, to the implicit `return` statement is "nothing" or a "null statement". We need to prove that (on the final iteration), the loop invariant AND the loop exit condidtion imply the post-condition. Imagine having to do that if there's some really complex code _after_ the loop body.
+3. The path in the program from the loop-invariant, through the final loop exit test, to the implicit `return` statement is "nothing" or a "null statement". The proof needs to establish that (on the final iteration), the loop invariant _and_ the loop exit condidtion imply the post-condition. Imagine having to do that if there's some really complex code _after_ the loop body.
 
 This pattern also brings up another important trick - the use of "null ranges" in FORALL expressions. Consider the loop invariant above. We need to prove that it's true on the first entry to the loop (i.e. when i == 0).
 
@@ -225,6 +227,9 @@ Edit the Makefile and update the definition of the following variables:
 
 For documentation of these (and the other) options, see the `cbmc/proofs/Makefile.common` file.
 
+The `USE_FUNCTION_CONTRACTS` option should be used where possible, since contracts enable modular proof, which is far more efficient
+ that inling, which tends to explode in complexity for higher-level functions.
+
 #### Z3 or Bitwuzla?
 
 We have found that it's better to use Bitwuzla in the initial stages of developing and debugging a new proof.
@@ -299,10 +304,10 @@ Before pushing a new proof for a new function, make sure that _all_ proofs run O
 
 ```
 export MLKEM_K=3 # or 2 or 4...
-./run-cbmc-proofs.py --summarize -j8
+./run-cbmc-proofs.py --summarize -j$(nproc)
 ```
 
-Change the "8" to match the number of CPU cores that you have available.
+That will use `$(nproc)` processor cores to run the proofs.
 
 ### Debugging a proof
 
@@ -368,12 +373,14 @@ We can use the macros in `cbmc.h` to help, thus:
 ```
 void poly_tobytes(uint8_t r[MLKEM_POLYBYTES], const poly *a)
      // clang-format off
-REQUIRES(a != NULL && IS_FRESH(a, sizeof(poly)))
+REQUIRES(IS_FRESH(a, sizeof(poly)))
 REQUIRES(ARRAY_IN_BOUNDS(int, k, 0, (MLKEM_N - 1), a->coeffs, 0, (MLKEM_Q - 1)))
 ASSIGNS(OBJECT_WHOLE(r));
 // clang-format on
 ```
 
+`ARRAY_IN_BOUNDS` is a macro that expands to a quantified expression that expresses that the elemtns of `a->coeffs` between index values `0` and `(MLKEM_N - 1)` (inclusive) are in the range `0` through `(MLKEM_Q - 1)` (also inclusive). See the macro definition in `mlkem/cbmc.h` for details.
+
 ### Interior contracts and loop invariants
 
 `poly_tobytes` has a reasonable simple, single loop statement:
@@ -401,6 +408,8 @@ Therefore, we add:
     { ... }
 ```
 
+Note that the invariant `i >= 0` could be ommitted since `i` is of an `unsigned` integer type. It is given here for clarity only.
+
 Another small set of changes is required to make CBMC happy with the loop body. By default, CBMC is pedantic and warns about conversions that potential truncate values of lose information via an implicit type conversion.
 
 In the original version of the function, we have 3 lines, the first of which is:
@@ -432,7 +441,7 @@ We can also use the higher-level Python script to prove just that one function:
 
 ```
 cd cbmc/proofs
-./run-cbmc-proofs.py --summarize -j8 -p poly_tobytes
+MLKEM_K=3 ./run-cbmc-proofs.py --summarize -j$(nproc) -p poly_tobytes
 ```
 yields
 ```