Remove NTT_BOUND_NATIVE and INVNTT_BOUND_NATIVE

The numeric macros NTT_BOUND_NATIVE and INVNTT_BOUND_NATIVE could be used by backends to specify an output bound for the forward and inverse NTT. We would then use STATIC_ASSERT's to check that those backend-specific bounds would imply the bounds (NTT_BOUND and INVNTT_BOUND) that the CBMC proofs work against. The added value of NTT_BOUND_NATIVE and INVNTT_BOUND_NATIVE is questionable. In the end, what we care about is that the native NTT and invNTT adhere to the bounds that CBMC relies on. Any strengthening of the bounds may be good to know, but is otherwise an unnecessary complication of the code. This commit removes NTT_BOUND_NATIVE and INVNTT_BOUND_NATIVE and uses the contractual bounds NTT_BOUND and INVNT_BOUND in their place. Similarly, INVNTT_BOUND_REF is removed, which is finer bound for the reference invNTT. Signed-off-by: Hanno Becker <[email protected]>
pq-code-package · Jan 13, 2025 · d1a18b0 · d1a18b0
1 parent 3c808fe
commit d1a18b0
Show file tree

Hide file tree

Showing 5 changed files with 3 additions and 49 deletions.
diff --git a/examples/monolithic_build/mlkem_native_monobuild.c b/examples/monolithic_build/mlkem_native_monobuild.c
@@ -1018,11 +1018,6 @@
 #undef MLKEM_USE_NATIVE_REJ_UNIFORM
 #endif
 
-/* mlkem/native/aarch64/src/clean_impl.h */
-#if defined(INVNTT_BOUND_NATIVE)
-#undef INVNTT_BOUND_NATIVE
-#endif
-
 /* mlkem/native/aarch64/src/consts.h */
 #if defined(MLKEM_NATIVE_AARCH64_CONSTS)
 #undef MLKEM_NATIVE_AARCH64_CONSTS
@@ -1083,16 +1078,6 @@
 #undef MLKEM_USE_NATIVE_REJ_UNIFORM
 #endif
 
-/* mlkem/native/aarch64/src/opt_impl.h */
-#if defined(NTT_BOUND_NATIVE)
-#undef NTT_BOUND_NATIVE
-#endif
-
-/* mlkem/native/aarch64/src/opt_impl.h */
-#if defined(INVNTT_BOUND_NATIVE)
-#undef INVNTT_BOUND_NATIVE
-#endif
-
 /* mlkem/native/aarch64/src/rej_uniform_table.c */
 #if defined(empty_cu_aarch64_rej_uniform_table)
 #undef empty_cu_aarch64_rej_uniform_table
@@ -1463,16 +1448,6 @@
 #undef MLKEM_USE_NATIVE_POLY_FROMBYTES
 #endif
 
-/* mlkem/native/x86_64/src/default_impl.h */
-#if defined(INVNTT_BOUND_NATIVE)
-#undef INVNTT_BOUND_NATIVE
-#endif
-
-/* mlkem/native/x86_64/src/default_impl.h */
-#if defined(NTT_BOUND_NATIVE)
-#undef NTT_BOUND_NATIVE
-#endif
-
 /* mlkem/native/x86_64/src/rej_uniform_avx2.c */
 #if defined(_mm256_cmpge_epu16)
 #undef _mm256_cmpge_epu16
@@ -1508,11 +1483,6 @@
 #undef invntt_layer
 #endif
 
-/* mlkem/ntt.c */
-#if defined(INVNTT_BOUND_REF)
-#undef INVNTT_BOUND_REF
-#endif
-
 /* mlkem/ntt.h */
 #if defined(NTT_H)
 #undef NTT_H

diff --git a/mlkem/native/aarch64/src/clean_impl.h b/mlkem/native/aarch64/src/clean_impl.h
@@ -31,7 +31,6 @@ static INLINE void ntt_native(poly *data)
                 aarch64_ntt_zetas_layer56);
 }
 
