88#include "polyvec.h"
99#include "polyvec_lazy.h"
1010
11- #define mld_pack_pk MLD_NAMESPACE_KL(pack_pk)
12- /*************************************************
13- * Name: mld_pack_pk
14- *
15- * Description: Bit-pack public key pk = (rho, t1).
16- *
17- * Arguments: - uint8_t pk[]: output byte array
18- * - const uint8_t rho[]: byte array containing rho
19- * - const mld_polyveck *t1: pointer to vector t1
20- **************************************************/
21- MLD_INTERNAL_API
22- void mld_pack_pk (uint8_t pk [MLDSA_CRYPTO_PUBLICKEYBYTES ],
23- const uint8_t rho [MLDSA_SEEDBYTES ], const mld_polyveck * t1 )
24- __contract__ (
25- requires (memory_no_alias (pk , MLDSA_CRYPTO_PUBLICKEYBYTES ))
26- requires (memory_no_alias (rho , MLDSA_SEEDBYTES ))
27- requires (memory_no_alias (t1 , sizeof (mld_polyveck )))
28- requires (forall (k0 , 0 , MLDSA_K ,
29- array_bound (t1 - > vec [k0 ].coeffs , 0 , MLDSA_N , 0 , 1 << 10 )))
30- assigns (memory_slice (pk , MLDSA_CRYPTO_PUBLICKEYBYTES ))
31- );
32-
3311
3412#define mld_pack_sk_s1 MLD_NAMESPACE_KL(pack_sk_s1)
3513/*************************************************
@@ -51,41 +29,82 @@ __contract__(
5129 assigns (memory_slice (sk , MLDSA_CRYPTO_SECRETKEYBYTES ))
5230);
5331
54- #define mld_pack_sk_rho_key_tr_s2_t0 MLD_NAMESPACE_KL(pack_sk_rho_key_tr_s2_t0 )
32+ #define mld_pack_sk_rho_key_tr_s2 MLD_NAMESPACE_KL(pack_sk_rho_key_tr_s2 )
5533/*************************************************
56- * Name: mld_pack_sk_rho_key_tr_s2_t0
34+ * Name: mld_pack_sk_rho_key_tr_s2
5735 *
58- * Description: Bit-pack rho, key, tr, s2, t0 into the secret key.
36+ * Description: Bit-pack rho, key, tr, s2 into the secret key.
5937 * s1 must already be packed via mld_pack_sk_s1.
38+ * t0 is packed per row by the caller (see
39+ * mld_pack_sk_t0).
6040 *
6141 * Arguments: - uint8_t sk[]: output byte array
6242 * - const uint8_t rho[]: byte array containing rho
6343 * - const uint8_t tr[]: byte array containing tr
6444 * - const uint8_t key[]: byte array containing key
65- * - const mld_polyveck *t0: pointer to vector t0
6645 * - const mld_polyveck *s2: pointer to vector s2
6746 **************************************************/
6847MLD_INTERNAL_API
69- void mld_pack_sk_rho_key_tr_s2_t0 (uint8_t sk [MLDSA_CRYPTO_SECRETKEYBYTES ],
70- const uint8_t rho [MLDSA_SEEDBYTES ],
71- const uint8_t tr [MLDSA_TRBYTES ],
72- const uint8_t key [MLDSA_SEEDBYTES ],
73- const mld_polyveck * t0 ,
74- const mld_polyveck * s2 )
48+ void mld_pack_sk_rho_key_tr_s2 (uint8_t sk [MLDSA_CRYPTO_SECRETKEYBYTES ],
49+ const uint8_t rho [MLDSA_SEEDBYTES ],
50+ const uint8_t tr [MLDSA_TRBYTES ],
51+ const uint8_t key [MLDSA_SEEDBYTES ],
52+ const mld_polyveck * s2 )
7553__contract__ (
7654 requires (memory_no_alias (sk , MLDSA_CRYPTO_SECRETKEYBYTES ))
7755 requires (memory_no_alias (rho , MLDSA_SEEDBYTES ))
7856 requires (memory_no_alias (tr , MLDSA_TRBYTES ))
7957 requires (memory_no_alias (key , MLDSA_SEEDBYTES ))
80- requires (memory_no_alias (t0 , sizeof (mld_polyveck )))
8158 requires (memory_no_alias (s2 , sizeof (mld_polyveck )))
82- requires (forall (k0 , 0 , MLDSA_K ,
83- array_bound (t0 - > vec [k0 ].coeffs , 0 , MLDSA_N , - (1 <<(MLDSA_D - 1 )) + 1 , (1 <<(MLDSA_D - 1 )) + 1 )))
8459 requires (forall (k2 , 0 , MLDSA_K ,
8560 array_abs_bound (s2 - > vec [k2 ].coeffs , 0 , MLDSA_N , MLDSA_ETA + 1 )))
8661 assigns (memory_slice (sk , MLDSA_CRYPTO_SECRETKEYBYTES ))
8762);
8863
64+ #define mld_pack_sk_t0 MLD_NAMESPACE_KL(pack_sk_t0)
65+ /*************************************************
66+ * Name: mld_pack_sk_t0
67+ *
68+ * Description: Bit-pack a single t0 polynomial t0[k] at the
69+ * corresponding offset in the secret key.
70+ *
71+ * Arguments: - uint8_t sk[]: output byte array (full secret key)
72+ * - unsigned int k: row index, must be < MLDSA_K
73+ * - const mld_poly *t0k: pointer to t0[k]
74+ **************************************************/
75+ MLD_INTERNAL_API
76+ void mld_pack_sk_t0 (uint8_t sk [MLDSA_CRYPTO_SECRETKEYBYTES ], unsigned int k ,
77+ const mld_poly * t0k )
78+ __contract__ (
79+ requires (memory_no_alias (sk , MLDSA_CRYPTO_SECRETKEYBYTES ))
80+ requires (memory_no_alias (t0k , sizeof (mld_poly )))
81+ requires (k < MLDSA_K )
82+ requires (array_bound (t0k - > coeffs , 0 , MLDSA_N , - (1 <<(MLDSA_D - 1 )) + 1 , (1 <<(MLDSA_D - 1 )) + 1 ))
83+ assigns (memory_slice (sk , MLDSA_CRYPTO_SECRETKEYBYTES ))
84+ );
85+
86+ #define mld_pack_pk_t1 MLD_NAMESPACE_KL(pack_pk_t1)
87+ /*************************************************
88+ * Name: mld_pack_pk_t1
89+ *
90+ * Description: Bit-pack a single t1 polynomial t1[k] at the
91+ * corresponding offset in the public key.
92+ *
93+ * Arguments: - uint8_t pk[]: output byte array (full public key)
94+ * - unsigned int k: row index, must be < MLDSA_K
95+ * - const mld_poly *t1k: pointer to t1[k]
96+ **************************************************/
97+ MLD_INTERNAL_API
98+ void mld_pack_pk_t1 (uint8_t pk [MLDSA_CRYPTO_PUBLICKEYBYTES ], unsigned int k ,
99+ const mld_poly * t1k )
100+ __contract__ (
101+ requires (memory_no_alias (pk , MLDSA_CRYPTO_PUBLICKEYBYTES ))
102+ requires (memory_no_alias (t1k , sizeof (mld_poly )))
103+ requires (k < MLDSA_K )
104+ requires (array_bound (t1k - > coeffs , 0 , MLDSA_N , 0 , 1 << 10 ))
105+ assigns (memory_slice (pk , MLDSA_CRYPTO_PUBLICKEYBYTES ))
106+ );
107+
89108
90109#define mld_pack_sig_c MLD_NAMESPACE_KL(pack_sig_c)
91110/*************************************************
0 commit comments