1. Change mlkem-c-aarch64 to mlkem-native throughout.

2. Correct heading level typo in 1 place.

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

cbmc/proofs/proof_guide.md

@@ -1,13 +1,13 @@
 [//]: # (SPDX-License-Identifier: CC-BY-4.0)
 
-# CBMC Proof Guide and Cookbook for mlkem-c-aarch64
+# CBMC Proof Guide and Cookbook for mlkem-native
 
 This doc acts as a guide to developing proofs of C code using [CBMC](https://model-checking.github.io/cbmc-training/). It concentrates
 on the use of _contracts_ to achieve _unbounded_ and _modular_ proofs of type-safety
 and correctness properties.
 
 This document uses the abbreviated forms of the [CBMC contracts](https://diffblue.github.io/cbmc/contracts-user.html) defined by macros in the
-[cbmc.h](../../mlkem/cbmc.h) header file in the mlkem-c-aarch64 sources.
+[cbmc.h](../../mlkem/cbmc.h) header file in the mlkem-native sources.
 
 ## Common Proof Patterns
 
@@ -195,7 +195,7 @@ These steps are expanded on in the following sub-sections
 
 ### Populate a proof directory
 
-For mlkem-c-aarch64, proof directories lie below `cbmc/proofs`
+For mlkem-native, proof directories lie below `cbmc/proofs`
 
 Create a new sub-directory in there, where the name of the directory is the name of the function _without_ the `$(MLKEM_NAMESPACE)` prefix.
 
@@ -267,7 +267,7 @@ The harness should _not_ contain
 
 Using contracts, this harness function should not need to contain any CBMC `ASSUME` or `ASSERT` statements at all.
 
-# Supply top-level contracts
+### Supply top-level contracts
 
 Now for the tricky bit. Does `XXX` need any top-level pre- and post-condition contracts, other than those inferred from its type-signature?