Update READMEs to reflect x86_64 assembly verification coverage

All x86_64 ML-KEM arithmetic intrinsics have been rewritten in
assembly and verified, so update the verification claims accordingly.
Note that the x86_64 FIPS-202 (Keccak) backend remains in C
intrinsics and is not yet covered by proof.

Signed-off-by: Matthias J. Kannwischer <matthias@kannwischer.eu>

Author: mkannwischer

README.md

@@ -17,8 +17,8 @@ mlkem-native is a secure, fast, and portable C90[^C90] implementation of ML-KEM[
 It is a fork of the ML-KEM reference implementation[^REF].
 
 All C code in [mlkem/src/*](mlkem) and [mlkem/src/fips202/*](mlkem/src/fips202) is proved memory-safe (no memory overflow) and type-safe (no integer overflow)
-using [CBMC](https://github.com/diffblue/cbmc). All AArch64 assembly is proved functionally correct at the object code level using
-[HOL-Light](https://github.com/jrh13/hol-light).
+using [CBMC](https://github.com/diffblue/cbmc). All AArch64 assembly and all x86_64 ML-KEM arithmetic assembly is proved functionally correct at the object code level using
+[HOL-Light](https://github.com/jrh13/hol-light). The x86_64 FIPS-202 (Keccak) backend is still in C intrinsics and not yet covered by proof.
 
 mlkem-native includes native backends for Arm (64-bit, Neon), Intel/AMD (64-bit, AVX2), and RISC-V (64-bit, RVV). See [benchmarks](https://pq-code-package.github.io/mlkem-native/dev/bench/) for performance data.
 
@@ -61,9 +61,10 @@ All C code in [mlkem/src/*](mlkem) and [mlkem/src/fips202/*](mlkem/src/fips202)
 This uses the [C Bounded Model Checker (CBMC)](https://github.com/diffblue/cbmc) and builds on function contracts and loop invariant annotations
 in the source code. See [proofs/cbmc](proofs/cbmc) for details.
 
-All AArch64 assembly is proved functionally correct at the object-code level. This uses the [HOL-Light](https://github.com/jrh13/hol-light)
-interactive theorem prover and the [s2n-bignum](https://github.com/awslabs/s2n-bignum/) verification infrastructure (which includes a model of the
-relevant parts of the Arm architecture). See [proofs/hol_light/aarch64](proofs/hol_light/aarch64) for details.
+All AArch64 assembly and all x86_64 ML-KEM arithmetic assembly is proved functionally correct at the object-code level. This uses the [HOL-Light](https://github.com/jrh13/hol-light)
+interactive theorem prover and the [s2n-bignum](https://github.com/awslabs/s2n-bignum/) verification infrastructure (which includes models of the
+relevant parts of the Arm and x86 architectures). See [proofs/hol_light](proofs/hol_light) for details.
+The x86_64 FIPS-202 (Keccak) backend is still in C intrinsics and not yet covered by proof.
 
 ## Security
 

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/aarch64](hol_light/aarch64).
+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 all AArch64 assembly and all x86_64 ML-KEM arithmetic assembly in mlkem-native at the object-code level. See [proofs/hol_light](hol_light).

proofs/hol_light/README.md

@@ -2,7 +2,7 @@
 
 # HOL Light functional correctness proofs
 
-This directory contains functional correctness proofs for all of the AArch64 and x86_64 assembly in mlkem-native.
+This directory contains functional correctness proofs for all AArch64 assembly and all x86_64 ML-KEM arithmetic assembly in mlkem-native.
 They 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).
 
@@ -11,8 +11,7 @@ contains the byte code being verified, as well as the specification that is bein
 
 ## Intrinsics
 
-The x86_64 backend still includes some native code written in C intrinsics. This code is **not** covered by proof, currently.
-We are working on rewriting all intrinsics code in assembly and verifying it in HOL-Light/s2n-bignum.
+The x86_64 FIPS-202 (Keccak) backend is still in C intrinsics and not yet covered by proof.
 
 ## Primer
 
@@ -99,7 +98,9 @@ echo '1+1;;' | nc -w 5 127.0.0.1 2012
 
 ## What is covered?
 
-All AArch64 assembly routines used in mlkem-native are covered. Those are:
+All AArch64 assembly routines and all x86_64 ML-KEM arithmetic assembly routines used in mlkem-native are covered. The x86_64 FIPS-202 (Keccak) backend is still in C intrinsics and not yet covered; see [above](#intrinsics).
+
+### AArch64
 
 - ML-KEM Arithmetic:
   * AArch64 forward NTT: [mlkem_ntt.S](aarch64/mlkem/mlkem_ntt.S)
@@ -119,22 +120,20 @@ All AArch64 assembly routines used in mlkem-native are covered. Those are:
 
 The NTT and invNTT functions are super-optimized using [SLOTHY](https://github.com/slothy-optimizer/slothy/).
 
-All x86_64 assembly routines used in mlkem-native are covered:
+### x86_64
 - ML-KEM Arithmetic:
   * x86_64 forward NTT: [mlkem_ntt.S](x86_64/mlkem/mlkem_ntt.S)
   * x86_64 inverse NTT: [mlkem_intt.S](x86_64/mlkem/mlkem_intt.S)
   * x86_64 base multiplications: [mlkem_poly_basemul_acc_montgomery_cached_k2.S](x86_64/mlkem/mlkem_poly_basemul_acc_montgomery_cached_k2.S) [mlkem_poly_basemul_acc_montgomery_cached_k3.S](x86_64/mlkem/mlkem_poly_basemul_acc_montgomery_cached_k3.S) [mlkem_poly_basemul_acc_montgomery_cached_k4.S](x86_64/mlkem/mlkem_poly_basemul_acc_montgomery_cached_k4.S)
   * x86_64 modular reduction: [mlkem_reduce.S](x86_64/mlkem/mlkem_reduce.S)
-  * x86_64 polynomial compression: [mlkem_tobytes.S](x86_64/mlkem/mlkem_tobytes.S)
+  * x86_64 polynomial compression: [mlkem_tobytes.S](x86_64/mlkem/mlkem_tobytes.S) [mlkem_poly_compress_d4.S](x86_64/mlkem/mlkem_poly_compress_d4.S) [mlkem_poly_compress_d5.S](x86_64/mlkem/mlkem_poly_compress_d5.S) [mlkem_poly_compress_d10.S](x86_64/mlkem/mlkem_poly_compress_d10.S) [mlkem_poly_compress_d11.S](x86_64/mlkem/mlkem_poly_compress_d11.S)
   * x86_64 rejection sampling: [mlkem_rej_uniform.S](x86_64/mlkem/mlkem_rej_uniform.S)
   * x86_64 polynomial deserialization: [mlkem_frombytes.S](x86_64/mlkem/mlkem_frombytes.S)
   * x86_64 conversion to Montgomery form: [mlkem_tomont.S](x86_64/mlkem/mlkem_tomont.S)
   * x86_64 polynomial unpacking: [mlkem_unpack.S](x86_64/mlkem/mlkem_unpack.S)
   * x86_64 'multiplication cache' computation: [mlkem_mulcache_compute.S](x86_64/mlkem/mlkem_mulcache_compute.S)
   * x86_64 polynomial decompression: [mlkem_poly_decompress_d4.S](x86_64/mlkem/mlkem_poly_decompress_d4.S) [mlkem_poly_decompress_d5.S](x86_64/mlkem/mlkem_poly_decompress_d5.S) [mlkem_poly_decompress_d10.S](x86_64/mlkem/mlkem_poly_decompress_d10.S) [mlkem_poly_decompress_d11.S](x86_64/mlkem/mlkem_poly_decompress_d11.S)
 
-Note again, though, that parts of the x86_64 backend are still in intrinsics; see [above](#intrinsics).
-
 <!--- bibliography --->
 [^HYBRID]: Becker, Kannwischer: Hybrid scalar/vector implementations of Keccak and SPHINCS+ on AArch64, [https://eprint.iacr.org/2022/1243](https://eprint.iacr.org/2022/1243)
 [^SLOTHY]: Abdulrahman, Becker, Kannwischer, Klein: SLOTHY superoptimizer, [https://github.com/slothy-optimizer/slothy/](https://github.com/slothy-optimizer/slothy/)