CBMC: Unify native vs. non-native rej_uniform C code

[hanno-becker]

Unlike most other native routines which are a drop-in replacement for their C counterparts, native rej_uniform implementations can reject their input, in which case the caller calls back to the C implementation. This leads to a divergence of the frontend C code depending on the backend, which is not ideal:

#if !defined(MLKEM_USE_NATIVE_REJ_UNIFORM)
unsigned int rej_uniform(int16_t *r, unsigned int target, unsigned int offset,
                         const uint8_t *buf, unsigned int buflen)
{
  return rej_uniform_scalar(r, target, offset, buf, buflen);
}
#else  /* MLKEM_USE_NATIVE_REJ_UNIFORM */

unsigned int rej_uniform(int16_t *r, unsigned int target, unsigned int offset,
                         const uint8_t *buf, unsigned int buflen)
{
  int ret;

  /* Sample from large buffer with full lane as much as possible. */
  ret = rej_uniform_native(r + offset, target - offset, buf, buflen);
  if (ret != -1)
    return offset + (unsigned)ret;

  return rej_uniform_scalar(r, target, offset, buf, buflen);
}
#endif /* MLKEM_USE_NATIVE_REJ_UNIFORM */

In particular, the CBMC proofs do not cover the fallback logic.

Task: Rewrite rej_uniform() so that the fallback logic is always exercised, but implement rej_uniform_native() as a no-op in case no native implementation is provided. In CBMC, specify rej_uniform_native and conduct the proof of rej_uniform against this spec.