Unify native interface for verify with other native functions

Signed-off-by: Hanno Becker <[email protected]>

mlkem/native/aarch64/arith_native_aarch64.h

@@ -83,6 +83,5 @@ void polyvec_basemul_acc_montgomery_cached_asm_opt(int16_t *r, const int16_t *a,
                                                    const int16_t *b,
                                                    const int16_t *b_cache);
 
-
 #endif /* MLKEM_USE_NATIVE_AARCH64 */
 #endif /* MLKEM_AARCH64_NATIVE_H */

mlkem/native/aarch64/profiles/clean.h

@@ -74,4 +74,6 @@ static inline int rej_uniform_native(int16_t *r, unsigned int len,
   return (int)rej_uniform_asm_clean(r, buf, buflen);
 }
 
+#include "../verify-aarch64.h"
+
 #endif /* MLKEM_ARITH_NATIVE_PROFILE_H */

mlkem/native/aarch64/profiles/opt.h

@@ -74,4 +74,6 @@ static inline int rej_uniform_native(int16_t *r, unsigned int len,
   return (int)rej_uniform_asm_clean(r, buf, buflen);
 }
 
+#include "../verify-aarch64.h"
+
 #endif /* MLKEM_ARITH_NATIVE_PROFILE_H */

mlkem/native/aarch64/verify-aarch64.h

@@ -40,7 +40,6 @@ static inline void cmov_native(uint8_t *r, const uint8_t *x, size_t len,
   }
 }
 
-
 static inline void cmov_int16_native(int16_t *r, const int16_t v,
                                      const uint16_t b)
 {

mlkem/native/arith_native.h

@@ -43,6 +43,52 @@
 // The macro before each declaration controls whether a native
 // implementation is present.
 
+#if defined(MLKEM_USE_NATIVE_VERIFY)
+/*************************************************
+ * Name:        verify_native
+ *
+ * Description: Compare two arrays for equality in constant time.
+ *
+ * Arguments:   const uint8_t *a: pointer to first byte array
+ *              const uint8_t *b: pointer to second byte array
+ *              size_t len:       length of the byte arrays
+ *
+ * Returns 0 if the byte arrays are equal, 1 otherwise
+ **************************************************/
+static inline int verify_native(const uint8_t *a, const uint8_t *b,
+                                const size_t len);
+
+/*************************************************
+ * Name:        cmov
+ *
+ * Description: Copy len bytes from x to r if b is 1;
+ *              don't modify x if b is 0. Requires b to be in {0,1};
+ *              assumes two's complement representation of negative integers.
+ *              Runs in constant time.
+ *
+ * Arguments:   uint8_t *r:       pointer to output byte array
+ *              const uint8_t *x: pointer to input byte array
+ *              size_t len:       Amount of bytes to be copied
+ *              uint8_t b:        Condition bit; has to be in {0,1}
+ **************************************************/
+static inline void cmov_native(uint8_t *r, const uint8_t *x, size_t len,
+                               uint8_t b);
+
+/*************************************************
+ * Name:        cmov_int16_native
+ *
+ * Description: Copy input v to *r if b is 1, don't modify *r if b is 0.
+ *              Requires b to be in {0,1};
+ *              Runs in constant time.
+ *
+ * Arguments:   int16_t *r:       pointer to output int16_t
+ *              int16_t v:        input int16_t. Must not be NULL
+ *              uint16_t b:       Condition bit; has to be in {0,1}
+ **************************************************/
+static inline void cmov_int16_native(int16_t *r, const int16_t v,
+                                     const uint16_t b);
+#endif /* MLKEM_USE_NATIVE_VERIFY */
+
 #if defined(MLKEM_USE_NATIVE_NTT)
 /*************************************************
  * Name:        ntt_native

mlkem/native/x86_64/profiles/default.h

@@ -101,4 +101,6 @@ static inline void poly_frombytes_native(poly *r,
   nttfrombytes_avx2((__m256i *)r->coeffs, a, qdata.vec);
 }
 
+#include "../verify-x86_64.h"
+
 #endif /* MLKEM_ARITH_NATIVE_PROFILE_H */

mlkem/verify.h

@@ -10,24 +10,6 @@
 #include "cbmc.h"
 #include "params.h"
 
-// If a native backend is used, we include the native implementations from the
-// backend as those are using inline assembly. This guarantees that these
-// gadgets are constant-time, but also allows the compiler to inline them.
-// Otherwise, we use the reference code (verify.c) in a separate compilation
-// unit.
-#if defined(MLKEM_USE_NATIVE_VERIFY)
-#include "cpucap.h"
-
-#if defined(SYS_AARCH64)
-#include "verify-aarch64.h"
-#endif /* SYS_AARCH64 */
-
-#if defined(SYS_X86_64)
-#include "verify-x86_64.h"
-#endif /* SYS_X86_64 */
-#endif
-
-
 #define verify MLKEM_NAMESPACE(verify)
 /*************************************************
  * Name:        verify