Doc improvements

API-CONVENTIONS.md

@@ -20,6 +20,8 @@ All pointers are assumed to be valid and non-NULL, and every buffer is assumed t
 
 Every buffer in the ML-KEM API has a fixed size determined by the parameter set. There are no pointer/length pairs, and therefore no empty buffers for which a NULL pointer would be admissible.
 
+Buffers passed to the same function must not overlap.
+
 ## Output buffers on error
 
 When a function returns an error, each caller-owned output buffer is left either unchanged or fully zeroized. An output buffer is never left holding partially computed or otherwise stale data that could be mistaken for a valid result.

README.md

@@ -13,7 +13,7 @@
 mlkem-native is a secure, fast, and portable C90[^C90] implementation of ML-KEM[^FIPS203].
 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)
+All C code in [mlkem/src/*](mlkem) and [mlkem/src/fips202/*](mlkem/src/fips202), except for the backends for platforms other than AArch64 and x86_64 and the debug code, is proved memory-safe (no memory overflow) and type-safe (no integer overflow)
 using CBMC[^CBMC]. All AArch64 and x86_64 assembly is proved to be functionally correct,
 memory-safe, and of secret-independent timing (constant-time), using HOL-Light[^HOL-Light].
 
@@ -54,7 +54,7 @@ mlkem-native is used in
 
 ## Formal Verification
 
-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).
+All C code in [mlkem/src/*](mlkem) and [mlkem/src/fips202/*](mlkem/src/fips202), except for the backends for platforms other than AArch64 and x86_64 and the debug code, is proved memory-safe (no memory overflow) and type-safe (no integer overflow).
 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.
 
@@ -72,7 +72,8 @@ All AArch64 and x86_64 assembly in mlkem-native is formally proved in [HOL Light
 memory access patterns, and variable-latency instructions, thwarting most timing side channels
 (see [proofs/hol_light](proofs/hol_light) for details). C code is hardened against
 compiler-introduced timing side channels (such as KyberSlash[^KyberSlash] or clangover[^clangover])
-through suitable barriers and constant-time patterns.
+through suitable barriers and constant-time patterns. The C code assumes constant-time 32x32->32 and 32x32->64 multiplication,
+which some targets do not provide, e.g., cores without a hardware multiplier or with early-terminating multiply instructions.
 
 Absence of secret-dependent branches, memory-access patterns and variable-latency instructions is also tested using `valgrind`
 with various combinations of compilers and compilation options.

SOUNDNESS.md

@@ -180,11 +180,14 @@ intermediate computations would be flagged as undefined behavior. Constant-time
 are tested empirically using valgrind across many compilers and optimization levels (see
 the corresponding [CI job](.github/workflows/ct-tests.yml) for
 the full list), and the C code uses value barriers to prevent harmful compiler optimizations.
+These tests run on x86_64 and AArch64 in the default configuration only; other platforms and
+non-default configurations are not covered.
 
 **Potential improvements.**
 - Add automatic extraction of compiler coverage documentation from CI. ([#1608](https://github.com/pq-code-package/mlkem-native/issues/1608))
 - Introduce additional verification tooling that allows us to express functional correctness
   and constant-time properties for the C code. ([#1597](https://github.com/pq-code-package/mlkem-native/issues/1597), [#1598](https://github.com/pq-code-package/mlkem-native/issues/1598))
+- Run the constant-time tests on the RISC-V and PowerPC backends. ([#1788](https://github.com/pq-code-package/mlkem-native/issues/1788))
 
 ### A3. Specification faithfulness
 

mlkem/mlkem_native.h

@@ -32,7 +32,9 @@
  * # API conventions
  *
  * Conventions shared by all functions below (return values, pointer validity,
- * output buffers on error) are documented in API-CONVENTIONS.md.
+ * buffer overlap, output buffers on error) are documented in
+ * API-CONVENTIONS.md. In particular, buffers passed to the same function must
+ * not overlap.
  *
  * # Multi-level builds
  *