val aead_decrypt:aead_decrypt_st M32
let aead_decrypt : aead_decrypt_st M32 =
  chacha20poly1305_aead_decrypt_higher #M32 True Hacl.Chacha20.chacha20_encrypt poly1305_do_32
val aead_decrypt:aead_decrypt_st M32
let aead_decrypt:aead_decrypt_st M32 =
chacha20poly1305_aead_decrypt_higher #M32 True Hacl.Chacha20.chacha20_encrypt poly1305_do_32
Hacl.Chacha20Poly1305_32.fst.checked
prims.fst.checked Hacl.Poly1305_32.fsti.checked Hacl.Meta.Chacha20Poly1305.fst.checked Hacl.Impl.Poly1305.Fields.fst.checked Hacl.Impl.Chacha20Poly1305.PolyCore.fst.checked Hacl.Impl.Chacha20Poly1305.fst.checked Hacl.Chacha20.fst.checked FStar.Pervasives.fsti.checked
Hacl.Chacha20Poly1305_32.fst
Hacl.Meta.Chacha20Poly1305.chacha20poly1305_aead_decrypt_higher Hacl.Impl.Poly1305.Fields.M32 Prims.l_True Hacl.Chacha20.chacha20_encrypt Hacl.Chacha20Poly1305_32.poly1305_do_32
module Hacl.Chacha20Poly1305_32

open Hacl.Meta.Chacha20Poly1305
open Hacl.Impl.Chacha20Poly1305
open Hacl.Impl.Poly1305.Fields
open Hacl.Poly1305_32

#set-options "--z3rlimit 50 --max_fuel 0 --max_ifuel 0"

[@CInline]
private
let poly1305_padded_32 = Hacl.Impl.Chacha20Poly1305.PolyCore.poly1305_padded #M32

[@CInline]
private
let poly1305_do_32 = chacha20poly1305_poly1305_do_higher #M32 True poly1305_finish poly1305_init poly1305_padded_32

[@@ Comment "Encrypt a message `m` with key `k`.

The arguments `k`, `n`, `aadlen`, and `aad` are same in encryption/decryption.
Note: Encryption and decryption can be executed in-place, i.e., `m` and `cipher` can point to the same memory.

@param k Pointer to 32 bytes of memory where the AEAD key is read from.
@param n Pointer to 12 bytes of memory where the AEAD nonce is read from.
@param aadlen Length of the associated data.
@param aad Pointer to `aadlen` bytes of memory where the associated data is read from.

@param mlen Length of the message.
@param m Pointer to `mlen` bytes of memory where the message is read from.
@param cipher Pointer to `mlen` bytes of memory where the ciphertext is written to.
@param mac Pointer to 16 bytes of memory where the mac is written to."]
let aead_encrypt : aead_encrypt_st M32 =
  chacha20poly1305_aead_encrypt_higher #M32 True poly1305_do_32 Hacl.Chacha20.chacha20_encrypt

[@@ Comment "Decrypt a ciphertext `cipher` with key `k`.

The arguments `k`, `n`, `aadlen`, and `aad` are same in encryption/decryption.
Note: Encryption and decryption can be executed in-place, i.e., `m` and `cipher` can point to the same memory.

If decryption succeeds, the resulting plaintext is stored in `m` and the function returns the success code 0.
If decryption fails, the array `m` remains unchanged and the function returns the error code 1.

@param k Pointer to 32 bytes of memory where the AEAD key is read from.
@param n Pointer to 12 bytes of memory where the AEAD nonce is read from.
@param aadlen Length of the associated data.
@param aad Pointer to `aadlen` bytes of memory where the associated data is read from.

@param mlen Length of the ciphertext.
@param m Pointer to `mlen` bytes of memory where the message is written to.
@param cipher Pointer to `mlen` bytes of memory where the ciphertext is read from.
@param mac Pointer to 16 bytes of memory where the mac is read from.

@returns 0 on succeess; 1 on failure."]
val aead_decrypt:aead_decrypt_st M32
Hacl.Impl.Chacha20Poly1305.aead_decrypt_st Hacl.Impl.Poly1305.Fields.M32