FallenSigh a734eb2cad feat(dec): Decaps D6 - c' = K-PKE.Encrypt(ek_pke, m', r') ...

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.

2026-06-29 21:19:38 +08:00

112 KiB

Raw Blame History

View Raw