1919 * - const mld_polyveck *t1: pointer to vector t1
2020 **************************************************/
2121MLD_INTERNAL_API
22- void mld_pack_pk (uint8_t pk [CRYPTO_PUBLICKEYBYTES ],
22+ void mld_pack_pk (uint8_t pk [MLDSA_CRYPTO_PUBLICKEYBYTES ],
2323 const uint8_t rho [MLDSA_SEEDBYTES ], const mld_polyveck * t1 )
2424__contract__ (
25- requires (memory_no_alias (pk , CRYPTO_PUBLICKEYBYTES ))
25+ requires (memory_no_alias (pk , MLDSA_CRYPTO_PUBLICKEYBYTES ))
2626 requires (memory_no_alias (rho , MLDSA_SEEDBYTES ))
2727 requires (memory_no_alias (t1 , sizeof (mld_polyveck )))
2828 requires (forall (k0 , 0 , MLDSA_K ,
2929 array_bound (t1 - > vec [k0 ].coeffs , 0 , MLDSA_N , 0 , 1 << 10 )))
30- assigns (memory_slice (pk , CRYPTO_PUBLICKEYBYTES ))
30+ assigns (memory_slice (pk , MLDSA_CRYPTO_PUBLICKEYBYTES ))
3131);
3232
3333
@@ -46,13 +46,13 @@ __contract__(
4646 * - const mld_polyveck *s2: pointer to vector s2
4747 **************************************************/
4848MLD_INTERNAL_API
49- void mld_pack_sk (uint8_t sk [CRYPTO_SECRETKEYBYTES ],
49+ void mld_pack_sk (uint8_t sk [MLDSA_CRYPTO_SECRETKEYBYTES ],
5050 const uint8_t rho [MLDSA_SEEDBYTES ],
5151 const uint8_t tr [MLDSA_TRBYTES ],
5252 const uint8_t key [MLDSA_SEEDBYTES ], const mld_polyveck * t0 ,
5353 const mld_polyvecl * s1 , const mld_polyveck * s2 )
5454__contract__ (
55- requires (memory_no_alias (sk , CRYPTO_SECRETKEYBYTES ))
55+ requires (memory_no_alias (sk , MLDSA_CRYPTO_SECRETKEYBYTES ))
5656 requires (memory_no_alias (rho , MLDSA_SEEDBYTES ))
5757 requires (memory_no_alias (tr , MLDSA_TRBYTES ))
5858 requires (memory_no_alias (key , MLDSA_SEEDBYTES ))
@@ -65,7 +65,7 @@ __contract__(
6565 array_abs_bound (s1 - > vec [k1 ].coeffs , 0 , MLDSA_N , MLDSA_ETA + 1 )))
6666 requires (forall (k2 , 0 , MLDSA_K ,
6767 array_abs_bound (s2 - > vec [k2 ].coeffs , 0 , MLDSA_N , MLDSA_ETA + 1 )))
68- assigns (memory_slice (sk , CRYPTO_SECRETKEYBYTES ))
68+ assigns (memory_slice (sk , MLDSA_CRYPTO_SECRETKEYBYTES ))
6969);
7070
7171
@@ -88,11 +88,11 @@ __contract__(
8888 * proof of type safety.
8989 **************************************************/
9090MLD_INTERNAL_API
91- void mld_pack_sig (uint8_t sig [CRYPTO_BYTES ], const uint8_t c [ MLDSA_CTILDEBYTES ],
92- const mld_polyvecl * z , const mld_polyveck * h ,
93- const unsigned int number_of_hints )
91+ void mld_pack_sig (uint8_t sig [MLDSA_CRYPTO_BYTES ],
92+ const uint8_t c [ MLDSA_CTILDEBYTES ] , const mld_polyvecl * z ,
93+ const mld_polyveck * h , const unsigned int number_of_hints )
9494__contract__ (
95- requires (memory_no_alias (sig , CRYPTO_BYTES ))
95+ requires (memory_no_alias (sig , MLDSA_CRYPTO_BYTES ))
9696 requires (memory_no_alias (c , MLDSA_CTILDEBYTES ))
9797 requires (memory_no_alias (z , sizeof (mld_polyvecl )))
9898 requires (memory_no_alias (h , sizeof (mld_polyveck )))
@@ -101,7 +101,7 @@ __contract__(
101101 requires (forall (k1 , 0 , MLDSA_K ,
102102 array_bound (h - > vec [k1 ].coeffs , 0 , MLDSA_N , 0 , 2 )))
103103 requires (number_of_hints <= MLDSA_OMEGA )
104- assigns (memory_slice (sig , CRYPTO_BYTES ))
104+ assigns (memory_slice (sig , MLDSA_CRYPTO_BYTES ))
105105);
106106
107107#define mld_unpack_pk MLD_NAMESPACE_KL(unpack_pk)
@@ -116,9 +116,9 @@ __contract__(
116116 **************************************************/
117117MLD_INTERNAL_API
118118void mld_unpack_pk (uint8_t rho [MLDSA_SEEDBYTES ], mld_polyveck * t1 ,
119- const uint8_t pk [CRYPTO_PUBLICKEYBYTES ])
119+ const uint8_t pk [MLDSA_CRYPTO_PUBLICKEYBYTES ])
120120__contract__ (
121- requires (memory_no_alias (pk , CRYPTO_PUBLICKEYBYTES ))
121+ requires (memory_no_alias (pk , MLDSA_CRYPTO_PUBLICKEYBYTES ))
122122 requires (memory_no_alias (rho , MLDSA_SEEDBYTES ))
123123 requires (memory_no_alias (t1 , sizeof (mld_polyveck )))
124124 assigns (memory_slice (rho , MLDSA_SEEDBYTES ))
@@ -146,15 +146,15 @@ MLD_INTERNAL_API
146146void mld_unpack_sk (uint8_t rho [MLDSA_SEEDBYTES ], uint8_t tr [MLDSA_TRBYTES ],
147147 uint8_t key [MLDSA_SEEDBYTES ], mld_polyveck * t0 ,
148148 mld_polyvecl * s1 , mld_polyveck * s2 ,
149- const uint8_t sk [CRYPTO_SECRETKEYBYTES ])
149+ const uint8_t sk [MLDSA_CRYPTO_SECRETKEYBYTES ])
150150__contract__ (
151151 requires (memory_no_alias (rho , MLDSA_SEEDBYTES ))
152152 requires (memory_no_alias (tr , MLDSA_TRBYTES ))
153153 requires (memory_no_alias (key , MLDSA_SEEDBYTES ))
154154 requires (memory_no_alias (t0 , sizeof (mld_polyveck )))
155155 requires (memory_no_alias (s1 , sizeof (mld_polyvecl )))
156156 requires (memory_no_alias (s2 , sizeof (mld_polyveck )))
157- requires (memory_no_alias (sk , CRYPTO_SECRETKEYBYTES ))
157+ requires (memory_no_alias (sk , MLDSA_CRYPTO_SECRETKEYBYTES ))
158158 assigns (memory_slice (rho , MLDSA_SEEDBYTES ))
159159 assigns (memory_slice (tr , MLDSA_TRBYTES ))
160160 assigns (memory_slice (key , MLDSA_SEEDBYTES ))
@@ -185,9 +185,9 @@ __contract__(
185185 **************************************************/
186186MLD_INTERNAL_API
187187int mld_unpack_sig (uint8_t c [MLDSA_CTILDEBYTES ], mld_polyvecl * z ,
188- mld_polyveck * h , const uint8_t sig [CRYPTO_BYTES ])
188+ mld_polyveck * h , const uint8_t sig [MLDSA_CRYPTO_BYTES ])
189189__contract__ (
190- requires (memory_no_alias (sig , CRYPTO_BYTES ))
190+ requires (memory_no_alias (sig , MLDSA_CRYPTO_BYTES ))
191191 requires (memory_no_alias (c , MLDSA_CTILDEBYTES ))
192192 requires (memory_no_alias (z , sizeof (mld_polyvecl )))
193193 requires (memory_no_alias (h , sizeof (mld_polyveck )))
0 commit comments