Introduce helper functions for signed<-> unsigned conversions

This commit introduces helper functions mld_cast_uint32_to_int32,
mld_cast_int32_to_uint32, and mld_cast_int64_to_uint32
for int64_t->uint32_t, and int32_t <-> uint32_t.

This cleans up prior code and also removes the need for some pragmas stopping
CBMC from flagging value-changing integer conversions.

This commit is based on
pq-code-package/mlkem-native@e5adf3a
(but for 32-bit integers.

Signed-off-by: Matthias J. Kannwischer <[email protected]>

Author: mkannwischer

mldsa/ct.h

@@ -111,18 +111,67 @@ __contract__(ensures(return_value == b))
 }
 #endif /* MLD_USE_ASM_VALUE_BARRIER */
 
-
-/*
- * The mld_ct_sel_int32 function below makes deliberate use of unsigned
- * to signed integer conversion, which is implementation-defined
- * behaviour. Here, we assume that uint16_t -> int16_t is inverse
- * to int16_t -> uint16_t.
- */
 #ifdef CBMC
 #pragma CPROVER check push
 #pragma CPROVER check disable "conversion"
 #endif
 
+/*************************************************
+ * Name:        mld_cast_uint32_to_int32
+ *
+ * Description: Cast uint32 value to int32
+ *
+ * Returns:     For uint32_t x, the unique y in int32_t
+ *              so that x == y mod 2^32.
+ *
+ *              Concretely:
+ *              - x <  2^31: returns x
+ *              - x >= 2^31: returns x - 2^31
+ *
+ **************************************************/
+static MLD_ALWAYS_INLINE int32_t mld_cast_uint32_to_int32(uint32_t x)
+{
+  /*
+   * PORTABILITY: This relies on uint32_t -> int32_t
+   * being implemented as the inverse of int32_t -> uint32_t,
+   * which is implementation-defined (C99 6.3.1.3 (3))
+   * CBMC (correctly) fails to prove this conversion is OK,
+   * so we have to suppress that check here
+   */
+  return (int32_t)x;
+}
+
+#ifdef CBMC
+#pragma CPROVER check pop
+#endif
+
+
+/*************************************************
+ * Name:        mld_cast_int64_to_uint32
+ *
+ * Description: Cast int64 value to uint32 as per C standard.
+ *
+ * Returns:     For int64_t x, the unique y in uint32_t
+ *              so that x == y mod 2^32.
+ **************************************************/
+static MLD_ALWAYS_INLINE uint32_t mld_cast_int64_to_uint32(int64_t x)
+{
+  return (uint32_t)(x & (int64_t)UINT32_MAX);
+}
+
+/*************************************************
+ * Name:        mld_cast_int32_to_uint32
+ *
+ * Description: Cast int32 value to uint32 as per C standard.
+ *
+ * Returns:     For int32_t x, the unique y in uint32_t
+ *              so that x == y mod 2^32.
+ **************************************************/
+static MLD_ALWAYS_INLINE uint32_t mld_cast_int32_to_uint32(int32_t x)
+{
+  return mld_cast_int64_to_uint32((int64_t)x);
+}
+
 /*************************************************
  * Name:        mld_ct_sel_int32
  *
@@ -137,35 +186,17 @@ __contract__(ensures(return_value == b))
  *
  **************************************************/
 static MLD_INLINE int32_t mld_ct_sel_int32(int32_t a, int32_t b, uint32_t cond)
-/* TODO: proof */
 __contract__(
   requires(cond == 0x0 || cond == 0xFFFFFFFF)
   ensures(return_value == (cond ? a : b))
 )
 {
-  uint32_t au = a, bu = b;
+  uint32_t au = mld_cast_int32_to_uint32(a);
+  uint32_t bu = mld_cast_int32_to_uint32(b);
   uint32_t res = bu ^ (mld_value_barrier_u32(cond) & (au ^ bu));
-  return (int32_t)res;
+  return mld_cast_uint32_to_int32(res);
 }
 
-/* Put unsigned-to-signed warnings in CBMC back into scope */
-#ifdef CBMC
-#pragma CPROVER check pop
-#endif
-
-
-
-/*
- * The mld_ct_cmask_neg_i32 function below makes deliberate use of
- * signed to unsigned integer conversion, which is fully defined
- * behaviour in C. It is thus safe to disable this warning.
- */
-#ifdef CBMC
-#pragma CPROVER check push
-#pragma CPROVER check disable "conversion"
-#endif
-
-
 /*************************************************
  * Name:        mld_ct_cmask_neg_i32
  *
@@ -174,22 +205,16 @@ __contract__(
  * Arguments:   int32_t x: Value to be converted into a mask
  *
  **************************************************/
-/* TODO: proof */
 static MLD_INLINE uint32_t mld_ct_cmask_neg_i32(int32_t x)
 __contract__(
   ensures(return_value == ((x < 0) ? 0xFFFFFFFF : 0))
 )
 {
   int64_t tmp = mld_value_barrier_i64((int64_t)x);
   tmp >>= 31;
-  return (uint32_t)tmp;
+  return mld_cast_int64_to_uint32(tmp);
 }
 
-/* Put signed-to-unsigned warnings in CBMC back into scope */
-#ifdef CBMC
-#pragma CPROVER check pop
-#endif
-
 /*************************************************
  * Name:        mld_ct_abs_i32
  *
@@ -198,7 +223,6 @@ __contract__(
  * Arguments:   int32_t x: Input value
  *
  **************************************************/
-/* TODO: proof */
 static MLD_INLINE int32_t mld_ct_abs_i32(int32_t x)
 __contract__(
   requires(x >= -INT32_MAX)

mldsa/reduce.h

@@ -27,36 +27,6 @@
 /* Absolute bound for tight domain of mld_montgomery_reduce() */
 #define MONTGOMERY_REDUCE_STRONG_DOMAIN_MAX ((int64_t)INT32_MIN * -MLDSA_Q)
 
-
-
-/*************************************************
- * Name:        mld_cast_uint32_to_int32
- *
- * Description: Cast uint32 value to int32
- *
- * Returns:
- *   input x in     0 .. 2^31-1: returns value unchanged
- *   input x in  2^31 .. 2^32-1: returns (x - 2^32)
- **************************************************/
-#ifdef CBMC
-#pragma CPROVER check push
-#pragma CPROVER check disable "conversion"
-#endif
-static MLD_INLINE int32_t mld_cast_uint32_to_int32(uint32_t x)
-{
-  /*
-   * PORTABILITY: This relies on uint32_t -> int32_t
-   * being implemented as the inverse of int32_t -> uint32_t,
-   * which is implementation-defined (C99 6.3.1.3 (3))
-   * CBMC (correctly) fails to prove this conversion is OK,
-   * so we have to suppress that check here
-   */
-  return (int32_t)x;
-}
-#ifdef CBMC
-#pragma CPROVER check pop
-#endif
-
 /*************************************************
  * Name:        mld_montgomery_reduce
  *