Final FO step (FIPS 203 Alg 17 steps 9-11): compare c' to c and select the
shared secret with implicit rejection. Completes full ML-KEM Decaps.
- ST_DEC_CMP walks all ct bytes (no early-out: constant work, matching the
constant-time spec intent), reading c' (ct_bram) and c (c_in_bram) in
parallel, OR-ing every byte difference into cmp_neq; the final byte latches
dec_reject.
- ss_o = dec_reject ? kbar_r (K-bar) : ss_r (K'). KeyGen/Encaps leave
dec_reject=0 so ss_r passes through unchanged.
- ST_ENC_C2 terminal branches on op_r: Decaps -> ST_DEC_CMP, Encaps -> DONE.
The dec TB now runs end-to-end twice per case (dk loaded once):
- valid ct : ss_o == KAT ss (c'==c -> K'), dec_reject==0
- corrupt ct: ss_o == KAT ss_n (c'!=c -> K-bar=J(z||ct_n)), dec_reject==1
exercising both the accept and implicit-reject paths against the KAT's own
ct_n/ss_n reject vectors.
Verified: dec D7 K=2/3/4 all cases PASS (accept + reject); KeyGen + Encaps
unregressed. Full ML-KEM (KeyGen + Encaps + Decaps w/ implicit rejection) now
works in hardware across all three parameter sets.
FallenSigh
2b70431923