1pub const Hacl_Impl_Blake2_Core_M32: u32 = 0;
4pub const Hacl_Impl_Blake2_Core_M128: u32 = 1;
5pub const Hacl_Impl_Blake2_Core_M256: u32 = 2;
6pub const Spec_Blake2_Blake2S: u32 = 0;
7pub const Spec_Blake2_Blake2B: u32 = 1;
8pub const Spec_Hash_Definitions_SHA2_224: u32 = 0;
9pub const Spec_Hash_Definitions_SHA2_256: u32 = 1;
10pub const Spec_Hash_Definitions_SHA2_384: u32 = 2;
11pub const Spec_Hash_Definitions_SHA2_512: u32 = 3;
12pub const Spec_Hash_Definitions_SHA1: u32 = 4;
13pub const Spec_Hash_Definitions_MD5: u32 = 5;
14pub const Spec_Hash_Definitions_Blake2S: u32 = 6;
15pub const Spec_Hash_Definitions_Blake2B: u32 = 7;
16pub const Spec_FFDHE_FFDHE2048: u32 = 0;
17pub const Spec_FFDHE_FFDHE3072: u32 = 1;
18pub const Spec_FFDHE_FFDHE4096: u32 = 2;
19pub const Spec_FFDHE_FFDHE6144: u32 = 3;
20pub const Spec_FFDHE_FFDHE8192: u32 = 4;
21pub const Spec_Agile_Cipher_AES128: u32 = 0;
22pub const Spec_Agile_Cipher_AES256: u32 = 1;
23pub const Spec_Agile_Cipher_CHACHA20: u32 = 2;
24pub const Spec_Cipher_Expansion_Hacl_CHACHA20: u32 = 0;
25pub const Spec_Cipher_Expansion_Vale_AES128: u32 = 1;
26pub const Spec_Cipher_Expansion_Vale_AES256: u32 = 2;
27pub const Spec_Agile_AEAD_AES128_GCM: u32 = 0;
28pub const Spec_Agile_AEAD_AES256_GCM: u32 = 1;
29pub const Spec_Agile_AEAD_CHACHA20_POLY1305: u32 = 2;
30pub const Spec_Agile_AEAD_AES128_CCM: u32 = 3;
31pub const Spec_Agile_AEAD_AES256_CCM: u32 = 4;
32pub const Spec_Agile_AEAD_AES128_CCM8: u32 = 5;
33pub const Spec_Agile_AEAD_AES256_CCM8: u32 = 6;
34pub const Spec_Frodo_Params_SHAKE128: u32 = 0;
35pub const Spec_Frodo_Params_AES128: u32 = 1;
36pub const EverCrypt_Hash_MD5_s: u32 = 0;
37pub const EverCrypt_Hash_SHA1_s: u32 = 1;
38pub const EverCrypt_Hash_SHA2_224_s: u32 = 2;
39pub const EverCrypt_Hash_SHA2_256_s: u32 = 3;
40pub const EverCrypt_Hash_SHA2_384_s: u32 = 4;
41pub const EverCrypt_Hash_SHA2_512_s: u32 = 5;
42pub const EverCrypt_Hash_Blake2S_s: u32 = 6;
43pub const EverCrypt_Hash_Blake2B_s: u32 = 7;
44pub const EverCrypt_Error_Success: u32 = 0;
45pub const EverCrypt_Error_UnsupportedAlgorithm: u32 = 1;
46pub const EverCrypt_Error_InvalidKey: u32 = 2;
47pub const EverCrypt_Error_AuthenticationFailure: u32 = 3;
48pub const EverCrypt_Error_InvalidIVLength: u32 = 4;
49pub const EverCrypt_Error_DecodeError: u32 = 5;
50pub const EverCrypt_DRBG_SHA1_s: u32 = 0;
51pub const EverCrypt_DRBG_SHA2_256_s: u32 = 1;
52pub const EverCrypt_DRBG_SHA2_384_s: u32 = 2;
53pub const EverCrypt_DRBG_SHA2_512_s: u32 = 3;
54pub type C_String_t = *const ::std::os::raw::c_char;
55pub type FStar_UInt128_uint128 = u128;
56extern "C" {
57 pub static Hacl_Impl_Blake2_Constants_sigmaTable: [u32; 160usize];
58}
59extern "C" {
60 pub static Hacl_Impl_Blake2_Constants_ivTable_S: [u32; 8usize];
61}
62extern "C" {
63 pub static Hacl_Impl_Blake2_Constants_ivTable_B: [u64; 8usize];
64}
65pub type Hacl_Impl_Blake2_Core_m_spec = u8;
66extern "C" {
67 pub fn Hacl_Blake2b_32_blake2b_init(hash: *mut u64, kk: u32, nn: u32);
68}
69extern "C" {
70 pub fn Hacl_Blake2b_32_blake2b_update_key(wv: *mut u64, hash: *mut u64, kk: u32, k: *mut u8, ll: u32);
71}
72extern "C" {
73 pub fn Hacl_Blake2b_32_blake2b_finish(nn: u32, output: *mut u8, hash: *mut u64);
74}
75extern "C" {
76 pub fn Hacl_Blake2b_32_blake2b(nn: u32, output: *mut u8, ll: u32, d: *mut u8, kk: u32, k: *mut u8);
77}
78extern "C" {
79 pub fn Hacl_Blake2s_32_blake2s_init(hash: *mut u32, kk: u32, nn: u32);
80}
81extern "C" {
82 pub fn Hacl_Blake2s_32_blake2s_update_key(wv: *mut u32, hash: *mut u32, kk: u32, k: *mut u8, ll: u32);
83}
84extern "C" {
85 pub fn Hacl_Blake2s_32_blake2s_update_multi(
86 len: u32,
87 wv: *mut u32,
88 hash: *mut u32,
89 prev: u64,
90 blocks: *mut u8,
91 nb: u32,
92 );
93}
94extern "C" {
95 pub fn Hacl_Blake2s_32_blake2s_update_last(len: u32, wv: *mut u32, hash: *mut u32, prev: u64, rem: u32, d: *mut u8);
96}
97extern "C" {
98 pub fn Hacl_Blake2s_32_blake2s_finish(nn: u32, output: *mut u8, hash: *mut u32);
99}
100extern "C" {
101 pub fn Hacl_Blake2s_32_blake2s(nn: u32, output: *mut u8, ll: u32, d: *mut u8, kk: u32, k: *mut u8);
102}
103pub type Spec_Blake2_alg = u8;
104pub type Spec_Hash_Definitions_hash_alg = u8;
105pub type Spec_FFDHE_ffdhe_alg = u8;
106pub type Spec_Agile_Cipher_cipher_alg = u8;
107pub type Spec_Cipher_Expansion_impl = u8;
108pub type Spec_Agile_AEAD_alg = u8;
109pub type Spec_Frodo_Params_frodo_gen_a = u8;
110extern "C" {
111 pub static Hacl_Impl_SHA3_keccak_rotc: [u32; 24usize];
112}
113extern "C" {
114 pub static Hacl_Impl_SHA3_keccak_piln: [u32; 24usize];
115}
116extern "C" {
117 pub static Hacl_Impl_SHA3_keccak_rndc: [u64; 24usize];
118}
119extern "C" {
120 pub fn Hacl_Impl_SHA3_rotl(a: u64, b: u32) -> u64;
121}
122extern "C" {
123 pub fn Hacl_Impl_SHA3_state_permute(s: *mut u64);
124}
125extern "C" {
126 pub fn Hacl_Impl_SHA3_loadState(rateInBytes: u32, input: *mut u8, s: *mut u64);
127}
128extern "C" {
129 pub fn Hacl_Impl_SHA3_storeState(rateInBytes: u32, s: *mut u64, res: *mut u8);
130}
131extern "C" {
132 pub fn Hacl_Impl_SHA3_absorb(s: *mut u64, rateInBytes: u32, inputByteLen: u32, input: *mut u8, delimitedSuffix: u8);
133}
134extern "C" {
135 pub fn Hacl_Impl_SHA3_squeeze(s: *mut u64, rateInBytes: u32, outputByteLen: u32, output: *mut u8);
136}
137extern "C" {
138 pub fn Hacl_Impl_SHA3_keccak(
139 rate: u32,
140 capacity: u32,
141 inputByteLen: u32,
142 input: *mut u8,
143 delimitedSuffix: u8,
144 outputByteLen: u32,
145 output: *mut u8,
146 );
147}
148extern "C" {
149 pub fn Hacl_SHA3_shake128_hacl(inputByteLen: u32, input: *mut u8, outputByteLen: u32, output: *mut u8);
150}
151extern "C" {
152 pub fn Hacl_SHA3_shake256_hacl(inputByteLen: u32, input: *mut u8, outputByteLen: u32, output: *mut u8);
153}
154extern "C" {
155 pub fn Hacl_SHA3_sha3_224(inputByteLen: u32, input: *mut u8, output: *mut u8);
156}
157extern "C" {
158 pub fn Hacl_SHA3_sha3_256(inputByteLen: u32, input: *mut u8, output: *mut u8);
159}
160extern "C" {
161 pub fn Hacl_SHA3_sha3_384(inputByteLen: u32, input: *mut u8, output: *mut u8);
162}
163extern "C" {
164 pub fn Hacl_SHA3_sha3_512(inputByteLen: u32, input: *mut u8, output: *mut u8);
165}
166extern "C" {
167 pub static Hacl_Impl_Frodo_Params_cdf_table640: [u16; 13usize];
168}
169extern "C" {
170 pub static Hacl_Impl_Frodo_Params_cdf_table976: [u16; 11usize];
171}
172extern "C" {
173 pub static Hacl_Impl_Frodo_Params_cdf_table1344: [u16; 7usize];
174}
175extern "C" {
176 pub static mut Hacl_Poly1305_32_blocklen: u32;
177}
178pub type Hacl_Poly1305_32_poly1305_ctx = *mut u64;
179extern "C" {
180 pub fn Hacl_Poly1305_32_poly1305_init(ctx: *mut u64, key: *mut u8);
181}
182extern "C" {
183 pub fn Hacl_Poly1305_32_poly1305_update1(ctx: *mut u64, text: *mut u8);
184}
185extern "C" {
186 pub fn Hacl_Poly1305_32_poly1305_update(ctx: *mut u64, len: u32, text: *mut u8);
187}
188extern "C" {
189 pub fn Hacl_Poly1305_32_poly1305_finish(tag: *mut u8, key: *mut u8, ctx: *mut u64);
190}
191extern "C" {
192 pub fn Hacl_Poly1305_32_poly1305_mac(tag: *mut u8, len: u32, text: *mut u8, key: *mut u8);
193}
194extern "C" {
195 pub fn Hacl_Chacha20_chacha20_encrypt(len: u32, out: *mut u8, text: *mut u8, key: *mut u8, n: *mut u8, ctr: u32);
196}
197extern "C" {
198 pub fn Hacl_Chacha20_chacha20_decrypt(len: u32, out: *mut u8, cipher: *mut u8, key: *mut u8, n: *mut u8, ctr: u32);
199}
200extern "C" {
201 pub fn Hacl_Chacha20Poly1305_32_aead_encrypt(
202 k: *mut u8,
203 n: *mut u8,
204 aadlen: u32,
205 aad: *mut u8,
206 mlen: u32,
207 m: *mut u8,
208 cipher: *mut u8,
209 mac: *mut u8,
210 );
211}
212extern "C" {
213 pub fn Hacl_Chacha20Poly1305_32_aead_decrypt(
214 k: *mut u8,
215 n: *mut u8,
216 aadlen: u32,
217 aad: *mut u8,
218 mlen: u32,
219 m: *mut u8,
220 cipher: *mut u8,
221 mac: *mut u8,
222 ) -> u32;
223}
224extern "C" {
225 pub static mut Hacl_Poly1305_256_blocklen: u32;
226}
227pub type Hacl_Poly1305_256_poly1305_ctx = *mut *mut ::std::os::raw::c_void;
228extern "C" {
229 pub fn Hacl_Poly1305_256_poly1305_init(ctx: *mut *mut ::std::os::raw::c_void, key: *mut u8);
230}
231extern "C" {
232 pub fn Hacl_Poly1305_256_poly1305_update1(ctx: *mut *mut ::std::os::raw::c_void, text: *mut u8);
233}
234extern "C" {
235 pub fn Hacl_Poly1305_256_poly1305_update(ctx: *mut *mut ::std::os::raw::c_void, len: u32, text: *mut u8);
236}
237extern "C" {
238 pub fn Hacl_Poly1305_256_poly1305_finish(tag: *mut u8, key: *mut u8, ctx: *mut *mut ::std::os::raw::c_void);
239}
240extern "C" {
241 pub fn Hacl_Poly1305_256_poly1305_mac(tag: *mut u8, len: u32, text: *mut u8, key: *mut u8);
242}
243extern "C" {
244 pub fn Hacl_Chacha20_Vec256_chacha20_encrypt_256(
245 len: u32,
246 out: *mut u8,
247 text: *mut u8,
248 key: *mut u8,
249 n: *mut u8,
250 ctr: u32,
251 );
252}
253extern "C" {
254 pub fn Hacl_Chacha20_Vec256_chacha20_decrypt_256(
255 len: u32,
256 out: *mut u8,
257 cipher: *mut u8,
258 key: *mut u8,
259 n: *mut u8,
260 ctr: u32,
261 );
262}
263extern "C" {
264 pub fn Hacl_Chacha20Poly1305_256_aead_encrypt(
265 k: *mut u8,
266 n: *mut u8,
267 aadlen: u32,
268 aad: *mut u8,
269 mlen: u32,
270 m: *mut u8,
271 cipher: *mut u8,
272 mac: *mut u8,
273 );
274}
275extern "C" {
276 pub fn Hacl_Chacha20Poly1305_256_aead_decrypt(
277 k: *mut u8,
278 n: *mut u8,
279 aadlen: u32,
280 aad: *mut u8,
281 mlen: u32,
282 m: *mut u8,
283 cipher: *mut u8,
284 mac: *mut u8,
285 ) -> u32;
286}
287extern "C" {
288 pub static mut Hacl_Poly1305_128_blocklen: u32;
289}
290pub type Hacl_Poly1305_128_poly1305_ctx = *mut *mut ::std::os::raw::c_void;
291extern "C" {
292 pub fn Hacl_Poly1305_128_poly1305_init(ctx: *mut *mut ::std::os::raw::c_void, key: *mut u8);
293}
294extern "C" {
295 pub fn Hacl_Poly1305_128_poly1305_update1(ctx: *mut *mut ::std::os::raw::c_void, text: *mut u8);
296}
297extern "C" {
298 pub fn Hacl_Poly1305_128_poly1305_update(ctx: *mut *mut ::std::os::raw::c_void, len: u32, text: *mut u8);
299}
300extern "C" {
301 pub fn Hacl_Poly1305_128_poly1305_finish(tag: *mut u8, key: *mut u8, ctx: *mut *mut ::std::os::raw::c_void);
302}
303extern "C" {
304 pub fn Hacl_Poly1305_128_poly1305_mac(tag: *mut u8, len: u32, text: *mut u8, key: *mut u8);
305}
306extern "C" {
307 pub fn Hacl_Chacha20_Vec128_chacha20_encrypt_128(
308 len: u32,
309 out: *mut u8,
310 text: *mut u8,
311 key: *mut u8,
312 n: *mut u8,
313 ctr: u32,
314 );
315}
316extern "C" {
317 pub fn Hacl_Chacha20_Vec128_chacha20_decrypt_128(
318 len: u32,
319 out: *mut u8,
320 cipher: *mut u8,
321 key: *mut u8,
322 n: *mut u8,
323 ctr: u32,
324 );
325}
326extern "C" {
327 pub fn Hacl_Chacha20Poly1305_128_aead_encrypt(
328 k: *mut u8,
329 n: *mut u8,
330 aadlen: u32,
331 aad: *mut u8,
332 mlen: u32,
333 m: *mut u8,
334 cipher: *mut u8,
335 mac: *mut u8,
336 );
337}
338extern "C" {
339 pub fn Hacl_Chacha20Poly1305_128_aead_decrypt(
340 k: *mut u8,
341 n: *mut u8,
342 aadlen: u32,
343 aad: *mut u8,
344 mlen: u32,
345 m: *mut u8,
346 cipher: *mut u8,
347 mac: *mut u8,
348 ) -> u32;
349}
350extern "C" {
351 pub fn EverCrypt_AutoConfig2_has_shaext() -> bool;
352}
353extern "C" {
354 pub fn EverCrypt_AutoConfig2_has_aesni() -> bool;
355}
356extern "C" {
357 pub fn EverCrypt_AutoConfig2_has_pclmulqdq() -> bool;
358}
359extern "C" {
360 pub fn EverCrypt_AutoConfig2_has_avx2() -> bool;
361}
362extern "C" {
363 pub fn EverCrypt_AutoConfig2_has_avx() -> bool;
364}
365extern "C" {
366 pub fn EverCrypt_AutoConfig2_has_bmi2() -> bool;
367}
368extern "C" {
369 pub fn EverCrypt_AutoConfig2_has_adx() -> bool;
370}
371extern "C" {
372 pub fn EverCrypt_AutoConfig2_has_sse() -> bool;
373}
374extern "C" {
375 pub fn EverCrypt_AutoConfig2_has_movbe() -> bool;
376}
377extern "C" {
378 pub fn EverCrypt_AutoConfig2_has_rdrand() -> bool;
379}
380extern "C" {
381 pub fn EverCrypt_AutoConfig2_has_avx512() -> bool;
382}
383extern "C" {
384 pub fn EverCrypt_AutoConfig2_wants_vale() -> bool;
385}
386extern "C" {
387 pub fn EverCrypt_AutoConfig2_wants_hacl() -> bool;
388}
389extern "C" {
390 pub fn EverCrypt_AutoConfig2_wants_openssl() -> bool;
391}
392extern "C" {
393 pub fn EverCrypt_AutoConfig2_wants_bcrypt() -> bool;
394}
395extern "C" {
396 pub fn EverCrypt_AutoConfig2_recall();
397}
398extern "C" {
399 pub fn EverCrypt_AutoConfig2_init();
400}
401pub type EverCrypt_AutoConfig2_disabler = ::std::option::Option<unsafe extern "C" fn()>;
402extern "C" {
403 pub fn EverCrypt_AutoConfig2_disable_avx2();
404}
405extern "C" {
406 pub fn EverCrypt_AutoConfig2_disable_avx();
407}
408extern "C" {
409 pub fn EverCrypt_AutoConfig2_disable_bmi2();
410}
411extern "C" {
412 pub fn EverCrypt_AutoConfig2_disable_adx();
413}
414extern "C" {
415 pub fn EverCrypt_AutoConfig2_disable_shaext();
416}
417extern "C" {
418 pub fn EverCrypt_AutoConfig2_disable_aesni();
419}
420extern "C" {
421 pub fn EverCrypt_AutoConfig2_disable_pclmulqdq();
422}
423extern "C" {
424 pub fn EverCrypt_AutoConfig2_disable_sse();
425}
426extern "C" {
427 pub fn EverCrypt_AutoConfig2_disable_movbe();
428}
429extern "C" {
430 pub fn EverCrypt_AutoConfig2_disable_rdrand();
431}
432extern "C" {
433 pub fn EverCrypt_AutoConfig2_disable_avx512();
434}
435extern "C" {
436 pub fn EverCrypt_AutoConfig2_disable_vale();
437}
438extern "C" {
439 pub fn EverCrypt_AutoConfig2_disable_hacl();
440}
441extern "C" {
442 pub fn EverCrypt_AutoConfig2_disable_openssl();
443}
444extern "C" {
445 pub fn EverCrypt_AutoConfig2_disable_bcrypt();
446}
447extern "C" {
448 pub fn EverCrypt_AutoConfig2_has_vec128() -> bool;
449}
450extern "C" {
451 pub fn EverCrypt_AutoConfig2_has_vec256() -> bool;
452}
453extern "C" {
454 pub fn EverCrypt_Chacha20Poly1305_aead_encrypt(
455 k: *mut u8,
456 n: *mut u8,
457 aadlen: u32,
458 aad: *mut u8,
459 mlen: u32,
460 m: *mut u8,
461 cipher: *mut u8,
462 tag: *mut u8,
463 );
464}
465extern "C" {
466 pub fn EverCrypt_Chacha20Poly1305_aead_decrypt(
467 k: *mut u8,
468 n: *mut u8,
469 aadlen: u32,
470 aad: *mut u8,
471 mlen: u32,
472 m: *mut u8,
473 cipher: *mut u8,
474 tag: *mut u8,
475 ) -> u32;
476}
477extern "C" {
478 pub static Hacl_Impl_SHA2_Generic_h224: [u32; 8usize];
479}
480extern "C" {
481 pub static Hacl_Impl_SHA2_Generic_h256: [u32; 8usize];
482}
483extern "C" {
484 pub static Hacl_Impl_SHA2_Generic_h384: [u64; 8usize];
485}
486extern "C" {
487 pub static Hacl_Impl_SHA2_Generic_h512: [u64; 8usize];
488}
489extern "C" {
490 pub static Hacl_Impl_SHA2_Generic_k224_256: [u32; 64usize];
491}
492extern "C" {
493 pub static Hacl_Impl_SHA2_Generic_k384_512: [u64; 80usize];
494}
495extern "C" {
496 pub fn Hacl_SHA2_Vec128_sha224_4(
497 dst0: *mut u8,
498 dst1: *mut u8,
499 dst2: *mut u8,
500 dst3: *mut u8,
501 input_len: u32,
502 input0: *mut u8,
503 input1: *mut u8,
504 input2: *mut u8,
505 input3: *mut u8,
506 );
507}
508extern "C" {
509 pub fn Hacl_SHA2_Vec128_sha256_4(
510 dst0: *mut u8,
511 dst1: *mut u8,
512 dst2: *mut u8,
513 dst3: *mut u8,
514 input_len: u32,
515 input0: *mut u8,
516 input1: *mut u8,
517 input2: *mut u8,
518 input3: *mut u8,
519 );
520}
521extern "C" {
522 pub fn Hacl_Curve25519_51_scalarmult(out: *mut u8, priv_: *mut u8, pub_: *mut u8);
523}
524extern "C" {
525 pub fn Hacl_Curve25519_51_secret_to_public(pub_: *mut u8, priv_: *mut u8);
526}
527extern "C" {
528 pub fn Hacl_Curve25519_51_ecdh(out: *mut u8, priv_: *mut u8, pub_: *mut u8) -> bool;
529}
530extern "C" {
531 pub fn Hacl_Hash_SHA2_update_multi_224(s: *mut u32, blocks: *mut u8, n_blocks: u32);
532}
533extern "C" {
534 pub fn Hacl_Hash_SHA2_update_multi_256(s: *mut u32, blocks: *mut u8, n_blocks: u32);
535}
536extern "C" {
537 pub fn Hacl_Hash_SHA2_update_multi_384(s: *mut u64, blocks: *mut u8, n_blocks: u32);
538}
539extern "C" {
540 pub fn Hacl_Hash_SHA2_update_multi_512(s: *mut u64, blocks: *mut u8, n_blocks: u32);
541}
542extern "C" {
543 pub fn Hacl_Hash_SHA2_update_last_224(s: *mut u32, prev_len: u64, input: *mut u8, input_len: u32);
544}
545extern "C" {
546 pub fn Hacl_Hash_SHA2_update_last_256(s: *mut u32, prev_len: u64, input: *mut u8, input_len: u32);
547}
548extern "C" {
549 pub fn Hacl_Hash_SHA2_hash_224(input: *mut u8, input_len: u32, dst: *mut u8);
550}
551extern "C" {
552 pub fn Hacl_Hash_SHA2_hash_256(input: *mut u8, input_len: u32, dst: *mut u8);
553}
554extern "C" {
555 pub fn Hacl_Hash_SHA2_hash_384(input: *mut u8, input_len: u32, dst: *mut u8);
556}
557extern "C" {
558 pub fn Hacl_Hash_SHA2_hash_512(input: *mut u8, input_len: u32, dst: *mut u8);
559}
560extern "C" {
561 pub fn Hacl_Hash_SHA1_legacy_update_multi(s: *mut u32, blocks: *mut u8, n_blocks: u32);
562}
563extern "C" {
564 pub fn Hacl_Hash_SHA1_legacy_update_last(s: *mut u32, prev_len: u64, input: *mut u8, input_len: u32);
565}
566extern "C" {
567 pub fn Hacl_Hash_SHA1_legacy_hash(input: *mut u8, input_len: u32, dst: *mut u8);
568}
569extern "C" {
570 pub fn Hacl_HMAC_legacy_compute_sha1(dst: *mut u8, key: *mut u8, key_len: u32, data: *mut u8, data_len: u32);
571}
572extern "C" {
573 pub fn Hacl_HMAC_compute_sha2_256(dst: *mut u8, key: *mut u8, key_len: u32, data: *mut u8, data_len: u32);
574}
575extern "C" {
576 pub fn Hacl_HMAC_compute_sha2_384(dst: *mut u8, key: *mut u8, key_len: u32, data: *mut u8, data_len: u32);
577}
578extern "C" {
579 pub fn Hacl_HMAC_compute_sha2_512(dst: *mut u8, key: *mut u8, key_len: u32, data: *mut u8, data_len: u32);
580}
581extern "C" {
582 pub fn Hacl_HMAC_compute_blake2s_32(dst: *mut u8, key: *mut u8, key_len: u32, data: *mut u8, data_len: u32);
583}
584extern "C" {
585 pub fn Hacl_HMAC_compute_blake2b_32(dst: *mut u8, key: *mut u8, key_len: u32, data: *mut u8, data_len: u32);
586}
587extern "C" {
588 pub fn Hacl_HKDF_expand_sha2_256(okm: *mut u8, prk: *mut u8, prklen: u32, info: *mut u8, infolen: u32, len: u32);
589}
590extern "C" {
591 pub fn Hacl_HKDF_extract_sha2_256(prk: *mut u8, salt: *mut u8, saltlen: u32, ikm: *mut u8, ikmlen: u32);
592}
593extern "C" {
594 pub fn Hacl_HKDF_expand_sha2_512(okm: *mut u8, prk: *mut u8, prklen: u32, info: *mut u8, infolen: u32, len: u32);
595}
596extern "C" {
597 pub fn Hacl_HKDF_extract_sha2_512(prk: *mut u8, salt: *mut u8, saltlen: u32, ikm: *mut u8, ikmlen: u32);
598}
599extern "C" {
600 pub fn Hacl_HKDF_expand_blake2s_32(okm: *mut u8, prk: *mut u8, prklen: u32, info: *mut u8, infolen: u32, len: u32);
601}
602extern "C" {
603 pub fn Hacl_HKDF_extract_blake2s_32(prk: *mut u8, salt: *mut u8, saltlen: u32, ikm: *mut u8, ikmlen: u32);
604}
605extern "C" {
606 pub fn Hacl_HKDF_expand_blake2b_32(okm: *mut u8, prk: *mut u8, prklen: u32, info: *mut u8, infolen: u32, len: u32);
607}
608extern "C" {
609 pub fn Hacl_HKDF_extract_blake2b_32(prk: *mut u8, salt: *mut u8, saltlen: u32, ikm: *mut u8, ikmlen: u32);
610}
611extern "C" {
612 pub fn Hacl_Curve25519_64_scalarmult(out: *mut u8, priv_: *mut u8, pub_: *mut u8);
613}
614extern "C" {
615 pub fn Hacl_Curve25519_64_secret_to_public(pub_: *mut u8, priv_: *mut u8);
616}
617extern "C" {
618 pub fn Hacl_Curve25519_64_ecdh(out: *mut u8, priv_: *mut u8, pub_: *mut u8) -> bool;
619}
620extern "C" {
621 pub fn Hacl_HPKE_Curve64_CP128_SHA512_setupBaseI(
622 o_pkE: *mut u8,
623 o_k: *mut u8,
624 o_n: *mut u8,
625 skE: *mut u8,
626 pkR: *mut u8,
627 infolen: u32,
628 info: *mut u8,
629 ) -> u32;
630}
631extern "C" {
632 pub fn Hacl_HPKE_Curve64_CP128_SHA512_setupBaseR(
633 o_key_aead: *mut u8,
634 o_nonce_aead: *mut u8,
635 pkE: *mut u8,
636 skR: *mut u8,
637 infolen: u32,
638 info: *mut u8,
639 ) -> u32;
640}
641extern "C" {
642 pub fn Hacl_HPKE_Curve64_CP128_SHA512_sealBase(
643 skE: *mut u8,
644 pkR: *mut u8,
645 mlen: u32,
646 m: *mut u8,
647 infolen: u32,
648 info: *mut u8,
649 output: *mut u8,
650 ) -> u32;
651}
652extern "C" {
653 pub fn Hacl_HPKE_Curve64_CP128_SHA512_openBase(
654 pkE: *mut u8,
655 skR: *mut u8,
656 mlen: u32,
657 m: *mut u8,
658 infolen: u32,
659 info: *mut u8,
660 output: *mut u8,
661 ) -> u32;
662}
663extern "C" {
664 pub fn Hacl_Bignum256_add(a: *mut u64, b: *mut u64, res: *mut u64) -> u64;
665}
666extern "C" {
667 pub fn Hacl_Bignum256_sub(a: *mut u64, b: *mut u64, res: *mut u64) -> u64;
668}
669extern "C" {
670 pub fn Hacl_Bignum256_add_mod(n: *mut u64, a: *mut u64, b: *mut u64, res: *mut u64);
671}
672extern "C" {
673 pub fn Hacl_Bignum256_sub_mod(n: *mut u64, a: *mut u64, b: *mut u64, res: *mut u64);
674}
675extern "C" {
676 pub fn Hacl_Bignum256_mul(a: *mut u64, b: *mut u64, res: *mut u64);
677}
678extern "C" {
679 pub fn Hacl_Bignum256_sqr(a: *mut u64, res: *mut u64);
680}
681extern "C" {
682 pub fn Hacl_Bignum256_mod(n: *mut u64, a: *mut u64, res: *mut u64) -> bool;
683}
684extern "C" {
685 pub fn Hacl_Bignum256_mod_exp_vartime(n: *mut u64, a: *mut u64, bBits: u32, b: *mut u64, res: *mut u64) -> bool;
686}
687extern "C" {
688 pub fn Hacl_Bignum256_mod_exp_consttime(n: *mut u64, a: *mut u64, bBits: u32, b: *mut u64, res: *mut u64) -> bool;
689}
690extern "C" {
691 pub fn Hacl_Bignum256_mod_inv_prime_vartime(n: *mut u64, a: *mut u64, res: *mut u64) -> bool;
692}
693#[repr(C)]
694#[derive(Debug, Copy, Clone)]
695pub struct Hacl_Bignum_MontArithmetic_bn_mont_ctx_u64_s {
696 pub len: u32,
697 pub n: *mut u64,
698 pub mu: u64,
699 pub r2: *mut u64,
700}
701pub type Hacl_Bignum_MontArithmetic_bn_mont_ctx_u64 = Hacl_Bignum_MontArithmetic_bn_mont_ctx_u64_s;
702extern "C" {
703 pub fn Hacl_Bignum256_mont_ctx_init(n: *mut u64) -> *mut Hacl_Bignum_MontArithmetic_bn_mont_ctx_u64;
704}
705extern "C" {
706 pub fn Hacl_Bignum256_mont_ctx_free(k: *mut Hacl_Bignum_MontArithmetic_bn_mont_ctx_u64);
707}
708extern "C" {
709 pub fn Hacl_Bignum256_mod_precomp(k: *mut Hacl_Bignum_MontArithmetic_bn_mont_ctx_u64, a: *mut u64, res: *mut u64);
710}
711extern "C" {
712 pub fn Hacl_Bignum256_mod_exp_vartime_precomp(
713 k: *mut Hacl_Bignum_MontArithmetic_bn_mont_ctx_u64,
714 a: *mut u64,
715 bBits: u32,
716 b: *mut u64,
717 res: *mut u64,
718 );
719}
720extern "C" {
721 pub fn Hacl_Bignum256_mod_exp_consttime_precomp(
722 k: *mut Hacl_Bignum_MontArithmetic_bn_mont_ctx_u64,
723 a: *mut u64,
724 bBits: u32,
725 b: *mut u64,
726 res: *mut u64,
727 );
728}
729extern "C" {
730 pub fn Hacl_Bignum256_mod_inv_prime_vartime_precomp(
731 k: *mut Hacl_Bignum_MontArithmetic_bn_mont_ctx_u64,
732 a: *mut u64,
733 res: *mut u64,
734 );
735}
736extern "C" {
737 pub fn Hacl_Bignum256_new_bn_from_bytes_be(len: u32, b: *mut u8) -> *mut u64;
738}
739extern "C" {
740 pub fn Hacl_Bignum256_new_bn_from_bytes_le(len: u32, b: *mut u8) -> *mut u64;
741}
742extern "C" {
743 pub fn Hacl_Bignum256_bn_to_bytes_be(b: *mut u64, res: *mut u8);
744}
745extern "C" {
746 pub fn Hacl_Bignum256_bn_to_bytes_le(b: *mut u64, res: *mut u8);
747}
748extern "C" {
749 pub fn Hacl_Bignum256_lt_mask(a: *mut u64, b: *mut u64) -> u64;
750}
751extern "C" {
752 pub fn Hacl_Bignum256_eq_mask(a: *mut u64, b: *mut u64) -> u64;
753}
754extern "C" {
755 pub fn Hacl_HMAC_Blake2b_256_compute_blake2b_256(
756 dst: *mut u8,
757 key: *mut u8,
758 key_len: u32,
759 data: *mut u8,
760 data_len: u32,
761 );
762}
763#[repr(C)]
764#[derive(Debug, Copy, Clone)]
765pub struct Hacl_Bignum_MontArithmetic_bn_mont_ctx_u32_s {
766 pub len: u32,
767 pub n: *mut u32,
768 pub mu: u32,
769 pub r2: *mut u32,
770}
771pub type Hacl_Bignum_MontArithmetic_bn_mont_ctx_u32 = Hacl_Bignum_MontArithmetic_bn_mont_ctx_u32_s;
772pub type Hacl_GenericField32_pbn_mont_ctx_u32 = *mut Hacl_Bignum_MontArithmetic_bn_mont_ctx_u32;
773extern "C" {
774 #[doc = "A verified field arithmetic library."]
775 #[doc = ""]
776 #[doc = "This is a 32-bit optimized version, where bignums are represented as an array"]
777 #[doc = "of `len` unsigned 32-bit integers, i.e. uint32_t[len]."]
778 #[doc = ""]
779 #[doc = "All the arithmetic operations are performed in the Montgomery domain."]
780 #[doc = ""]
781 #[doc = "All the functions below preserve the following invariant for a bignum `aM` in"]
782 #[doc = "Montgomery form."]
783 #[doc = "• aM < n"]
784 pub fn Hacl_GenericField32_field_modulus_check(len: u32, n: *mut u32) -> bool;
785}
786extern "C" {
787 pub fn Hacl_GenericField32_field_init(len: u32, n: *mut u32) -> *mut Hacl_Bignum_MontArithmetic_bn_mont_ctx_u32;
788}
789extern "C" {
790 pub fn Hacl_GenericField32_field_free(k: *mut Hacl_Bignum_MontArithmetic_bn_mont_ctx_u32);
791}
792extern "C" {
793 pub fn Hacl_GenericField32_field_get_len(k: *mut Hacl_Bignum_MontArithmetic_bn_mont_ctx_u32) -> u32;
794}
795extern "C" {
796 pub fn Hacl_GenericField32_to_field(k: *mut Hacl_Bignum_MontArithmetic_bn_mont_ctx_u32, a: *mut u32, aM: *mut u32);
797}
798extern "C" {
799 pub fn Hacl_GenericField32_from_field(
800 k: *mut Hacl_Bignum_MontArithmetic_bn_mont_ctx_u32,
801 aM: *mut u32,
802 a: *mut u32,
803 );
804}
805extern "C" {
806 pub fn Hacl_GenericField32_add(
807 k: *mut Hacl_Bignum_MontArithmetic_bn_mont_ctx_u32,
808 aM: *mut u32,
809 bM: *mut u32,
810 cM: *mut u32,
811 );
812}
813extern "C" {
814 pub fn Hacl_GenericField32_sub(
815 k: *mut Hacl_Bignum_MontArithmetic_bn_mont_ctx_u32,
816 aM: *mut u32,
817 bM: *mut u32,
818 cM: *mut u32,
819 );
820}
821extern "C" {
822 pub fn Hacl_GenericField32_mul(
823 k: *mut Hacl_Bignum_MontArithmetic_bn_mont_ctx_u32,
824 aM: *mut u32,
825 bM: *mut u32,
826 cM: *mut u32,
827 );
828}
829extern "C" {
830 pub fn Hacl_GenericField32_sqr(k: *mut Hacl_Bignum_MontArithmetic_bn_mont_ctx_u32, aM: *mut u32, cM: *mut u32);
831}
832extern "C" {
833 pub fn Hacl_GenericField32_one(k: *mut Hacl_Bignum_MontArithmetic_bn_mont_ctx_u32, oneM: *mut u32);
834}
835extern "C" {
836 pub fn Hacl_GenericField32_exp_consttime(
837 k: *mut Hacl_Bignum_MontArithmetic_bn_mont_ctx_u32,
838 aM: *mut u32,
839 bBits: u32,
840 b: *mut u32,
841 resM: *mut u32,
842 );
843}
844extern "C" {
845 pub fn Hacl_GenericField32_exp_vartime(
846 k: *mut Hacl_Bignum_MontArithmetic_bn_mont_ctx_u32,
847 aM: *mut u32,
848 bBits: u32,
849 b: *mut u32,
850 resM: *mut u32,
851 );
852}
853extern "C" {
854 pub fn Hacl_GenericField32_inverse(
855 k: *mut Hacl_Bignum_MontArithmetic_bn_mont_ctx_u32,
856 aM: *mut u32,
857 aInvM: *mut u32,
858 );
859}
860extern "C" {
861 pub fn Hacl_Bignum4096_32_add(a: *mut u32, b: *mut u32, res: *mut u32) -> u32;
862}
863extern "C" {
864 pub fn Hacl_Bignum4096_32_sub(a: *mut u32, b: *mut u32, res: *mut u32) -> u32;
865}
866extern "C" {
867 pub fn Hacl_Bignum4096_32_add_mod(n: *mut u32, a: *mut u32, b: *mut u32, res: *mut u32);
868}
869extern "C" {
870 pub fn Hacl_Bignum4096_32_sub_mod(n: *mut u32, a: *mut u32, b: *mut u32, res: *mut u32);
871}
872extern "C" {
873 pub fn Hacl_Bignum4096_32_mul(a: *mut u32, b: *mut u32, res: *mut u32);
874}
875extern "C" {
876 pub fn Hacl_Bignum4096_32_sqr(a: *mut u32, res: *mut u32);
877}
878extern "C" {
879 pub fn Hacl_Bignum4096_32_mod(n: *mut u32, a: *mut u32, res: *mut u32) -> bool;
880}
881extern "C" {
882 pub fn Hacl_Bignum4096_32_mod_exp_vartime(n: *mut u32, a: *mut u32, bBits: u32, b: *mut u32, res: *mut u32)
883 -> bool;
884}
885extern "C" {
886 pub fn Hacl_Bignum4096_32_mod_exp_consttime(
887 n: *mut u32,
888 a: *mut u32,
889 bBits: u32,
890 b: *mut u32,
891 res: *mut u32,
892 ) -> bool;
893}
894extern "C" {
895 pub fn Hacl_Bignum4096_32_mod_inv_prime_vartime(n: *mut u32, a: *mut u32, res: *mut u32) -> bool;
896}
897extern "C" {
898 pub fn Hacl_Bignum4096_32_mont_ctx_init(n: *mut u32) -> *mut Hacl_Bignum_MontArithmetic_bn_mont_ctx_u32;
899}
900extern "C" {
901 pub fn Hacl_Bignum4096_32_mont_ctx_free(k: *mut Hacl_Bignum_MontArithmetic_bn_mont_ctx_u32);
902}
903extern "C" {
904 pub fn Hacl_Bignum4096_32_mod_precomp(
905 k: *mut Hacl_Bignum_MontArithmetic_bn_mont_ctx_u32,
906 a: *mut u32,
907 res: *mut u32,
908 );
909}
910extern "C" {
911 pub fn Hacl_Bignum4096_32_mod_exp_vartime_precomp(
912 k: *mut Hacl_Bignum_MontArithmetic_bn_mont_ctx_u32,
913 a: *mut u32,
914 bBits: u32,
915 b: *mut u32,
916 res: *mut u32,
917 );
918}
919extern "C" {
920 pub fn Hacl_Bignum4096_32_mod_exp_consttime_precomp(
921 k: *mut Hacl_Bignum_MontArithmetic_bn_mont_ctx_u32,
922 a: *mut u32,
923 bBits: u32,
924 b: *mut u32,
925 res: *mut u32,
926 );
927}
928extern "C" {
929 pub fn Hacl_Bignum4096_32_mod_inv_prime_vartime_precomp(
930 k: *mut Hacl_Bignum_MontArithmetic_bn_mont_ctx_u32,
931 a: *mut u32,
932 res: *mut u32,
933 );
934}
935extern "C" {
936 pub fn Hacl_Bignum4096_32_new_bn_from_bytes_be(len: u32, b: *mut u8) -> *mut u32;
937}
938extern "C" {
939 pub fn Hacl_Bignum4096_32_new_bn_from_bytes_le(len: u32, b: *mut u8) -> *mut u32;
940}
941extern "C" {
942 pub fn Hacl_Bignum4096_32_bn_to_bytes_be(b: *mut u32, res: *mut u8);
943}
944extern "C" {
945 pub fn Hacl_Bignum4096_32_bn_to_bytes_le(b: *mut u32, res: *mut u8);
946}
947extern "C" {
948 pub fn Hacl_Bignum4096_32_lt_mask(a: *mut u32, b: *mut u32) -> u32;
949}
950extern "C" {
951 pub fn Hacl_Bignum4096_32_eq_mask(a: *mut u32, b: *mut u32) -> u32;
952}
953extern "C" {
954 pub fn Hacl_Streaming_Blake2_blocks_state_len(a: Spec_Blake2_alg, m: Hacl_Impl_Blake2_Core_m_spec) -> u32;
955}
956#[repr(C)]
957#[derive(Debug, Copy, Clone)]
958pub struct Hacl_Streaming_Blake2_blake2s_32_block_state_s {
959 pub fst: *mut u32,
960 pub snd: *mut u32,
961}
962pub type Hacl_Streaming_Blake2_blake2s_32_block_state = Hacl_Streaming_Blake2_blake2s_32_block_state_s;
963#[repr(C)]
964#[derive(Debug, Copy, Clone)]
965pub struct Hacl_Streaming_Blake2_blake2s_32_state_s {
966 pub block_state: Hacl_Streaming_Blake2_blake2s_32_block_state,
967 pub buf: *mut u8,
968 pub total_len: u64,
969}
970pub type Hacl_Streaming_Blake2_blake2s_32_state = Hacl_Streaming_Blake2_blake2s_32_state_s;
971extern "C" {
972 pub fn Hacl_Streaming_Blake2_blake2s_32_no_key_create_in() -> *mut Hacl_Streaming_Blake2_blake2s_32_state;
973}
974extern "C" {
975 pub fn Hacl_Streaming_Blake2_blake2s_32_no_key_init(s1: *mut Hacl_Streaming_Blake2_blake2s_32_state);
976}
977extern "C" {
978 pub fn Hacl_Streaming_Blake2_blake2s_32_no_key_update(
979 p: *mut Hacl_Streaming_Blake2_blake2s_32_state,
980 data: *mut u8,
981 len: u32,
982 );
983}
984extern "C" {
985 pub fn Hacl_Streaming_Blake2_blake2s_32_no_key_finish(p: *mut Hacl_Streaming_Blake2_blake2s_32_state, dst: *mut u8);
986}
987extern "C" {
988 pub fn Hacl_Streaming_Blake2_blake2s_32_no_key_free(s1: *mut Hacl_Streaming_Blake2_blake2s_32_state);
989}
990#[repr(C)]
991#[derive(Debug, Copy, Clone)]
992pub struct Hacl_Streaming_Blake2_blake2b_32_block_state_s {
993 pub fst: *mut u64,
994 pub snd: *mut u64,
995}
996pub type Hacl_Streaming_Blake2_blake2b_32_block_state = Hacl_Streaming_Blake2_blake2b_32_block_state_s;
997#[repr(C)]
998#[derive(Debug, Copy, Clone)]
999pub struct Hacl_Streaming_Blake2_blake2b_32_state_s {
1000 pub block_state: Hacl_Streaming_Blake2_blake2b_32_block_state,
1001 pub buf: *mut u8,
1002 pub total_len: u64,
1003}
1004pub type Hacl_Streaming_Blake2_blake2b_32_state = Hacl_Streaming_Blake2_blake2b_32_state_s;
1005extern "C" {
1006 pub fn Hacl_Streaming_Blake2_blake2b_32_no_key_create_in() -> *mut Hacl_Streaming_Blake2_blake2b_32_state;
1007}
1008extern "C" {
1009 pub fn Hacl_Streaming_Blake2_blake2b_32_no_key_init(s1: *mut Hacl_Streaming_Blake2_blake2b_32_state);
1010}
1011extern "C" {
1012 pub fn Hacl_Streaming_Blake2_blake2b_32_no_key_update(
1013 p: *mut Hacl_Streaming_Blake2_blake2b_32_state,
1014 data: *mut u8,
1015 len: u32,
1016 );
1017}
1018extern "C" {
1019 pub fn Hacl_Streaming_Blake2_blake2b_32_no_key_finish(p: *mut Hacl_Streaming_Blake2_blake2b_32_state, dst: *mut u8);
1020}
1021extern "C" {
1022 pub fn Hacl_Streaming_Blake2_blake2b_32_no_key_free(s1: *mut Hacl_Streaming_Blake2_blake2b_32_state);
1023}
1024extern "C" {
1025 pub fn Hacl_Blake2s_128_blake2s_init(hash: *mut *mut ::std::os::raw::c_void, kk: u32, nn: u32);
1026}
1027extern "C" {
1028 pub fn Hacl_Blake2s_128_blake2s_update_key(
1029 wv: *mut *mut ::std::os::raw::c_void,
1030 hash: *mut *mut ::std::os::raw::c_void,
1031 kk: u32,
1032 k: *mut u8,
1033 ll: u32,
1034 );
1035}
1036extern "C" {
1037 pub fn Hacl_Blake2s_128_blake2s_update_multi(
1038 len: u32,
1039 wv: *mut *mut ::std::os::raw::c_void,
1040 hash: *mut *mut ::std::os::raw::c_void,
1041 prev: u64,
1042 blocks: *mut u8,
1043 nb: u32,
1044 );
1045}
1046extern "C" {
1047 pub fn Hacl_Blake2s_128_blake2s_update_last(
1048 len: u32,
1049 wv: *mut *mut ::std::os::raw::c_void,
1050 hash: *mut *mut ::std::os::raw::c_void,
1051 prev: u64,
1052 rem: u32,
1053 d: *mut u8,
1054 );
1055}
1056extern "C" {
1057 pub fn Hacl_Blake2s_128_blake2s_finish(nn: u32, output: *mut u8, hash: *mut *mut ::std::os::raw::c_void);
1058}
1059extern "C" {
1060 pub fn Hacl_Blake2s_128_blake2s(nn: u32, output: *mut u8, ll: u32, d: *mut u8, kk: u32, k: *mut u8);
1061}
1062#[repr(C)]
1063#[derive(Debug, Copy, Clone)]
1064pub struct Hacl_Streaming_Blake2s_128_blake2s_128_block_state_s {
1065 pub fst: *mut *mut ::std::os::raw::c_void,
1066 pub snd: *mut *mut ::std::os::raw::c_void,
1067}
1068pub type Hacl_Streaming_Blake2s_128_blake2s_128_block_state = Hacl_Streaming_Blake2s_128_blake2s_128_block_state_s;
1069#[repr(C)]
1070#[derive(Debug, Copy, Clone)]
1071pub struct Hacl_Streaming_Blake2s_128_blake2s_128_state_s {
1072 pub block_state: Hacl_Streaming_Blake2s_128_blake2s_128_block_state,
1073 pub buf: *mut u8,
1074 pub total_len: u64,
1075}
1076pub type Hacl_Streaming_Blake2s_128_blake2s_128_state = Hacl_Streaming_Blake2s_128_blake2s_128_state_s;
1077extern "C" {
1078 pub fn Hacl_Streaming_Blake2s_128_blake2s_128_no_key_create_in() -> *mut Hacl_Streaming_Blake2s_128_blake2s_128_state;
1079}
1080extern "C" {
1081 pub fn Hacl_Streaming_Blake2s_128_blake2s_128_no_key_init(s: *mut Hacl_Streaming_Blake2s_128_blake2s_128_state);
1082}
1083extern "C" {
1084 pub fn Hacl_Streaming_Blake2s_128_blake2s_128_no_key_update(
1085 p: *mut Hacl_Streaming_Blake2s_128_blake2s_128_state,
1086 data: *mut u8,
1087 len: u32,
1088 );
1089}
1090extern "C" {
1091 pub fn Hacl_Streaming_Blake2s_128_blake2s_128_no_key_finish(
1092 p: *mut Hacl_Streaming_Blake2s_128_blake2s_128_state,
1093 dst: *mut u8,
1094 );
1095}
1096extern "C" {
1097 pub fn Hacl_Streaming_Blake2s_128_blake2s_128_no_key_free(s: *mut Hacl_Streaming_Blake2s_128_blake2s_128_state);
1098}
1099extern "C" {
1100 pub fn EverCrypt_Poly1305_poly1305(dst: *mut u8, src: *mut u8, len: u32, key: *mut u8);
1101}
1102extern "C" {
1103 pub fn Hacl_Hash_MD5_legacy_update_multi(s: *mut u32, blocks: *mut u8, n_blocks: u32);
1104}
1105extern "C" {
1106 pub fn Hacl_Hash_MD5_legacy_update_last(s: *mut u32, prev_len: u64, input: *mut u8, input_len: u32);
1107}
1108extern "C" {
1109 pub fn Hacl_Hash_MD5_legacy_hash(input: *mut u8, input_len: u32, dst: *mut u8);
1110}
1111pub type EverCrypt_Hash_alg = Spec_Hash_Definitions_hash_alg;
1112extern "C" {
1113 pub fn EverCrypt_Hash_string_of_alg(uu___: Spec_Hash_Definitions_hash_alg) -> C_String_t;
1114}
1115pub type EverCrypt_Hash_broken_alg = Spec_Hash_Definitions_hash_alg;
1116pub type EverCrypt_Hash_alg13 = Spec_Hash_Definitions_hash_alg;
1117pub type EverCrypt_Hash_e_alg = *mut ::std::os::raw::c_void;
1118pub type EverCrypt_Hash_state_s_tags = u8;
1119#[repr(C)]
1120#[derive(Copy, Clone)]
1121pub struct EverCrypt_Hash_state_s_s {
1122 pub tag: EverCrypt_Hash_state_s_tags,
1123 pub val: EverCrypt_Hash_state_s_s__bindgen_ty_1,
1124}
1125#[repr(C)]
1126#[derive(Copy, Clone)]
1127pub union EverCrypt_Hash_state_s_s__bindgen_ty_1 {
1128 pub case_MD5_s: *mut u32,
1129 pub case_SHA1_s: *mut u32,
1130 pub case_SHA2_224_s: *mut u32,
1131 pub case_SHA2_256_s: *mut u32,
1132 pub case_SHA2_384_s: *mut u64,
1133 pub case_SHA2_512_s: *mut u64,
1134 pub case_Blake2S_s: *mut u32,
1135 pub case_Blake2B_s: *mut u64,
1136}
1137pub type EverCrypt_Hash_state_s = EverCrypt_Hash_state_s_s;
1138extern "C" {
1139 pub fn EverCrypt_Hash_uu___is_MD5_s(
1140 uu___: Spec_Hash_Definitions_hash_alg,
1141 projectee: EverCrypt_Hash_state_s,
1142 ) -> bool;
1143}
1144extern "C" {
1145 pub fn EverCrypt_Hash_uu___is_SHA1_s(
1146 uu___: Spec_Hash_Definitions_hash_alg,
1147 projectee: EverCrypt_Hash_state_s,
1148 ) -> bool;
1149}
1150extern "C" {
1151 pub fn EverCrypt_Hash_uu___is_SHA2_224_s(
1152 uu___: Spec_Hash_Definitions_hash_alg,
1153 projectee: EverCrypt_Hash_state_s,
1154 ) -> bool;
1155}
1156extern "C" {
1157 pub fn EverCrypt_Hash_uu___is_SHA2_256_s(
1158 uu___: Spec_Hash_Definitions_hash_alg,
1159 projectee: EverCrypt_Hash_state_s,
1160 ) -> bool;
1161}
1162extern "C" {
1163 pub fn EverCrypt_Hash_uu___is_SHA2_384_s(
1164 uu___: Spec_Hash_Definitions_hash_alg,
1165 projectee: EverCrypt_Hash_state_s,
1166 ) -> bool;
1167}
1168extern "C" {
1169 pub fn EverCrypt_Hash_uu___is_SHA2_512_s(
1170 uu___: Spec_Hash_Definitions_hash_alg,
1171 projectee: EverCrypt_Hash_state_s,
1172 ) -> bool;
1173}
1174extern "C" {
1175 pub fn EverCrypt_Hash_uu___is_Blake2S_s(
1176 uu___: Spec_Hash_Definitions_hash_alg,
1177 projectee: EverCrypt_Hash_state_s,
1178 ) -> bool;
1179}
1180extern "C" {
1181 pub fn EverCrypt_Hash_uu___is_Blake2B_s(
1182 uu___: Spec_Hash_Definitions_hash_alg,
1183 projectee: EverCrypt_Hash_state_s,
1184 ) -> bool;
1185}
1186extern "C" {
1187 pub fn EverCrypt_Hash_alg_of_state(s: *mut EverCrypt_Hash_state_s) -> Spec_Hash_Definitions_hash_alg;
1188}
1189extern "C" {
1190 pub fn EverCrypt_Hash_create_in(a: Spec_Hash_Definitions_hash_alg) -> *mut EverCrypt_Hash_state_s;
1191}
1192extern "C" {
1193 pub fn EverCrypt_Hash_create(a: Spec_Hash_Definitions_hash_alg) -> *mut EverCrypt_Hash_state_s;
1194}
1195extern "C" {
1196 pub fn EverCrypt_Hash_init(s: *mut EverCrypt_Hash_state_s);
1197}
1198extern "C" {
1199 pub fn EverCrypt_Hash_update_multi_256(s: *mut u32, blocks: *mut u8, n: u32);
1200}
1201extern "C" {
1202 pub fn EverCrypt_Hash_update2(s: *mut EverCrypt_Hash_state_s, prevlen: u64, block: *mut u8);
1203}
1204extern "C" {
1205 pub fn EverCrypt_Hash_update(s: *mut EverCrypt_Hash_state_s, block: *mut u8);
1206}
1207extern "C" {
1208 pub fn EverCrypt_Hash_update_multi2(s: *mut EverCrypt_Hash_state_s, prevlen: u64, blocks: *mut u8, len: u32);
1209}
1210extern "C" {
1211 pub fn EverCrypt_Hash_update_multi(s: *mut EverCrypt_Hash_state_s, blocks: *mut u8, len: u32);
1212}
1213extern "C" {
1214 pub fn EverCrypt_Hash_update_last_256(s: *mut u32, input: u64, input_len: *mut u8, input_len1: u32);
1215}
1216extern "C" {
1217 pub fn EverCrypt_Hash_update_last2(s: *mut EverCrypt_Hash_state_s, prev_len: u64, last: *mut u8, last_len: u32);
1218}
1219extern "C" {
1220 pub fn EverCrypt_Hash_update_last(s: *mut EverCrypt_Hash_state_s, last: *mut u8, total_len: u64);
1221}
1222extern "C" {
1223 pub fn EverCrypt_Hash_finish(s: *mut EverCrypt_Hash_state_s, dst: *mut u8);
1224}
1225extern "C" {
1226 pub fn EverCrypt_Hash_free(s: *mut EverCrypt_Hash_state_s);
1227}
1228extern "C" {
1229 pub fn EverCrypt_Hash_copy(s_src: *mut EverCrypt_Hash_state_s, s_dst: *mut EverCrypt_Hash_state_s);
1230}
1231extern "C" {
1232 pub fn EverCrypt_Hash_hash_256(input: *mut u8, input_len: u32, dst: *mut u8);
1233}
1234extern "C" {
1235 pub fn EverCrypt_Hash_hash_224(input: *mut u8, input_len: u32, dst: *mut u8);
1236}
1237extern "C" {
1238 pub fn EverCrypt_Hash_hash(a: Spec_Hash_Definitions_hash_alg, dst: *mut u8, input: *mut u8, len: u32);
1239}
1240extern "C" {
1241 pub fn EverCrypt_Hash_Incremental_hash_len(a: Spec_Hash_Definitions_hash_alg) -> u32;
1242}
1243extern "C" {
1244 pub fn EverCrypt_Hash_Incremental_block_len(a: Spec_Hash_Definitions_hash_alg) -> u32;
1245}
1246#[repr(C)]
1247#[derive(Debug, Copy, Clone)]
1248pub struct Hacl_Streaming_Functor_state_s___EverCrypt_Hash_state_s_____s {
1249 pub block_state: *mut EverCrypt_Hash_state_s,
1250 pub buf: *mut u8,
1251 pub total_len: u64,
1252}
1253pub type Hacl_Streaming_Functor_state_s___EverCrypt_Hash_state_s____ =
1254 Hacl_Streaming_Functor_state_s___EverCrypt_Hash_state_s_____s;
1255extern "C" {
1256 pub fn EverCrypt_Hash_Incremental_create_in(
1257 a: Spec_Hash_Definitions_hash_alg,
1258 ) -> *mut Hacl_Streaming_Functor_state_s___EverCrypt_Hash_state_s____;
1259}
1260extern "C" {
1261 pub fn EverCrypt_Hash_Incremental_init(s: *mut Hacl_Streaming_Functor_state_s___EverCrypt_Hash_state_s____);
1262}
1263extern "C" {
1264 pub fn EverCrypt_Hash_Incremental_update(
1265 p: *mut Hacl_Streaming_Functor_state_s___EverCrypt_Hash_state_s____,
1266 data: *mut u8,
1267 len: u32,
1268 );
1269}
1270extern "C" {
1271 pub fn EverCrypt_Hash_Incremental_finish_md5(
1272 p: *mut Hacl_Streaming_Functor_state_s___EverCrypt_Hash_state_s____,
1273 dst: *mut u8,
1274 );
1275}
1276extern "C" {
1277 pub fn EverCrypt_Hash_Incremental_finish_sha1(
1278 p: *mut Hacl_Streaming_Functor_state_s___EverCrypt_Hash_state_s____,
1279 dst: *mut u8,
1280 );
1281}
1282extern "C" {
1283 pub fn EverCrypt_Hash_Incremental_finish_sha224(
1284 p: *mut Hacl_Streaming_Functor_state_s___EverCrypt_Hash_state_s____,
1285 dst: *mut u8,
1286 );
1287}
1288extern "C" {
1289 pub fn EverCrypt_Hash_Incremental_finish_sha256(
1290 p: *mut Hacl_Streaming_Functor_state_s___EverCrypt_Hash_state_s____,
1291 dst: *mut u8,
1292 );
1293}
1294extern "C" {
1295 pub fn EverCrypt_Hash_Incremental_finish_sha384(
1296 p: *mut Hacl_Streaming_Functor_state_s___EverCrypt_Hash_state_s____,
1297 dst: *mut u8,
1298 );
1299}
1300extern "C" {
1301 pub fn EverCrypt_Hash_Incremental_finish_sha512(
1302 p: *mut Hacl_Streaming_Functor_state_s___EverCrypt_Hash_state_s____,
1303 dst: *mut u8,
1304 );
1305}
1306extern "C" {
1307 pub fn EverCrypt_Hash_Incremental_finish_blake2s(
1308 p: *mut Hacl_Streaming_Functor_state_s___EverCrypt_Hash_state_s____,
1309 dst: *mut u8,
1310 );
1311}
1312extern "C" {
1313 pub fn EverCrypt_Hash_Incremental_finish_blake2b(
1314 p: *mut Hacl_Streaming_Functor_state_s___EverCrypt_Hash_state_s____,
1315 dst: *mut u8,
1316 );
1317}
1318extern "C" {
1319 pub fn EverCrypt_Hash_Incremental_alg_of_state(
1320 s: *mut Hacl_Streaming_Functor_state_s___EverCrypt_Hash_state_s____,
1321 ) -> Spec_Hash_Definitions_hash_alg;
1322}
1323extern "C" {
1324 pub fn EverCrypt_Hash_Incremental_finish(
1325 s: *mut Hacl_Streaming_Functor_state_s___EverCrypt_Hash_state_s____,
1326 dst: *mut u8,
1327 );
1328}
1329extern "C" {
1330 pub fn EverCrypt_Hash_Incremental_free(s: *mut Hacl_Streaming_Functor_state_s___EverCrypt_Hash_state_s____);
1331}
1332extern "C" {
1333 pub fn EverCrypt_HMAC_compute_sha1(dst: *mut u8, key: *mut u8, key_len: u32, data: *mut u8, data_len: u32);
1334}
1335extern "C" {
1336 pub fn EverCrypt_HMAC_compute_sha2_256(dst: *mut u8, key: *mut u8, key_len: u32, data: *mut u8, data_len: u32);
1337}
1338extern "C" {
1339 pub fn EverCrypt_HMAC_compute_sha2_384(dst: *mut u8, key: *mut u8, key_len: u32, data: *mut u8, data_len: u32);
1340}
1341extern "C" {
1342 pub fn EverCrypt_HMAC_compute_sha2_512(dst: *mut u8, key: *mut u8, key_len: u32, data: *mut u8, data_len: u32);
1343}
1344extern "C" {
1345 pub fn EverCrypt_HMAC_compute_blake2s(dst: *mut u8, key: *mut u8, key_len: u32, data: *mut u8, data_len: u32);
1346}
1347extern "C" {
1348 pub fn EverCrypt_HMAC_compute_blake2b(dst: *mut u8, key: *mut u8, key_len: u32, data: *mut u8, data_len: u32);
1349}
1350extern "C" {
1351 pub fn EverCrypt_HMAC_is_supported_alg(uu___: Spec_Hash_Definitions_hash_alg) -> bool;
1352}
1353pub type EverCrypt_HMAC_supported_alg = Spec_Hash_Definitions_hash_alg;
1354extern "C" {
1355 pub fn EverCrypt_HMAC_compute(
1356 a: Spec_Hash_Definitions_hash_alg,
1357 mac: *mut u8,
1358 key: *mut u8,
1359 keylen: u32,
1360 data: *mut u8,
1361 datalen: u32,
1362 );
1363}
1364extern "C" {
1365 pub fn EverCrypt_HKDF_expand_sha1(okm: *mut u8, prk: *mut u8, prklen: u32, info: *mut u8, infolen: u32, len: u32);
1366}
1367extern "C" {
1368 pub fn EverCrypt_HKDF_extract_sha1(prk: *mut u8, salt: *mut u8, saltlen: u32, ikm: *mut u8, ikmlen: u32);
1369}
1370extern "C" {
1371 pub fn EverCrypt_HKDF_expand_sha2_256(
1372 okm: *mut u8,
1373 prk: *mut u8,
1374 prklen: u32,
1375 info: *mut u8,
1376 infolen: u32,
1377 len: u32,
1378 );
1379}
1380extern "C" {
1381 pub fn EverCrypt_HKDF_extract_sha2_256(prk: *mut u8, salt: *mut u8, saltlen: u32, ikm: *mut u8, ikmlen: u32);
1382}
1383extern "C" {
1384 pub fn EverCrypt_HKDF_expand_sha2_384(
1385 okm: *mut u8,
1386 prk: *mut u8,
1387 prklen: u32,
1388 info: *mut u8,
1389 infolen: u32,
1390 len: u32,
1391 );
1392}
1393extern "C" {
1394 pub fn EverCrypt_HKDF_extract_sha2_384(prk: *mut u8, salt: *mut u8, saltlen: u32, ikm: *mut u8, ikmlen: u32);
1395}
1396extern "C" {
1397 pub fn EverCrypt_HKDF_expand_sha2_512(
1398 okm: *mut u8,
1399 prk: *mut u8,
1400 prklen: u32,
1401 info: *mut u8,
1402 infolen: u32,
1403 len: u32,
1404 );
1405}
1406extern "C" {
1407 pub fn EverCrypt_HKDF_extract_sha2_512(prk: *mut u8, salt: *mut u8, saltlen: u32, ikm: *mut u8, ikmlen: u32);
1408}
1409extern "C" {
1410 pub fn EverCrypt_HKDF_expand_blake2s(
1411 okm: *mut u8,
1412 prk: *mut u8,
1413 prklen: u32,
1414 info: *mut u8,
1415 infolen: u32,
1416 len: u32,
1417 );
1418}
1419extern "C" {
1420 pub fn EverCrypt_HKDF_extract_blake2s(prk: *mut u8, salt: *mut u8, saltlen: u32, ikm: *mut u8, ikmlen: u32);
1421}
1422extern "C" {
1423 pub fn EverCrypt_HKDF_expand_blake2b(
1424 okm: *mut u8,
1425 prk: *mut u8,
1426 prklen: u32,
1427 info: *mut u8,
1428 infolen: u32,
1429 len: u32,
1430 );
1431}
1432extern "C" {
1433 pub fn EverCrypt_HKDF_extract_blake2b(prk: *mut u8, salt: *mut u8, saltlen: u32, ikm: *mut u8, ikmlen: u32);
1434}
1435extern "C" {
1436 pub fn EverCrypt_HKDF_expand(
1437 a: Spec_Hash_Definitions_hash_alg,
1438 okm: *mut u8,
1439 prk: *mut u8,
1440 prklen: u32,
1441 info: *mut u8,
1442 infolen: u32,
1443 len: u32,
1444 );
1445}
1446extern "C" {
1447 pub fn EverCrypt_HKDF_extract(
1448 a: Spec_Hash_Definitions_hash_alg,
1449 prk: *mut u8,
1450 salt: *mut u8,
1451 saltlen: u32,
1452 ikm: *mut u8,
1453 ikmlen: u32,
1454 );
1455}
1456extern "C" {
1457 pub fn EverCrypt_HKDF_hkdf_expand(
1458 a: Spec_Hash_Definitions_hash_alg,
1459 okm: *mut u8,
1460 prk: *mut u8,
1461 prklen: u32,
1462 info: *mut u8,
1463 infolen: u32,
1464 len: u32,
1465 );
1466}
1467extern "C" {
1468 pub fn EverCrypt_HKDF_hkdf_extract(
1469 a: Spec_Hash_Definitions_hash_alg,
1470 prk: *mut u8,
1471 salt: *mut u8,
1472 saltlen: u32,
1473 ikm: *mut u8,
1474 ikmlen: u32,
1475 );
1476}
1477extern "C" {
1478 pub static mut Hacl_Frodo640_crypto_bytes: u32;
1479}
1480extern "C" {
1481 pub static mut Hacl_Frodo640_crypto_publickeybytes: u32;
1482}
1483extern "C" {
1484 pub static mut Hacl_Frodo640_crypto_secretkeybytes: u32;
1485}
1486extern "C" {
1487 pub static mut Hacl_Frodo640_crypto_ciphertextbytes: u32;
1488}
1489extern "C" {
1490 pub fn Hacl_Frodo640_crypto_kem_keypair(pk: *mut u8, sk: *mut u8) -> u32;
1491}
1492extern "C" {
1493 pub fn Hacl_Frodo640_crypto_kem_enc(ct: *mut u8, ss: *mut u8, pk: *mut u8) -> u32;
1494}
1495extern "C" {
1496 pub fn Hacl_Frodo640_crypto_kem_dec(ss: *mut u8, ct: *mut u8, sk: *mut u8) -> u32;
1497}
1498pub type Hacl_HMAC_DRBG_supported_alg = Spec_Hash_Definitions_hash_alg;
1499extern "C" {
1500 pub static mut Hacl_HMAC_DRBG_reseed_interval: u32;
1501}
1502extern "C" {
1503 pub static mut Hacl_HMAC_DRBG_max_output_length: u32;
1504}
1505extern "C" {
1506 pub static mut Hacl_HMAC_DRBG_max_length: u32;
1507}
1508extern "C" {
1509 pub static mut Hacl_HMAC_DRBG_max_personalization_string_length: u32;
1510}
1511extern "C" {
1512 pub static mut Hacl_HMAC_DRBG_max_additional_input_length: u32;
1513}
1514extern "C" {
1515 pub fn Hacl_HMAC_DRBG_min_length(a: Spec_Hash_Definitions_hash_alg) -> u32;
1516}
1517#[repr(C)]
1518#[derive(Debug, Copy, Clone)]
1519pub struct Hacl_HMAC_DRBG_state_s {
1520 pub k: *mut u8,
1521 pub v: *mut u8,
1522 pub reseed_counter: *mut u32,
1523}
1524pub type Hacl_HMAC_DRBG_state = Hacl_HMAC_DRBG_state_s;
1525extern "C" {
1526 pub fn Hacl_HMAC_DRBG_uu___is_State(a: Spec_Hash_Definitions_hash_alg, projectee: Hacl_HMAC_DRBG_state) -> bool;
1527}
1528extern "C" {
1529 pub fn Hacl_HMAC_DRBG_create_in(a: Spec_Hash_Definitions_hash_alg) -> Hacl_HMAC_DRBG_state;
1530}
1531extern "C" {
1532 pub fn Hacl_HMAC_DRBG_instantiate(
1533 a: Spec_Hash_Definitions_hash_alg,
1534 st: Hacl_HMAC_DRBG_state,
1535 entropy_input_len: u32,
1536 entropy_input: *mut u8,
1537 nonce_len: u32,
1538 nonce: *mut u8,
1539 personalization_string_len: u32,
1540 personalization_string: *mut u8,
1541 );
1542}
1543extern "C" {
1544 pub fn Hacl_HMAC_DRBG_reseed(
1545 a: Spec_Hash_Definitions_hash_alg,
1546 st: Hacl_HMAC_DRBG_state,
1547 entropy_input_len: u32,
1548 entropy_input: *mut u8,
1549 additional_input_input_len: u32,
1550 additional_input_input: *mut u8,
1551 );
1552}
1553extern "C" {
1554 pub fn Hacl_HMAC_DRBG_generate(
1555 a: Spec_Hash_Definitions_hash_alg,
1556 output: *mut u8,
1557 st: Hacl_HMAC_DRBG_state,
1558 n: u32,
1559 additional_input_len: u32,
1560 additional_input: *mut u8,
1561 ) -> bool;
1562}
1563extern "C" {
1564 pub fn Hacl_HPKE_P256_CP32_SHA256_setupBaseI(
1565 o_pkE: *mut u8,
1566 o_k: *mut u8,
1567 o_n: *mut u8,
1568 skE: *mut u8,
1569 pkR: *mut u8,
1570 infolen: u32,
1571 info: *mut u8,
1572 ) -> u32;
1573}
1574extern "C" {
1575 pub fn Hacl_HPKE_P256_CP32_SHA256_setupBaseR(
1576 o_key_aead: *mut u8,
1577 o_nonce_aead: *mut u8,
1578 pkE: *mut u8,
1579 skR: *mut u8,
1580 infolen: u32,
1581 info: *mut u8,
1582 ) -> u32;
1583}
1584extern "C" {
1585 pub fn Hacl_HPKE_P256_CP32_SHA256_sealBase(
1586 skE: *mut u8,
1587 pkR: *mut u8,
1588 mlen: u32,
1589 m: *mut u8,
1590 infolen: u32,
1591 info: *mut u8,
1592 output: *mut u8,
1593 ) -> u32;
1594}
1595extern "C" {
1596 pub fn Hacl_HPKE_P256_CP32_SHA256_openBase(
1597 pkE: *mut u8,
1598 skR: *mut u8,
1599 mlen: u32,
1600 m: *mut u8,
1601 infolen: u32,
1602 info: *mut u8,
1603 output: *mut u8,
1604 ) -> u32;
1605}
1606extern "C" {
1607 pub fn Hacl_HPKE_Curve64_CP128_SHA256_setupBaseI(
1608 o_pkE: *mut u8,
1609 o_k: *mut u8,
1610 o_n: *mut u8,
1611 skE: *mut u8,
1612 pkR: *mut u8,
1613 infolen: u32,
1614 info: *mut u8,
1615 ) -> u32;
1616}
1617extern "C" {
1618 pub fn Hacl_HPKE_Curve64_CP128_SHA256_setupBaseR(
1619 o_key_aead: *mut u8,
1620 o_nonce_aead: *mut u8,
1621 pkE: *mut u8,
1622 skR: *mut u8,
1623 infolen: u32,
1624 info: *mut u8,
1625 ) -> u32;
1626}
1627extern "C" {
1628 pub fn Hacl_HPKE_Curve64_CP128_SHA256_sealBase(
1629 skE: *mut u8,
1630 pkR: *mut u8,
1631 mlen: u32,
1632 m: *mut u8,
1633 infolen: u32,
1634 info: *mut u8,
1635 output: *mut u8,
1636 ) -> u32;
1637}
1638extern "C" {
1639 pub fn Hacl_HPKE_Curve64_CP128_SHA256_openBase(
1640 pkE: *mut u8,
1641 skR: *mut u8,
1642 mlen: u32,
1643 m: *mut u8,
1644 infolen: u32,
1645 info: *mut u8,
1646 output: *mut u8,
1647 ) -> u32;
1648}
1649pub type Hacl_Bignum64_pbn_mont_ctx_u64 = *mut Hacl_Bignum_MontArithmetic_bn_mont_ctx_u64;
1650extern "C" {
1651 pub fn Hacl_Bignum64_add(len: u32, a: *mut u64, b: *mut u64, res: *mut u64) -> u64;
1652}
1653extern "C" {
1654 pub fn Hacl_Bignum64_sub(len: u32, a: *mut u64, b: *mut u64, res: *mut u64) -> u64;
1655}
1656extern "C" {
1657 pub fn Hacl_Bignum64_add_mod(len: u32, n: *mut u64, a: *mut u64, b: *mut u64, res: *mut u64);
1658}
1659extern "C" {
1660 pub fn Hacl_Bignum64_sub_mod(len: u32, n: *mut u64, a: *mut u64, b: *mut u64, res: *mut u64);
1661}
1662extern "C" {
1663 pub fn Hacl_Bignum64_mul(len: u32, a: *mut u64, b: *mut u64, res: *mut u64);
1664}
1665extern "C" {
1666 pub fn Hacl_Bignum64_sqr(len: u32, a: *mut u64, res: *mut u64);
1667}
1668extern "C" {
1669 pub fn Hacl_Bignum64_mod(len: u32, n: *mut u64, a: *mut u64, res: *mut u64) -> bool;
1670}
1671extern "C" {
1672 pub fn Hacl_Bignum64_mod_exp_vartime(
1673 len: u32,
1674 n: *mut u64,
1675 a: *mut u64,
1676 bBits: u32,
1677 b: *mut u64,
1678 res: *mut u64,
1679 ) -> bool;
1680}
1681extern "C" {
1682 pub fn Hacl_Bignum64_mod_exp_consttime(
1683 len: u32,
1684 n: *mut u64,
1685 a: *mut u64,
1686 bBits: u32,
1687 b: *mut u64,
1688 res: *mut u64,
1689 ) -> bool;
1690}
1691extern "C" {
1692 pub fn Hacl_Bignum64_mod_inv_prime_vartime(len: u32, n: *mut u64, a: *mut u64, res: *mut u64) -> bool;
1693}
1694extern "C" {
1695 pub fn Hacl_Bignum64_mont_ctx_init(len: u32, n: *mut u64) -> *mut Hacl_Bignum_MontArithmetic_bn_mont_ctx_u64;
1696}
1697extern "C" {
1698 pub fn Hacl_Bignum64_mont_ctx_free(k: *mut Hacl_Bignum_MontArithmetic_bn_mont_ctx_u64);
1699}
1700extern "C" {
1701 pub fn Hacl_Bignum64_mod_precomp(k: *mut Hacl_Bignum_MontArithmetic_bn_mont_ctx_u64, a: *mut u64, res: *mut u64);
1702}
1703extern "C" {
1704 pub fn Hacl_Bignum64_mod_exp_vartime_precomp(
1705 k: *mut Hacl_Bignum_MontArithmetic_bn_mont_ctx_u64,
1706 a: *mut u64,
1707 bBits: u32,
1708 b: *mut u64,
1709 res: *mut u64,
1710 );
1711}
1712extern "C" {
1713 pub fn Hacl_Bignum64_mod_exp_consttime_precomp(
1714 k: *mut Hacl_Bignum_MontArithmetic_bn_mont_ctx_u64,
1715 a: *mut u64,
1716 bBits: u32,
1717 b: *mut u64,
1718 res: *mut u64,
1719 );
1720}
1721extern "C" {
1722 pub fn Hacl_Bignum64_mod_inv_prime_vartime_precomp(
1723 k: *mut Hacl_Bignum_MontArithmetic_bn_mont_ctx_u64,
1724 a: *mut u64,
1725 res: *mut u64,
1726 );
1727}
1728extern "C" {
1729 pub fn Hacl_Bignum64_new_bn_from_bytes_be(len: u32, b: *mut u8) -> *mut u64;
1730}
1731extern "C" {
1732 pub fn Hacl_Bignum64_new_bn_from_bytes_le(len: u32, b: *mut u8) -> *mut u64;
1733}
1734extern "C" {
1735 pub fn Hacl_Bignum64_bn_to_bytes_be(len: u32, b: *mut u64, res: *mut u8);
1736}
1737extern "C" {
1738 pub fn Hacl_Bignum64_bn_to_bytes_le(len: u32, b: *mut u64, res: *mut u8);
1739}
1740extern "C" {
1741 pub fn Hacl_Bignum64_lt_mask(len: u32, a: *mut u64, b: *mut u64) -> u64;
1742}
1743extern "C" {
1744 pub fn Hacl_Bignum64_eq_mask(len: u32, a: *mut u64, b: *mut u64) -> u64;
1745}
1746#[repr(C)]
1747#[derive(Debug, Copy, Clone)]
1748pub struct Hacl_Streaming_SHA2_state_sha2_224_s {
1749 pub block_state: *mut u32,
1750 pub buf: *mut u8,
1751 pub total_len: u64,
1752}
1753pub type Hacl_Streaming_SHA2_state_sha2_224 = Hacl_Streaming_SHA2_state_sha2_224_s;
1754pub type Hacl_Streaming_SHA2_state_sha2_256 = Hacl_Streaming_SHA2_state_sha2_224;
1755#[repr(C)]
1756#[derive(Debug, Copy, Clone)]
1757pub struct Hacl_Streaming_SHA2_state_sha2_384_s {
1758 pub block_state: *mut u64,
1759 pub buf: *mut u8,
1760 pub total_len: u64,
1761}
1762pub type Hacl_Streaming_SHA2_state_sha2_384 = Hacl_Streaming_SHA2_state_sha2_384_s;
1763pub type Hacl_Streaming_SHA2_state_sha2_512 = Hacl_Streaming_SHA2_state_sha2_384;
1764extern "C" {
1765 pub fn Hacl_Streaming_SHA2_create_in_224() -> *mut Hacl_Streaming_SHA2_state_sha2_224;
1766}
1767extern "C" {
1768 pub fn Hacl_Streaming_SHA2_init_224(s: *mut Hacl_Streaming_SHA2_state_sha2_224);
1769}
1770extern "C" {
1771 pub fn Hacl_Streaming_SHA2_update_224(p: *mut Hacl_Streaming_SHA2_state_sha2_224, data: *mut u8, len: u32);
1772}
1773extern "C" {
1774 pub fn Hacl_Streaming_SHA2_finish_224(p: *mut Hacl_Streaming_SHA2_state_sha2_224, dst: *mut u8);
1775}
1776extern "C" {
1777 pub fn Hacl_Streaming_SHA2_free_224(s: *mut Hacl_Streaming_SHA2_state_sha2_224);
1778}
1779extern "C" {
1780 pub fn Hacl_Streaming_SHA2_create_in_256() -> *mut Hacl_Streaming_SHA2_state_sha2_224;
1781}
1782extern "C" {
1783 pub fn Hacl_Streaming_SHA2_init_256(s: *mut Hacl_Streaming_SHA2_state_sha2_224);
1784}
1785extern "C" {
1786 pub fn Hacl_Streaming_SHA2_update_256(p: *mut Hacl_Streaming_SHA2_state_sha2_224, data: *mut u8, len: u32);
1787}
1788extern "C" {
1789 pub fn Hacl_Streaming_SHA2_finish_256(p: *mut Hacl_Streaming_SHA2_state_sha2_224, dst: *mut u8);
1790}
1791extern "C" {
1792 pub fn Hacl_Streaming_SHA2_free_256(s: *mut Hacl_Streaming_SHA2_state_sha2_224);
1793}
1794extern "C" {
1795 pub fn Hacl_Streaming_SHA2_create_in_384() -> *mut Hacl_Streaming_SHA2_state_sha2_384;
1796}
1797extern "C" {
1798 pub fn Hacl_Streaming_SHA2_init_384(s: *mut Hacl_Streaming_SHA2_state_sha2_384);
1799}
1800extern "C" {
1801 pub fn Hacl_Streaming_SHA2_update_384(p: *mut Hacl_Streaming_SHA2_state_sha2_384, data: *mut u8, len: u32);
1802}
1803extern "C" {
1804 pub fn Hacl_Streaming_SHA2_finish_384(p: *mut Hacl_Streaming_SHA2_state_sha2_384, dst: *mut u8);
1805}
1806extern "C" {
1807 pub fn Hacl_Streaming_SHA2_free_384(s: *mut Hacl_Streaming_SHA2_state_sha2_384);
1808}
1809extern "C" {
1810 pub fn Hacl_Streaming_SHA2_create_in_512() -> *mut Hacl_Streaming_SHA2_state_sha2_384;
1811}
1812extern "C" {
1813 pub fn Hacl_Streaming_SHA2_init_512(s: *mut Hacl_Streaming_SHA2_state_sha2_384);
1814}
1815extern "C" {
1816 pub fn Hacl_Streaming_SHA2_update_512(p: *mut Hacl_Streaming_SHA2_state_sha2_384, data: *mut u8, len: u32);
1817}
1818extern "C" {
1819 pub fn Hacl_Streaming_SHA2_finish_512(p: *mut Hacl_Streaming_SHA2_state_sha2_384, dst: *mut u8);
1820}
1821extern "C" {
1822 pub fn Hacl_Streaming_SHA2_free_512(s: *mut Hacl_Streaming_SHA2_state_sha2_384);
1823}
1824pub type Hacl_Streaming_SHA1_state_sha1 = Hacl_Streaming_SHA2_state_sha2_224;
1825extern "C" {
1826 pub fn Hacl_Streaming_SHA1_legacy_create_in_sha1() -> *mut Hacl_Streaming_SHA2_state_sha2_224;
1827}
1828extern "C" {
1829 pub fn Hacl_Streaming_SHA1_legacy_init_sha1(s: *mut Hacl_Streaming_SHA2_state_sha2_224);
1830}
1831extern "C" {
1832 pub fn Hacl_Streaming_SHA1_legacy_update_sha1(p: *mut Hacl_Streaming_SHA2_state_sha2_224, data: *mut u8, len: u32);
1833}
1834extern "C" {
1835 pub fn Hacl_Streaming_SHA1_legacy_finish_sha1(p: *mut Hacl_Streaming_SHA2_state_sha2_224, dst: *mut u8);
1836}
1837extern "C" {
1838 pub fn Hacl_Streaming_SHA1_legacy_free_sha1(s: *mut Hacl_Streaming_SHA2_state_sha2_224);
1839}
1840extern "C" {
1841 pub fn Hacl_HMAC_Blake2s_128_compute_blake2s_128(
1842 dst: *mut u8,
1843 key: *mut u8,
1844 key_len: u32,
1845 data: *mut u8,
1846 data_len: u32,
1847 );
1848}
1849pub type Hacl_Streaming_MD5_state_md5 = Hacl_Streaming_SHA2_state_sha2_224;
1850extern "C" {
1851 pub fn Hacl_Streaming_MD5_legacy_create_in_md5() -> *mut Hacl_Streaming_SHA2_state_sha2_224;
1852}
1853extern "C" {
1854 pub fn Hacl_Streaming_MD5_legacy_init_md5(s: *mut Hacl_Streaming_SHA2_state_sha2_224);
1855}
1856extern "C" {
1857 pub fn Hacl_Streaming_MD5_legacy_update_md5(p: *mut Hacl_Streaming_SHA2_state_sha2_224, data: *mut u8, len: u32);
1858}
1859extern "C" {
1860 pub fn Hacl_Streaming_MD5_legacy_finish_md5(p: *mut Hacl_Streaming_SHA2_state_sha2_224, dst: *mut u8);
1861}
1862extern "C" {
1863 pub fn Hacl_Streaming_MD5_legacy_free_md5(s: *mut Hacl_Streaming_SHA2_state_sha2_224);
1864}
1865extern "C" {
1866 pub fn Hacl_Blake2b_256_blake2b_init(hash: *mut *mut ::std::os::raw::c_void, kk: u32, nn: u32);
1867}
1868extern "C" {
1869 pub fn Hacl_Blake2b_256_blake2b_update_key(
1870 wv: *mut *mut ::std::os::raw::c_void,
1871 hash: *mut *mut ::std::os::raw::c_void,
1872 kk: u32,
1873 k: *mut u8,
1874 ll: u32,
1875 );
1876}
1877extern "C" {
1878 pub fn Hacl_Blake2b_256_blake2b_finish(nn: u32, output: *mut u8, hash: *mut *mut ::std::os::raw::c_void);
1879}
1880extern "C" {
1881 pub fn Hacl_Blake2b_256_blake2b(nn: u32, output: *mut u8, ll: u32, d: *mut u8, kk: u32, k: *mut u8);
1882}
1883#[repr(C)]
1884#[derive(Debug, Copy, Clone)]
1885pub struct Hacl_Streaming_Blake2b_256_blake2b_256_block_state_s {
1886 pub fst: *mut *mut ::std::os::raw::c_void,
1887 pub snd: *mut *mut ::std::os::raw::c_void,
1888}
1889pub type Hacl_Streaming_Blake2b_256_blake2b_256_block_state = Hacl_Streaming_Blake2b_256_blake2b_256_block_state_s;
1890#[repr(C)]
1891#[derive(Debug, Copy, Clone)]
1892pub struct Hacl_Streaming_Blake2b_256_blake2b_256_state_s {
1893 pub block_state: Hacl_Streaming_Blake2b_256_blake2b_256_block_state,
1894 pub buf: *mut u8,
1895 pub total_len: u64,
1896}
1897pub type Hacl_Streaming_Blake2b_256_blake2b_256_state = Hacl_Streaming_Blake2b_256_blake2b_256_state_s;
1898extern "C" {
1899 pub fn Hacl_Streaming_Blake2b_256_blake2b_256_no_key_create_in() -> *mut Hacl_Streaming_Blake2b_256_blake2b_256_state;
1900}
1901extern "C" {
1902 pub fn Hacl_Streaming_Blake2b_256_blake2b_256_no_key_init(s: *mut Hacl_Streaming_Blake2b_256_blake2b_256_state);
1903}
1904extern "C" {
1905 pub fn Hacl_Streaming_Blake2b_256_blake2b_256_no_key_update(
1906 p: *mut Hacl_Streaming_Blake2b_256_blake2b_256_state,
1907 data: *mut u8,
1908 len: u32,
1909 );
1910}
1911extern "C" {
1912 pub fn Hacl_Streaming_Blake2b_256_blake2b_256_no_key_finish(
1913 p: *mut Hacl_Streaming_Blake2b_256_blake2b_256_state,
1914 dst: *mut u8,
1915 );
1916}
1917extern "C" {
1918 pub fn Hacl_Streaming_Blake2b_256_blake2b_256_no_key_free(s: *mut Hacl_Streaming_Blake2b_256_blake2b_256_state);
1919}
1920extern "C" {
1921 pub fn Hacl_Bignum256_32_add(a: *mut u32, b: *mut u32, res: *mut u32) -> u32;
1922}
1923extern "C" {
1924 pub fn Hacl_Bignum256_32_sub(a: *mut u32, b: *mut u32, res: *mut u32) -> u32;
1925}
1926extern "C" {
1927 pub fn Hacl_Bignum256_32_add_mod(n: *mut u32, a: *mut u32, b: *mut u32, res: *mut u32);
1928}
1929extern "C" {
1930 pub fn Hacl_Bignum256_32_sub_mod(n: *mut u32, a: *mut u32, b: *mut u32, res: *mut u32);
1931}
1932extern "C" {
1933 pub fn Hacl_Bignum256_32_mul(a: *mut u32, b: *mut u32, res: *mut u32);
1934}
1935extern "C" {
1936 pub fn Hacl_Bignum256_32_sqr(a: *mut u32, res: *mut u32);
1937}
1938extern "C" {
1939 pub fn Hacl_Bignum256_32_mod(n: *mut u32, a: *mut u32, res: *mut u32) -> bool;
1940}
1941extern "C" {
1942 pub fn Hacl_Bignum256_32_mod_exp_vartime(n: *mut u32, a: *mut u32, bBits: u32, b: *mut u32, res: *mut u32) -> bool;
1943}
1944extern "C" {
1945 pub fn Hacl_Bignum256_32_mod_exp_consttime(
1946 n: *mut u32,
1947 a: *mut u32,
1948 bBits: u32,
1949 b: *mut u32,
1950 res: *mut u32,
1951 ) -> bool;
1952}
1953extern "C" {
1954 pub fn Hacl_Bignum256_32_mod_inv_prime_vartime(n: *mut u32, a: *mut u32, res: *mut u32) -> bool;
1955}
1956extern "C" {
1957 pub fn Hacl_Bignum256_32_mont_ctx_init(n: *mut u32) -> *mut Hacl_Bignum_MontArithmetic_bn_mont_ctx_u32;
1958}
1959extern "C" {
1960 pub fn Hacl_Bignum256_32_mont_ctx_free(k: *mut Hacl_Bignum_MontArithmetic_bn_mont_ctx_u32);
1961}
1962extern "C" {
1963 pub fn Hacl_Bignum256_32_mod_precomp(
1964 k: *mut Hacl_Bignum_MontArithmetic_bn_mont_ctx_u32,
1965 a: *mut u32,
1966 res: *mut u32,
1967 );
1968}
1969extern "C" {
1970 pub fn Hacl_Bignum256_32_mod_exp_vartime_precomp(
1971 k: *mut Hacl_Bignum_MontArithmetic_bn_mont_ctx_u32,
1972 a: *mut u32,
1973 bBits: u32,
1974 b: *mut u32,
1975 res: *mut u32,
1976 );
1977}
1978extern "C" {
1979 pub fn Hacl_Bignum256_32_mod_exp_consttime_precomp(
1980 k: *mut Hacl_Bignum_MontArithmetic_bn_mont_ctx_u32,
1981 a: *mut u32,
1982 bBits: u32,
1983 b: *mut u32,
1984 res: *mut u32,
1985 );
1986}
1987extern "C" {
1988 pub fn Hacl_Bignum256_32_mod_inv_prime_vartime_precomp(
1989 k: *mut Hacl_Bignum_MontArithmetic_bn_mont_ctx_u32,
1990 a: *mut u32,
1991 res: *mut u32,
1992 );
1993}
1994extern "C" {
1995 pub fn Hacl_Bignum256_32_new_bn_from_bytes_be(len: u32, b: *mut u8) -> *mut u32;
1996}
1997extern "C" {
1998 pub fn Hacl_Bignum256_32_new_bn_from_bytes_le(len: u32, b: *mut u8) -> *mut u32;
1999}
2000extern "C" {
2001 pub fn Hacl_Bignum256_32_bn_to_bytes_be(b: *mut u32, res: *mut u8);
2002}
2003extern "C" {
2004 pub fn Hacl_Bignum256_32_bn_to_bytes_le(b: *mut u32, res: *mut u8);
2005}
2006extern "C" {
2007 pub fn Hacl_Bignum256_32_lt_mask(a: *mut u32, b: *mut u32) -> u32;
2008}
2009extern "C" {
2010 pub fn Hacl_Bignum256_32_eq_mask(a: *mut u32, b: *mut u32) -> u32;
2011}
2012#[repr(C)]
2013#[derive(Debug, Copy, Clone)]
2014pub struct Hacl_Streaming_Poly1305_128_poly1305_128_state_s {
2015 pub block_state: *mut *mut ::std::os::raw::c_void,
2016 pub buf: *mut u8,
2017 pub total_len: u64,
2018 pub p_key: *mut u8,
2019}
2020pub type Hacl_Streaming_Poly1305_128_poly1305_128_state = Hacl_Streaming_Poly1305_128_poly1305_128_state_s;
2021extern "C" {
2022 pub fn Hacl_Streaming_Poly1305_128_create_in(k: *mut u8) -> *mut Hacl_Streaming_Poly1305_128_poly1305_128_state;
2023}
2024extern "C" {
2025 pub fn Hacl_Streaming_Poly1305_128_init(k: *mut u8, s: *mut Hacl_Streaming_Poly1305_128_poly1305_128_state);
2026}
2027extern "C" {
2028 pub fn Hacl_Streaming_Poly1305_128_update(
2029 p: *mut Hacl_Streaming_Poly1305_128_poly1305_128_state,
2030 data: *mut u8,
2031 len: u32,
2032 );
2033}
2034extern "C" {
2035 pub fn Hacl_Streaming_Poly1305_128_finish(p: *mut Hacl_Streaming_Poly1305_128_poly1305_128_state, dst: *mut u8);
2036}
2037extern "C" {
2038 pub fn Hacl_Streaming_Poly1305_128_free(s: *mut Hacl_Streaming_Poly1305_128_poly1305_128_state);
2039}
2040extern "C" {
2041 pub fn Hacl_HPKE_Curve64_CP32_SHA256_setupBaseI(
2042 o_pkE: *mut u8,
2043 o_k: *mut u8,
2044 o_n: *mut u8,
2045 skE: *mut u8,
2046 pkR: *mut u8,
2047 infolen: u32,
2048 info: *mut u8,
2049 ) -> u32;
2050}
2051extern "C" {
2052 pub fn Hacl_HPKE_Curve64_CP32_SHA256_setupBaseR(
2053 o_key_aead: *mut u8,
2054 o_nonce_aead: *mut u8,
2055 pkE: *mut u8,
2056 skR: *mut u8,
2057 infolen: u32,
2058 info: *mut u8,
2059 ) -> u32;
2060}
2061extern "C" {
2062 pub fn Hacl_HPKE_Curve64_CP32_SHA256_sealBase(
2063 skE: *mut u8,
2064 pkR: *mut u8,
2065 mlen: u32,
2066 m: *mut u8,
2067 infolen: u32,
2068 info: *mut u8,
2069 output: *mut u8,
2070 ) -> u32;
2071}
2072extern "C" {
2073 pub fn Hacl_HPKE_Curve64_CP32_SHA256_openBase(
2074 pkE: *mut u8,
2075 skR: *mut u8,
2076 mlen: u32,
2077 m: *mut u8,
2078 infolen: u32,
2079 info: *mut u8,
2080 output: *mut u8,
2081 ) -> u32;
2082}
2083extern "C" {
2084 pub fn Hacl_Salsa20_salsa20_encrypt(len: u32, out: *mut u8, text: *mut u8, key: *mut u8, n: *mut u8, ctr: u32);
2085}
2086extern "C" {
2087 pub fn Hacl_Salsa20_salsa20_decrypt(len: u32, out: *mut u8, cipher: *mut u8, key: *mut u8, n: *mut u8, ctr: u32);
2088}
2089extern "C" {
2090 pub fn Hacl_Salsa20_salsa20_key_block0(out: *mut u8, key: *mut u8, n: *mut u8);
2091}
2092extern "C" {
2093 pub fn Hacl_Salsa20_hsalsa20(out: *mut u8, key: *mut u8, n: *mut u8);
2094}
2095extern "C" {
2096 pub fn Hacl_HPKE_Curve64_CP256_SHA512_setupBaseI(
2097 o_pkE: *mut u8,
2098 o_k: *mut u8,
2099 o_n: *mut u8,
2100 skE: *mut u8,
2101 pkR: *mut u8,
2102 infolen: u32,
2103 info: *mut u8,
2104 ) -> u32;
2105}
2106extern "C" {
2107 pub fn Hacl_HPKE_Curve64_CP256_SHA512_setupBaseR(
2108 o_key_aead: *mut u8,
2109 o_nonce_aead: *mut u8,
2110 pkE: *mut u8,
2111 skR: *mut u8,
2112 infolen: u32,
2113 info: *mut u8,
2114 ) -> u32;
2115}
2116extern "C" {
2117 pub fn Hacl_HPKE_Curve64_CP256_SHA512_sealBase(
2118 skE: *mut u8,
2119 pkR: *mut u8,
2120 mlen: u32,
2121 m: *mut u8,
2122 infolen: u32,
2123 info: *mut u8,
2124 output: *mut u8,
2125 ) -> u32;
2126}
2127extern "C" {
2128 pub fn Hacl_HPKE_Curve64_CP256_SHA512_openBase(
2129 pkE: *mut u8,
2130 skR: *mut u8,
2131 mlen: u32,
2132 m: *mut u8,
2133 infolen: u32,
2134 info: *mut u8,
2135 output: *mut u8,
2136 ) -> u32;
2137}
2138extern "C" {
2139 pub fn Hacl_Bignum4096_add(a: *mut u64, b: *mut u64, res: *mut u64) -> u64;
2140}
2141extern "C" {
2142 pub fn Hacl_Bignum4096_sub(a: *mut u64, b: *mut u64, res: *mut u64) -> u64;
2143}
2144extern "C" {
2145 pub fn Hacl_Bignum4096_add_mod(n: *mut u64, a: *mut u64, b: *mut u64, res: *mut u64);
2146}
2147extern "C" {
2148 pub fn Hacl_Bignum4096_sub_mod(n: *mut u64, a: *mut u64, b: *mut u64, res: *mut u64);
2149}
2150extern "C" {
2151 pub fn Hacl_Bignum4096_mul(a: *mut u64, b: *mut u64, res: *mut u64);
2152}
2153extern "C" {
2154 pub fn Hacl_Bignum4096_sqr(a: *mut u64, res: *mut u64);
2155}
2156extern "C" {
2157 pub fn Hacl_Bignum4096_mod(n: *mut u64, a: *mut u64, res: *mut u64) -> bool;
2158}
2159extern "C" {
2160 pub fn Hacl_Bignum4096_mod_exp_vartime(n: *mut u64, a: *mut u64, bBits: u32, b: *mut u64, res: *mut u64) -> bool;
2161}
2162extern "C" {
2163 pub fn Hacl_Bignum4096_mod_exp_consttime(n: *mut u64, a: *mut u64, bBits: u32, b: *mut u64, res: *mut u64) -> bool;
2164}
2165extern "C" {
2166 pub fn Hacl_Bignum4096_mod_inv_prime_vartime(n: *mut u64, a: *mut u64, res: *mut u64) -> bool;
2167}
2168extern "C" {
2169 pub fn Hacl_Bignum4096_mont_ctx_init(n: *mut u64) -> *mut Hacl_Bignum_MontArithmetic_bn_mont_ctx_u64;
2170}
2171extern "C" {
2172 pub fn Hacl_Bignum4096_mont_ctx_free(k: *mut Hacl_Bignum_MontArithmetic_bn_mont_ctx_u64);
2173}
2174extern "C" {
2175 pub fn Hacl_Bignum4096_mod_precomp(k: *mut Hacl_Bignum_MontArithmetic_bn_mont_ctx_u64, a: *mut u64, res: *mut u64);
2176}
2177extern "C" {
2178 pub fn Hacl_Bignum4096_mod_exp_vartime_precomp(
2179 k: *mut Hacl_Bignum_MontArithmetic_bn_mont_ctx_u64,
2180 a: *mut u64,
2181 bBits: u32,
2182 b: *mut u64,
2183 res: *mut u64,
2184 );
2185}
2186extern "C" {
2187 pub fn Hacl_Bignum4096_mod_exp_consttime_precomp(
2188 k: *mut Hacl_Bignum_MontArithmetic_bn_mont_ctx_u64,
2189 a: *mut u64,
2190 bBits: u32,
2191 b: *mut u64,
2192 res: *mut u64,
2193 );
2194}
2195extern "C" {
2196 pub fn Hacl_Bignum4096_mod_inv_prime_vartime_precomp(
2197 k: *mut Hacl_Bignum_MontArithmetic_bn_mont_ctx_u64,
2198 a: *mut u64,
2199 res: *mut u64,
2200 );
2201}
2202extern "C" {
2203 pub fn Hacl_Bignum4096_new_bn_from_bytes_be(len: u32, b: *mut u8) -> *mut u64;
2204}
2205extern "C" {
2206 pub fn Hacl_Bignum4096_new_bn_from_bytes_le(len: u32, b: *mut u8) -> *mut u64;
2207}
2208extern "C" {
2209 pub fn Hacl_Bignum4096_bn_to_bytes_be(b: *mut u64, res: *mut u8);
2210}
2211extern "C" {
2212 pub fn Hacl_Bignum4096_bn_to_bytes_le(b: *mut u64, res: *mut u8);
2213}
2214extern "C" {
2215 pub fn Hacl_Bignum4096_lt_mask(a: *mut u64, b: *mut u64) -> u64;
2216}
2217extern "C" {
2218 pub fn Hacl_Bignum4096_eq_mask(a: *mut u64, b: *mut u64) -> u64;
2219}
2220extern "C" {
2221 pub fn Hacl_HPKE_Curve64_CP32_SHA512_setupBaseI(
2222 o_pkE: *mut u8,
2223 o_k: *mut u8,
2224 o_n: *mut u8,
2225 skE: *mut u8,
2226 pkR: *mut u8,
2227 infolen: u32,
2228 info: *mut u8,
2229 ) -> u32;
2230}
2231extern "C" {
2232 pub fn Hacl_HPKE_Curve64_CP32_SHA512_setupBaseR(
2233 o_key_aead: *mut u8,
2234 o_nonce_aead: *mut u8,
2235 pkE: *mut u8,
2236 skR: *mut u8,
2237 infolen: u32,
2238 info: *mut u8,
2239 ) -> u32;
2240}
2241extern "C" {
2242 pub fn Hacl_HPKE_Curve64_CP32_SHA512_sealBase(
2243 skE: *mut u8,
2244 pkR: *mut u8,
2245 mlen: u32,
2246 m: *mut u8,
2247 infolen: u32,
2248 info: *mut u8,
2249 output: *mut u8,
2250 ) -> u32;
2251}
2252extern "C" {
2253 pub fn Hacl_HPKE_Curve64_CP32_SHA512_openBase(
2254 pkE: *mut u8,
2255 skR: *mut u8,
2256 mlen: u32,
2257 m: *mut u8,
2258 infolen: u32,
2259 info: *mut u8,
2260 output: *mut u8,
2261 ) -> u32;
2262}
2263extern "C" {
2264 pub fn Hacl_HPKE_Curve64_CP256_SHA256_setupBaseI(
2265 o_pkE: *mut u8,
2266 o_k: *mut u8,
2267 o_n: *mut u8,
2268 skE: *mut u8,
2269 pkR: *mut u8,
2270 infolen: u32,
2271 info: *mut u8,
2272 ) -> u32;
2273}
2274extern "C" {
2275 pub fn Hacl_HPKE_Curve64_CP256_SHA256_setupBaseR(
2276 o_key_aead: *mut u8,
2277 o_nonce_aead: *mut u8,
2278 pkE: *mut u8,
2279 skR: *mut u8,
2280 infolen: u32,
2281 info: *mut u8,
2282 ) -> u32;
2283}
2284extern "C" {
2285 pub fn Hacl_HPKE_Curve64_CP256_SHA256_sealBase(
2286 skE: *mut u8,
2287 pkR: *mut u8,
2288 mlen: u32,
2289 m: *mut u8,
2290 infolen: u32,
2291 info: *mut u8,
2292 output: *mut u8,
2293 ) -> u32;
2294}
2295extern "C" {
2296 pub fn Hacl_HPKE_Curve64_CP256_SHA256_openBase(
2297 pkE: *mut u8,
2298 skR: *mut u8,
2299 mlen: u32,
2300 m: *mut u8,
2301 infolen: u32,
2302 info: *mut u8,
2303 output: *mut u8,
2304 ) -> u32;
2305}
2306extern "C" {
2307 pub fn Hacl_Hash_Definitions_word_len(a: Spec_Hash_Definitions_hash_alg) -> u32;
2308}
2309extern "C" {
2310 pub fn Hacl_Hash_Definitions_block_len(a: Spec_Hash_Definitions_hash_alg) -> u32;
2311}
2312extern "C" {
2313 pub fn Hacl_Hash_Definitions_hash_word_len(a: Spec_Hash_Definitions_hash_alg) -> u32;
2314}
2315extern "C" {
2316 pub fn Hacl_Hash_Definitions_hash_len(a: Spec_Hash_Definitions_hash_alg) -> u32;
2317}
2318extern "C" {
2319 pub fn Hacl_Ed25519_sign(signature: *mut u8, priv_: *mut u8, len: u32, msg: *mut u8);
2320}
2321extern "C" {
2322 pub fn Hacl_Ed25519_verify(pub_: *mut u8, len: u32, msg: *mut u8, signature: *mut u8) -> bool;
2323}
2324extern "C" {
2325 pub fn Hacl_Ed25519_secret_to_public(pub_: *mut u8, priv_: *mut u8);
2326}
2327extern "C" {
2328 pub fn Hacl_Ed25519_expand_keys(ks: *mut u8, priv_: *mut u8);
2329}
2330extern "C" {
2331 pub fn Hacl_Ed25519_sign_expanded(signature: *mut u8, ks: *mut u8, len: u32, msg: *mut u8);
2332}
2333extern "C" {
2334 pub static Hacl_Impl_FFDHE_Constants_ffdhe_g2: [u8; 1usize];
2335}
2336extern "C" {
2337 pub static Hacl_Impl_FFDHE_Constants_ffdhe_p2048: [u8; 256usize];
2338}
2339extern "C" {
2340 pub static Hacl_Impl_FFDHE_Constants_ffdhe_p3072: [u8; 384usize];
2341}
2342extern "C" {
2343 pub static Hacl_Impl_FFDHE_Constants_ffdhe_p4096: [u8; 512usize];
2344}
2345extern "C" {
2346 pub static Hacl_Impl_FFDHE_Constants_ffdhe_p6144: [u8; 768usize];
2347}
2348extern "C" {
2349 pub static Hacl_Impl_FFDHE_Constants_ffdhe_p8192: [u8; 1024usize];
2350}
2351extern "C" {
2352 pub fn Hacl_FFDHE_ffdhe_len(a: Spec_FFDHE_ffdhe_alg) -> u32;
2353}
2354extern "C" {
2355 pub fn Hacl_FFDHE_new_ffdhe_precomp_p(a: Spec_FFDHE_ffdhe_alg) -> *mut u64;
2356}
2357extern "C" {
2358 pub fn Hacl_FFDHE_ffdhe_secret_to_public_precomp(
2359 a: Spec_FFDHE_ffdhe_alg,
2360 p_r2_n: *mut u64,
2361 sk: *mut u8,
2362 pk: *mut u8,
2363 );
2364}
2365extern "C" {
2366 pub fn Hacl_FFDHE_ffdhe_secret_to_public(a: Spec_FFDHE_ffdhe_alg, sk: *mut u8, pk: *mut u8);
2367}
2368extern "C" {
2369 pub fn Hacl_FFDHE_ffdhe_shared_secret_precomp(
2370 a: Spec_FFDHE_ffdhe_alg,
2371 p_r2_n: *mut u64,
2372 sk: *mut u8,
2373 pk: *mut u8,
2374 ss: *mut u8,
2375 ) -> u64;
2376}
2377extern "C" {
2378 pub fn Hacl_FFDHE_ffdhe_shared_secret(a: Spec_FFDHE_ffdhe_alg, sk: *mut u8, pk: *mut u8, ss: *mut u8) -> u64;
2379}
2380extern "C" {
2381 pub fn EverCrypt_Curve25519_secret_to_public(pub_: *mut u8, priv_: *mut u8);
2382}
2383extern "C" {
2384 pub fn EverCrypt_Curve25519_scalarmult(shared: *mut u8, my_priv: *mut u8, their_pub: *mut u8);
2385}
2386extern "C" {
2387 pub fn EverCrypt_Curve25519_ecdh(shared: *mut u8, my_priv: *mut u8, their_pub: *mut u8) -> bool;
2388}
2389extern "C" {
2390 pub fn Hacl_EC_Ed25519_mk_felem_zero(b: *mut u64);
2391}
2392extern "C" {
2393 pub fn Hacl_EC_Ed25519_mk_felem_one(b: *mut u64);
2394}
2395extern "C" {
2396 pub fn Hacl_EC_Ed25519_felem_add(a: *mut u64, b: *mut u64, out: *mut u64);
2397}
2398extern "C" {
2399 pub fn Hacl_EC_Ed25519_felem_sub(a: *mut u64, b: *mut u64, out: *mut u64);
2400}
2401extern "C" {
2402 pub fn Hacl_EC_Ed25519_felem_mul(a: *mut u64, b: *mut u64, out: *mut u64);
2403}
2404extern "C" {
2405 pub fn Hacl_EC_Ed25519_felem_inv(a: *mut u64, out: *mut u64);
2406}
2407extern "C" {
2408 pub fn Hacl_EC_Ed25519_felem_load(b: *mut u8, out: *mut u64);
2409}
2410extern "C" {
2411 pub fn Hacl_EC_Ed25519_felem_store(a: *mut u64, out: *mut u8);
2412}
2413extern "C" {
2414 pub fn Hacl_EC_Ed25519_mk_point_at_inf(p: *mut u64);
2415}
2416extern "C" {
2417 pub fn Hacl_EC_Ed25519_mk_base_point(p: *mut u64);
2418}
2419extern "C" {
2420 pub fn Hacl_EC_Ed25519_point_negate(p: *mut u64, out: *mut u64);
2421}
2422extern "C" {
2423 pub fn Hacl_EC_Ed25519_point_add(p: *mut u64, q: *mut u64, out: *mut u64);
2424}
2425extern "C" {
2426 pub fn Hacl_EC_Ed25519_point_mul(scalar: *mut u8, p: *mut u64, out: *mut u64);
2427}
2428extern "C" {
2429 pub fn Hacl_EC_Ed25519_point_eq(p: *mut u64, q: *mut u64) -> bool;
2430}
2431extern "C" {
2432 pub fn Hacl_EC_Ed25519_point_compress(p: *mut u64, out: *mut u8);
2433}
2434extern "C" {
2435 pub fn Hacl_EC_Ed25519_point_decompress(s: *mut u8, out: *mut u64) -> bool;
2436}
2437extern "C" {
2438 pub fn Hacl_HPKE_Curve51_CP256_SHA512_setupBaseI(
2439 o_pkE: *mut u8,
2440 o_k: *mut u8,
2441 o_n: *mut u8,
2442 skE: *mut u8,
2443 pkR: *mut u8,
2444 infolen: u32,
2445 info: *mut u8,
2446 ) -> u32;
2447}
2448extern "C" {
2449 pub fn Hacl_HPKE_Curve51_CP256_SHA512_setupBaseR(
2450 o_key_aead: *mut u8,
2451 o_nonce_aead: *mut u8,
2452 pkE: *mut u8,
2453 skR: *mut u8,
2454 infolen: u32,
2455 info: *mut u8,
2456 ) -> u32;
2457}
2458extern "C" {
2459 pub fn Hacl_HPKE_Curve51_CP256_SHA512_sealBase(
2460 skE: *mut u8,
2461 pkR: *mut u8,
2462 mlen: u32,
2463 m: *mut u8,
2464 infolen: u32,
2465 info: *mut u8,
2466 output: *mut u8,
2467 ) -> u32;
2468}
2469extern "C" {
2470 pub fn Hacl_HPKE_Curve51_CP256_SHA512_openBase(
2471 pkE: *mut u8,
2472 skR: *mut u8,
2473 mlen: u32,
2474 m: *mut u8,
2475 infolen: u32,
2476 info: *mut u8,
2477 output: *mut u8,
2478 ) -> u32;
2479}
2480extern "C" {
2481 pub fn EverCrypt_Ed25519_sign(signature: *mut u8, secret: *mut u8, len: u32, msg: *mut u8);
2482}
2483extern "C" {
2484 pub fn EverCrypt_Ed25519_verify(pubkey: *mut u8, len: u32, msg: *mut u8, signature: *mut u8) -> bool;
2485}
2486extern "C" {
2487 pub fn EverCrypt_Ed25519_secret_to_public(output: *mut u8, secret: *mut u8);
2488}
2489extern "C" {
2490 pub fn EverCrypt_Ed25519_expand_keys(ks: *mut u8, secret: *mut u8);
2491}
2492extern "C" {
2493 pub fn EverCrypt_Ed25519_sign_expanded(signature: *mut u8, ks: *mut u8, len: u32, msg: *mut u8);
2494}
2495extern "C" {
2496 pub static mut Hacl_Frodo976_crypto_bytes: u32;
2497}
2498extern "C" {
2499 pub static mut Hacl_Frodo976_crypto_publickeybytes: u32;
2500}
2501extern "C" {
2502 pub static mut Hacl_Frodo976_crypto_secretkeybytes: u32;
2503}
2504extern "C" {
2505 pub static mut Hacl_Frodo976_crypto_ciphertextbytes: u32;
2506}
2507extern "C" {
2508 pub fn Hacl_Frodo976_crypto_kem_keypair(pk: *mut u8, sk: *mut u8) -> u32;
2509}
2510extern "C" {
2511 pub fn Hacl_Frodo976_crypto_kem_enc(ct: *mut u8, ss: *mut u8, pk: *mut u8) -> u32;
2512}
2513extern "C" {
2514 pub fn Hacl_Frodo976_crypto_kem_dec(ss: *mut u8, ct: *mut u8, sk: *mut u8) -> u32;
2515}
2516pub type Hacl_GenericField64_pbn_mont_ctx_u64 = *mut Hacl_Bignum_MontArithmetic_bn_mont_ctx_u64;
2517extern "C" {
2518 #[doc = "A verified field arithmetic library."]
2519 #[doc = ""]
2520 #[doc = "This is a 64-bit optimized version, where bignums are represented as an array"]
2521 #[doc = "of `len` unsigned 64-bit integers, i.e. uint64_t[len]."]
2522 #[doc = ""]
2523 #[doc = "All the arithmetic operations are performed in the Montgomery domain."]
2524 #[doc = ""]
2525 #[doc = "All the functions below preserve the following invariant for a bignum `aM` in"]
2526 #[doc = "Montgomery form."]
2527 #[doc = "• aM < n"]
2528 pub fn Hacl_GenericField64_field_modulus_check(len: u32, n: *mut u64) -> bool;
2529}
2530extern "C" {
2531 pub fn Hacl_GenericField64_field_init(len: u32, n: *mut u64) -> *mut Hacl_Bignum_MontArithmetic_bn_mont_ctx_u64;
2532}
2533extern "C" {
2534 pub fn Hacl_GenericField64_field_free(k: *mut Hacl_Bignum_MontArithmetic_bn_mont_ctx_u64);
2535}
2536extern "C" {
2537 pub fn Hacl_GenericField64_field_get_len(k: *mut Hacl_Bignum_MontArithmetic_bn_mont_ctx_u64) -> u32;
2538}
2539extern "C" {
2540 pub fn Hacl_GenericField64_to_field(k: *mut Hacl_Bignum_MontArithmetic_bn_mont_ctx_u64, a: *mut u64, aM: *mut u64);
2541}
2542extern "C" {
2543 pub fn Hacl_GenericField64_from_field(
2544 k: *mut Hacl_Bignum_MontArithmetic_bn_mont_ctx_u64,
2545 aM: *mut u64,
2546 a: *mut u64,
2547 );
2548}
2549extern "C" {
2550 pub fn Hacl_GenericField64_add(
2551 k: *mut Hacl_Bignum_MontArithmetic_bn_mont_ctx_u64,
2552 aM: *mut u64,
2553 bM: *mut u64,
2554 cM: *mut u64,
2555 );
2556}
2557extern "C" {
2558 pub fn Hacl_GenericField64_sub(
2559 k: *mut Hacl_Bignum_MontArithmetic_bn_mont_ctx_u64,
2560 aM: *mut u64,
2561 bM: *mut u64,
2562 cM: *mut u64,
2563 );
2564}
2565extern "C" {
2566 pub fn Hacl_GenericField64_mul(
2567 k: *mut Hacl_Bignum_MontArithmetic_bn_mont_ctx_u64,
2568 aM: *mut u64,
2569 bM: *mut u64,
2570 cM: *mut u64,
2571 );
2572}
2573extern "C" {
2574 pub fn Hacl_GenericField64_sqr(k: *mut Hacl_Bignum_MontArithmetic_bn_mont_ctx_u64, aM: *mut u64, cM: *mut u64);
2575}
2576extern "C" {
2577 pub fn Hacl_GenericField64_one(k: *mut Hacl_Bignum_MontArithmetic_bn_mont_ctx_u64, oneM: *mut u64);
2578}
2579extern "C" {
2580 pub fn Hacl_GenericField64_exp_consttime(
2581 k: *mut Hacl_Bignum_MontArithmetic_bn_mont_ctx_u64,
2582 aM: *mut u64,
2583 bBits: u32,
2584 b: *mut u64,
2585 resM: *mut u64,
2586 );
2587}
2588extern "C" {
2589 pub fn Hacl_GenericField64_exp_vartime(
2590 k: *mut Hacl_Bignum_MontArithmetic_bn_mont_ctx_u64,
2591 aM: *mut u64,
2592 bBits: u32,
2593 b: *mut u64,
2594 resM: *mut u64,
2595 );
2596}
2597extern "C" {
2598 pub fn Hacl_GenericField64_inverse(
2599 k: *mut Hacl_Bignum_MontArithmetic_bn_mont_ctx_u64,
2600 aM: *mut u64,
2601 aInvM: *mut u64,
2602 );
2603}
2604pub type Hacl_Bignum32_pbn_mont_ctx_u32 = *mut Hacl_Bignum_MontArithmetic_bn_mont_ctx_u32;
2605extern "C" {
2606 pub fn Hacl_Bignum32_add(len: u32, a: *mut u32, b: *mut u32, res: *mut u32) -> u32;
2607}
2608extern "C" {
2609 pub fn Hacl_Bignum32_sub(len: u32, a: *mut u32, b: *mut u32, res: *mut u32) -> u32;
2610}
2611extern "C" {
2612 pub fn Hacl_Bignum32_add_mod(len: u32, n: *mut u32, a: *mut u32, b: *mut u32, res: *mut u32);
2613}
2614extern "C" {
2615 pub fn Hacl_Bignum32_sub_mod(len: u32, n: *mut u32, a: *mut u32, b: *mut u32, res: *mut u32);
2616}
2617extern "C" {
2618 pub fn Hacl_Bignum32_mul(len: u32, a: *mut u32, b: *mut u32, res: *mut u32);
2619}
2620extern "C" {
2621 pub fn Hacl_Bignum32_sqr(len: u32, a: *mut u32, res: *mut u32);
2622}
2623extern "C" {
2624 pub fn Hacl_Bignum32_mod(len: u32, n: *mut u32, a: *mut u32, res: *mut u32) -> bool;
2625}
2626extern "C" {
2627 pub fn Hacl_Bignum32_mod_exp_vartime(
2628 len: u32,
2629 n: *mut u32,
2630 a: *mut u32,
2631 bBits: u32,
2632 b: *mut u32,
2633 res: *mut u32,
2634 ) -> bool;
2635}
2636extern "C" {
2637 pub fn Hacl_Bignum32_mod_exp_consttime(
2638 len: u32,
2639 n: *mut u32,
2640 a: *mut u32,
2641 bBits: u32,
2642 b: *mut u32,
2643 res: *mut u32,
2644 ) -> bool;
2645}
2646extern "C" {
2647 pub fn Hacl_Bignum32_mod_inv_prime_vartime(len: u32, n: *mut u32, a: *mut u32, res: *mut u32) -> bool;
2648}
2649extern "C" {
2650 pub fn Hacl_Bignum32_mont_ctx_init(len: u32, n: *mut u32) -> *mut Hacl_Bignum_MontArithmetic_bn_mont_ctx_u32;
2651}
2652extern "C" {
2653 pub fn Hacl_Bignum32_mont_ctx_free(k: *mut Hacl_Bignum_MontArithmetic_bn_mont_ctx_u32);
2654}
2655extern "C" {
2656 pub fn Hacl_Bignum32_mod_precomp(k: *mut Hacl_Bignum_MontArithmetic_bn_mont_ctx_u32, a: *mut u32, res: *mut u32);
2657}
2658extern "C" {
2659 pub fn Hacl_Bignum32_mod_exp_vartime_precomp(
2660 k: *mut Hacl_Bignum_MontArithmetic_bn_mont_ctx_u32,
2661 a: *mut u32,
2662 bBits: u32,
2663 b: *mut u32,
2664 res: *mut u32,
2665 );
2666}
2667extern "C" {
2668 pub fn Hacl_Bignum32_mod_exp_consttime_precomp(
2669 k: *mut Hacl_Bignum_MontArithmetic_bn_mont_ctx_u32,
2670 a: *mut u32,
2671 bBits: u32,
2672 b: *mut u32,
2673 res: *mut u32,
2674 );
2675}
2676extern "C" {
2677 pub fn Hacl_Bignum32_mod_inv_prime_vartime_precomp(
2678 k: *mut Hacl_Bignum_MontArithmetic_bn_mont_ctx_u32,
2679 a: *mut u32,
2680 res: *mut u32,
2681 );
2682}
2683extern "C" {
2684 pub fn Hacl_Bignum32_new_bn_from_bytes_be(len: u32, b: *mut u8) -> *mut u32;
2685}
2686extern "C" {
2687 pub fn Hacl_Bignum32_new_bn_from_bytes_le(len: u32, b: *mut u8) -> *mut u32;
2688}
2689extern "C" {
2690 pub fn Hacl_Bignum32_bn_to_bytes_be(len: u32, b: *mut u32, res: *mut u8);
2691}
2692extern "C" {
2693 pub fn Hacl_Bignum32_bn_to_bytes_le(len: u32, b: *mut u32, res: *mut u8);
2694}
2695extern "C" {
2696 pub fn Hacl_Bignum32_lt_mask(len: u32, a: *mut u32, b: *mut u32) -> u32;
2697}
2698extern "C" {
2699 pub fn Hacl_Bignum32_eq_mask(len: u32, a: *mut u32, b: *mut u32) -> u32;
2700}
2701extern "C" {
2702 pub fn Hacl_P256_ecdsa_sign_p256_sha2(result: *mut u8, mLen: u32, m: *mut u8, privKey: *mut u8, k: *mut u8)
2703 -> bool;
2704}
2705extern "C" {
2706 pub fn Hacl_P256_ecdsa_sign_p256_sha384(
2707 result: *mut u8,
2708 mLen: u32,
2709 m: *mut u8,
2710 privKey: *mut u8,
2711 k: *mut u8,
2712 ) -> bool;
2713}
2714extern "C" {
2715 pub fn Hacl_P256_ecdsa_sign_p256_sha512(
2716 result: *mut u8,
2717 mLen: u32,
2718 m: *mut u8,
2719 privKey: *mut u8,
2720 k: *mut u8,
2721 ) -> bool;
2722}
2723extern "C" {
2724 pub fn Hacl_P256_ecdsa_sign_p256_without_hash(
2725 result: *mut u8,
2726 mLen: u32,
2727 m: *mut u8,
2728 privKey: *mut u8,
2729 k: *mut u8,
2730 ) -> bool;
2731}
2732extern "C" {
2733 pub fn Hacl_P256_ecdsa_verif_p256_sha2(mLen: u32, m: *mut u8, pubKey: *mut u8, r: *mut u8, s: *mut u8) -> bool;
2734}
2735extern "C" {
2736 pub fn Hacl_P256_ecdsa_verif_p256_sha384(mLen: u32, m: *mut u8, pubKey: *mut u8, r: *mut u8, s: *mut u8) -> bool;
2737}
2738extern "C" {
2739 pub fn Hacl_P256_ecdsa_verif_p256_sha512(mLen: u32, m: *mut u8, pubKey: *mut u8, r: *mut u8, s: *mut u8) -> bool;
2740}
2741extern "C" {
2742 pub fn Hacl_P256_ecdsa_verif_without_hash(mLen: u32, m: *mut u8, pubKey: *mut u8, r: *mut u8, s: *mut u8) -> bool;
2743}
2744extern "C" {
2745 pub fn Hacl_P256_verify_q(pubKey: *mut u8) -> bool;
2746}
2747extern "C" {
2748 pub fn Hacl_P256_decompression_not_compressed_form(b: *mut u8, result: *mut u8) -> bool;
2749}
2750extern "C" {
2751 pub fn Hacl_P256_decompression_compressed_form(b: *mut u8, result: *mut u8) -> bool;
2752}
2753extern "C" {
2754 pub fn Hacl_P256_compression_not_compressed_form(b: *mut u8, result: *mut u8);
2755}
2756extern "C" {
2757 pub fn Hacl_P256_compression_compressed_form(b: *mut u8, result: *mut u8);
2758}
2759extern "C" {
2760 pub fn Hacl_P256_ecp256dh_i(result: *mut u8, scalar: *mut u8) -> bool;
2761}
2762extern "C" {
2763 pub fn Hacl_P256_ecp256dh_r(result: *mut u8, pubKey: *mut u8, scalar: *mut u8) -> bool;
2764}
2765extern "C" {
2766 pub fn Hacl_P256_is_more_than_zero_less_than_order(x: *mut u8) -> bool;
2767}
2768extern "C" {
2769 pub fn Hacl_HPKE_Curve51_CP256_SHA256_setupBaseI(
2770 o_pkE: *mut u8,
2771 o_k: *mut u8,
2772 o_n: *mut u8,
2773 skE: *mut u8,
2774 pkR: *mut u8,
2775 infolen: u32,
2776 info: *mut u8,
2777 ) -> u32;
2778}
2779extern "C" {
2780 pub fn Hacl_HPKE_Curve51_CP256_SHA256_setupBaseR(
2781 o_key_aead: *mut u8,
2782 o_nonce_aead: *mut u8,
2783 pkE: *mut u8,
2784 skR: *mut u8,
2785 infolen: u32,
2786 info: *mut u8,
2787 ) -> u32;
2788}
2789extern "C" {
2790 pub fn Hacl_HPKE_Curve51_CP256_SHA256_sealBase(
2791 skE: *mut u8,
2792 pkR: *mut u8,
2793 mlen: u32,
2794 m: *mut u8,
2795 infolen: u32,
2796 info: *mut u8,
2797 output: *mut u8,
2798 ) -> u32;
2799}
2800extern "C" {
2801 pub fn Hacl_HPKE_Curve51_CP256_SHA256_openBase(
2802 pkE: *mut u8,
2803 skR: *mut u8,
2804 mlen: u32,
2805 m: *mut u8,
2806 infolen: u32,
2807 info: *mut u8,
2808 output: *mut u8,
2809 ) -> u32;
2810}
2811extern "C" {
2812 pub fn Hacl_Curve25519_64_Slow_scalarmult(out: *mut u8, priv_: *mut u8, pub_: *mut u8);
2813}
2814extern "C" {
2815 pub fn Hacl_Curve25519_64_Slow_secret_to_public(pub_: *mut u8, priv_: *mut u8);
2816}
2817extern "C" {
2818 pub fn Hacl_Curve25519_64_Slow_ecdh(out: *mut u8, priv_: *mut u8, pub_: *mut u8) -> bool;
2819}
2820extern "C" {
2821 pub static mut EverCrypt_StaticConfig_hacl: bool;
2822}
2823extern "C" {
2824 pub static mut EverCrypt_StaticConfig_vale: bool;
2825}
2826extern "C" {
2827 pub static mut EverCrypt_StaticConfig_openssl: bool;
2828}
2829extern "C" {
2830 pub static mut EverCrypt_StaticConfig_bcrypt: bool;
2831}
2832extern "C" {
2833 pub static mut Hacl_Frodo1344_crypto_bytes: u32;
2834}
2835extern "C" {
2836 pub static mut Hacl_Frodo1344_crypto_publickeybytes: u32;
2837}
2838extern "C" {
2839 pub static mut Hacl_Frodo1344_crypto_secretkeybytes: u32;
2840}
2841extern "C" {
2842 pub static mut Hacl_Frodo1344_crypto_ciphertextbytes: u32;
2843}
2844extern "C" {
2845 pub fn Hacl_Frodo1344_crypto_kem_keypair(pk: *mut u8, sk: *mut u8) -> u32;
2846}
2847extern "C" {
2848 pub fn Hacl_Frodo1344_crypto_kem_enc(ct: *mut u8, ss: *mut u8, pk: *mut u8) -> u32;
2849}
2850extern "C" {
2851 pub fn Hacl_Frodo1344_crypto_kem_dec(ss: *mut u8, ct: *mut u8, sk: *mut u8) -> u32;
2852}
2853#[repr(C)]
2854#[derive(Debug, Copy, Clone)]
2855pub struct Hacl_Streaming_Poly1305_256_poly1305_256_state_s {
2856 pub block_state: *mut *mut ::std::os::raw::c_void,
2857 pub buf: *mut u8,
2858 pub total_len: u64,
2859 pub p_key: *mut u8,
2860}
2861pub type Hacl_Streaming_Poly1305_256_poly1305_256_state = Hacl_Streaming_Poly1305_256_poly1305_256_state_s;
2862extern "C" {
2863 pub fn Hacl_Streaming_Poly1305_256_create_in(k: *mut u8) -> *mut Hacl_Streaming_Poly1305_256_poly1305_256_state;
2864}
2865extern "C" {
2866 pub fn Hacl_Streaming_Poly1305_256_init(k: *mut u8, s: *mut Hacl_Streaming_Poly1305_256_poly1305_256_state);
2867}
2868extern "C" {
2869 pub fn Hacl_Streaming_Poly1305_256_update(
2870 p: *mut Hacl_Streaming_Poly1305_256_poly1305_256_state,
2871 data: *mut u8,
2872 len: u32,
2873 );
2874}
2875extern "C" {
2876 pub fn Hacl_Streaming_Poly1305_256_finish(p: *mut Hacl_Streaming_Poly1305_256_poly1305_256_state, dst: *mut u8);
2877}
2878extern "C" {
2879 pub fn Hacl_Streaming_Poly1305_256_free(s: *mut Hacl_Streaming_Poly1305_256_poly1305_256_state);
2880}
2881extern "C" {
2882 pub fn Hacl_HPKE_P256_CP128_SHA256_setupBaseI(
2883 o_pkE: *mut u8,
2884 o_k: *mut u8,
2885 o_n: *mut u8,
2886 skE: *mut u8,
2887 pkR: *mut u8,
2888 infolen: u32,
2889 info: *mut u8,
2890 ) -> u32;
2891}
2892extern "C" {
2893 pub fn Hacl_HPKE_P256_CP128_SHA256_setupBaseR(
2894 o_key_aead: *mut u8,
2895 o_nonce_aead: *mut u8,
2896 pkE: *mut u8,
2897 skR: *mut u8,
2898 infolen: u32,
2899 info: *mut u8,
2900 ) -> u32;
2901}
2902extern "C" {
2903 pub fn Hacl_HPKE_P256_CP128_SHA256_sealBase(
2904 skE: *mut u8,
2905 pkR: *mut u8,
2906 mlen: u32,
2907 m: *mut u8,
2908 infolen: u32,
2909 info: *mut u8,
2910 output: *mut u8,
2911 ) -> u32;
2912}
2913extern "C" {
2914 pub fn Hacl_HPKE_P256_CP128_SHA256_openBase(
2915 pkE: *mut u8,
2916 skR: *mut u8,
2917 mlen: u32,
2918 m: *mut u8,
2919 infolen: u32,
2920 info: *mut u8,
2921 output: *mut u8,
2922 ) -> u32;
2923}
2924extern "C" {
2925 pub fn Hacl_HPKE_Curve51_CP128_SHA512_setupBaseI(
2926 o_pkE: *mut u8,
2927 o_k: *mut u8,
2928 o_n: *mut u8,
2929 skE: *mut u8,
2930 pkR: *mut u8,
2931 infolen: u32,
2932 info: *mut u8,
2933 ) -> u32;
2934}
2935extern "C" {
2936 pub fn Hacl_HPKE_Curve51_CP128_SHA512_setupBaseR(
2937 o_key_aead: *mut u8,
2938 o_nonce_aead: *mut u8,
2939 pkE: *mut u8,
2940 skR: *mut u8,
2941 infolen: u32,
2942 info: *mut u8,
2943 ) -> u32;
2944}
2945extern "C" {
2946 pub fn Hacl_HPKE_Curve51_CP128_SHA512_sealBase(
2947 skE: *mut u8,
2948 pkR: *mut u8,
2949 mlen: u32,
2950 m: *mut u8,
2951 infolen: u32,
2952 info: *mut u8,
2953 output: *mut u8,
2954 ) -> u32;
2955}
2956extern "C" {
2957 pub fn Hacl_HPKE_Curve51_CP128_SHA512_openBase(
2958 pkE: *mut u8,
2959 skR: *mut u8,
2960 mlen: u32,
2961 m: *mut u8,
2962 infolen: u32,
2963 info: *mut u8,
2964 output: *mut u8,
2965 ) -> u32;
2966}
2967extern "C" {
2968 pub fn Hacl_HKDF_Blake2b_256_expand_blake2b_256(
2969 okm: *mut u8,
2970 prk: *mut u8,
2971 prklen: u32,
2972 info: *mut u8,
2973 infolen: u32,
2974 len: u32,
2975 );
2976}
2977extern "C" {
2978 pub fn Hacl_HKDF_Blake2b_256_extract_blake2b_256(
2979 prk: *mut u8,
2980 salt: *mut u8,
2981 saltlen: u32,
2982 ikm: *mut u8,
2983 ikmlen: u32,
2984 );
2985}
2986extern "C" {
2987 pub fn Hacl_HPKE_Curve51_CP32_SHA512_setupBaseI(
2988 o_pkE: *mut u8,
2989 o_k: *mut u8,
2990 o_n: *mut u8,
2991 skE: *mut u8,
2992 pkR: *mut u8,
2993 infolen: u32,
2994 info: *mut u8,
2995 ) -> u32;
2996}
2997extern "C" {
2998 pub fn Hacl_HPKE_Curve51_CP32_SHA512_setupBaseR(
2999 o_key_aead: *mut u8,
3000 o_nonce_aead: *mut u8,
3001 pkE: *mut u8,
3002 skR: *mut u8,
3003 infolen: u32,
3004 info: *mut u8,
3005 ) -> u32;
3006}
3007extern "C" {
3008 pub fn Hacl_HPKE_Curve51_CP32_SHA512_sealBase(
3009 skE: *mut u8,
3010 pkR: *mut u8,
3011 mlen: u32,
3012 m: *mut u8,
3013 infolen: u32,
3014 info: *mut u8,
3015 output: *mut u8,
3016 ) -> u32;
3017}
3018extern "C" {
3019 pub fn Hacl_HPKE_Curve51_CP32_SHA512_openBase(
3020 pkE: *mut u8,
3021 skR: *mut u8,
3022 mlen: u32,
3023 m: *mut u8,
3024 infolen: u32,
3025 info: *mut u8,
3026 output: *mut u8,
3027 ) -> u32;
3028}
3029pub type EverCrypt_Error_error_code = u8;
3030extern "C" {
3031 pub fn EverCrypt_Error_uu___is_Success(projectee: EverCrypt_Error_error_code) -> bool;
3032}
3033extern "C" {
3034 pub fn EverCrypt_Error_uu___is_UnsupportedAlgorithm(projectee: EverCrypt_Error_error_code) -> bool;
3035}
3036extern "C" {
3037 pub fn EverCrypt_Error_uu___is_InvalidKey(projectee: EverCrypt_Error_error_code) -> bool;
3038}
3039extern "C" {
3040 pub fn EverCrypt_Error_uu___is_AuthenticationFailure(projectee: EverCrypt_Error_error_code) -> bool;
3041}
3042extern "C" {
3043 pub fn EverCrypt_Error_uu___is_InvalidIVLength(projectee: EverCrypt_Error_error_code) -> bool;
3044}
3045extern "C" {
3046 pub fn EverCrypt_Error_uu___is_DecodeError(projectee: EverCrypt_Error_error_code) -> bool;
3047}
3048#[repr(C)]
3049#[derive(Debug, Copy, Clone)]
3050pub struct EverCrypt_CTR_state_s_s {
3051 _unused: [u8; 0],
3052}
3053pub type EverCrypt_CTR_state_s = EverCrypt_CTR_state_s_s;
3054extern "C" {
3055 pub fn EverCrypt_CTR_uu___is_State(a: Spec_Agile_Cipher_cipher_alg, projectee: EverCrypt_CTR_state_s) -> bool;
3056}
3057pub type EverCrypt_CTR_uint8 = u8;
3058extern "C" {
3059 pub fn EverCrypt_CTR_xor8(a: u8, b: u8) -> u8;
3060}
3061pub type EverCrypt_CTR_e_alg = *mut ::std::os::raw::c_void;
3062extern "C" {
3063 pub fn EverCrypt_CTR_alg_of_state(s: *mut EverCrypt_CTR_state_s) -> Spec_Agile_Cipher_cipher_alg;
3064}
3065extern "C" {
3066 pub fn EverCrypt_CTR_create_in(
3067 a: Spec_Agile_Cipher_cipher_alg,
3068 dst: *mut *mut EverCrypt_CTR_state_s,
3069 k: *mut u8,
3070 iv: *mut u8,
3071 iv_len: u32,
3072 c: u32,
3073 ) -> EverCrypt_Error_error_code;
3074}
3075extern "C" {
3076 pub fn EverCrypt_CTR_init(p: *mut EverCrypt_CTR_state_s, k: *mut u8, iv: *mut u8, iv_len: u32, c: u32);
3077}
3078extern "C" {
3079 pub fn EverCrypt_CTR_update_block(p: *mut EverCrypt_CTR_state_s, dst: *mut u8, src: *mut u8);
3080}
3081extern "C" {
3082 pub fn EverCrypt_CTR_free(p: *mut EverCrypt_CTR_state_s);
3083}
3084pub type EverCrypt_Helpers_uint8_t = u8;
3085pub type EverCrypt_Helpers_uint16_t = u16;
3086pub type EverCrypt_Helpers_uint32_t = u32;
3087pub type EverCrypt_Helpers_uint64_t = u64;
3088pub type EverCrypt_Helpers_uint8_p = *mut u8;
3089pub type EverCrypt_Helpers_uint16_p = *mut u16;
3090pub type EverCrypt_Helpers_uint32_p = *mut u32;
3091pub type EverCrypt_Helpers_uint64_p = *mut u64;
3092extern "C" {
3093 pub fn Hacl_HPKE_Curve51_CP128_SHA256_setupBaseI(
3094 o_pkE: *mut u8,
3095 o_k: *mut u8,
3096 o_n: *mut u8,
3097 skE: *mut u8,
3098 pkR: *mut u8,
3099 infolen: u32,
3100 info: *mut u8,
3101 ) -> u32;
3102}
3103extern "C" {
3104 pub fn Hacl_HPKE_Curve51_CP128_SHA256_setupBaseR(
3105 o_key_aead: *mut u8,
3106 o_nonce_aead: *mut u8,
3107 pkE: *mut u8,
3108 skR: *mut u8,
3109 infolen: u32,
3110 info: *mut u8,
3111 ) -> u32;
3112}
3113extern "C" {
3114 pub fn Hacl_HPKE_Curve51_CP128_SHA256_sealBase(
3115 skE: *mut u8,
3116 pkR: *mut u8,
3117 mlen: u32,
3118 m: *mut u8,
3119 infolen: u32,
3120 info: *mut u8,
3121 output: *mut u8,
3122 ) -> u32;
3123}
3124extern "C" {
3125 pub fn Hacl_HPKE_Curve51_CP128_SHA256_openBase(
3126 pkE: *mut u8,
3127 skR: *mut u8,
3128 mlen: u32,
3129 m: *mut u8,
3130 infolen: u32,
3131 info: *mut u8,
3132 output: *mut u8,
3133 ) -> u32;
3134}
3135extern "C" {
3136 pub static mut Hacl_Frodo64_crypto_bytes: u32;
3137}
3138extern "C" {
3139 pub static mut Hacl_Frodo64_crypto_publickeybytes: u32;
3140}
3141extern "C" {
3142 pub static mut Hacl_Frodo64_crypto_secretkeybytes: u32;
3143}
3144extern "C" {
3145 pub static mut Hacl_Frodo64_crypto_ciphertextbytes: u32;
3146}
3147extern "C" {
3148 pub fn Hacl_Frodo64_crypto_kem_keypair(pk: *mut u8, sk: *mut u8) -> u32;
3149}
3150extern "C" {
3151 pub fn Hacl_Frodo64_crypto_kem_enc(ct: *mut u8, ss: *mut u8, pk: *mut u8) -> u32;
3152}
3153extern "C" {
3154 pub fn Hacl_Frodo64_crypto_kem_dec(ss: *mut u8, ct: *mut u8, sk: *mut u8) -> u32;
3155}
3156pub type EverCrypt_DRBG_supported_alg = Spec_Hash_Definitions_hash_alg;
3157extern "C" {
3158 pub static mut EverCrypt_DRBG_reseed_interval: u32;
3159}
3160extern "C" {
3161 pub static mut EverCrypt_DRBG_max_output_length: u32;
3162}
3163extern "C" {
3164 pub static mut EverCrypt_DRBG_max_length: u32;
3165}
3166extern "C" {
3167 pub static mut EverCrypt_DRBG_max_personalization_string_length: u32;
3168}
3169extern "C" {
3170 pub static mut EverCrypt_DRBG_max_additional_input_length: u32;
3171}
3172extern "C" {
3173 pub fn EverCrypt_DRBG_min_length(a: Spec_Hash_Definitions_hash_alg) -> u32;
3174}
3175pub type EverCrypt_DRBG_state_s_tags = u8;
3176#[repr(C)]
3177#[derive(Debug, Copy, Clone)]
3178pub struct EverCrypt_DRBG_state_s_s {
3179 _unused: [u8; 0],
3180}
3181pub type EverCrypt_DRBG_state_s = EverCrypt_DRBG_state_s_s;
3182extern "C" {
3183 pub fn EverCrypt_DRBG_uu___is_SHA1_s(
3184 uu___: Spec_Hash_Definitions_hash_alg,
3185 projectee: EverCrypt_DRBG_state_s,
3186 ) -> bool;
3187}
3188extern "C" {
3189 pub fn EverCrypt_DRBG_uu___is_SHA2_256_s(
3190 uu___: Spec_Hash_Definitions_hash_alg,
3191 projectee: EverCrypt_DRBG_state_s,
3192 ) -> bool;
3193}
3194extern "C" {
3195 pub fn EverCrypt_DRBG_uu___is_SHA2_384_s(
3196 uu___: Spec_Hash_Definitions_hash_alg,
3197 projectee: EverCrypt_DRBG_state_s,
3198 ) -> bool;
3199}
3200extern "C" {
3201 pub fn EverCrypt_DRBG_uu___is_SHA2_512_s(
3202 uu___: Spec_Hash_Definitions_hash_alg,
3203 projectee: EverCrypt_DRBG_state_s,
3204 ) -> bool;
3205}
3206extern "C" {
3207 pub fn EverCrypt_DRBG_create(a: Spec_Hash_Definitions_hash_alg) -> *mut EverCrypt_DRBG_state_s;
3208}
3209extern "C" {
3210 pub fn EverCrypt_DRBG_instantiate_sha1(
3211 st: *mut EverCrypt_DRBG_state_s,
3212 personalization_string: *mut u8,
3213 personalization_string_len: u32,
3214 ) -> bool;
3215}
3216extern "C" {
3217 pub fn EverCrypt_DRBG_instantiate_sha2_256(
3218 st: *mut EverCrypt_DRBG_state_s,
3219 personalization_string: *mut u8,
3220 personalization_string_len: u32,
3221 ) -> bool;
3222}
3223extern "C" {
3224 pub fn EverCrypt_DRBG_instantiate_sha2_384(
3225 st: *mut EverCrypt_DRBG_state_s,
3226 personalization_string: *mut u8,
3227 personalization_string_len: u32,
3228 ) -> bool;
3229}
3230extern "C" {
3231 pub fn EverCrypt_DRBG_instantiate_sha2_512(
3232 st: *mut EverCrypt_DRBG_state_s,
3233 personalization_string: *mut u8,
3234 personalization_string_len: u32,
3235 ) -> bool;
3236}
3237extern "C" {
3238 pub fn EverCrypt_DRBG_reseed_sha1(
3239 st: *mut EverCrypt_DRBG_state_s,
3240 additional_input: *mut u8,
3241 additional_input_len: u32,
3242 ) -> bool;
3243}
3244extern "C" {
3245 pub fn EverCrypt_DRBG_reseed_sha2_256(
3246 st: *mut EverCrypt_DRBG_state_s,
3247 additional_input: *mut u8,
3248 additional_input_len: u32,
3249 ) -> bool;
3250}
3251extern "C" {
3252 pub fn EverCrypt_DRBG_reseed_sha2_384(
3253 st: *mut EverCrypt_DRBG_state_s,
3254 additional_input: *mut u8,
3255 additional_input_len: u32,
3256 ) -> bool;
3257}
3258extern "C" {
3259 pub fn EverCrypt_DRBG_reseed_sha2_512(
3260 st: *mut EverCrypt_DRBG_state_s,
3261 additional_input: *mut u8,
3262 additional_input_len: u32,
3263 ) -> bool;
3264}
3265extern "C" {
3266 pub fn EverCrypt_DRBG_generate_sha1(
3267 output: *mut u8,
3268 st: *mut EverCrypt_DRBG_state_s,
3269 n: u32,
3270 additional_input: *mut u8,
3271 additional_input_len: u32,
3272 ) -> bool;
3273}
3274extern "C" {
3275 pub fn EverCrypt_DRBG_generate_sha2_256(
3276 output: *mut u8,
3277 st: *mut EverCrypt_DRBG_state_s,
3278 n: u32,
3279 additional_input: *mut u8,
3280 additional_input_len: u32,
3281 ) -> bool;
3282}
3283extern "C" {
3284 pub fn EverCrypt_DRBG_generate_sha2_384(
3285 output: *mut u8,
3286 st: *mut EverCrypt_DRBG_state_s,
3287 n: u32,
3288 additional_input: *mut u8,
3289 additional_input_len: u32,
3290 ) -> bool;
3291}
3292extern "C" {
3293 pub fn EverCrypt_DRBG_generate_sha2_512(
3294 output: *mut u8,
3295 st: *mut EverCrypt_DRBG_state_s,
3296 n: u32,
3297 additional_input: *mut u8,
3298 additional_input_len: u32,
3299 ) -> bool;
3300}
3301extern "C" {
3302 pub fn EverCrypt_DRBG_uninstantiate_sha1(st: *mut EverCrypt_DRBG_state_s);
3303}
3304extern "C" {
3305 pub fn EverCrypt_DRBG_uninstantiate_sha2_256(st: *mut EverCrypt_DRBG_state_s);
3306}
3307extern "C" {
3308 pub fn EverCrypt_DRBG_uninstantiate_sha2_384(st: *mut EverCrypt_DRBG_state_s);
3309}
3310extern "C" {
3311 pub fn EverCrypt_DRBG_uninstantiate_sha2_512(st: *mut EverCrypt_DRBG_state_s);
3312}
3313extern "C" {
3314 pub fn EverCrypt_DRBG_instantiate(
3315 st: *mut EverCrypt_DRBG_state_s,
3316 personalization_string: *mut u8,
3317 personalization_string_len: u32,
3318 ) -> bool;
3319}
3320extern "C" {
3321 pub fn EverCrypt_DRBG_reseed(
3322 st: *mut EverCrypt_DRBG_state_s,
3323 additional_input: *mut u8,
3324 additional_input_len: u32,
3325 ) -> bool;
3326}
3327extern "C" {
3328 pub fn EverCrypt_DRBG_generate(
3329 output: *mut u8,
3330 st: *mut EverCrypt_DRBG_state_s,
3331 n: u32,
3332 additional_input: *mut u8,
3333 additional_input_len: u32,
3334 ) -> bool;
3335}
3336extern "C" {
3337 pub fn EverCrypt_DRBG_uninstantiate(st: *mut EverCrypt_DRBG_state_s);
3338}
3339extern "C" {
3340 pub fn Hacl_NaCl_crypto_secretbox_detached(
3341 c: *mut u8,
3342 tag: *mut u8,
3343 m: *mut u8,
3344 mlen: u32,
3345 n: *mut u8,
3346 k: *mut u8,
3347 ) -> u32;
3348}
3349extern "C" {
3350 pub fn Hacl_NaCl_crypto_secretbox_open_detached(
3351 m: *mut u8,
3352 c: *mut u8,
3353 tag: *mut u8,
3354 mlen: u32,
3355 n: *mut u8,
3356 k: *mut u8,
3357 ) -> u32;
3358}
3359extern "C" {
3360 pub fn Hacl_NaCl_crypto_secretbox_easy(c: *mut u8, m: *mut u8, mlen: u32, n: *mut u8, k: *mut u8) -> u32;
3361}
3362extern "C" {
3363 pub fn Hacl_NaCl_crypto_secretbox_open_easy(m: *mut u8, c: *mut u8, clen: u32, n: *mut u8, k: *mut u8) -> u32;
3364}
3365extern "C" {
3366 pub fn Hacl_NaCl_crypto_box_beforenm(k: *mut u8, pk: *mut u8, sk: *mut u8) -> u32;
3367}
3368extern "C" {
3369 pub fn Hacl_NaCl_crypto_box_detached_afternm(
3370 c: *mut u8,
3371 tag: *mut u8,
3372 m: *mut u8,
3373 mlen: u32,
3374 n: *mut u8,
3375 k: *mut u8,
3376 ) -> u32;
3377}
3378extern "C" {
3379 pub fn Hacl_NaCl_crypto_box_detached(
3380 c: *mut u8,
3381 tag: *mut u8,
3382 m: *mut u8,
3383 mlen: u32,
3384 n: *mut u8,
3385 pk: *mut u8,
3386 sk: *mut u8,
3387 ) -> u32;
3388}
3389extern "C" {
3390 pub fn Hacl_NaCl_crypto_box_open_detached_afternm(
3391 m: *mut u8,
3392 c: *mut u8,
3393 tag: *mut u8,
3394 mlen: u32,
3395 n: *mut u8,
3396 k: *mut u8,
3397 ) -> u32;
3398}
3399extern "C" {
3400 pub fn Hacl_NaCl_crypto_box_open_detached(
3401 m: *mut u8,
3402 c: *mut u8,
3403 tag: *mut u8,
3404 mlen: u32,
3405 n: *mut u8,
3406 pk: *mut u8,
3407 sk: *mut u8,
3408 ) -> u32;
3409}
3410extern "C" {
3411 pub fn Hacl_NaCl_crypto_box_easy_afternm(c: *mut u8, m: *mut u8, mlen: u32, n: *mut u8, k: *mut u8) -> u32;
3412}
3413extern "C" {
3414 pub fn Hacl_NaCl_crypto_box_easy(c: *mut u8, m: *mut u8, mlen: u32, n: *mut u8, pk: *mut u8, sk: *mut u8) -> u32;
3415}
3416extern "C" {
3417 pub fn Hacl_NaCl_crypto_box_open_easy_afternm(m: *mut u8, c: *mut u8, clen: u32, n: *mut u8, k: *mut u8) -> u32;
3418}
3419extern "C" {
3420 pub fn Hacl_NaCl_crypto_box_open_easy(
3421 m: *mut u8,
3422 c: *mut u8,
3423 clen: u32,
3424 n: *mut u8,
3425 pk: *mut u8,
3426 sk: *mut u8,
3427 ) -> u32;
3428}
3429extern "C" {
3430 pub fn Hacl_AES128_aes128_key_expansion(key: *mut u8, expanded_key: *mut u8);
3431}
3432extern "C" {
3433 pub fn Hacl_AES128_aes128_encrypt_block(cipher: *mut u16, plain: *mut u16, expanded_key: *mut u8);
3434}
3435extern "C" {
3436 pub fn EverCrypt_Cipher_chacha20(len: u32, dst: *mut u8, src: *mut u8, key: *mut u8, iv: *mut u8, ctr: u32);
3437}
3438#[repr(C)]
3439#[derive(Debug, Copy, Clone)]
3440pub struct Hacl_Streaming_Poly1305_32_poly1305_32_state_s {
3441 pub block_state: *mut u64,
3442 pub buf: *mut u8,
3443 pub total_len: u64,
3444 pub p_key: *mut u8,
3445}
3446pub type Hacl_Streaming_Poly1305_32_poly1305_32_state = Hacl_Streaming_Poly1305_32_poly1305_32_state_s;
3447extern "C" {
3448 pub fn Hacl_Streaming_Poly1305_32_create_in(k: *mut u8) -> *mut Hacl_Streaming_Poly1305_32_poly1305_32_state;
3449}
3450extern "C" {
3451 pub fn Hacl_Streaming_Poly1305_32_init(k: *mut u8, s: *mut Hacl_Streaming_Poly1305_32_poly1305_32_state);
3452}
3453extern "C" {
3454 pub fn Hacl_Streaming_Poly1305_32_update(
3455 p: *mut Hacl_Streaming_Poly1305_32_poly1305_32_state,
3456 data: *mut u8,
3457 len: u32,
3458 );
3459}
3460extern "C" {
3461 pub fn Hacl_Streaming_Poly1305_32_finish(p: *mut Hacl_Streaming_Poly1305_32_poly1305_32_state, dst: *mut u8);
3462}
3463extern "C" {
3464 pub fn Hacl_Streaming_Poly1305_32_free(s: *mut Hacl_Streaming_Poly1305_32_poly1305_32_state);
3465}
3466extern "C" {
3467 pub fn Hacl_RSAPSS_rsapss_sign(
3468 a: Spec_Hash_Definitions_hash_alg,
3469 modBits: u32,
3470 eBits: u32,
3471 dBits: u32,
3472 skey: *mut u64,
3473 saltLen: u32,
3474 salt: *mut u8,
3475 msgLen: u32,
3476 msg: *mut u8,
3477 sgnt: *mut u8,
3478 ) -> bool;
3479}
3480extern "C" {
3481 pub fn Hacl_RSAPSS_rsapss_verify(
3482 a: Spec_Hash_Definitions_hash_alg,
3483 modBits: u32,
3484 eBits: u32,
3485 pkey: *mut u64,
3486 saltLen: u32,
3487 sgntLen: u32,
3488 sgnt: *mut u8,
3489 msgLen: u32,
3490 msg: *mut u8,
3491 ) -> bool;
3492}
3493extern "C" {
3494 pub fn Hacl_RSAPSS_new_rsapss_load_pkey(modBits: u32, eBits: u32, nb: *mut u8, eb: *mut u8) -> *mut u64;
3495}
3496extern "C" {
3497 pub fn Hacl_RSAPSS_new_rsapss_load_skey(
3498 modBits: u32,
3499 eBits: u32,
3500 dBits: u32,
3501 nb: *mut u8,
3502 eb: *mut u8,
3503 db: *mut u8,
3504 ) -> *mut u64;
3505}
3506extern "C" {
3507 pub fn Hacl_RSAPSS_rsapss_skey_sign(
3508 a: Spec_Hash_Definitions_hash_alg,
3509 modBits: u32,
3510 eBits: u32,
3511 dBits: u32,
3512 nb: *mut u8,
3513 eb: *mut u8,
3514 db: *mut u8,
3515 saltLen: u32,
3516 salt: *mut u8,
3517 msgLen: u32,
3518 msg: *mut u8,
3519 sgnt: *mut u8,
3520 ) -> bool;
3521}
3522extern "C" {
3523 pub fn Hacl_RSAPSS_rsapss_pkey_verify(
3524 a: Spec_Hash_Definitions_hash_alg,
3525 modBits: u32,
3526 eBits: u32,
3527 nb: *mut u8,
3528 eb: *mut u8,
3529 saltLen: u32,
3530 sgntLen: u32,
3531 sgnt: *mut u8,
3532 msgLen: u32,
3533 msg: *mut u8,
3534 ) -> bool;
3535}
3536extern "C" {
3537 pub fn Hacl_HPKE_Curve51_CP32_SHA256_setupBaseI(
3538 o_pkE: *mut u8,
3539 o_k: *mut u8,
3540 o_n: *mut u8,
3541 skE: *mut u8,
3542 pkR: *mut u8,
3543 infolen: u32,
3544 info: *mut u8,
3545 ) -> u32;
3546}
3547extern "C" {
3548 pub fn Hacl_HPKE_Curve51_CP32_SHA256_setupBaseR(
3549 o_key_aead: *mut u8,
3550 o_nonce_aead: *mut u8,
3551 pkE: *mut u8,
3552 skR: *mut u8,
3553 infolen: u32,
3554 info: *mut u8,
3555 ) -> u32;
3556}
3557extern "C" {
3558 pub fn Hacl_HPKE_Curve51_CP32_SHA256_sealBase(
3559 skE: *mut u8,
3560 pkR: *mut u8,
3561 mlen: u32,
3562 m: *mut u8,
3563 infolen: u32,
3564 info: *mut u8,
3565 output: *mut u8,
3566 ) -> u32;
3567}
3568extern "C" {
3569 pub fn Hacl_HPKE_Curve51_CP32_SHA256_openBase(
3570 pkE: *mut u8,
3571 skR: *mut u8,
3572 mlen: u32,
3573 m: *mut u8,
3574 infolen: u32,
3575 info: *mut u8,
3576 output: *mut u8,
3577 ) -> u32;
3578}
3579extern "C" {
3580 pub fn Hacl_HKDF_Blake2s_128_expand_blake2s_128(
3581 okm: *mut u8,
3582 prk: *mut u8,
3583 prklen: u32,
3584 info: *mut u8,
3585 infolen: u32,
3586 len: u32,
3587 );
3588}
3589extern "C" {
3590 pub fn Hacl_HKDF_Blake2s_128_extract_blake2s_128(
3591 prk: *mut u8,
3592 salt: *mut u8,
3593 saltlen: u32,
3594 ikm: *mut u8,
3595 ikmlen: u32,
3596 );
3597}
3598#[repr(C)]
3599#[derive(Debug, Copy, Clone)]
3600pub struct EverCrypt_AEAD_state_s_s {
3601 _unused: [u8; 0],
3602}
3603pub type EverCrypt_AEAD_state_s = EverCrypt_AEAD_state_s_s;
3604extern "C" {
3605 pub fn EverCrypt_AEAD_uu___is_Ek(a: Spec_Agile_AEAD_alg, projectee: EverCrypt_AEAD_state_s) -> bool;
3606}
3607extern "C" {
3608 pub fn EverCrypt_AEAD_alg_of_state(s: *mut EverCrypt_AEAD_state_s) -> Spec_Agile_AEAD_alg;
3609}
3610extern "C" {
3611 pub fn EverCrypt_AEAD_create_in(
3612 a: Spec_Agile_AEAD_alg,
3613 dst: *mut *mut EverCrypt_AEAD_state_s,
3614 k: *mut u8,
3615 ) -> EverCrypt_Error_error_code;
3616}
3617extern "C" {
3618 pub fn EverCrypt_AEAD_encrypt(
3619 s: *mut EverCrypt_AEAD_state_s,
3620 iv: *mut u8,
3621 iv_len: u32,
3622 ad: *mut u8,
3623 ad_len: u32,
3624 plain: *mut u8,
3625 plain_len: u32,
3626 cipher: *mut u8,
3627 tag: *mut u8,
3628 ) -> EverCrypt_Error_error_code;
3629}
3630extern "C" {
3631 pub fn EverCrypt_AEAD_encrypt_expand_aes128_gcm_no_check(
3632 k: *mut u8,
3633 iv: *mut u8,
3634 iv_len: u32,
3635 ad: *mut u8,
3636 ad_len: u32,
3637 plain: *mut u8,
3638 plain_len: u32,
3639 cipher: *mut u8,
3640 tag: *mut u8,
3641 ) -> EverCrypt_Error_error_code;
3642}
3643extern "C" {
3644 pub fn EverCrypt_AEAD_encrypt_expand_aes256_gcm_no_check(
3645 k: *mut u8,
3646 iv: *mut u8,
3647 iv_len: u32,
3648 ad: *mut u8,
3649 ad_len: u32,
3650 plain: *mut u8,
3651 plain_len: u32,
3652 cipher: *mut u8,
3653 tag: *mut u8,
3654 ) -> EverCrypt_Error_error_code;
3655}
3656extern "C" {
3657 pub fn EverCrypt_AEAD_encrypt_expand_aes128_gcm(
3658 k: *mut u8,
3659 iv: *mut u8,
3660 iv_len: u32,
3661 ad: *mut u8,
3662 ad_len: u32,
3663 plain: *mut u8,
3664 plain_len: u32,
3665 cipher: *mut u8,
3666 tag: *mut u8,
3667 ) -> EverCrypt_Error_error_code;
3668}
3669extern "C" {
3670 pub fn EverCrypt_AEAD_encrypt_expand_aes256_gcm(
3671 k: *mut u8,
3672 iv: *mut u8,
3673 iv_len: u32,
3674 ad: *mut u8,
3675 ad_len: u32,
3676 plain: *mut u8,
3677 plain_len: u32,
3678 cipher: *mut u8,
3679 tag: *mut u8,
3680 ) -> EverCrypt_Error_error_code;
3681}
3682extern "C" {
3683 pub fn EverCrypt_AEAD_encrypt_expand_chacha20_poly1305(
3684 k: *mut u8,
3685 iv: *mut u8,
3686 iv_len: u32,
3687 ad: *mut u8,
3688 ad_len: u32,
3689 plain: *mut u8,
3690 plain_len: u32,
3691 cipher: *mut u8,
3692 tag: *mut u8,
3693 ) -> EverCrypt_Error_error_code;
3694}
3695extern "C" {
3696 pub fn EverCrypt_AEAD_encrypt_expand(
3697 a: Spec_Agile_AEAD_alg,
3698 k: *mut u8,
3699 iv: *mut u8,
3700 iv_len: u32,
3701 ad: *mut u8,
3702 ad_len: u32,
3703 plain: *mut u8,
3704 plain_len: u32,
3705 cipher: *mut u8,
3706 tag: *mut u8,
3707 ) -> EverCrypt_Error_error_code;
3708}
3709extern "C" {
3710 pub fn EverCrypt_AEAD_decrypt(
3711 s: *mut EverCrypt_AEAD_state_s,
3712 iv: *mut u8,
3713 iv_len: u32,
3714 ad: *mut u8,
3715 ad_len: u32,
3716 cipher: *mut u8,
3717 cipher_len: u32,
3718 tag: *mut u8,
3719 dst: *mut u8,
3720 ) -> EverCrypt_Error_error_code;
3721}
3722extern "C" {
3723 pub fn EverCrypt_AEAD_decrypt_expand_aes128_gcm_no_check(
3724 k: *mut u8,
3725 iv: *mut u8,
3726 iv_len: u32,
3727 ad: *mut u8,
3728 ad_len: u32,
3729 cipher: *mut u8,
3730 cipher_len: u32,
3731 tag: *mut u8,
3732 dst: *mut u8,
3733 ) -> EverCrypt_Error_error_code;
3734}
3735extern "C" {
3736 pub fn EverCrypt_AEAD_decrypt_expand_aes256_gcm_no_check(
3737 k: *mut u8,
3738 iv: *mut u8,
3739 iv_len: u32,
3740 ad: *mut u8,
3741 ad_len: u32,
3742 cipher: *mut u8,
3743 cipher_len: u32,
3744 tag: *mut u8,
3745 dst: *mut u8,
3746 ) -> EverCrypt_Error_error_code;
3747}
3748extern "C" {
3749 pub fn EverCrypt_AEAD_decrypt_expand_aes128_gcm(
3750 k: *mut u8,
3751 iv: *mut u8,
3752 iv_len: u32,
3753 ad: *mut u8,
3754 ad_len: u32,
3755 cipher: *mut u8,
3756 cipher_len: u32,
3757 tag: *mut u8,
3758 dst: *mut u8,
3759 ) -> EverCrypt_Error_error_code;
3760}
3761extern "C" {
3762 pub fn EverCrypt_AEAD_decrypt_expand_aes256_gcm(
3763 k: *mut u8,
3764 iv: *mut u8,
3765 iv_len: u32,
3766 ad: *mut u8,
3767 ad_len: u32,
3768 cipher: *mut u8,
3769 cipher_len: u32,
3770 tag: *mut u8,
3771 dst: *mut u8,
3772 ) -> EverCrypt_Error_error_code;
3773}
3774extern "C" {
3775 pub fn EverCrypt_AEAD_decrypt_expand_chacha20_poly1305(
3776 k: *mut u8,
3777 iv: *mut u8,
3778 iv_len: u32,
3779 ad: *mut u8,
3780 ad_len: u32,
3781 cipher: *mut u8,
3782 cipher_len: u32,
3783 tag: *mut u8,
3784 dst: *mut u8,
3785 ) -> EverCrypt_Error_error_code;
3786}
3787extern "C" {
3788 pub fn EverCrypt_AEAD_decrypt_expand(
3789 a: Spec_Agile_AEAD_alg,
3790 k: *mut u8,
3791 iv: *mut u8,
3792 iv_len: u32,
3793 ad: *mut u8,
3794 ad_len: u32,
3795 cipher: *mut u8,
3796 cipher_len: u32,
3797 tag: *mut u8,
3798 dst: *mut u8,
3799 ) -> EverCrypt_Error_error_code;
3800}
3801extern "C" {
3802 pub fn EverCrypt_AEAD_free(s: *mut EverCrypt_AEAD_state_s);
3803}
3804extern "C" {
3805 pub fn Hacl_HPKE_P256_CP256_SHA256_setupBaseI(
3806 o_pkE: *mut u8,
3807 o_k: *mut u8,
3808 o_n: *mut u8,
3809 skE: *mut u8,
3810 pkR: *mut u8,
3811 infolen: u32,
3812 info: *mut u8,
3813 ) -> u32;
3814}
3815extern "C" {
3816 pub fn Hacl_HPKE_P256_CP256_SHA256_setupBaseR(
3817 o_key_aead: *mut u8,
3818 o_nonce_aead: *mut u8,
3819 pkE: *mut u8,
3820 skR: *mut u8,
3821 infolen: u32,
3822 info: *mut u8,
3823 ) -> u32;
3824}
3825extern "C" {
3826 pub fn Hacl_HPKE_P256_CP256_SHA256_sealBase(
3827 skE: *mut u8,
3828 pkR: *mut u8,
3829 mlen: u32,
3830 m: *mut u8,
3831 infolen: u32,
3832 info: *mut u8,
3833 output: *mut u8,
3834 ) -> u32;
3835}
3836extern "C" {
3837 pub fn Hacl_HPKE_P256_CP256_SHA256_openBase(
3838 pkE: *mut u8,
3839 skR: *mut u8,
3840 mlen: u32,
3841 m: *mut u8,
3842 infolen: u32,
3843 info: *mut u8,
3844 output: *mut u8,
3845 ) -> u32;
3846}
3847extern "C" {
3848 pub fn Hacl_Chacha20_Vec32_chacha20_encrypt_32(
3849 len: u32,
3850 out: *mut u8,
3851 text: *mut u8,
3852 key: *mut u8,
3853 n: *mut u8,
3854 ctr: u32,
3855 );
3856}
3857extern "C" {
3858 pub fn Hacl_Chacha20_Vec32_chacha20_decrypt_32(
3859 len: u32,
3860 out: *mut u8,
3861 cipher: *mut u8,
3862 key: *mut u8,
3863 n: *mut u8,
3864 ctr: u32,
3865 );
3866}
3867extern "C" {
3868 pub fn Hacl_SHA2_Vec256_sha224_8(
3869 dst0: *mut u8,
3870 dst1: *mut u8,
3871 dst2: *mut u8,
3872 dst3: *mut u8,
3873 dst4: *mut u8,
3874 dst5: *mut u8,
3875 dst6: *mut u8,
3876 dst7: *mut u8,
3877 input_len: u32,
3878 input0: *mut u8,
3879 input1: *mut u8,
3880 input2: *mut u8,
3881 input3: *mut u8,
3882 input4: *mut u8,
3883 input5: *mut u8,
3884 input6: *mut u8,
3885 input7: *mut u8,
3886 );
3887}
3888extern "C" {
3889 pub fn Hacl_SHA2_Vec256_sha256_8(
3890 dst0: *mut u8,
3891 dst1: *mut u8,
3892 dst2: *mut u8,
3893 dst3: *mut u8,
3894 dst4: *mut u8,
3895 dst5: *mut u8,
3896 dst6: *mut u8,
3897 dst7: *mut u8,
3898 input_len: u32,
3899 input0: *mut u8,
3900 input1: *mut u8,
3901 input2: *mut u8,
3902 input3: *mut u8,
3903 input4: *mut u8,
3904 input5: *mut u8,
3905 input6: *mut u8,
3906 input7: *mut u8,
3907 );
3908}
3909extern "C" {
3910 pub fn Hacl_SHA2_Vec256_sha384_4(
3911 dst0: *mut u8,
3912 dst1: *mut u8,
3913 dst2: *mut u8,
3914 dst3: *mut u8,
3915 input_len: u32,
3916 input0: *mut u8,
3917 input1: *mut u8,
3918 input2: *mut u8,
3919 input3: *mut u8,
3920 );
3921}
3922extern "C" {
3923 pub fn Hacl_SHA2_Vec256_sha512_4(
3924 dst0: *mut u8,
3925 dst1: *mut u8,
3926 dst2: *mut u8,
3927 dst3: *mut u8,
3928 input_len: u32,
3929 input0: *mut u8,
3930 input1: *mut u8,
3931 input2: *mut u8,
3932 input3: *mut u8,
3933 );
3934}
3935extern "C" {
3936 pub fn Hacl_SHA2_Scalar32_sha224(dst: *mut u8, input_len: u32, input: *mut u8);
3937}
3938extern "C" {
3939 pub fn Hacl_SHA2_Scalar32_sha256(dst: *mut u8, input_len: u32, input: *mut u8);
3940}
3941extern "C" {
3942 pub fn Hacl_SHA2_Scalar32_sha384(dst: *mut u8, input_len: u32, input: *mut u8);
3943}
3944extern "C" {
3945 pub fn Hacl_SHA2_Scalar32_sha512(dst: *mut u8, input_len: u32, input: *mut u8);
3946}