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.
Re-encryption step of the FO transform (FIPS 203 Alg 17 step 8), done by
reusing the ENTIRE Encaps E1-E7 pipeline rather than duplicating it:
- FSM: ST_DEC_J (D5) -> ST_ENC_LOAD, then the existing Encaps chain
LOAD->A->C->N->U->C1->TDEC->E2MV->V->C2 runs unchanged and writes c' to
ct_bram. The reuse preconditions are all in place: rho loads from ek_bram's
ek_pke region (same 384k offset Encaps uses; populated at D0 load via
dk_ld_ekpke), the CBD seed is r_r (r' from D5), and ek_pke is in ek_bram.
- D4 now packs the recovered message directly into m_r (dropping the separate
mprime_r register): Encaps V's mu reads m_r[idx] and dbg_mprime_o now aliases
m_r, so the re-encrypt sees m' with no extra plumbing.
- ST_ENC_LOAD arming generalized to fire when entered from ST_ENC_G (Encaps)
or ST_DEC_J (Decaps re-encrypt).
The re-encrypt overwrites bank_a/bank_se/bank_t, so the bank-based stage checks
(D1 v', D2 s_hat/u_hat, D3 w) are no longer valid at end-of-run. The dec TB now
verifies the surviving register/BRAM artifacts: dk parse (D0), m' (D4, in m_r),
K'/r'/K-bar (D5), and the 768/1088/1568-byte c' against golden (D6). Earlier
stages remain proven by their per-stage builds and transitively by c'.
Verified: dec D6 K=2/3/4 all cases PASS (c' == golden == valid ciphertext c);
KeyGen + Encaps unregressed.
FO transform hash derivations (FIPS 203 Alg 17 steps 6-7), reusing the
shared SHA3 core:
- ST_DEC_G: (K',r') = G(m'||h) via the single-block SHA3-512 path (mode 11,
dec_g_data = {hek_r, mprime_r}; h was captured into hek_r at D0 load).
K' -> ss_r (candidate shared secret, ss_o), r' -> r_r (PRF seed for D6).
- ST_DEC_J: K-bar = J(z||c) via the multi-block absorb port (mb_en=1),
modeled on the H(ek) machine: assemble 136-byte blocks, byte source is
z_r (g<32), c_in_bram (32<=g<msglen), or SHAKE256 pad (0x1F suffix, last
byte |=0x80 -- the only difference from H's 0x06). mb_* inputs muxed
between H and J by state. K-bar -> kbar_r (dbg_kbar_o).
- FSM: MENC -> G -> J -> DONE.
Bring-up note: c_in_bram read through cin_rd_addr_r (a register) plus the
registered BRAM is 2-cycle latency, but the assemble/writeback pipeline only
budgets 1 -- so the first c byte at the z->c boundary read X and poisoned the
whole sponge. Fixed by driving cin_rd_addr combinationally from dj_c_idx
during ST_DEC_J (dropping the register stage) so data lands the next cycle.
Verified: dec D5 K=2/3/4 all cases PASS (ct 768/1088/1568B -> 6/9/12 J blocks);
K' matches the KAT shared secret for valid ciphertexts; KeyGen + Encaps
unregressed.
Completes K-PKE.Decrypt (FIPS 203 Alg 15) in hardware: m' is recovered.
D3 (ST_DEC_W) reuses the Encaps V MAC/INTT machine (u_row tied to 0):
- MAC s_hat[j] (bank_a slot j*K) o u_hat[j] (bank_se rel j) -> psum bank_t[UPSUM]
-- identical addressing to Encaps V (t_hat[j] o y_hat[j]), so free reuse.
- INTT(psum) in place.
- SUB: w = v' - psum mod Q (negative -> +Q), written to bank_t[UPSUM].
To read v' and psum in parallel during SUB (one read port per bank), D1's v'
write was relocated from bank_t to bank_a slot DEC_VASLOT=1 (always free:
s_hat occupies j*K, slot 1 is unused for K>=2). This mirrors V-ADD reading
psum (bank_t) + e2 (bank_a) simultaneously.
D4 (ST_DEC_MENC): m' = byteEncode_1(Compress_1(w)). Compress_1(w)=1 iff
832 < w <= 2496 (Q=3329); bits packed LSB-first into mprime_r, exposed on
dbg_mprime_o (was a placeholder tied to m_r).
Added ST_DEC_W to the u_* machine muxes/sub-phases and the FSM chain
NTT->W->MENC->DONE. TB verify_d3 checks w (bank_t UPSUM); verify_d4 checks the
32-byte m' against golden (== the KAT-decrypted m == original message).
Verified: dec D1-D4 K=2/3/4 all cases PASS; KeyGen + Encaps unregressed.
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.
