Remove now-redundant preconditions

Signed-off-by: Rod Chapman <[email protected]>

Author: rod-chapman

mldsa/src/polyvec.h

@@ -93,8 +93,6 @@ __contract__(
   requires(forall(p0, 0, MLDSA_L, array_abs_bound(u->vec[p0].coeffs, 0 , MLDSA_N, MLD_INTT_BOUND)))
   requires(forall(p1, 0, MLDSA_L,
                   array_bound(v->vec[p1].coeffs, 0, MLDSA_N, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1)))
-  requires(forall(p2, 0, MLDSA_L, forall(p3, 0, MLDSA_N, (int64_t) u->vec[p2].coeffs[p3] + v->vec[p2].coeffs[p3] < REDUCE32_DOMAIN_MAX)))
-  requires(forall(p4, 0, MLDSA_L, forall(p5, 0, MLDSA_N, (int64_t) u->vec[p4].coeffs[p5] + v->vec[p4].coeffs[p5] >= INT32_MIN)))
   assigns(object_whole(u))
   ensures(forall(q0, 0, MLDSA_L, forall(q1, 0, MLDSA_N, u->vec[q0].coeffs[q1] == old(*u).vec[q0].coeffs[q1] + v->vec[q0].coeffs[q1])))
   ensures(forall(q2, 0, MLDSA_L,
@@ -294,8 +292,6 @@ __contract__(
   requires(forall(p0, 0, MLDSA_K, array_abs_bound(u->vec[p0].coeffs, 0, MLDSA_N, MLD_INTT_BOUND)))
   requires(forall(p1, 0, MLDSA_K,
     array_bound(v->vec[p1].coeffs, 0, MLDSA_N, -REDUCE32_RANGE_MAX, REDUCE32_RANGE_MAX)))
-  requires(forall(p2, 0, MLDSA_K, forall(p3, 0, MLDSA_N, (int64_t) u->vec[p2].coeffs[p3] + v->vec[p2].coeffs[p3] < REDUCE32_DOMAIN_MAX)))
-  requires(forall(p4, 0, MLDSA_K, forall(p5, 0, MLDSA_N, (int64_t) u->vec[p4].coeffs[p5] + v->vec[p4].coeffs[p5] >= INT32_MIN)))
   assigns(object_whole(u))
   ensures(forall(q0, 0, MLDSA_K, forall(q1, 0, MLDSA_N, u->vec[q0].coeffs[q1] == old(*u).vec[q0].coeffs[q1] + v->vec[q0].coeffs[q1])))
   ensures(forall(q2, 0, MLDSA_L,