K-PKE.Decrypt steps 2-3 (FIPS 203 Alg 15), both by reusing Encaps machines:
- ST_DEC_SDEC reuses the Encaps TDEC (byteDecode12) machine: only the byte
source changes (td_byte mux -> dkp_rd_data; dkp_rd_addr driven by td_ekaddr
in SDEC). Decodes dk_pke -> s_hat[j] into bank_a slot j*K, the same layout
t_hat uses, so the D3 MAC can read s_hat[j] with the existing addressing.
- ST_DEC_NTT reuses the forward-NTT machine (n_slot_max=k_r) to transform
u'[i] in place in bank_se rel slots 0..K-1 -> u_hat[i]. Added ST_DEC_NTT to
the bank_se read/write muxes and the NTT load/process/arm blocks alongside
ST_N/ST_ENC_N.
- FSM: DECOMP -> SDEC -> NTT -> DONE.
TB verify_d2 checks s_hat[i] (bank_a slot i*K) and u_hat[i] (bank_se rel i)
against golden. verify_d1 narrowed to v' only: D2's in-place NTT overwrites u'
in bank_se, so u' correctness is now proven transitively via u_hat==NTT(u').
Verified: dec D2 K=2/3/4 all cases PASS; KeyGen + Encaps unregressed.
K-PKE.Decrypt step 1 (FIPS 203 Alg 15): decode+decompress the ciphertext.
- comp_decomp_sync instance made mode-selectable: Encaps C1/C2 still compress
(mode 0), Decaps ST_DEC_DECOMP decompresses (mode 1) with d=du/dv.
- New ST_DEC_DECOMP state with an inline byteDecode_d walker (reverse of the
C1/C2 bit-packer): walks c_in_bram bytes, accumulates LSB-first into a bit
buffer, extracts d-bit symbols, feeds comp_decomp, writes each decompressed
coeff (mod q) to a bank.
c1 = K polys, d=du -> u'[i] in bank_se rel slot i (0..K-1)
c2 = 1 poly, d=dv -> v' in bank_t rel slot DEC_VSLOT=2 (avoids UPSUM=1)
- dbg_slot_i widened 4->6 bits so the TB can read v' (abs slot 26 at K=4).
- bse/bt write muxes gain the DECOMP writeback paths (dec_u_we / dec_v_we).
Verification: examples/dump_decaps.rs (ml-kem-r worktree) emits per-stage
golden (u'/v'/s_hat/u_hat/w/m') into vectors/decgold/. TB verify_d1 reads back
u'[i] and v' and compares all 256 coeffs each.
Bring-up note: dbg coeff readback latency is bank(1)+dbg_coeff_r(1); the TB's
rdcoeff initially waited 2 cyc and saw data shifted by one index -> fixed to 3.
Verified: dec D1 K=2/3/4 all cases PASS; KeyGen + Encaps unregressed.
Scaffolding for ML-KEM Decaps (FIPS 203 Alg 18):
- op_i widened to 2-bit: 00=KeyGen, 01=Encaps, 10=Decaps (op_r too).
- New ST_DEC_LOAD state (D0: settles to DONE so load/parse is dbg-checkable).
- dk (=sk) streamed via dk_in_*; load logic routes each byte by region:
[0,384K)->dk_pke (dkp_bram), [384K,768K+32)->ek_pke (ek_bram),
[768K+32,+32)->H(ek) (hek_r), [768K+64,+32)->z (z_r). Routing uses the
LIVE k_i input, not start-captured k_r (dk is streamed before start_i).
- c (=ct) streamed via c_in_* into a SEPARATE c_in_bram, so the computed c'
(ct_bram) can later be compared against original c and J(z||c) can read c.
- New dbg taps: dbg_mprime_o/dbg_kbar_o/dbg_decz_o/dbg_dech_o.
TB: tb_mlkem_dec_katK_xsim verifies dk parse (H(ek), z, ek_pke/dk_pke BRAM
round-trip). gen_decaps_vectors.py emits dec_k{K}_c{N}_{dk,ct,ss,ctn,ssn}.hex
from the NIST KAT. run_tb.sh gains a 'dec' module (mirrors 'enc').
Regression fix: old KeyGen/Encaps TBs didn't connect the new input ports,
floating them to X and corrupting the ek/dkp write muxes -> tied off
dk_in_*/c_in_*/new dbg taps in both.
Verified: dec D0 K=2/3/4 PASS; KeyGen K=2 + Encaps K=2 unregressed.
