FIPS202: Add native x4 XOR/extract bytes interface

Extend the FIPS202 native backend API to support implementing XORBytes and
ExtractBytes steps in native code.

This is essential for backends using custom state representations (e.g.,
bit-interleaved state), where these functions handle conversion to/from
the internal format on-the-fly. In such cases, they also account for a
significant amount of processing time.

New flags:
- MLD_USE_FIPS202_X4_XOR_BYTES_NATIVE: Backend provides native XOR bytes
- MLD_USE_FIPS202_X4_EXTRACT_BYTES_NATIVE: Backend provides native extract bytes

When set, backends provide native implementations for:
- mld_keccakf1600_xor_bytes_x4_native: XOR input data into state
- mld_keccakf1600_extract_bytes_x4_native: Extract output from state

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

Author: mkannwischer

mldsa/src/fips202/native/api.h

@@ -66,4 +66,64 @@ __contract__(
 );
 #endif /* MLD_USE_FIPS202_X4_NATIVE */
 
+/*
+ * Native x4 XOR bytes and extract bytes interface.
+ *
+ * These functions allow backends to provide optimized implementations for
+ * XORing input data into the state and extracting output data from the state.
+ * This is particularly useful for backends that use a different internal state
+ * representation (e.g., bit-interleaved), as conversion can happen during
+ * XOR/extract rather than before/after each permutation.
+ *
+ * NOTE: We assume that the custom representation of the zero state is the
+ * all-zero state.
+ *
+ * MLD_USE_FIPS202_X4_XOR_BYTES_NATIVE: Backend provides native XOR bytes
+ * MLD_USE_FIPS202_X4_EXTRACT_BYTES_NATIVE: Backend provides native extract
+ * bytes
+ */
+
+#if defined(MLD_USE_FIPS202_X4_XOR_BYTES_NATIVE)
+MLD_MUST_CHECK_RETURN_VALUE
+static MLD_INLINE int mld_keccakf1600_xor_bytes_x4_native(
+    uint64_t *state, const unsigned char *data0, const unsigned char *data1,
+    const unsigned char *data2, const unsigned char *data3, unsigned offset,
+    unsigned length)
+__contract__(
+  requires(0 <= offset && offset <= 25 * sizeof(uint64_t) &&
+           0 <= length && length <= 25 * sizeof(uint64_t) - offset)
+  requires(memory_no_alias(state, sizeof(uint64_t) * 25 * 4))
+  requires(memory_no_alias(data0, length))
+  requires((data0 == data1 &&
+            data0 == data2 &&
+            data0 == data3) ||
+           (memory_no_alias(data1, length) &&
+            memory_no_alias(data2, length) &&
+            memory_no_alias(data3, length)))
+  assigns(memory_slice(state, sizeof(uint64_t) * 25 * 4))
+  ensures(return_value == MLD_NATIVE_FUNC_FALLBACK || return_value == MLD_NATIVE_FUNC_SUCCESS)
+  ensures((return_value == MLD_NATIVE_FUNC_FALLBACK) ==> array_unchanged_u64(state, 25 * 4)));
+#endif /* MLD_USE_FIPS202_X4_XOR_BYTES_NATIVE */
+
+#if defined(MLD_USE_FIPS202_X4_EXTRACT_BYTES_NATIVE)
+MLD_MUST_CHECK_RETURN_VALUE
+static MLD_INLINE int mld_keccakf1600_extract_bytes_x4_native(
+    uint64_t *state, unsigned char *data0, unsigned char *data1,
+    unsigned char *data2, unsigned char *data3, unsigned offset,
+    unsigned length)
+__contract__(
+  requires(0 <= offset && offset <= 25 * sizeof(uint64_t) &&
+           0 <= length && length <= 25 * sizeof(uint64_t) - offset)
+  requires(memory_no_alias(state, sizeof(uint64_t) * 25 * 4))
+  requires(memory_no_alias(data0, length))
+  requires(memory_no_alias(data1, length))
+  requires(memory_no_alias(data2, length))
+  requires(memory_no_alias(data3, length))
+  assigns(memory_slice(data0, length))
+  assigns(memory_slice(data1, length))
+  assigns(memory_slice(data2, length))
+  assigns(memory_slice(data3, length))
+  ensures(return_value == MLD_NATIVE_FUNC_FALLBACK || return_value == MLD_NATIVE_FUNC_SUCCESS));
+#endif /* MLD_USE_FIPS202_X4_EXTRACT_BYTES_NATIVE */
+
 #endif /* !MLD_FIPS202_NATIVE_API_H */