Remove unnecessary weak spec for mld_montgomery_reduce()

mld_montgomery_reduce() so far had two CBMC specs with varying
input/output bounds. However, it appears that the weak version
is not necessary and can be removed.

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

Author: hanno-becker

mldsa/reduce.h

@@ -48,12 +48,8 @@
  **************************************************/
 int32_t mld_montgomery_reduce(int64_t a)
 __contract__(
-  requires(a >= -MONTGOMERY_REDUCE_DOMAIN_MAX && a <= MONTGOMERY_REDUCE_DOMAIN_MAX)
-  ensures(return_value >= INT32_MIN && return_value < REDUCE32_DOMAIN_MAX)
-
-  /* Special case - for stronger input bounds, we can ensure stronger bounds on the output */
-  ensures((a >= -MONTGOMERY_REDUCE_STRONG_DOMAIN_MAX && a < MONTGOMERY_REDUCE_STRONG_DOMAIN_MAX) ==>
-          (return_value > -MLDSA_Q && return_value < MLDSA_Q))
+  requires(a >= -MONTGOMERY_REDUCE_STRONG_DOMAIN_MAX && a < MONTGOMERY_REDUCE_STRONG_DOMAIN_MAX)
+  ensures(return_value > -MLDSA_Q && return_value < MLDSA_Q)
 );
 
 #define mld_reduce32 MLD_NAMESPACE(reduce32)