From a734eb2cad8c10fb94e722ab727aa2d70b966f29 Mon Sep 17 00:00:00 2001 From: FallenSigh Date: Mon, 29 Jun 2026 21:19:38 +0800 Subject: [PATCH] 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. --- .claude/plans/decaps_plan.md | 2 +- sync_rtl/top/TB/tb_mlkem_dec_katK_xsim.v | 46 +++++++++++++++++++----- sync_rtl/top/mlkem_top.v | 26 ++++++++------ 3 files changed, 55 insertions(+), 19 deletions(-) diff --git a/.claude/plans/decaps_plan.md b/.claude/plans/decaps_plan.md index 2029012..d375e6f 100644 --- a/.claude/plans/decaps_plan.md +++ b/.claude/plans/decaps_plan.md @@ -67,7 +67,7 @@ - **D3 — w = v' − INTT(Σ s∘u_hat)** ✅:复用 Encaps V 机(ST_DEC_W,u_row=0 单多项式)。MAC s_hat[j](bank_a slot j*K)∘ u_hat[j](bank_se rel j)→psum bank_t[UPSUM],与 V MAC 完全同址,免改。INTT 原地。SUB:w = v' − psum,(v'−psum) 负则 +Q。**关键:v'/psum 读口冲突 → D1 把 v' 落到 bank_a slot DEC_VASLOT=1(s_hat 在 j*K,slot 1 恒空 K≥2),SUB 时 psum(bank_t)+v'(bank_a)并行读,正如 V-ADD 并读 psum+e2。** K=2/3/4 w 全过。 - **D4 — m' = byteEncode₁(Compress₁(w))** ✅:ST_DEC_MENC,逐系数读 bank_t[UPSUM] 的 w,Compress₁(w)=1 iff 832 12'd832) && (bt_rd_data <= 12'd2496); // Compress_1 @@ -1126,7 +1128,10 @@ module mlkem_top #( ST_DEC_MENC: if (men_done) st_next = ST_DEC_G; // D5: (K',r') = G(m'||h) single-block, then K-bar = J(z||c) multi-block. ST_DEC_G: if (sha3_vo) st_next = ST_DEC_J; - ST_DEC_J: if (dj_done) st_next = ST_DONE; + // D5 J done -> D6 re-encrypt: c' = K-PKE.Encrypt(ek_pke, m', r'). + // Reuse the entire Encaps pipeline (rho load -> A -> C -> ... -> C2). + // r' is in r_r (CBD seed), m' in m_r (V/mu), ek_pke in ek_bram. + ST_DEC_J: if (dj_done) st_next = ST_ENC_LOAD; ST_G: if (sha3_vo) st_next = ST_A; ST_A: if (a_pair >= kk_rt) st_next = ST_C; ST_C: if (c_poly >= {1'b0, k_r, 1'b0}) st_next = ST_N; @@ -1270,7 +1275,6 @@ module mlkem_top #( men_idx <= 8'd0; men_ph <= 2'd0; men_done <= 1'b0; - mprime_r <= 256'd0; dj_blk <= 4'd0; dj_byte <= 8'd0; dj_phase <= 2'd0; @@ -1946,7 +1950,7 @@ module mlkem_top #( end // Arm Decaps D5 G when m' is ready (ST_DEC_MENC -> ST_DEC_G): fire the - // 64-byte single-block G(m'||h). dec_g_data = {hek_r, mprime_r}. + // 64-byte single-block G(m'||h). dec_g_data = {hek_r, m_r}. if (st == ST_DEC_MENC && st_next == ST_DEC_G) begin sha3_valid <= 1'b1; sha3_ack <= 1'b1; @@ -2033,7 +2037,9 @@ module mlkem_top #( end // Arm rho-load when entering ST_ENC_LOAD. rho = ek[384k .. 384k+31]. - if (st == ST_ENC_G && st_next == ST_ENC_LOAD) begin + // Entered from Encaps G (ST_ENC_G) or Decaps D6 re-encrypt (ST_DEC_J). + if (st_next == ST_ENC_LOAD && + (st == ST_ENC_G || st == ST_DEC_J)) begin rl_idx <= 6'd0; rl_widx <= 6'd0; rl_vld <= 1'b0; @@ -2173,13 +2179,13 @@ module mlkem_top #( // ---- ST_DEC_MENC (D4): m' = byteEncode_1(Compress_1(w)) ---- // Compress_1(w)=1 iff 832 < w <= 2496 (Q=3329). Pack 256 bits - // LSB-first into mprime_r (bit men_idx). Read w from bank_t[UPSUM]. + // LSB-first into m_r (bit men_idx). Read w from bank_t[UPSUM]. // ph0: present w[men_idx] addr; ph1: bt_rd_data valid -> set bit. if (st == ST_DEC_MENC && !men_done) begin case (men_ph) 2'd0: men_ph <= 2'd1; // addr presented; wait read default: begin // ph1: bt_rd_data = w[men_idx] - mprime_r[men_idx] <= men_w_bit; + m_r[men_idx] <= men_w_bit; if (men_idx == 8'd255) men_done <= 1'b1; else men_idx <= men_idx + 8'd1; men_ph <= 2'd0;