1pub const Spec_Hash_Definitions_SHA2_224: u32 = 0;
4pub const Spec_Hash_Definitions_SHA2_256: u32 = 1;
5pub const Spec_Hash_Definitions_SHA2_384: u32 = 2;
6pub const Spec_Hash_Definitions_SHA2_512: u32 = 3;
7pub const Spec_Hash_Definitions_SHA1: u32 = 4;
8pub const Spec_Hash_Definitions_MD5: u32 = 5;
9pub const Spec_Hash_Definitions_Blake2S: u32 = 6;
10pub const Spec_Hash_Definitions_Blake2B: u32 = 7;
11pub const Spec_Hash_Definitions_SHA3_256: u32 = 8;
12pub const Spec_Hash_Definitions_SHA3_224: u32 = 9;
13pub const Spec_Hash_Definitions_SHA3_384: u32 = 10;
14pub const Spec_Hash_Definitions_SHA3_512: u32 = 11;
15pub const Spec_Hash_Definitions_Shake128: u32 = 12;
16pub const Spec_Hash_Definitions_Shake256: u32 = 13;
17pub const Hacl_Streaming_Types_Success: u32 = 0;
18pub const Hacl_Streaming_Types_InvalidAlgorithm: u32 = 1;
19pub const Hacl_Streaming_Types_InvalidLength: u32 = 2;
20pub const Hacl_Streaming_Types_MaximumLengthExceeded: u32 = 3;
21pub const Spec_FFDHE_FFDHE2048: u32 = 0;
22pub const Spec_FFDHE_FFDHE3072: u32 = 1;
23pub const Spec_FFDHE_FFDHE4096: u32 = 2;
24pub const Spec_FFDHE_FFDHE6144: u32 = 3;
25pub const Spec_FFDHE_FFDHE8192: u32 = 4;
26pub const Spec_Agile_AEAD_AES128_GCM: u32 = 0;
27pub const Spec_Agile_AEAD_AES256_GCM: u32 = 1;
28pub const Spec_Agile_AEAD_CHACHA20_POLY1305: u32 = 2;
29pub const Spec_Agile_AEAD_AES128_CCM: u32 = 3;
30pub const Spec_Agile_AEAD_AES256_CCM: u32 = 4;
31pub const Spec_Agile_AEAD_AES128_CCM8: u32 = 5;
32pub const Spec_Agile_AEAD_AES256_CCM8: u32 = 6;
33extern "C" {
34 #[doc = "Compute the scalar multiple of a point.\n\n@param out Pointer to 32 bytes of memory, allocated by the caller, where the resulting point is written to.\n@param priv Pointer to 32 bytes of memory where the secret/private key is read from.\n@param pub Pointer to 32 bytes of memory where the public point is read from."]
35 pub fn Hacl_Curve25519_64_scalarmult(out: *mut u8, priv_: *mut u8, pub_: *mut u8);
36}
37extern "C" {
38 #[doc = "Calculate a public point from a secret/private key.\n\nThis computes a scalar multiplication of the secret/private key with the curve's basepoint.\n\n@param pub Pointer to 32 bytes of memory, allocated by the caller, where the resulting point is written to.\n@param priv Pointer to 32 bytes of memory where the secret/private key is read from."]
39 pub fn Hacl_Curve25519_64_secret_to_public(pub_: *mut u8, priv_: *mut u8);
40}
41extern "C" {
42 #[doc = "Execute the diffie-hellmann key exchange.\n\n@param out Pointer to 32 bytes of memory, allocated by the caller, where the resulting point is written to.\n@param priv Pointer to 32 bytes of memory where **our** secret/private key is read from.\n@param pub Pointer to 32 bytes of memory where **their** public point is read from."]
43 pub fn Hacl_Curve25519_64_ecdh(out: *mut u8, priv_: *mut u8, pub_: *mut u8) -> bool;
44}
45extern "C" {
46 #[doc = "Encrypt a message `input` with key `key`.\n\nThe arguments `key`, `nonce`, `data`, and `data_len` are same in encryption/decryption.\nNote: Encryption and decryption can be executed in-place, i.e., `input` and `output` can point to the same memory.\n\n@param output Pointer to `input_len` bytes of memory where the ciphertext is written to.\n@param tag Pointer to 16 bytes of memory where the mac is written to.\n@param input Pointer to `input_len` bytes of memory where the message is read from.\n@param input_len Length of the message.\n@param data Pointer to `data_len` bytes of memory where the associated data is read from.\n@param data_len Length of the associated data.\n@param key Pointer to 32 bytes of memory where the AEAD key is read from.\n@param nonce Pointer to 12 bytes of memory where the AEAD nonce is read from."]
47 pub fn Hacl_AEAD_Chacha20Poly1305_encrypt(
48 output: *mut u8,
49 tag: *mut u8,
50 input: *mut u8,
51 input_len: u32,
52 data: *mut u8,
53 data_len: u32,
54 key: *mut u8,
55 nonce: *mut u8,
56 );
57}
58extern "C" {
59 #[doc = "Decrypt a ciphertext `input` with key `key`.\n\nThe arguments `key`, `nonce`, `data`, and `data_len` are same in encryption/decryption.\nNote: Encryption and decryption can be executed in-place, i.e., `output` and `input` can point to the same memory.\n\nIf decryption succeeds, the resulting plaintext is stored in `output` and the function returns the success code 0.\nIf decryption fails, the array `output` remains unchanged and the function returns the error code 1.\n\n@param output Pointer to `input_len` bytes of memory where the message is written to.\n@param input Pointer to `input_len` bytes of memory where the ciphertext is read from.\n@param input_len Length of the ciphertext.\n@param data Pointer to `data_len` bytes of memory where the associated data is read from.\n@param data_len Length of the associated data.\n@param key Pointer to 32 bytes of memory where the AEAD key is read from.\n@param nonce Pointer to 12 bytes of memory where the AEAD nonce is read from.\n@param tag Pointer to 16 bytes of memory where the mac is read from.\n\n@returns 0 on succeess; 1 on failure."]
60 pub fn Hacl_AEAD_Chacha20Poly1305_decrypt(
61 output: *mut u8,
62 input: *mut u8,
63 input_len: u32,
64 data: *mut u8,
65 data_len: u32,
66 key: *mut u8,
67 nonce: *mut u8,
68 tag: *mut u8,
69 ) -> u32;
70}
71extern "C" {
72 #[doc = "Compute the scalar multiple of a point.\n\n@param out Pointer to 32 bytes of memory, allocated by the caller, where the resulting point is written to.\n@param priv Pointer to 32 bytes of memory where the secret/private key is read from.\n@param pub Pointer to 32 bytes of memory where the public point is read from."]
73 pub fn Hacl_Curve25519_51_scalarmult(out: *mut u8, priv_: *mut u8, pub_: *mut u8);
74}
75extern "C" {
76 #[doc = "Calculate a public point from a secret/private key.\n\nThis computes a scalar multiplication of the secret/private key with the curve's basepoint.\n\n@param pub Pointer to 32 bytes of memory, allocated by the caller, where the resulting point is written to.\n@param priv Pointer to 32 bytes of memory where the secret/private key is read from."]
77 pub fn Hacl_Curve25519_51_secret_to_public(pub_: *mut u8, priv_: *mut u8);
78}
79extern "C" {
80 #[doc = "Execute the diffie-hellmann key exchange.\n\n@param out Pointer to 32 bytes of memory, allocated by the caller, where the resulting point is written to.\n@param priv Pointer to 32 bytes of memory where **our** secret/private key is read from.\n@param pub Pointer to 32 bytes of memory where **their** public point is read from."]
81 pub fn Hacl_Curve25519_51_ecdh(out: *mut u8, priv_: *mut u8, pub_: *mut u8) -> bool;
82}
83pub type Spec_Hash_Definitions_hash_alg = u8;
84pub type Hacl_Streaming_Types_error_code = u8;
85#[repr(C)]
86#[derive(Debug, Copy, Clone)]
87pub struct Hacl_Streaming_MD_state_32_s {
88 pub block_state: *mut u32,
89 pub buf: *mut u8,
90 pub total_len: u64,
91}
92pub type Hacl_Streaming_MD_state_32 = Hacl_Streaming_MD_state_32_s;
93#[repr(C)]
94#[derive(Debug, Copy, Clone)]
95pub struct Hacl_Streaming_MD_state_64_s {
96 pub block_state: *mut u64,
97 pub buf: *mut u8,
98 pub total_len: u64,
99}
100pub type Hacl_Streaming_MD_state_64 = Hacl_Streaming_MD_state_64_s;
101pub type Hacl_Hash_SHA1_state_t = Hacl_Streaming_MD_state_32;
102extern "C" {
103 pub fn Hacl_Hash_SHA1_malloc() -> *mut Hacl_Streaming_MD_state_32;
104}
105extern "C" {
106 pub fn Hacl_Hash_SHA1_reset(state: *mut Hacl_Streaming_MD_state_32);
107}
108extern "C" {
109 #[doc = "0 = success, 1 = max length exceeded"]
110 pub fn Hacl_Hash_SHA1_update(
111 state: *mut Hacl_Streaming_MD_state_32,
112 chunk: *mut u8,
113 chunk_len: u32,
114 ) -> Hacl_Streaming_Types_error_code;
115}
116extern "C" {
117 pub fn Hacl_Hash_SHA1_digest(state: *mut Hacl_Streaming_MD_state_32, output: *mut u8);
118}
119extern "C" {
120 pub fn Hacl_Hash_SHA1_free(state: *mut Hacl_Streaming_MD_state_32);
121}
122extern "C" {
123 pub fn Hacl_Hash_SHA1_copy(
124 state: *mut Hacl_Streaming_MD_state_32,
125 ) -> *mut Hacl_Streaming_MD_state_32;
126}
127extern "C" {
128 pub fn Hacl_Hash_SHA1_hash(output: *mut u8, input: *mut u8, input_len: u32);
129}
130pub type Hacl_Hash_SHA2_state_t_224 = Hacl_Streaming_MD_state_32;
131pub type Hacl_Hash_SHA2_state_t_256 = Hacl_Streaming_MD_state_32;
132pub type Hacl_Hash_SHA2_state_t_384 = Hacl_Streaming_MD_state_64;
133pub type Hacl_Hash_SHA2_state_t_512 = Hacl_Streaming_MD_state_64;
134extern "C" {
135 #[doc = "Allocate initial state for the SHA2_256 hash. The state is to be freed by\ncalling `free_256`."]
136 pub fn Hacl_Hash_SHA2_malloc_256() -> *mut Hacl_Streaming_MD_state_32;
137}
138extern "C" {
139 #[doc = "Copies the state passed as argument into a newly allocated state (deep copy).\nThe state is to be freed by calling `free_256`. Cloning the state this way is\nuseful, for instance, if your control-flow diverges and you need to feed\nmore (different) data into the hash in each branch."]
140 pub fn Hacl_Hash_SHA2_copy_256(
141 state: *mut Hacl_Streaming_MD_state_32,
142 ) -> *mut Hacl_Streaming_MD_state_32;
143}
144extern "C" {
145 #[doc = "Reset an existing state to the initial hash state with empty data."]
146 pub fn Hacl_Hash_SHA2_reset_256(state: *mut Hacl_Streaming_MD_state_32);
147}
148extern "C" {
149 #[doc = "Feed an arbitrary amount of data into the hash. This function returns 0 for\nsuccess, or 1 if the combined length of all of the data passed to `update_256`\n(since the last call to `reset_256`) exceeds 2^61-1 bytes.\n\nThis function is identical to the update function for SHA2_224."]
150 pub fn Hacl_Hash_SHA2_update_256(
151 state: *mut Hacl_Streaming_MD_state_32,
152 input: *mut u8,
153 input_len: u32,
154 ) -> Hacl_Streaming_Types_error_code;
155}
156extern "C" {
157 #[doc = "Write the resulting hash into `output`, an array of 32 bytes. The state remains\nvalid after a call to `digest_256`, meaning the user may feed more data into\nthe hash via `update_256`. (The digest_256 function operates on an internal copy of\nthe state and therefore does not invalidate the client-held state `p`.)"]
158 pub fn Hacl_Hash_SHA2_digest_256(state: *mut Hacl_Streaming_MD_state_32, output: *mut u8);
159}
160extern "C" {
161 #[doc = "Free a state allocated with `malloc_256`.\n\nThis function is identical to the free function for SHA2_224."]
162 pub fn Hacl_Hash_SHA2_free_256(state: *mut Hacl_Streaming_MD_state_32);
163}
164extern "C" {
165 #[doc = "Hash `input`, of len `input_len`, into `output`, an array of 32 bytes."]
166 pub fn Hacl_Hash_SHA2_hash_256(output: *mut u8, input: *mut u8, input_len: u32);
167}
168extern "C" {
169 pub fn Hacl_Hash_SHA2_malloc_224() -> *mut Hacl_Streaming_MD_state_32;
170}
171extern "C" {
172 pub fn Hacl_Hash_SHA2_reset_224(state: *mut Hacl_Streaming_MD_state_32);
173}
174extern "C" {
175 pub fn Hacl_Hash_SHA2_update_224(
176 state: *mut Hacl_Streaming_MD_state_32,
177 input: *mut u8,
178 input_len: u32,
179 ) -> Hacl_Streaming_Types_error_code;
180}
181extern "C" {
182 #[doc = "Write the resulting hash into `output`, an array of 28 bytes. The state remains\nvalid after a call to `digest_224`, meaning the user may feed more data into\nthe hash via `update_224`."]
183 pub fn Hacl_Hash_SHA2_digest_224(state: *mut Hacl_Streaming_MD_state_32, output: *mut u8);
184}
185extern "C" {
186 pub fn Hacl_Hash_SHA2_free_224(state: *mut Hacl_Streaming_MD_state_32);
187}
188extern "C" {
189 #[doc = "Hash `input`, of len `input_len`, into `output`, an array of 28 bytes."]
190 pub fn Hacl_Hash_SHA2_hash_224(output: *mut u8, input: *mut u8, input_len: u32);
191}
192extern "C" {
193 pub fn Hacl_Hash_SHA2_malloc_512() -> *mut Hacl_Streaming_MD_state_64;
194}
195extern "C" {
196 #[doc = "Copies the state passed as argument into a newly allocated state (deep copy).\nThe state is to be freed by calling `free_512`. Cloning the state this way is\nuseful, for instance, if your control-flow diverges and you need to feed\nmore (different) data into the hash in each branch."]
197 pub fn Hacl_Hash_SHA2_copy_512(
198 state: *mut Hacl_Streaming_MD_state_64,
199 ) -> *mut Hacl_Streaming_MD_state_64;
200}
201extern "C" {
202 pub fn Hacl_Hash_SHA2_reset_512(state: *mut Hacl_Streaming_MD_state_64);
203}
204extern "C" {
205 #[doc = "Feed an arbitrary amount of data into the hash. This function returns 0 for\nsuccess, or 1 if the combined length of all of the data passed to `update_512`\n(since the last call to `reset_512`) exceeds 2^125-1 bytes.\n\nThis function is identical to the update function for SHA2_384."]
206 pub fn Hacl_Hash_SHA2_update_512(
207 state: *mut Hacl_Streaming_MD_state_64,
208 input: *mut u8,
209 input_len: u32,
210 ) -> Hacl_Streaming_Types_error_code;
211}
212extern "C" {
213 #[doc = "Write the resulting hash into `output`, an array of 64 bytes. The state remains\nvalid after a call to `digest_512`, meaning the user may feed more data into\nthe hash via `update_512`. (The digest_512 function operates on an internal copy of\nthe state and therefore does not invalidate the client-held state `p`.)"]
214 pub fn Hacl_Hash_SHA2_digest_512(state: *mut Hacl_Streaming_MD_state_64, output: *mut u8);
215}
216extern "C" {
217 #[doc = "Free a state allocated with `malloc_512`.\n\nThis function is identical to the free function for SHA2_384."]
218 pub fn Hacl_Hash_SHA2_free_512(state: *mut Hacl_Streaming_MD_state_64);
219}
220extern "C" {
221 #[doc = "Hash `input`, of len `input_len`, into `output`, an array of 64 bytes."]
222 pub fn Hacl_Hash_SHA2_hash_512(output: *mut u8, input: *mut u8, input_len: u32);
223}
224extern "C" {
225 pub fn Hacl_Hash_SHA2_malloc_384() -> *mut Hacl_Streaming_MD_state_64;
226}
227extern "C" {
228 pub fn Hacl_Hash_SHA2_reset_384(state: *mut Hacl_Streaming_MD_state_64);
229}
230extern "C" {
231 pub fn Hacl_Hash_SHA2_update_384(
232 state: *mut Hacl_Streaming_MD_state_64,
233 input: *mut u8,
234 input_len: u32,
235 ) -> Hacl_Streaming_Types_error_code;
236}
237extern "C" {
238 #[doc = "Write the resulting hash into `output`, an array of 48 bytes. The state remains\nvalid after a call to `digest_384`, meaning the user may feed more data into\nthe hash via `update_384`."]
239 pub fn Hacl_Hash_SHA2_digest_384(state: *mut Hacl_Streaming_MD_state_64, output: *mut u8);
240}
241extern "C" {
242 pub fn Hacl_Hash_SHA2_free_384(state: *mut Hacl_Streaming_MD_state_64);
243}
244extern "C" {
245 #[doc = "Hash `input`, of len `input_len`, into `output`, an array of 48 bytes."]
246 pub fn Hacl_Hash_SHA2_hash_384(output: *mut u8, input: *mut u8, input_len: u32);
247}
248#[repr(C)]
249#[derive(Debug, Copy, Clone)]
250pub struct Hacl_Hash_SHA3_hash_buf_s {
251 pub fst: Spec_Hash_Definitions_hash_alg,
252 pub snd: *mut u64,
253}
254pub type Hacl_Hash_SHA3_hash_buf = Hacl_Hash_SHA3_hash_buf_s;
255#[repr(C)]
256#[derive(Debug, Copy, Clone)]
257pub struct Hacl_Hash_SHA3_state_t_s {
258 pub block_state: Hacl_Hash_SHA3_hash_buf,
259 pub buf: *mut u8,
260 pub total_len: u64,
261}
262pub type Hacl_Hash_SHA3_state_t = Hacl_Hash_SHA3_state_t_s;
263extern "C" {
264 pub fn Hacl_Hash_SHA3_get_alg(s: *mut Hacl_Hash_SHA3_state_t)
265 -> Spec_Hash_Definitions_hash_alg;
266}
267extern "C" {
268 pub fn Hacl_Hash_SHA3_malloc(a: Spec_Hash_Definitions_hash_alg) -> *mut Hacl_Hash_SHA3_state_t;
269}
270extern "C" {
271 pub fn Hacl_Hash_SHA3_free(state: *mut Hacl_Hash_SHA3_state_t);
272}
273extern "C" {
274 pub fn Hacl_Hash_SHA3_copy(state: *mut Hacl_Hash_SHA3_state_t) -> *mut Hacl_Hash_SHA3_state_t;
275}
276extern "C" {
277 pub fn Hacl_Hash_SHA3_reset(state: *mut Hacl_Hash_SHA3_state_t);
278}
279extern "C" {
280 pub fn Hacl_Hash_SHA3_update(
281 state: *mut Hacl_Hash_SHA3_state_t,
282 chunk: *mut u8,
283 chunk_len: u32,
284 ) -> Hacl_Streaming_Types_error_code;
285}
286extern "C" {
287 pub fn Hacl_Hash_SHA3_digest(
288 state: *mut Hacl_Hash_SHA3_state_t,
289 output: *mut u8,
290 ) -> Hacl_Streaming_Types_error_code;
291}
292extern "C" {
293 pub fn Hacl_Hash_SHA3_squeeze(
294 s: *mut Hacl_Hash_SHA3_state_t,
295 dst: *mut u8,
296 l: u32,
297 ) -> Hacl_Streaming_Types_error_code;
298}
299extern "C" {
300 pub fn Hacl_Hash_SHA3_block_len(s: *mut Hacl_Hash_SHA3_state_t) -> u32;
301}
302extern "C" {
303 pub fn Hacl_Hash_SHA3_hash_len(s: *mut Hacl_Hash_SHA3_state_t) -> u32;
304}
305extern "C" {
306 pub fn Hacl_Hash_SHA3_is_shake(s: *mut Hacl_Hash_SHA3_state_t) -> bool;
307}
308extern "C" {
309 pub fn Hacl_Hash_SHA3_shake128_hacl(
310 inputByteLen: u32,
311 input: *mut u8,
312 outputByteLen: u32,
313 output: *mut u8,
314 );
315}
316extern "C" {
317 pub fn Hacl_Hash_SHA3_shake256_hacl(
318 inputByteLen: u32,
319 input: *mut u8,
320 outputByteLen: u32,
321 output: *mut u8,
322 );
323}
324extern "C" {
325 pub fn Hacl_Hash_SHA3_sha3_224(output: *mut u8, input: *mut u8, input_len: u32);
326}
327extern "C" {
328 pub fn Hacl_Hash_SHA3_sha3_256(output: *mut u8, input: *mut u8, input_len: u32);
329}
330extern "C" {
331 pub fn Hacl_Hash_SHA3_sha3_384(output: *mut u8, input: *mut u8, input_len: u32);
332}
333extern "C" {
334 pub fn Hacl_Hash_SHA3_sha3_512(output: *mut u8, input: *mut u8, input_len: u32);
335}
336extern "C" {
337 pub fn Hacl_Hash_SHA3_absorb_inner(rateInBytes: u32, block: *mut u8, s: *mut u64);
338}
339extern "C" {
340 pub fn Hacl_Hash_SHA3_squeeze0(
341 s: *mut u64,
342 rateInBytes: u32,
343 outputByteLen: u32,
344 output: *mut u8,
345 );
346}
347extern "C" {
348 pub fn Hacl_Hash_SHA3_keccak(
349 rate: u32,
350 capacity: u32,
351 inputByteLen: u32,
352 input: *mut u8,
353 delimitedSuffix: u8,
354 outputByteLen: u32,
355 output: *mut u8,
356 );
357}
358#[repr(C)]
359#[derive(Debug, Copy, Clone)]
360pub struct Hacl_Hash_Blake2b_block_state_t_s {
361 pub fst: *mut u64,
362 pub snd: *mut u64,
363}
364pub type Hacl_Hash_Blake2b_block_state_t = Hacl_Hash_Blake2b_block_state_t_s;
365#[repr(C)]
366#[derive(Debug, Copy, Clone)]
367pub struct Hacl_Hash_Blake2b_state_t_s {
368 pub block_state: Hacl_Hash_Blake2b_block_state_t,
369 pub buf: *mut u8,
370 pub total_len: u64,
371}
372pub type Hacl_Hash_Blake2b_state_t = Hacl_Hash_Blake2b_state_t_s;
373extern "C" {
374 #[doc = "State allocation function when there is no key"]
375 pub fn Hacl_Hash_Blake2b_malloc() -> *mut Hacl_Hash_Blake2b_state_t;
376}
377extern "C" {
378 #[doc = "Re-initialization function when there is no key"]
379 pub fn Hacl_Hash_Blake2b_reset(state: *mut Hacl_Hash_Blake2b_state_t);
380}
381extern "C" {
382 #[doc = "Update function when there is no key; 0 = success, 1 = max length exceeded"]
383 pub fn Hacl_Hash_Blake2b_update(
384 state: *mut Hacl_Hash_Blake2b_state_t,
385 chunk: *mut u8,
386 chunk_len: u32,
387 ) -> Hacl_Streaming_Types_error_code;
388}
389extern "C" {
390 #[doc = "Finish function when there is no key"]
391 pub fn Hacl_Hash_Blake2b_digest(state: *mut Hacl_Hash_Blake2b_state_t, output: *mut u8);
392}
393extern "C" {
394 #[doc = "Free state function when there is no key"]
395 pub fn Hacl_Hash_Blake2b_free(state: *mut Hacl_Hash_Blake2b_state_t);
396}
397extern "C" {
398 #[doc = "Write the BLAKE2b digest of message `input` using key `key` into `output`.\n\n@param output Pointer to `output_len` bytes of memory where the digest is written to.\n@param output_len Length of the to-be-generated digest with 1 <= `output_len` <= 64.\n@param input Pointer to `input_len` bytes of memory where the input message is read from.\n@param input_len Length of the input message.\n@param key Pointer to `key_len` bytes of memory where the key is read from.\n@param key_len Length of the key. Can be 0."]
399 pub fn Hacl_Hash_Blake2b_hash_with_key(
400 output: *mut u8,
401 output_len: u32,
402 input: *mut u8,
403 input_len: u32,
404 key: *mut u8,
405 key_len: u32,
406 );
407}
408#[repr(C)]
409#[derive(Debug, Copy, Clone)]
410pub struct Hacl_Hash_Blake2s_block_state_t_s {
411 pub fst: *mut u32,
412 pub snd: *mut u32,
413}
414pub type Hacl_Hash_Blake2s_block_state_t = Hacl_Hash_Blake2s_block_state_t_s;
415#[repr(C)]
416#[derive(Debug, Copy, Clone)]
417pub struct Hacl_Hash_Blake2s_state_t_s {
418 pub block_state: Hacl_Hash_Blake2s_block_state_t,
419 pub buf: *mut u8,
420 pub total_len: u64,
421}
422pub type Hacl_Hash_Blake2s_state_t = Hacl_Hash_Blake2s_state_t_s;
423extern "C" {
424 #[doc = "State allocation function when there is no key"]
425 pub fn Hacl_Hash_Blake2s_malloc() -> *mut Hacl_Hash_Blake2s_state_t;
426}
427extern "C" {
428 #[doc = "Re-initialization function when there is no key"]
429 pub fn Hacl_Hash_Blake2s_reset(state: *mut Hacl_Hash_Blake2s_state_t);
430}
431extern "C" {
432 #[doc = "Update function when there is no key; 0 = success, 1 = max length exceeded"]
433 pub fn Hacl_Hash_Blake2s_update(
434 state: *mut Hacl_Hash_Blake2s_state_t,
435 chunk: *mut u8,
436 chunk_len: u32,
437 ) -> Hacl_Streaming_Types_error_code;
438}
439extern "C" {
440 #[doc = "Finish function when there is no key"]
441 pub fn Hacl_Hash_Blake2s_digest(state: *mut Hacl_Hash_Blake2s_state_t, output: *mut u8);
442}
443extern "C" {
444 #[doc = "Free state function when there is no key"]
445 pub fn Hacl_Hash_Blake2s_free(state: *mut Hacl_Hash_Blake2s_state_t);
446}
447extern "C" {
448 #[doc = "Write the BLAKE2s digest of message `input` using key `key` into `output`.\n\n@param output Pointer to `output_len` bytes of memory where the digest is written to.\n@param output_len Length of the to-be-generated digest with 1 <= `output_len` <= 32.\n@param input Pointer to `input_len` bytes of memory where the input message is read from.\n@param input_len Length of the input message.\n@param key Pointer to `key_len` bytes of memory where the key is read from.\n@param key_len Length of the key. Can be 0."]
449 pub fn Hacl_Hash_Blake2s_hash_with_key(
450 output: *mut u8,
451 output_len: u32,
452 input: *mut u8,
453 input_len: u32,
454 key: *mut u8,
455 key_len: u32,
456 );
457}
458extern "C" {
459 #[doc = "Write the HMAC-SHA-1 MAC of a message (`data`) by using a key (`key`) into `dst`.\n\nThe key can be any length and will be hashed if it is longer and padded if it is shorter than 64 byte.\n`dst` must point to 20 bytes of memory."]
460 pub fn Hacl_HMAC_compute_sha1(
461 dst: *mut u8,
462 key: *mut u8,
463 key_len: u32,
464 data: *mut u8,
465 data_len: u32,
466 );
467}
468extern "C" {
469 #[doc = "Write the HMAC-SHA-2-256 MAC of a message (`data`) by using a key (`key`) into `dst`.\n\nThe key can be any length and will be hashed if it is longer and padded if it is shorter than 64 bytes.\n`dst` must point to 32 bytes of memory."]
470 pub fn Hacl_HMAC_compute_sha2_256(
471 dst: *mut u8,
472 key: *mut u8,
473 key_len: u32,
474 data: *mut u8,
475 data_len: u32,
476 );
477}
478extern "C" {
479 #[doc = "Write the HMAC-SHA-2-384 MAC of a message (`data`) by using a key (`key`) into `dst`.\n\nThe key can be any length and will be hashed if it is longer and padded if it is shorter than 128 bytes.\n`dst` must point to 48 bytes of memory."]
480 pub fn Hacl_HMAC_compute_sha2_384(
481 dst: *mut u8,
482 key: *mut u8,
483 key_len: u32,
484 data: *mut u8,
485 data_len: u32,
486 );
487}
488extern "C" {
489 #[doc = "Write the HMAC-SHA-2-512 MAC of a message (`data`) by using a key (`key`) into `dst`.\n\nThe key can be any length and will be hashed if it is longer and padded if it is shorter than 128 bytes.\n`dst` must point to 64 bytes of memory."]
490 pub fn Hacl_HMAC_compute_sha2_512(
491 dst: *mut u8,
492 key: *mut u8,
493 key_len: u32,
494 data: *mut u8,
495 data_len: u32,
496 );
497}
498extern "C" {
499 #[doc = "Write the HMAC-BLAKE2s MAC of a message (`data`) by using a key (`key`) into `dst`.\n\nThe key can be any length and will be hashed if it is longer and padded if it is shorter than 64 bytes.\n`dst` must point to 32 bytes of memory."]
500 pub fn Hacl_HMAC_compute_blake2s_32(
501 dst: *mut u8,
502 key: *mut u8,
503 key_len: u32,
504 data: *mut u8,
505 data_len: u32,
506 );
507}
508extern "C" {
509 #[doc = "Write the HMAC-BLAKE2b MAC of a message (`data`) by using a key (`key`) into `dst`.\n\nThe key can be any length and will be hashed if it is longer and padded if it is shorter than 128 bytes.\n`dst` must point to 64 bytes of memory."]
510 pub fn Hacl_HMAC_compute_blake2b_32(
511 dst: *mut u8,
512 key: *mut u8,
513 key_len: u32,
514 data: *mut u8,
515 data_len: u32,
516 );
517}
518pub type Hacl_HMAC_DRBG_supported_alg = Spec_Hash_Definitions_hash_alg;
519extern "C" {
520 #[doc = "Return the minimal entropy input length of the desired hash function.\n\n@param a Hash algorithm to use."]
521 pub fn Hacl_HMAC_DRBG_min_length(a: Spec_Hash_Definitions_hash_alg) -> u32;
522}
523#[repr(C)]
524#[derive(Debug, Copy, Clone)]
525pub struct Hacl_HMAC_DRBG_state_s {
526 pub k: *mut u8,
527 pub v: *mut u8,
528 pub reseed_counter: *mut u32,
529}
530pub type Hacl_HMAC_DRBG_state = Hacl_HMAC_DRBG_state_s;
531extern "C" {
532 pub fn Hacl_HMAC_DRBG_uu___is_State(
533 a: Spec_Hash_Definitions_hash_alg,
534 projectee: Hacl_HMAC_DRBG_state,
535 ) -> bool;
536}
537extern "C" {
538 #[doc = "Create a DRBG state.\n\n@param a Hash algorithm to use. The possible instantiations are ...\n `Spec_Hash_Definitions_SHA2_256`,\n `Spec_Hash_Definitions_SHA2_384`,\n `Spec_Hash_Definitions_SHA2_512`, and\n `Spec_Hash_Definitions_SHA1`."]
539 pub fn Hacl_HMAC_DRBG_create_in(a: Spec_Hash_Definitions_hash_alg) -> Hacl_HMAC_DRBG_state;
540}
541extern "C" {
542 #[doc = "Instantiate the DRBG.\n\n@param a Hash algorithm to use. (Value must match the value used in `Hacl_HMAC_DRBG_create_in`.)\n@param st Pointer to DRBG state.\n@param entropy_input_len Length of entropy input.\n@param entropy_input Pointer to `entropy_input_len` bytes of memory where entropy input is read from.\n@param nonce_len Length of nonce.\n@param nonce Pointer to `nonce_len` bytes of memory where nonce is read from.\n@param personalization_string_len length of personalization string.\n@param personalization_string Pointer to `personalization_string_len` bytes of memory where personalization string is read from."]
543 pub fn Hacl_HMAC_DRBG_instantiate(
544 a: Spec_Hash_Definitions_hash_alg,
545 st: Hacl_HMAC_DRBG_state,
546 entropy_input_len: u32,
547 entropy_input: *mut u8,
548 nonce_len: u32,
549 nonce: *mut u8,
550 personalization_string_len: u32,
551 personalization_string: *mut u8,
552 );
553}
554extern "C" {
555 #[doc = "Reseed the DRBG.\n\n@param a Hash algorithm to use. (Value must match the value used in `Hacl_HMAC_DRBG_create_in`.)\n@param st Pointer to DRBG state.\n@param entropy_input_len Length of entropy input.\n@param entropy_input Pointer to `entropy_input_len` bytes of memory where entropy input is read from.\n@param additional_input_input_len Length of additional input.\n@param additional_input_input Pointer to `additional_input_input_len` bytes of memory where additional input is read from."]
556 pub fn Hacl_HMAC_DRBG_reseed(
557 a: Spec_Hash_Definitions_hash_alg,
558 st: Hacl_HMAC_DRBG_state,
559 entropy_input_len: u32,
560 entropy_input: *mut u8,
561 additional_input_input_len: u32,
562 additional_input_input: *mut u8,
563 );
564}
565extern "C" {
566 #[doc = "Generate output.\n\n@param a Hash algorithm to use. (Value must match the value used in `create_in`.)\n@param output Pointer to `n` bytes of memory where random output is written to.\n@param st Pointer to DRBG state.\n@param n Length of desired output.\n@param additional_input_input_len Length of additional input.\n@param additional_input_input Pointer to `additional_input_input_len` bytes of memory where additional input is read from."]
567 pub fn Hacl_HMAC_DRBG_generate(
568 a: Spec_Hash_Definitions_hash_alg,
569 output: *mut u8,
570 st: Hacl_HMAC_DRBG_state,
571 n: u32,
572 additional_input_len: u32,
573 additional_input: *mut u8,
574 ) -> bool;
575}
576extern "C" {
577 pub fn Hacl_HMAC_DRBG_free(uu___: Spec_Hash_Definitions_hash_alg, s: Hacl_HMAC_DRBG_state);
578}
579extern "C" {
580 #[doc = "Compute the public key from the private key.\n\nThe outparam `public_key` points to 32 bytes of valid memory, i.e., uint8_t[32].\nThe argument `private_key` points to 32 bytes of valid memory, i.e., uint8_t[32]."]
581 pub fn Hacl_Ed25519_secret_to_public(public_key: *mut u8, private_key: *mut u8);
582}
583extern "C" {
584 #[doc = "Compute the expanded keys for an Ed25519 signature.\n\nThe outparam `expanded_keys` points to 96 bytes of valid memory, i.e., uint8_t[96].\nThe argument `private_key` points to 32 bytes of valid memory, i.e., uint8_t[32].\n\nIf one needs to sign several messages under the same private key, it is more efficient\nto call `expand_keys` only once and `sign_expanded` multiple times, for each message."]
585 pub fn Hacl_Ed25519_expand_keys(expanded_keys: *mut u8, private_key: *mut u8);
586}
587extern "C" {
588 #[doc = "Create an Ed25519 signature with the (precomputed) expanded keys.\n\nThe outparam `signature` points to 64 bytes of valid memory, i.e., uint8_t[64].\nThe argument `expanded_keys` points to 96 bytes of valid memory, i.e., uint8_t[96].\nThe argument `msg` points to `msg_len` bytes of valid memory, i.e., uint8_t[msg_len].\n\nThe argument `expanded_keys` is obtained through `expand_keys`.\n\nIf one needs to sign several messages under the same private key, it is more efficient\nto call `expand_keys` only once and `sign_expanded` multiple times, for each message."]
589 pub fn Hacl_Ed25519_sign_expanded(
590 signature: *mut u8,
591 expanded_keys: *mut u8,
592 msg_len: u32,
593 msg: *mut u8,
594 );
595}
596extern "C" {
597 #[doc = "Create an Ed25519 signature.\n\nThe outparam `signature` points to 64 bytes of valid memory, i.e., uint8_t[64].\nThe argument `private_key` points to 32 bytes of valid memory, i.e., uint8_t[32].\nThe argument `msg` points to `msg_len` bytes of valid memory, i.e., uint8_t[msg_len].\n\nThe function first calls `expand_keys` and then invokes `sign_expanded`.\n\nIf one needs to sign several messages under the same private key, it is more efficient\nto call `expand_keys` only once and `sign_expanded` multiple times, for each message."]
598 pub fn Hacl_Ed25519_sign(signature: *mut u8, private_key: *mut u8, msg_len: u32, msg: *mut u8);
599}
600extern "C" {
601 #[doc = "Verify an Ed25519 signature.\n\nThe function returns `true` if the signature is valid and `false` otherwise.\n\nThe argument `public_key` points to 32 bytes of valid memory, i.e., uint8_t[32].\nThe argument `msg` points to `msg_len` bytes of valid memory, i.e., uint8_t[msg_len].\nThe argument `signature` points to 64 bytes of valid memory, i.e., uint8_t[64]."]
602 pub fn Hacl_Ed25519_verify(
603 public_key: *mut u8,
604 msg_len: u32,
605 msg: *mut u8,
606 signature: *mut u8,
607 ) -> bool;
608}
609extern "C" {
610 #[doc = "Expand pseudorandom key to desired length.\n\n@param okm Pointer to `len` bytes of memory where output keying material is written to.\n@param prk Pointer to at least `HashLen` bytes of memory where pseudorandom key is read from. Usually, this points to the output from the extract step.\n@param prklen Length of pseudorandom key.\n@param info Pointer to `infolen` bytes of memory where context and application specific information is read from. Can be a zero-length string.\n@param infolen Length of context and application specific information.\n@param len Length of output keying material."]
611 pub fn Hacl_HKDF_expand_sha2_256(
612 okm: *mut u8,
613 prk: *mut u8,
614 prklen: u32,
615 info: *mut u8,
616 infolen: u32,
617 len: u32,
618 );
619}
620extern "C" {
621 #[doc = "Extract a fixed-length pseudorandom key from input keying material.\n\n@param prk Pointer to `HashLen` bytes of memory where pseudorandom key is written to.\n@param salt Pointer to `saltlen` bytes of memory where salt value is read from.\n@param saltlen Length of salt value.\n@param ikm Pointer to `ikmlen` bytes of memory where input keying material is read from.\n@param ikmlen Length of input keying material."]
622 pub fn Hacl_HKDF_extract_sha2_256(
623 prk: *mut u8,
624 salt: *mut u8,
625 saltlen: u32,
626 ikm: *mut u8,
627 ikmlen: u32,
628 );
629}
630extern "C" {
631 #[doc = "Expand pseudorandom key to desired length.\n\n@param okm Pointer to `len` bytes of memory where output keying material is written to.\n@param prk Pointer to at least `HashLen` bytes of memory where pseudorandom key is read from. Usually, this points to the output from the extract step.\n@param prklen Length of pseudorandom key.\n@param info Pointer to `infolen` bytes of memory where context and application specific information is read from. Can be a zero-length string.\n@param infolen Length of context and application specific information.\n@param len Length of output keying material."]
632 pub fn Hacl_HKDF_expand_sha2_384(
633 okm: *mut u8,
634 prk: *mut u8,
635 prklen: u32,
636 info: *mut u8,
637 infolen: u32,
638 len: u32,
639 );
640}
641extern "C" {
642 #[doc = "Extract a fixed-length pseudorandom key from input keying material.\n\n@param prk Pointer to `HashLen` bytes of memory where pseudorandom key is written to.\n@param salt Pointer to `saltlen` bytes of memory where salt value is read from.\n@param saltlen Length of salt value.\n@param ikm Pointer to `ikmlen` bytes of memory where input keying material is read from.\n@param ikmlen Length of input keying material."]
643 pub fn Hacl_HKDF_extract_sha2_384(
644 prk: *mut u8,
645 salt: *mut u8,
646 saltlen: u32,
647 ikm: *mut u8,
648 ikmlen: u32,
649 );
650}
651extern "C" {
652 #[doc = "Expand pseudorandom key to desired length.\n\n@param okm Pointer to `len` bytes of memory where output keying material is written to.\n@param prk Pointer to at least `HashLen` bytes of memory where pseudorandom key is read from. Usually, this points to the output from the extract step.\n@param prklen Length of pseudorandom key.\n@param info Pointer to `infolen` bytes of memory where context and application specific information is read from. Can be a zero-length string.\n@param infolen Length of context and application specific information.\n@param len Length of output keying material."]
653 pub fn Hacl_HKDF_expand_sha2_512(
654 okm: *mut u8,
655 prk: *mut u8,
656 prklen: u32,
657 info: *mut u8,
658 infolen: u32,
659 len: u32,
660 );
661}
662extern "C" {
663 #[doc = "Extract a fixed-length pseudorandom key from input keying material.\n\n@param prk Pointer to `HashLen` bytes of memory where pseudorandom key is written to.\n@param salt Pointer to `saltlen` bytes of memory where salt value is read from.\n@param saltlen Length of salt value.\n@param ikm Pointer to `ikmlen` bytes of memory where input keying material is read from.\n@param ikmlen Length of input keying material."]
664 pub fn Hacl_HKDF_extract_sha2_512(
665 prk: *mut u8,
666 salt: *mut u8,
667 saltlen: u32,
668 ikm: *mut u8,
669 ikmlen: u32,
670 );
671}
672extern "C" {
673 #[doc = "Expand pseudorandom key to desired length.\n\n@param okm Pointer to `len` bytes of memory where output keying material is written to.\n@param prk Pointer to at least `HashLen` bytes of memory where pseudorandom key is read from. Usually, this points to the output from the extract step.\n@param prklen Length of pseudorandom key.\n@param info Pointer to `infolen` bytes of memory where context and application specific information is read from. Can be a zero-length string.\n@param infolen Length of context and application specific information.\n@param len Length of output keying material."]
674 pub fn Hacl_HKDF_expand_blake2s_32(
675 okm: *mut u8,
676 prk: *mut u8,
677 prklen: u32,
678 info: *mut u8,
679 infolen: u32,
680 len: u32,
681 );
682}
683extern "C" {
684 #[doc = "Extract a fixed-length pseudorandom key from input keying material.\n\n@param prk Pointer to `HashLen` bytes of memory where pseudorandom key is written to.\n@param salt Pointer to `saltlen` bytes of memory where salt value is read from.\n@param saltlen Length of salt value.\n@param ikm Pointer to `ikmlen` bytes of memory where input keying material is read from.\n@param ikmlen Length of input keying material."]
685 pub fn Hacl_HKDF_extract_blake2s_32(
686 prk: *mut u8,
687 salt: *mut u8,
688 saltlen: u32,
689 ikm: *mut u8,
690 ikmlen: u32,
691 );
692}
693extern "C" {
694 #[doc = "Expand pseudorandom key to desired length.\n\n@param okm Pointer to `len` bytes of memory where output keying material is written to.\n@param prk Pointer to at least `HashLen` bytes of memory where pseudorandom key is read from. Usually, this points to the output from the extract step.\n@param prklen Length of pseudorandom key.\n@param info Pointer to `infolen` bytes of memory where context and application specific information is read from. Can be a zero-length string.\n@param infolen Length of context and application specific information.\n@param len Length of output keying material."]
695 pub fn Hacl_HKDF_expand_blake2b_32(
696 okm: *mut u8,
697 prk: *mut u8,
698 prklen: u32,
699 info: *mut u8,
700 infolen: u32,
701 len: u32,
702 );
703}
704extern "C" {
705 #[doc = "Extract a fixed-length pseudorandom key from input keying material.\n\n@param prk Pointer to `HashLen` bytes of memory where pseudorandom key is written to.\n@param salt Pointer to `saltlen` bytes of memory where salt value is read from.\n@param saltlen Length of salt value.\n@param ikm Pointer to `ikmlen` bytes of memory where input keying material is read from.\n@param ikmlen Length of input keying material."]
706 pub fn Hacl_HKDF_extract_blake2b_32(
707 prk: *mut u8,
708 salt: *mut u8,
709 saltlen: u32,
710 ikm: *mut u8,
711 ikmlen: u32,
712 );
713}
714extern "C" {
715 #[doc = "Create an ECDSA signature using SHA2-256.\n\nThe function returns `true` for successful creation of an ECDSA signature and `false` otherwise.\n\nThe outparam `signature` (R || S) points to 64 bytes of valid memory, i.e., uint8_t[64].\nThe argument `msg` points to `msg_len` bytes of valid memory, i.e., uint8_t[msg_len].\nThe arguments `private_key` and `nonce` point to 32 bytes of valid memory, i.e., uint8_t[32].\n\nThe function also checks whether `private_key` and `nonce` are valid:\n• 0 < `private_key` < the order of the curve\n• 0 < `nonce` < the order of the curve"]
716 pub fn Hacl_P256_ecdsa_sign_p256_sha2(
717 signature: *mut u8,
718 msg_len: u32,
719 msg: *mut u8,
720 private_key: *mut u8,
721 nonce: *mut u8,
722 ) -> bool;
723}
724extern "C" {
725 #[doc = "Create an ECDSA signature using SHA2-384.\n\nThe function returns `true` for successful creation of an ECDSA signature and `false` otherwise.\n\nThe outparam `signature` (R || S) points to 64 bytes of valid memory, i.e., uint8_t[64].\nThe argument `msg` points to `msg_len` bytes of valid memory, i.e., uint8_t[msg_len].\nThe arguments `private_key` and `nonce` point to 32 bytes of valid memory, i.e., uint8_t[32].\n\nThe function also checks whether `private_key` and `nonce` are valid:\n• 0 < `private_key` < the order of the curve\n• 0 < `nonce` < the order of the curve"]
726 pub fn Hacl_P256_ecdsa_sign_p256_sha384(
727 signature: *mut u8,
728 msg_len: u32,
729 msg: *mut u8,
730 private_key: *mut u8,
731 nonce: *mut u8,
732 ) -> bool;
733}
734extern "C" {
735 #[doc = "Create an ECDSA signature using SHA2-512.\n\nThe function returns `true` for successful creation of an ECDSA signature and `false` otherwise.\n\nThe outparam `signature` (R || S) points to 64 bytes of valid memory, i.e., uint8_t[64].\nThe argument `msg` points to `msg_len` bytes of valid memory, i.e., uint8_t[msg_len].\nThe arguments `private_key` and `nonce` point to 32 bytes of valid memory, i.e., uint8_t[32].\n\nThe function also checks whether `private_key` and `nonce` are valid:\n• 0 < `private_key` < the order of the curve\n• 0 < `nonce` < the order of the curve"]
736 pub fn Hacl_P256_ecdsa_sign_p256_sha512(
737 signature: *mut u8,
738 msg_len: u32,
739 msg: *mut u8,
740 private_key: *mut u8,
741 nonce: *mut u8,
742 ) -> bool;
743}
744extern "C" {
745 #[doc = "Create an ECDSA signature WITHOUT hashing first.\n\nThis function is intended to receive a hash of the input.\nFor convenience, we recommend using one of the hash-and-sign combined functions above.\n\nThe argument `msg` MUST be at least 32 bytes (i.e. `msg_len >= 32`).\n\nNOTE: The equivalent functions in OpenSSL and Fiat-Crypto both accept inputs\nsmaller than 32 bytes. These libraries left-pad the input with enough zeroes to\nreach the minimum 32 byte size. Clients who need behavior identical to OpenSSL\nneed to perform the left-padding themselves.\n\nThe function returns `true` for successful creation of an ECDSA signature and `false` otherwise.\n\nThe outparam `signature` (R || S) points to 64 bytes of valid memory, i.e., uint8_t[64].\nThe argument `msg` points to `msg_len` bytes of valid memory, i.e., uint8_t[msg_len].\nThe arguments `private_key` and `nonce` point to 32 bytes of valid memory, i.e., uint8_t[32].\n\nThe function also checks whether `private_key` and `nonce` are valid values:\n• 0 < `private_key` < the order of the curve\n• 0 < `nonce` < the order of the curve"]
746 pub fn Hacl_P256_ecdsa_sign_p256_without_hash(
747 signature: *mut u8,
748 msg_len: u32,
749 msg: *mut u8,
750 private_key: *mut u8,
751 nonce: *mut u8,
752 ) -> bool;
753}
754extern "C" {
755 #[doc = "Verify an ECDSA signature using SHA2-256.\n\nThe function returns `true` if the signature is valid and `false` otherwise.\n\nThe argument `msg` points to `msg_len` bytes of valid memory, i.e., uint8_t[msg_len].\nThe argument `public_key` (x || y) points to 64 bytes of valid memory, i.e., uint8_t[64].\nThe arguments `signature_r` and `signature_s` point to 32 bytes of valid memory, i.e., uint8_t[32].\n\nThe function also checks whether `public_key` is valid"]
756 pub fn Hacl_P256_ecdsa_verif_p256_sha2(
757 msg_len: u32,
758 msg: *mut u8,
759 public_key: *mut u8,
760 signature_r: *mut u8,
761 signature_s: *mut u8,
762 ) -> bool;
763}
764extern "C" {
765 #[doc = "Verify an ECDSA signature using SHA2-384.\n\nThe function returns `true` if the signature is valid and `false` otherwise.\n\nThe argument `msg` points to `msg_len` bytes of valid memory, i.e., uint8_t[msg_len].\nThe argument `public_key` (x || y) points to 64 bytes of valid memory, i.e., uint8_t[64].\nThe arguments `signature_r` and `signature_s` point to 32 bytes of valid memory, i.e., uint8_t[32].\n\nThe function also checks whether `public_key` is valid"]
766 pub fn Hacl_P256_ecdsa_verif_p256_sha384(
767 msg_len: u32,
768 msg: *mut u8,
769 public_key: *mut u8,
770 signature_r: *mut u8,
771 signature_s: *mut u8,
772 ) -> bool;
773}
774extern "C" {
775 #[doc = "Verify an ECDSA signature using SHA2-512.\n\nThe function returns `true` if the signature is valid and `false` otherwise.\n\nThe argument `msg` points to `msg_len` bytes of valid memory, i.e., uint8_t[msg_len].\nThe argument `public_key` (x || y) points to 64 bytes of valid memory, i.e., uint8_t[64].\nThe arguments `signature_r` and `signature_s` point to 32 bytes of valid memory, i.e., uint8_t[32].\n\nThe function also checks whether `public_key` is valid"]
776 pub fn Hacl_P256_ecdsa_verif_p256_sha512(
777 msg_len: u32,
778 msg: *mut u8,
779 public_key: *mut u8,
780 signature_r: *mut u8,
781 signature_s: *mut u8,
782 ) -> bool;
783}
784extern "C" {
785 #[doc = "Verify an ECDSA signature WITHOUT hashing first.\n\nThis function is intended to receive a hash of the input.\nFor convenience, we recommend using one of the hash-and-verify combined functions above.\n\nThe argument `msg` MUST be at least 32 bytes (i.e. `msg_len >= 32`).\n\nThe function returns `true` if the signature is valid and `false` otherwise.\n\nThe argument `msg` points to `msg_len` bytes of valid memory, i.e., uint8_t[msg_len].\nThe argument `public_key` (x || y) points to 64 bytes of valid memory, i.e., uint8_t[64].\nThe arguments `signature_r` and `signature_s` point to 32 bytes of valid memory, i.e., uint8_t[32].\n\nThe function also checks whether `public_key` is valid"]
786 pub fn Hacl_P256_ecdsa_verif_without_hash(
787 msg_len: u32,
788 msg: *mut u8,
789 public_key: *mut u8,
790 signature_r: *mut u8,
791 signature_s: *mut u8,
792 ) -> bool;
793}
794extern "C" {
795 #[doc = "Public key validation.\n\nThe function returns `true` if a public key is valid and `false` otherwise.\n\nThe argument `public_key` points to 64 bytes of valid memory, i.e., uint8_t[64].\n\nThe public key (x || y) is valid (with respect to SP 800-56A):\n• the public key is not the “point at infinity”, represented as O.\n• the affine x and y coordinates of the point represented by the public key are\nin the range [0, p – 1] where p is the prime defining the finite field.\n• y^2 = x^3 + ax + b where a and b are the coefficients of the curve equation.\nThe last extract is taken from: https://neilmadden.blog/2017/05/17/so-how-do-you-validate-nist-ecdh-public-keys/"]
796 pub fn Hacl_P256_validate_public_key(public_key: *mut u8) -> bool;
797}
798extern "C" {
799 #[doc = "Private key validation.\n\nThe function returns `true` if a private key is valid and `false` otherwise.\n\nThe argument `private_key` points to 32 bytes of valid memory, i.e., uint8_t[32].\n\nThe private key is valid:\n• 0 < `private_key` < the order of the curve"]
800 pub fn Hacl_P256_validate_private_key(private_key: *mut u8) -> bool;
801}
802extern "C" {
803 #[doc = "Convert a public key from uncompressed to its raw form.\n\nThe function returns `true` for successful conversion of a public key and `false` otherwise.\n\nThe outparam `pk_raw` points to 64 bytes of valid memory, i.e., uint8_t[64].\nThe argument `pk` points to 65 bytes of valid memory, i.e., uint8_t[65].\n\nThe function DOESN'T check whether (x, y) is a valid point."]
804 pub fn Hacl_P256_uncompressed_to_raw(pk: *mut u8, pk_raw: *mut u8) -> bool;
805}
806extern "C" {
807 #[doc = "Convert a public key from compressed to its raw form.\n\nThe function returns `true` for successful conversion of a public key and `false` otherwise.\n\nThe outparam `pk_raw` points to 64 bytes of valid memory, i.e., uint8_t[64].\nThe argument `pk` points to 33 bytes of valid memory, i.e., uint8_t[33].\n\nThe function also checks whether (x, y) is a valid point."]
808 pub fn Hacl_P256_compressed_to_raw(pk: *mut u8, pk_raw: *mut u8) -> bool;
809}
810extern "C" {
811 #[doc = "Convert a public key from raw to its uncompressed form.\n\nThe outparam `pk` points to 65 bytes of valid memory, i.e., uint8_t[65].\nThe argument `pk_raw` points to 64 bytes of valid memory, i.e., uint8_t[64].\n\nThe function DOESN'T check whether (x, y) is a valid point."]
812 pub fn Hacl_P256_raw_to_uncompressed(pk_raw: *mut u8, pk: *mut u8);
813}
814extern "C" {
815 #[doc = "Convert a public key from raw to its compressed form.\n\nThe outparam `pk` points to 33 bytes of valid memory, i.e., uint8_t[33].\nThe argument `pk_raw` points to 64 bytes of valid memory, i.e., uint8_t[64].\n\nThe function DOESN'T check whether (x, y) is a valid point."]
816 pub fn Hacl_P256_raw_to_compressed(pk_raw: *mut u8, pk: *mut u8);
817}
818extern "C" {
819 #[doc = "Compute the public key from the private key.\n\nThe function returns `true` if a private key is valid and `false` otherwise.\n\nThe outparam `public_key` points to 64 bytes of valid memory, i.e., uint8_t[64].\nThe argument `private_key` points to 32 bytes of valid memory, i.e., uint8_t[32].\n\nThe private key is valid:\n• 0 < `private_key` < the order of the curve."]
820 pub fn Hacl_P256_dh_initiator(public_key: *mut u8, private_key: *mut u8) -> bool;
821}
822extern "C" {
823 #[doc = "Execute the diffie-hellmann key exchange.\n\nThe function returns `true` for successful creation of an ECDH shared secret and\n`false` otherwise.\n\nThe outparam `shared_secret` points to 64 bytes of valid memory, i.e., uint8_t[64].\nThe argument `their_pubkey` points to 64 bytes of valid memory, i.e., uint8_t[64].\nThe argument `private_key` points to 32 bytes of valid memory, i.e., uint8_t[32].\n\nThe function also checks whether `private_key` and `their_pubkey` are valid."]
824 pub fn Hacl_P256_dh_responder(
825 shared_secret: *mut u8,
826 their_pubkey: *mut u8,
827 private_key: *mut u8,
828 ) -> bool;
829}
830extern "C" {
831 #[doc = "Sign a message `msg` and write the signature to `sgnt`.\n\n@param a Hash algorithm to use. Allowed values for `a` are ...\n- Spec_Hash_Definitions_SHA2_256,\n- Spec_Hash_Definitions_SHA2_384, and\n- Spec_Hash_Definitions_SHA2_512.\n@param modBits Count of bits in the modulus (`n`).\n@param eBits Count of bits in `e` value.\n@param dBits Count of bits in `d` value.\n@param skey Pointer to secret key created by `Hacl_RSAPSS_new_rsapss_load_skey`.\n@param saltLen Length of salt.\n@param salt Pointer to `saltLen` bytes where the salt is read from.\n@param msgLen Length of message.\n@param msg Pointer to `msgLen` bytes where the message is read from.\n@param sgnt Pointer to `ceil(modBits / 8)` bytes where the signature is written to.\n\n@return Returns true if and only if signing was successful."]
832 pub fn Hacl_RSAPSS_rsapss_sign(
833 a: Spec_Hash_Definitions_hash_alg,
834 modBits: u32,
835 eBits: u32,
836 dBits: u32,
837 skey: *mut u64,
838 saltLen: u32,
839 salt: *mut u8,
840 msgLen: u32,
841 msg: *mut u8,
842 sgnt: *mut u8,
843 ) -> bool;
844}
845extern "C" {
846 #[doc = "Verify the signature `sgnt` of a message `msg`.\n\n@param a Hash algorithm to use. Allowed values for `a` are ...\n- Spec_Hash_Definitions_SHA2_256,\n- Spec_Hash_Definitions_SHA2_384, and\n- Spec_Hash_Definitions_SHA2_512.\n@param modBits Count of bits in the modulus (`n`).\n@param eBits Count of bits in `e` value.\n@param pkey Pointer to public key created by `Hacl_RSAPSS_new_rsapss_load_pkey`.\n@param saltLen Length of salt.\n@param sgntLen Length of signature.\n@param sgnt Pointer to `sgntLen` bytes where the signature is read from.\n@param msgLen Length of message.\n@param msg Pointer to `msgLen` bytes where the message is read from.\n\n@return Returns true if and only if the signature is valid."]
847 pub fn Hacl_RSAPSS_rsapss_verify(
848 a: Spec_Hash_Definitions_hash_alg,
849 modBits: u32,
850 eBits: u32,
851 pkey: *mut u64,
852 saltLen: u32,
853 sgntLen: u32,
854 sgnt: *mut u8,
855 msgLen: u32,
856 msg: *mut u8,
857 ) -> bool;
858}
859extern "C" {
860 #[doc = "Load a public key from key parts.\n\n@param modBits Count of bits in modulus (`n`).\n@param eBits Count of bits in `e` value.\n@param nb Pointer to `ceil(modBits / 8)` bytes where the modulus (`n`), in big-endian byte order, is read from.\n@param eb Pointer to `ceil(modBits / 8)` bytes where the `e` value, in big-endian byte order, is read from.\n\n@return Returns an allocated public key upon success, otherwise, `NULL` if key part arguments are invalid or memory allocation fails. Note: caller must take care to `free()` the created key."]
861 pub fn Hacl_RSAPSS_new_rsapss_load_pkey(
862 modBits: u32,
863 eBits: u32,
864 nb: *mut u8,
865 eb: *mut u8,
866 ) -> *mut u64;
867}
868extern "C" {
869 #[doc = "Load a secret key from key parts.\n\n@param modBits Count of bits in modulus (`n`).\n@param eBits Count of bits in `e` value.\n@param dBits Count of bits in `d` value.\n@param nb Pointer to `ceil(modBits / 8)` bytes where the modulus (`n`), in big-endian byte order, is read from.\n@param eb Pointer to `ceil(modBits / 8)` bytes where the `e` value, in big-endian byte order, is read from.\n@param db Pointer to `ceil(modBits / 8)` bytes where the `d` value, in big-endian byte order, is read from.\n\n@return Returns an allocated secret key upon success, otherwise, `NULL` if key part arguments are invalid or memory allocation fails. Note: caller must take care to `free()` the created key."]
870 pub fn Hacl_RSAPSS_new_rsapss_load_skey(
871 modBits: u32,
872 eBits: u32,
873 dBits: u32,
874 nb: *mut u8,
875 eb: *mut u8,
876 db: *mut u8,
877 ) -> *mut u64;
878}
879extern "C" {
880 #[doc = "Sign a message `msg` and write the signature to `sgnt`.\n\n@param a Hash algorithm to use. Allowed values for `a` are ...\n- Spec_Hash_Definitions_SHA2_256,\n- Spec_Hash_Definitions_SHA2_384, and\n- Spec_Hash_Definitions_SHA2_512.\n@param modBits Count of bits in the modulus (`n`).\n@param eBits Count of bits in `e` value.\n@param dBits Count of bits in `d` value.\n@param nb Pointer to `ceil(modBits / 8)` bytes where the modulus (`n`), in big-endian byte order, is read from.\n@param eb Pointer to `ceil(modBits / 8)` bytes where the `e` value, in big-endian byte order, is read from.\n@param db Pointer to `ceil(modBits / 8)` bytes where the `d` value, in big-endian byte order, is read from.\n@param saltLen Length of salt.\n@param salt Pointer to `saltLen` bytes where the salt is read from.\n@param msgLen Length of message.\n@param msg Pointer to `msgLen` bytes where the message is read from.\n@param sgnt Pointer to `ceil(modBits / 8)` bytes where the signature is written to.\n\n@return Returns true if and only if signing was successful."]
881 pub fn Hacl_RSAPSS_rsapss_skey_sign(
882 a: Spec_Hash_Definitions_hash_alg,
883 modBits: u32,
884 eBits: u32,
885 dBits: u32,
886 nb: *mut u8,
887 eb: *mut u8,
888 db: *mut u8,
889 saltLen: u32,
890 salt: *mut u8,
891 msgLen: u32,
892 msg: *mut u8,
893 sgnt: *mut u8,
894 ) -> bool;
895}
896extern "C" {
897 #[doc = "Verify the signature `sgnt` of a message `msg`.\n\n@param a Hash algorithm to use. Allowed values for `a` are ...\n- Spec_Hash_Definitions_SHA2_256,\n- Spec_Hash_Definitions_SHA2_384, and\n- Spec_Hash_Definitions_SHA2_512.\n@param modBits Count of bits in the modulus (`n`).\n@param eBits Count of bits in `e` value.\n@param nb Pointer to `ceil(modBits / 8)` bytes where the modulus (`n`), in big-endian byte order, is read from.\n@param eb Pointer to `ceil(modBits / 8)` bytes where the `e` value, in big-endian byte order, is read from.\n@param saltLen Length of salt.\n@param sgntLen Length of signature.\n@param sgnt Pointer to `sgntLen` bytes where the signature is read from.\n@param msgLen Length of message.\n@param msg Pointer to `msgLen` bytes where the message is read from.\n\n@return Returns true if and only if the signature is valid."]
898 pub fn Hacl_RSAPSS_rsapss_pkey_verify(
899 a: Spec_Hash_Definitions_hash_alg,
900 modBits: u32,
901 eBits: u32,
902 nb: *mut u8,
903 eb: *mut u8,
904 saltLen: u32,
905 sgntLen: u32,
906 sgnt: *mut u8,
907 msgLen: u32,
908 msg: *mut u8,
909 ) -> bool;
910}
911extern "C" {
912 #[doc = "The mask generation function defined in the Public Key Cryptography Standard #1\n(https://www.ietf.org/rfc/rfc2437.txt Section 10.2.1)"]
913 pub fn Hacl_RSAPSS_mgf_hash(
914 a: Spec_Hash_Definitions_hash_alg,
915 len: u32,
916 mgfseed: *mut u8,
917 maskLen: u32,
918 res: *mut u8,
919 );
920}
921extern "C" {
922 pub fn hacl_free(ptr: *mut ::core::ffi::c_void);
923}
924extern "C" {
925 #[doc = "Encrypt a message `input` with key `key`.\n\nThe arguments `key`, `nonce`, `data`, and `data_len` are same in encryption/decryption.\nNote: Encryption and decryption can be executed in-place, i.e., `input` and `output` can point to the same memory.\n\n@param output Pointer to `input_len` bytes of memory where the ciphertext is written to.\n@param tag Pointer to 16 bytes of memory where the mac is written to.\n@param input Pointer to `input_len` bytes of memory where the message is read from.\n@param input_len Length of the message.\n@param data Pointer to `data_len` bytes of memory where the associated data is read from.\n@param data_len Length of the associated data.\n@param key Pointer to 32 bytes of memory where the AEAD key is read from.\n@param nonce Pointer to 12 bytes of memory where the AEAD nonce is read from."]
926 pub fn Hacl_AEAD_Chacha20Poly1305_Simd128_encrypt(
927 output: *mut u8,
928 tag: *mut u8,
929 input: *mut u8,
930 input_len: u32,
931 data: *mut u8,
932 data_len: u32,
933 key: *mut u8,
934 nonce: *mut u8,
935 );
936}
937extern "C" {
938 #[doc = "Decrypt a ciphertext `input` with key `key`.\n\nThe arguments `key`, `nonce`, `data`, and `data_len` are same in encryption/decryption.\nNote: Encryption and decryption can be executed in-place, i.e., `input` and `output` can point to the same memory.\n\nIf decryption succeeds, the resulting plaintext is stored in `output` and the function returns the success code 0.\nIf decryption fails, the array `output` remains unchanged and the function returns the error code 1.\n\n@param output Pointer to `input_len` bytes of memory where the message is written to.\n@param input Pointer to `input_len` bytes of memory where the ciphertext is read from.\n@param input_len Length of the ciphertext.\n@param data Pointer to `data_len` bytes of memory where the associated data is read from.\n@param data_len Length of the associated data.\n@param key Pointer to 32 bytes of memory where the AEAD key is read from.\n@param nonce Pointer to 12 bytes of memory where the AEAD nonce is read from.\n@param tag Pointer to 16 bytes of memory where the mac is read from.\n\n@returns 0 on succeess; 1 on failure."]
939 pub fn Hacl_AEAD_Chacha20Poly1305_Simd128_decrypt(
940 output: *mut u8,
941 input: *mut u8,
942 input_len: u32,
943 data: *mut u8,
944 data_len: u32,
945 key: *mut u8,
946 nonce: *mut u8,
947 tag: *mut u8,
948 ) -> u32;
949}
950pub type __m128i = [::core::ffi::c_longlong; 2usize];
951pub type Lib_IntVector_Intrinsics_vec128 = __m128i;
952pub type __m256i = [::core::ffi::c_longlong; 4usize];
953pub type Lib_IntVector_Intrinsics_vec256 = __m256i;
954#[repr(C)]
955#[derive(Debug, Copy, Clone)]
956pub struct Hacl_Hash_Blake2s_Simd128_block_state_t_s {
957 pub fst: *mut Lib_IntVector_Intrinsics_vec128,
958 pub snd: *mut Lib_IntVector_Intrinsics_vec128,
959}
960pub type Hacl_Hash_Blake2s_Simd128_block_state_t = Hacl_Hash_Blake2s_Simd128_block_state_t_s;
961#[repr(C)]
962#[derive(Debug, Copy, Clone)]
963pub struct Hacl_Hash_Blake2s_Simd128_state_t_s {
964 pub block_state: Hacl_Hash_Blake2s_Simd128_block_state_t,
965 pub buf: *mut u8,
966 pub total_len: u64,
967}
968pub type Hacl_Hash_Blake2s_Simd128_state_t = Hacl_Hash_Blake2s_Simd128_state_t_s;
969extern "C" {
970 #[doc = "State allocation function when there is no key"]
971 pub fn Hacl_Hash_Blake2s_Simd128_malloc() -> *mut Hacl_Hash_Blake2s_Simd128_state_t;
972}
973extern "C" {
974 #[doc = "Re-initialization function when there is no key"]
975 pub fn Hacl_Hash_Blake2s_Simd128_reset(state: *mut Hacl_Hash_Blake2s_Simd128_state_t);
976}
977extern "C" {
978 #[doc = "Update function when there is no key; 0 = success, 1 = max length exceeded"]
979 pub fn Hacl_Hash_Blake2s_Simd128_update(
980 state: *mut Hacl_Hash_Blake2s_Simd128_state_t,
981 chunk: *mut u8,
982 chunk_len: u32,
983 ) -> Hacl_Streaming_Types_error_code;
984}
985extern "C" {
986 #[doc = "Finish function when there is no key"]
987 pub fn Hacl_Hash_Blake2s_Simd128_digest(
988 state: *mut Hacl_Hash_Blake2s_Simd128_state_t,
989 output: *mut u8,
990 );
991}
992extern "C" {
993 #[doc = "Free state function when there is no key"]
994 pub fn Hacl_Hash_Blake2s_Simd128_free(state: *mut Hacl_Hash_Blake2s_Simd128_state_t);
995}
996extern "C" {
997 #[doc = "Write the BLAKE2s digest of message `input` using key `key` into `output`.\n\n@param output Pointer to `output_len` bytes of memory where the digest is written to.\n@param output_len Length of the to-be-generated digest with 1 <= `output_len` <= 32.\n@param input Pointer to `input_len` bytes of memory where the input message is read from.\n@param input_len Length of the input message.\n@param key Pointer to `key_len` bytes of memory where the key is read from.\n@param key_len Length of the key. Can be 0."]
998 pub fn Hacl_Hash_Blake2s_Simd128_hash_with_key(
999 output: *mut u8,
1000 output_len: u32,
1001 input: *mut u8,
1002 input_len: u32,
1003 key: *mut u8,
1004 key_len: u32,
1005 );
1006}
1007extern "C" {
1008 #[doc = "Encrypt a message `input` with key `key`.\n\nThe arguments `key`, `nonce`, `data`, and `data_len` are same in encryption/decryption.\nNote: Encryption and decryption can be executed in-place, i.e., `input` and `output` can point to the same memory.\n\n@param output Pointer to `input_len` bytes of memory where the ciphertext is written to.\n@param tag Pointer to 16 bytes of memory where the mac is written to.\n@param input Pointer to `input_len` bytes of memory where the message is read from.\n@param input_len Length of the message.\n@param data Pointer to `data_len` bytes of memory where the associated data is read from.\n@param data_len Length of the associated data.\n@param key Pointer to 32 bytes of memory where the AEAD key is read from.\n@param nonce Pointer to 12 bytes of memory where the AEAD nonce is read from."]
1009 pub fn Hacl_AEAD_Chacha20Poly1305_Simd256_encrypt(
1010 output: *mut u8,
1011 tag: *mut u8,
1012 input: *mut u8,
1013 input_len: u32,
1014 data: *mut u8,
1015 data_len: u32,
1016 key: *mut u8,
1017 nonce: *mut u8,
1018 );
1019}
1020extern "C" {
1021 #[doc = "Decrypt a ciphertext `input` with key `key`.\n\nThe arguments `key`, `nonce`, `data`, and `data_len` are same in encryption/decryption.\nNote: Encryption and decryption can be executed in-place, i.e., `input` and `output` can point to the same memory.\n\nIf decryption succeeds, the resulting plaintext is stored in `output` and the function returns the success code 0.\nIf decryption fails, the array `output` remains unchanged and the function returns the error code 1.\n\n@param output Pointer to `input_len` bytes of memory where the message is written to.\n@param input Pointer to `input_len` bytes of memory where the ciphertext is read from.\n@param input_len Length of the ciphertext.\n@param data Pointer to `data_len` bytes of memory where the associated data is read from.\n@param data_len Length of the associated data.\n@param key Pointer to 32 bytes of memory where the AEAD key is read from.\n@param nonce Pointer to 12 bytes of memory where the AEAD nonce is read from.\n@param tag Pointer to 16 bytes of memory where the mac is read from.\n\n@returns 0 on succeess; 1 on failure."]
1022 pub fn Hacl_AEAD_Chacha20Poly1305_Simd256_decrypt(
1023 output: *mut u8,
1024 input: *mut u8,
1025 input_len: u32,
1026 data: *mut u8,
1027 data_len: u32,
1028 key: *mut u8,
1029 nonce: *mut u8,
1030 tag: *mut u8,
1031 ) -> u32;
1032}
1033#[repr(C)]
1034#[derive(Debug, Copy, Clone)]
1035pub struct Hacl_Hash_Blake2b_Simd256_block_state_t_s {
1036 pub fst: *mut Lib_IntVector_Intrinsics_vec256,
1037 pub snd: *mut Lib_IntVector_Intrinsics_vec256,
1038}
1039pub type Hacl_Hash_Blake2b_Simd256_block_state_t = Hacl_Hash_Blake2b_Simd256_block_state_t_s;
1040#[repr(C)]
1041#[derive(Debug, Copy, Clone)]
1042pub struct Hacl_Hash_Blake2b_Simd256_state_t_s {
1043 pub block_state: Hacl_Hash_Blake2b_Simd256_block_state_t,
1044 pub buf: *mut u8,
1045 pub total_len: u64,
1046}
1047pub type Hacl_Hash_Blake2b_Simd256_state_t = Hacl_Hash_Blake2b_Simd256_state_t_s;
1048extern "C" {
1049 #[doc = "State allocation function when there is no key"]
1050 pub fn Hacl_Hash_Blake2b_Simd256_malloc() -> *mut Hacl_Hash_Blake2b_Simd256_state_t;
1051}
1052extern "C" {
1053 #[doc = "Re-initialization function when there is no key"]
1054 pub fn Hacl_Hash_Blake2b_Simd256_reset(state: *mut Hacl_Hash_Blake2b_Simd256_state_t);
1055}
1056extern "C" {
1057 #[doc = "Update function when there is no key; 0 = success, 1 = max length exceeded"]
1058 pub fn Hacl_Hash_Blake2b_Simd256_update(
1059 state: *mut Hacl_Hash_Blake2b_Simd256_state_t,
1060 chunk: *mut u8,
1061 chunk_len: u32,
1062 ) -> Hacl_Streaming_Types_error_code;
1063}
1064extern "C" {
1065 #[doc = "Finish function when there is no key"]
1066 pub fn Hacl_Hash_Blake2b_Simd256_digest(
1067 state: *mut Hacl_Hash_Blake2b_Simd256_state_t,
1068 output: *mut u8,
1069 );
1070}
1071extern "C" {
1072 #[doc = "Free state function when there is no key"]
1073 pub fn Hacl_Hash_Blake2b_Simd256_free(state: *mut Hacl_Hash_Blake2b_Simd256_state_t);
1074}
1075extern "C" {
1076 #[doc = "Write the BLAKE2b digest of message `input` using key `key` into `output`.\n\n@param output Pointer to `output_len` bytes of memory where the digest is written to.\n@param output_len Length of the to-be-generated digest with 1 <= `output_len` <= 64.\n@param input Pointer to `input_len` bytes of memory where the input message is read from.\n@param input_len Length of the input message.\n@param key Pointer to `key_len` bytes of memory where the key is read from.\n@param key_len Length of the key. Can be 0."]
1077 pub fn Hacl_Hash_Blake2b_Simd256_hash_with_key(
1078 output: *mut u8,
1079 output_len: u32,
1080 input: *mut u8,
1081 input_len: u32,
1082 key: *mut u8,
1083 key_len: u32,
1084 );
1085}
1086extern "C" {
1087 pub fn EverCrypt_AutoConfig2_has_shaext() -> bool;
1088}
1089extern "C" {
1090 pub fn EverCrypt_AutoConfig2_has_aesni() -> bool;
1091}
1092extern "C" {
1093 pub fn EverCrypt_AutoConfig2_has_pclmulqdq() -> bool;
1094}
1095extern "C" {
1096 pub fn EverCrypt_AutoConfig2_has_avx2() -> bool;
1097}
1098extern "C" {
1099 pub fn EverCrypt_AutoConfig2_has_avx() -> bool;
1100}
1101extern "C" {
1102 pub fn EverCrypt_AutoConfig2_has_bmi2() -> bool;
1103}
1104extern "C" {
1105 pub fn EverCrypt_AutoConfig2_has_adx() -> bool;
1106}
1107extern "C" {
1108 pub fn EverCrypt_AutoConfig2_has_sse() -> bool;
1109}
1110extern "C" {
1111 pub fn EverCrypt_AutoConfig2_has_movbe() -> bool;
1112}
1113extern "C" {
1114 pub fn EverCrypt_AutoConfig2_has_rdrand() -> bool;
1115}
1116extern "C" {
1117 pub fn EverCrypt_AutoConfig2_has_avx512() -> bool;
1118}
1119extern "C" {
1120 pub fn EverCrypt_AutoConfig2_recall();
1121}
1122extern "C" {
1123 pub fn EverCrypt_AutoConfig2_init();
1124}
1125extern "C" {
1126 pub fn EverCrypt_AutoConfig2_disable_avx2();
1127}
1128extern "C" {
1129 pub fn EverCrypt_AutoConfig2_disable_avx();
1130}
1131extern "C" {
1132 pub fn EverCrypt_AutoConfig2_disable_bmi2();
1133}
1134extern "C" {
1135 pub fn EverCrypt_AutoConfig2_disable_adx();
1136}
1137extern "C" {
1138 pub fn EverCrypt_AutoConfig2_disable_shaext();
1139}
1140extern "C" {
1141 pub fn EverCrypt_AutoConfig2_disable_aesni();
1142}
1143extern "C" {
1144 pub fn EverCrypt_AutoConfig2_disable_pclmulqdq();
1145}
1146extern "C" {
1147 pub fn EverCrypt_AutoConfig2_disable_sse();
1148}
1149extern "C" {
1150 pub fn EverCrypt_AutoConfig2_disable_movbe();
1151}
1152extern "C" {
1153 pub fn EverCrypt_AutoConfig2_disable_rdrand();
1154}
1155extern "C" {
1156 pub fn EverCrypt_AutoConfig2_disable_avx512();
1157}
1158extern "C" {
1159 pub fn EverCrypt_AutoConfig2_has_vec128() -> bool;
1160}
1161extern "C" {
1162 pub fn EverCrypt_AutoConfig2_has_vec256() -> bool;
1163}
1164pub type Spec_FFDHE_ffdhe_alg = u8;
1165pub type Spec_Agile_AEAD_alg = u8;
1166pub type EverCrypt_Error_error_code = u8;
1167#[repr(C)]
1168#[derive(Debug, Copy, Clone)]
1169pub struct EverCrypt_AEAD_state_s_s {
1170 _unused: [u8; 0],
1171}
1172pub type EverCrypt_AEAD_state_s = EverCrypt_AEAD_state_s_s;
1173extern "C" {
1174 #[doc = "Both encryption and decryption require a state that holds the key.\nThe state may be reused as many times as desired."]
1175 pub fn EverCrypt_AEAD_uu___is_Ek(
1176 a: Spec_Agile_AEAD_alg,
1177 projectee: EverCrypt_AEAD_state_s,
1178 ) -> bool;
1179}
1180extern "C" {
1181 #[doc = "Return the algorithm used in the AEAD state.\n\n@param s State of the AEAD algorithm.\n\n@return Algorithm used in the AEAD state."]
1182 pub fn EverCrypt_AEAD_alg_of_state(s: *mut EverCrypt_AEAD_state_s) -> Spec_Agile_AEAD_alg;
1183}
1184extern "C" {
1185 #[doc = "Create the required AEAD state for the algorithm.\n\nNote: The caller must free the AEAD state by calling `EverCrypt_AEAD_free`.\n\n@param a The argument `a` must be either of:\n `Spec_Agile_AEAD_AES128_GCM` (KEY_LEN=16),\n `Spec_Agile_AEAD_AES256_GCM` (KEY_LEN=32), or\n `Spec_Agile_AEAD_CHACHA20_POLY1305` (KEY_LEN=32).\n@param dst Pointer to a pointer where the address of the allocated AEAD state will be written to.\n@param k Pointer to `KEY_LEN` bytes of memory where the key is read from. The size depends on the used algorithm, see above.\n\n@return The function returns `EverCrypt_Error_Success` on success or\n`EverCrypt_Error_UnsupportedAlgorithm` in case of a bad algorithm identifier.\n(See `EverCrypt_Error.h`.)"]
1186 pub fn EverCrypt_AEAD_create_in(
1187 a: Spec_Agile_AEAD_alg,
1188 dst: *mut *mut EverCrypt_AEAD_state_s,
1189 k: *mut u8,
1190 ) -> EverCrypt_Error_error_code;
1191}
1192extern "C" {
1193 #[doc = "Encrypt and authenticate a message (`plain`) with associated data (`ad`).\n\n@param s Pointer to the The AEAD state created by `EverCrypt_AEAD_create_in`. It already contains the encryption key.\n@param iv Pointer to `iv_len` bytes of memory where the nonce is read from.\n@param iv_len Length of the nonce. Note: ChaCha20Poly1305 requires a 12 byte nonce.\n@param ad Pointer to `ad_len` bytes of memory where the associated data is read from.\n@param ad_len Length of the associated data.\n@param plain Pointer to `plain_len` bytes of memory where the to-be-encrypted plaintext is read from.\n@param plain_len Length of the to-be-encrypted plaintext.\n@param cipher Pointer to `plain_len` bytes of memory where the ciphertext is written to.\n@param tag Pointer to `TAG_LEN` bytes of memory where the tag is written to.\nThe length of the `tag` must be of a suitable length for the chosen algorithm:\n `Spec_Agile_AEAD_AES128_GCM` (TAG_LEN=16)\n `Spec_Agile_AEAD_AES256_GCM` (TAG_LEN=16)\n `Spec_Agile_AEAD_CHACHA20_POLY1305` (TAG_LEN=16)\n\n@return `EverCrypt_AEAD_encrypt` may return either `EverCrypt_Error_Success` or `EverCrypt_Error_InvalidKey` (`EverCrypt_error.h`). The latter is returned if and only if the `s` parameter is `NULL`."]
1194 pub fn EverCrypt_AEAD_encrypt(
1195 s: *mut EverCrypt_AEAD_state_s,
1196 iv: *mut u8,
1197 iv_len: u32,
1198 ad: *mut u8,
1199 ad_len: u32,
1200 plain: *mut u8,
1201 plain_len: u32,
1202 cipher: *mut u8,
1203 tag: *mut u8,
1204 ) -> EverCrypt_Error_error_code;
1205}
1206extern "C" {
1207 #[doc = "WARNING: this function doesn't perform any dynamic\nhardware check. You MUST make sure your hardware supports the\nimplementation of AESGCM. Besides, this function was not designed\nfor cross-compilation: if you compile it on a system which doesn't\nsupport Vale, it will compile it to a function which makes the\nprogram exit."]
1208 pub fn EverCrypt_AEAD_encrypt_expand_aes128_gcm_no_check(
1209 k: *mut u8,
1210 iv: *mut u8,
1211 iv_len: u32,
1212 ad: *mut u8,
1213 ad_len: u32,
1214 plain: *mut u8,
1215 plain_len: u32,
1216 cipher: *mut u8,
1217 tag: *mut u8,
1218 ) -> EverCrypt_Error_error_code;
1219}
1220extern "C" {
1221 #[doc = "WARNING: this function doesn't perform any dynamic\nhardware check. You MUST make sure your hardware supports the\nimplementation of AESGCM. Besides, this function was not designed\nfor cross-compilation: if you compile it on a system which doesn't\nsupport Vale, it will compile it to a function which makes the\nprogram exit."]
1222 pub fn EverCrypt_AEAD_encrypt_expand_aes256_gcm_no_check(
1223 k: *mut u8,
1224 iv: *mut u8,
1225 iv_len: u32,
1226 ad: *mut u8,
1227 ad_len: u32,
1228 plain: *mut u8,
1229 plain_len: u32,
1230 cipher: *mut u8,
1231 tag: *mut u8,
1232 ) -> EverCrypt_Error_error_code;
1233}
1234extern "C" {
1235 pub fn EverCrypt_AEAD_encrypt_expand_aes128_gcm(
1236 k: *mut u8,
1237 iv: *mut u8,
1238 iv_len: u32,
1239 ad: *mut u8,
1240 ad_len: u32,
1241 plain: *mut u8,
1242 plain_len: u32,
1243 cipher: *mut u8,
1244 tag: *mut u8,
1245 ) -> EverCrypt_Error_error_code;
1246}
1247extern "C" {
1248 pub fn EverCrypt_AEAD_encrypt_expand_aes256_gcm(
1249 k: *mut u8,
1250 iv: *mut u8,
1251 iv_len: u32,
1252 ad: *mut u8,
1253 ad_len: u32,
1254 plain: *mut u8,
1255 plain_len: u32,
1256 cipher: *mut u8,
1257 tag: *mut u8,
1258 ) -> EverCrypt_Error_error_code;
1259}
1260extern "C" {
1261 pub fn EverCrypt_AEAD_encrypt_expand_chacha20_poly1305(
1262 k: *mut u8,
1263 iv: *mut u8,
1264 iv_len: u32,
1265 ad: *mut u8,
1266 ad_len: u32,
1267 plain: *mut u8,
1268 plain_len: u32,
1269 cipher: *mut u8,
1270 tag: *mut u8,
1271 ) -> EverCrypt_Error_error_code;
1272}
1273extern "C" {
1274 pub fn EverCrypt_AEAD_encrypt_expand(
1275 a: Spec_Agile_AEAD_alg,
1276 k: *mut u8,
1277 iv: *mut u8,
1278 iv_len: u32,
1279 ad: *mut u8,
1280 ad_len: u32,
1281 plain: *mut u8,
1282 plain_len: u32,
1283 cipher: *mut u8,
1284 tag: *mut u8,
1285 ) -> EverCrypt_Error_error_code;
1286}
1287extern "C" {
1288 #[doc = "Verify the authenticity of `ad` || `cipher` and decrypt `cipher` into `dst`.\n\n@param s Pointer to the The AEAD state created by `EverCrypt_AEAD_create_in`. It already contains the encryption key.\n@param iv Pointer to `iv_len` bytes of memory where the nonce is read from.\n@param iv_len Length of the nonce. Note: ChaCha20Poly1305 requires a 12 byte nonce.\n@param ad Pointer to `ad_len` bytes of memory where the associated data is read from.\n@param ad_len Length of the associated data.\n@param cipher Pointer to `cipher_len` bytes of memory where the ciphertext is read from.\n@param cipher_len Length of the ciphertext.\n@param tag Pointer to `TAG_LEN` bytes of memory where the tag is read from.\nThe length of the `tag` must be of a suitable length for the chosen algorithm:\n `Spec_Agile_AEAD_AES128_GCM` (TAG_LEN=16)\n `Spec_Agile_AEAD_AES256_GCM` (TAG_LEN=16)\n `Spec_Agile_AEAD_CHACHA20_POLY1305` (TAG_LEN=16)\n@param dst Pointer to `cipher_len` bytes of memory where the decrypted plaintext will be written to.\n\n@return `EverCrypt_AEAD_decrypt` returns ...\n\n `EverCrypt_Error_Success`\n\n... on success and either of ...\n\n `EverCrypt_Error_InvalidKey` (returned if and only if the `s` parameter is `NULL`),\n `EverCrypt_Error_InvalidIVLength` (see note about requirements on IV size above), or\n `EverCrypt_Error_AuthenticationFailure` (in case the ciphertext could not be authenticated, e.g., due to modifications)\n\n... on failure (`EverCrypt_error.h`).\n\nUpon success, the plaintext will be written into `dst`."]
1289 pub fn EverCrypt_AEAD_decrypt(
1290 s: *mut EverCrypt_AEAD_state_s,
1291 iv: *mut u8,
1292 iv_len: u32,
1293 ad: *mut u8,
1294 ad_len: u32,
1295 cipher: *mut u8,
1296 cipher_len: u32,
1297 tag: *mut u8,
1298 dst: *mut u8,
1299 ) -> EverCrypt_Error_error_code;
1300}
1301extern "C" {
1302 #[doc = "WARNING: this function doesn't perform any dynamic\nhardware check. You MUST make sure your hardware supports the\nimplementation of AESGCM. Besides, this function was not designed\nfor cross-compilation: if you compile it on a system which doesn't\nsupport Vale, it will compile it to a function which makes the\nprogram exit."]
1303 pub fn EverCrypt_AEAD_decrypt_expand_aes128_gcm_no_check(
1304 k: *mut u8,
1305 iv: *mut u8,
1306 iv_len: u32,
1307 ad: *mut u8,
1308 ad_len: u32,
1309 cipher: *mut u8,
1310 cipher_len: u32,
1311 tag: *mut u8,
1312 dst: *mut u8,
1313 ) -> EverCrypt_Error_error_code;
1314}
1315extern "C" {
1316 #[doc = "WARNING: this function doesn't perform any dynamic\nhardware check. You MUST make sure your hardware supports the\nimplementation of AESGCM. Besides, this function was not designed\nfor cross-compilation: if you compile it on a system which doesn't\nsupport Vale, it will compile it to a function which makes the\nprogram exit."]
1317 pub fn EverCrypt_AEAD_decrypt_expand_aes256_gcm_no_check(
1318 k: *mut u8,
1319 iv: *mut u8,
1320 iv_len: u32,
1321 ad: *mut u8,
1322 ad_len: u32,
1323 cipher: *mut u8,
1324 cipher_len: u32,
1325 tag: *mut u8,
1326 dst: *mut u8,
1327 ) -> EverCrypt_Error_error_code;
1328}
1329extern "C" {
1330 pub fn EverCrypt_AEAD_decrypt_expand_aes128_gcm(
1331 k: *mut u8,
1332 iv: *mut u8,
1333 iv_len: u32,
1334 ad: *mut u8,
1335 ad_len: u32,
1336 cipher: *mut u8,
1337 cipher_len: u32,
1338 tag: *mut u8,
1339 dst: *mut u8,
1340 ) -> EverCrypt_Error_error_code;
1341}
1342extern "C" {
1343 pub fn EverCrypt_AEAD_decrypt_expand_aes256_gcm(
1344 k: *mut u8,
1345 iv: *mut u8,
1346 iv_len: u32,
1347 ad: *mut u8,
1348 ad_len: u32,
1349 cipher: *mut u8,
1350 cipher_len: u32,
1351 tag: *mut u8,
1352 dst: *mut u8,
1353 ) -> EverCrypt_Error_error_code;
1354}
1355extern "C" {
1356 pub fn EverCrypt_AEAD_decrypt_expand_chacha20_poly1305(
1357 k: *mut u8,
1358 iv: *mut u8,
1359 iv_len: u32,
1360 ad: *mut u8,
1361 ad_len: u32,
1362 cipher: *mut u8,
1363 cipher_len: u32,
1364 tag: *mut u8,
1365 dst: *mut u8,
1366 ) -> EverCrypt_Error_error_code;
1367}
1368extern "C" {
1369 pub fn EverCrypt_AEAD_decrypt_expand(
1370 a: Spec_Agile_AEAD_alg,
1371 k: *mut u8,
1372 iv: *mut u8,
1373 iv_len: u32,
1374 ad: *mut u8,
1375 ad_len: u32,
1376 cipher: *mut u8,
1377 cipher_len: u32,
1378 tag: *mut u8,
1379 dst: *mut u8,
1380 ) -> EverCrypt_Error_error_code;
1381}
1382extern "C" {
1383 #[doc = "Cleanup and free the AEAD state.\n\n@param s State of the AEAD algorithm."]
1384 pub fn EverCrypt_AEAD_free(s: *mut EverCrypt_AEAD_state_s);
1385}