Merge pull request #479 from pq-code-package/remove_todo

Resolve or remove various small TODOs

Author: hanno-becker

cbmc/proofs/poly_compress_du/Makefile

@@ -19,12 +19,16 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
 PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c
 
 CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)poly_compress_du
+USE_FUNCTION_CONTRACTS =
+
+# TODO: We should be calling scalar_decompress_xxx by contract here,
+# but it does not seem to work yet because they are marked as static inline.
 # For K = 2 or 3, the code calls scalar_compress_d10, so
-ifeq ($(MLKEM_K),4)
-USE_FUNCTION_CONTRACTS = scalar_compress_d11
-else
-USE_FUNCTION_CONTRACTS = scalar_compress_d10
-endif
+# ifeq ($(MLKEM_K),4)
+# USE_FUNCTION_CONTRACTS = scalar_compress_d11
+# else
+# USE_FUNCTION_CONTRACTS = scalar_compress_d10
+# endif
 
 APPLY_LOOP_CONTRACTS=on
 USE_DYNAMIC_FRAMES=1

cbmc/proofs/poly_compress_dv/Makefile

@@ -19,11 +19,15 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
 PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c
 
 CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)poly_compress_dv
-ifeq ($(MLKEM_K),4)
-USE_FUNCTION_CONTRACTS = scalar_compress_d5
-else
-USE_FUNCTION_CONTRACTS = scalar_compress_d4
-endif
+
+USE_FUNCTION_CONTRACTS =
+# TODO: We should be calling scalar_decompress_xxx by contract here,
+# but it does not seem to work yet because they are marked as static inline.
+# ifeq ($(MLKEM_K),4)
+# USE_FUNCTION_CONTRACTS = scalar_compress_d5
+# else
+# USE_FUNCTION_CONTRACTS = scalar_compress_d4
+# endif
 APPLY_LOOP_CONTRACTS=on
 USE_DYNAMIC_FRAMES=1
 

cbmc/proofs/poly_decompress_du/Makefile

@@ -20,12 +20,15 @@ PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c
 
 CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)poly_decompress_du
 
+USE_FUNCTION_CONTRACTS =
+# TODO: We should be calling scalar_decompress_xxx by contract here,
+# but it does not seem to work yet because they are marked as static inline.
 # For K = 2 or 3, the code calls scalar_decompress_d10, so
-ifeq ($(MLKEM_K),4)
-USE_FUNCTION_CONTRACTS = scalar_decompress_d11
-else
-USE_FUNCTION_CONTRACTS = scalar_decompress_d10
-endif
+# ifeq ($(MLKEM_K),4)
+# USE_FUNCTION_CONTRACTS = scalar_decompress_d11
+# else
+# USE_FUNCTION_CONTRACTS = scalar_decompress_d10
+# endif
 
 APPLY_LOOP_CONTRACTS=on
 USE_DYNAMIC_FRAMES=1

cbmc/proofs/poly_decompress_dv/Makefile

@@ -20,12 +20,15 @@ PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c
 
 CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)poly_decompress_dv
 
+USE_FUNCTION_CONTRACTS =
+# TODO: We should be calling scalar_decompress_xxx by contract here,
+# but it does not seem to work yet because they are marked as static inline.
 # For K = 2 or 3, the code calls scalar_decompress_d4, so
-ifeq ($(MLKEM_K),4)
-USE_FUNCTION_CONTRACTS = scalar_decompress_d5
-else
-USE_FUNCTION_CONTRACTS = scalar_decompress_d4
-endif
+# ifeq ($(MLKEM_K),4)
+# USE_FUNCTION_CONTRACTS = scalar_decompress_d5
+# else
+# USE_FUNCTION_CONTRACTS = scalar_decompress_d4
+# endif
 
 APPLY_LOOP_CONTRACTS=on
 USE_DYNAMIC_FRAMES=1

mlkem/indcpa.c

@@ -61,9 +61,11 @@ static void unpack_pk(polyvec *pk, uint8_t seed[MLKEM_SYMBYTES],
   memcpy(seed, packedpk + MLKEM_POLYVECBYTES, MLKEM_SYMBYTES);
 
   /*
-   * TODO! pk must be subject to a "modulus check" at the top-level
-   * crypto_kem_enc_derand(). Once that's done, the reduction is no
-   * longer necessary here.
+   * TODO! We know from the modulus check that this will result in an
+   * unsigned canonical polynomial, but CBMC does not know it. We should
+   * weaken the specification of `unpack_pk()` and all depending functions
+   * to work with the weaker 4096-bound, so that the proofs go through
+   * without the need of this redundant call to polyvec_reduce().
    */
   polyvec_reduce(pk);
 }
@@ -291,13 +293,6 @@ void gen_matrix(polyvec *a, const uint8_t seed[MLKEM_SYMBYTES], int transposed)
     memcpy(seedxy[j], seed, MLKEM_SYMBYTES);
   }
 
