README: Add warning that MLD_CONFIG_REDUCE_RAM is not covered by CBMC

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

Author: mkannwischer

README.md

@@ -50,6 +50,8 @@ make test
 
 We use the [C Bounded Model Checker (CBMC)](https://github.com/diffblue/cbmc) to prove absence of various classes of undefined behaviour in C, including out of bounds memory accesses and integer overflows. The proofs cover all C code in [mldsa/src/*](mldsa) and [mldsa/src/fips202/*](mldsa/src/fips202) involved in running mldsa-native with its C backend. See [proofs/cbmc](proofs/cbmc) for details.
 
+**Note:** The `MLD_CONFIG_REDUCE_RAM` configuration option is not currently covered by CBMC proofs.
+
 HOL-Light functional correctness proofs can be found in [proofs/hol_light/x86_64](proofs/hol_light/x86_64). So far, the following functions have been proven correct:
 
 - x86_64 NTT [ntt.S](mldsa/src/native/x86_64/src/ntt.S)