Documentation update

Signed-off-by: Jake Massimo <[email protected]>

Author: jakemas

proofs/README.md

@@ -10,4 +10,4 @@ We use the [C Bounded Model Checker (CBMC)](https://github.com/diffblue/cbmc) to
 
 ## Assembly verification: HOL-Light
 
-We use the [HOL-Light](https://github.com/jrh13/hol-light) interactive theorem prover alongside the verification infrastructure from [s2n-bignum](https://github.com/awslabs/s2n-bignum) to show the functional correctness of various highly optimized assembly routines in mlkem-native at the object-code level. See [proofs/hol_light/x86_64](hol_light/x86_64).
+We use the [HOL-Light](https://github.com/jrh13/hol-light) interactive theorem prover alongside the verification infrastructure from [s2n-bignum](https://github.com/awslabs/s2n-bignum) to show the functional correctness of highly optimized assembly routines in mlkem-native at the object-code level. See [proofs/hol_light/x86_64](hol_light/x86_64).

proofs/hol_light/x86_64/README.md

@@ -2,7 +2,7 @@
 
 # HOL Light functional correctness proofs
 
-This directory contains functional correctness proofs for all x86_64 assembly routines
+This directory contains functional correctness proofs for x86_64 assembly routines
 used in mldsa-native. The proofs were largely developed by John Harrison and Jake Massimo,
 and are written in the [HOL Light](https://hol-light.github.io/) theorem
 prover, utilizing the assembly verification infrastructure from [s2n-bignum](https://github.com/awslabs/s2n-bignum).