mldsa: remove tautological ret operand in two break-dominated inner loops

Premise:  each of the two inner loops is entered only from an outer loop whose
          own condition already established ret == 0 --
            wc_mldsa.c:8097 `for (r = 0; (ret == 0) && (r < params->k); r++)`
            wc_mldsa.c:8873 `for (; (ret == 0) && valid && (r < params->k); r++)`
          -- and nothing between the outer condition and the inner one assigns
          ret. (At :8884 the WC_MLDSA_FAULT_HARDEN check does write ret, but it
          `break`s out of the outer loop, so it never reaches the inner one.)
Claim:    the `ret == 0` operand of
            wc_mldsa.c:8103 `for (s = 0; (ret == 0) && (s < params->l); s++)`
            wc_mldsa.c:8895 `for (s = 0; (ret == 0) && (s < params->l); s++)`
Proof:    first evaluation: ret == 0 by the premise.
          Re-evaluations: every write to ret inside either body is immediately
          followed by an unconditional `break` --
            :8107 `ret = mldsa_rej_ntt_poly_ex(...)` / :8108 `if (ret != 0) break;`
            :8899 the same, and the WC_MLDSA_FAULT_HARDEN write at :8907, also
            followed by `break`.
          A scan of both bodies finds no other assignment to ret. So the loop
          condition is never re-evaluated with ret != 0, the operand is
          invariantly true, and its independence pair is unreachable.
Scope:    checked with and without WC_MLDSA_FAULT_HARDEN,
          WOLFSSL_MLDSA_SMALL_MEM_POLY64, WOLFSSL_MLDSA_SMALL and
          WOLFSSL_MLDSA_SIGN_SMALL_MEM_PRECALC_A -- every one of those either
          adds a break-terminated write or none at all.
Evidence: llvm-cov MC/DC records both conditions as never false
          (reports/mldsa/GAPS.md rows for 8103 and 8850, pre-drift numbering).

The two enclosing outer loops keep their `ret == 0` operand: they DO re-evaluate
after the inner `break`, so their false half is reachable.

Compiler cross-check: gcc -O2 emits byte-identical code for this file before
and after this commit -- the optimiser had already folded the removed
condition, independently confirming it was dead.
This commit is contained in:
Daniele Lacamera
2026-08-03 12:23:09 +02:00
parent 7daf4c3a1d
commit da46dcfdca
+2 -2
View File
@@ -8100,7 +8100,7 @@ static int mldsa_make_key_from_seed(wc_MlDsaKey* key, const byte* seed)
/* Put r/i into buffer to be hashed. */
aseed[MLDSA_PUB_SEED_SZ + 1] = (byte)r;
for (s = 0; (ret == 0) && (s < params->l); s++) {
for (s = 0; s < params->l; s++) {
/* Put s into buffer to be hashed. */
aseed[MLDSA_PUB_SEED_SZ + 0] = (byte)s;
/* Step 3: Expand public seed into a matrix of polynomials. */
@@ -8892,7 +8892,7 @@ static int mldsa_sign_with_seed_mu(wc_MlDsaKey* key,
/* Put r/i into buffer to be hashed. */
aseed[MLDSA_PUB_SEED_SZ + 1] = r;
/* Alg 26. Step 2: Loop over second dimension of matrix. */
for (s = 0; (ret == 0) && (s < params->l); s++) {
for (s = 0; s < params->l; s++) {
/* Put s into buffer to be hashed. */
aseed[MLDSA_PUB_SEED_SZ + 0] = s;
/* Alg 26. Step 3: Create polynomial from hashing seed. */