-#define INVNTT_BOUND_NATIVE (8 * MLKEM_Q)
 static INLINE void intt_native(poly *data)
 {
   intt_asm_clean(data->coeffs, aarch64_invntt_zetas_layer01234,

diff --git a/mlkem/native/aarch64/src/opt_impl.h b/mlkem/native/aarch64/src/opt_impl.h
@@ -25,14 +25,12 @@
 #define MLKEM_USE_NATIVE_POLY_TOBYTES
 #define MLKEM_USE_NATIVE_REJ_UNIFORM
 
-#define NTT_BOUND_NATIVE (6 * MLKEM_Q)
 static INLINE void ntt_native(poly *data)
 {
   ntt_asm_opt(data->coeffs, aarch64_ntt_zetas_layer01234,
               aarch64_ntt_zetas_layer56);
 }
 
-#define INVNTT_BOUND_NATIVE (8 * MLKEM_Q)
 static INLINE void intt_native(poly *data)
 {
   intt_asm_opt(data->coeffs, aarch64_invntt_zetas_layer01234,

diff --git a/mlkem/native/x86_64/src/default_impl.h b/mlkem/native/x86_64/src/default_impl.h
@@ -28,9 +28,6 @@
 #define MLKEM_USE_NATIVE_POLY_TOBYTES
 #define MLKEM_USE_NATIVE_POLY_FROMBYTES
 
-#define INVNTT_BOUND_NATIVE (8 * MLKEM_Q)
-#define NTT_BOUND_NATIVE (8 * MLKEM_Q)
-
 static INLINE void poly_permute_bitrev_to_custom(poly *data)
 {
   nttunpack_avx2((__m256i *)(data->coeffs), qdata.vec);

diff --git a/mlkem/ntt.c b/mlkem/ntt.c
@@ -148,24 +148,17 @@ void poly_ntt(poly *p)
 }
 #else  /* MLKEM_USE_NATIVE_NTT */
 
-/* Check that bound for native NTT implies contractual bound */
-STATIC_ASSERT(NTT_BOUND_NATIVE <= NTT_BOUND, invntt_bound)
-
 MLKEM_NATIVE_INTERNAL_API
 void poly_ntt(poly *p)
 {
   POLY_BOUND_MSG(p, MLKEM_Q, "native ntt input");
   ntt_native(p);
-  POLY_BOUND_MSG(p, NTT_BOUND_NATIVE, "native ntt output");
+  POLY_BOUND_MSG(p, NTT_BOUND, "native ntt output");
 }
 #endif /* MLKEM_USE_NATIVE_NTT */
 
 #if !defined(MLKEM_USE_NATIVE_INTT)
 
-/* Check that bound for reference invNTT implies contractual bound */
-#define INVNTT_BOUND_REF (3 * MLKEM_Q / 4)
-STATIC_ASSERT(INVNTT_BOUND_REF <= INVNTT_BOUND, invntt_bound)
-
 /* Compute one layer of inverse NTT */
 static void invntt_layer(int16_t *r, int len, int layer)
 __contract__(
@@ -232,18 +225,15 @@ void poly_invntt_tomont(poly *p)
     invntt_layer(p->coeffs, len, layer);
   }
 
-  POLY_BOUND_MSG(p, INVNTT_BOUND_REF, "ref intt output");
+  POLY_BOUND_MSG(p, INVNTT_BOUND, "ref intt output");
 }
 #else  /* MLKEM_USE_NATIVE_INTT */
 
-/* Check that bound for native invNTT implies contractual bound */
-STATIC_ASSERT(INVNTT_BOUND_NATIVE <= INVNTT_BOUND, invntt_bound)
-
 MLKEM_NATIVE_INTERNAL_API
 void poly_invntt_tomont(poly *p)
 {
   intt_native(p);
-  POLY_BOUND_MSG(p, INVNTT_BOUND_NATIVE, "native intt output");
+  POLY_BOUND_MSG(p, INVNTT_BOUND, "native intt output");
 }
 #endif /* MLKEM_USE_NATIVE_INTT */