-  /*
-   * TODO: All loops in this function should be unrolled for decent
-   * performance.
-   * Either add suitable pragmas, or split gen_matrix according to MLKEM_K
-   * and unroll by hand.
-   */
-
   for (i = 0; i < (MLKEM_K * MLKEM_K / KECCAK_WAY) * KECCAK_WAY;
        i += KECCAK_WAY)
   {

mlkem/native/arith_native.h

@@ -240,7 +240,7 @@ static INLINE void poly_frombytes_native(poly *a,
  *
  * Return -1 if the native implementation does not support the input lengths.
  * Otherwise, returns non-negative number of sampled 16-bit integers (at most
- *len).
+ * len).
  **************************************************/
 static INLINE int rej_uniform_native(int16_t *r, unsigned int len,
                                      const uint8_t *buf, unsigned int buflen);

mlkem/native/x86_64/arith_native_x86_64.h

@@ -20,7 +20,6 @@
   ((12 * MLKEM_N / 8 * (1 << 12) / MLKEM_Q + SHAKE128_RATE) / SHAKE128_RATE)
 #define REJ_UNIFORM_AVX_BUFLEN (REJ_UNIFORM_AVX_NBLOCKS * SHAKE128_RATE)
 
-/* TODO: Document buffer constraints */
 #define rej_uniform_avx2 MLKEM_NAMESPACE(rej_uniform_avx2)
 unsigned int rej_uniform_avx2(int16_t *r, const uint8_t *buf);
 

mlkem/native/x86_64/profiles/default.h

@@ -74,13 +74,7 @@ static INLINE void poly_mulcache_compute_native(poly_mulcache *x, const poly *y)
 {
   /* AVX2 backend does not use mulcache */
   ((void)y);
-
-  /*
-   * TODO! The mulcache is subject to the absolute bound < q
-   * This needs to be dropped if the mulcache is not present.
-   * Until that's done, memset to 0 to avoid failure.
-   */
-  memset(x, 0, sizeof(poly_mulcache));
+  ((void)x);
 }
 
 static INLINE void polyvec_basemul_acc_montgomery_cached_native(

mlkem/poly.c

@@ -456,6 +456,8 @@ void poly_basemul_montgomery_cached(poly *r, const poly *a, const poly *b,
                                     const poly_mulcache *b_cache)
 {
   int i;
+  POLY_BOUND(b_cache, MLKEM_Q);
+
   for (i = 0; i < MLKEM_N / 4; i++)
   __loop__(
     assigns(i, object_whole(r))
@@ -559,6 +561,8 @@ void poly_mulcache_compute(poly_mulcache *x, const poly *a)
 void poly_mulcache_compute(poly_mulcache *x, const poly *a)
 {
   poly_mulcache_compute_native(x, a);
-  POLY_BOUND(x, MLKEM_Q);
+  /* Omitting POLY_BOUND(x, MLKEM_Q) since native implementations may
+   * decide not to use a mulcache. Note that the C backend implementation
+   * of poly_basemul_montgomery_cached() does still include the check. */
 }
 #endif /* MLKEM_USE_NATIVE_POLY_MULCACHE_COMPUTE */

mlkem/poly.h

@@ -192,9 +192,7 @@ __contract__(
 #pragma CPROVER check push
 #pragma CPROVER check disable "unsigned-overflow"
 #endif
-/* TODO: do the same for the other static inline functions */
-STATIC_INLINE_TESTABLE
-uint32_t scalar_compress_d10(uint16_t u)
+static INLINE uint32_t scalar_compress_d10(uint16_t u)
 __contract__(
   requires(u <= MLKEM_Q - 1)
   ensures(return_value < (1u << 10))
@@ -244,8 +242,7 @@ __contract__(
 #pragma CPROVER check push
 #pragma CPROVER check disable "unsigned-overflow"
 #endif
-STATIC_INLINE_TESTABLE
-uint32_t scalar_compress_d11(uint16_t u)
+static INLINE uint32_t scalar_compress_d11(uint16_t u)
 __contract__(
   requires(u <= MLKEM_Q - 1)
   ensures(return_value < (1u << 11))
@@ -270,8 +267,7 @@ __contract__(
  * Arguments: - u: Unsigned canonical modulus modulo 16
  *                 to be decompressed.
  ************************************************************/
-STATIC_INLINE_TESTABLE
-uint16_t scalar_decompress_d11(uint32_t u)
+static INLINE uint16_t scalar_decompress_d11(uint32_t u)
 __contract__(
   requires(0 <= u && u < 2048)
   ensures(return_value <= (MLKEM_Q - 1))
@@ -295,8 +291,7 @@ __contract__(
  *
  * Arguments: c: signed coefficient to be converted
  ************************************************************/
-STATIC_INLINE_TESTABLE
-uint16_t scalar_signed_to_unsigned_q(int16_t c)
+static INLINE uint16_t scalar_signed_to_unsigned_q(int16_t c)
 __contract__(
   requires(c >= -(MLKEM_Q - 1) && c <= (MLKEM_Q - 1))
   ensures(return_value >= 0 && return_value <= (MLKEM_Q - 1))

mlkem/polyvec.c

@@ -128,7 +128,9 @@ void polyvec_basemul_acc_montgomery_cached(poly *r, const polyvec *a,
 {
   POLYVEC_BOUND(a, MLKEM_Q);
   POLYVEC_BOUND(b, NTT_BOUND);
-  POLYVEC_BOUND(b_cache, MLKEM_Q);
+  /* Omitting POLYVEC_BOUND(b_cache, MLKEM_Q) since native implementations may
+   * decide not to use a mulcache. Note that the C backend implementation
+   * of poly_basemul_montgomery_cached() does still include the check. */
   polyvec_basemul_acc_montgomery_cached_native(r, a, b, b_cache);
 }
 #endif /* MLKEM_USE_NATIVE_POLYVEC_BASEMUL_ACC_MONTGOMERY_CACHED */