val aead_encrypt_cp128 : aead_encrypt_st (S.Seal AEAD.CHACHA20_POLY1305)
let aead_encrypt_cp128 =
  fun _ key nonce alen aad len input output ->
    Hacl.Chacha20Poly1305_128.aead_encrypt key nonce alen aad len input (sub output 0ul len) (sub output len 16ul)
val aead_encrypt_cp128 : aead_encrypt_st (S.Seal AEAD.CHACHA20_POLY1305)
let aead_encrypt_cp128 =
fun _ key nonce alen aad len input output ->
  Hacl.Chacha20Poly1305_128.aead_encrypt key
    nonce
    alen
    aad
    len
    input
    (sub output 0ul len)
    (sub output len 16ul)
Hacl.HPKE.Interface.AEAD.fst.checked
Spec.Agile.AEAD.fst.checked prims.fst.checked Lib.Buffer.fsti.checked Hacl.Chacha20Poly1305_32.fst.checked Hacl.Chacha20Poly1305_256.fst.checked Hacl.Chacha20Poly1305_128.fst.checked FStar.UInt32.fsti.checked FStar.Pervasives.fsti.checked FStar.HyperStack.All.fst.checked FStar.HyperStack.fst.checked
Hacl.HPKE.Interface.AEAD.fst
Prims.squash Prims.l_and Prims.b2t Spec.Agile.HPKE.uu___is_Seal Spec.Agile.HPKE.Seal Spec.Agile.AEAD.CHACHA20_POLY1305 Spec.Agile.HPKE.is_valid_aead Hacl.HPKE.Interface.AEAD.kv Spec.Agile.HPKE.__proj__Seal__item__alg Hacl.HPKE.Interface.AEAD.iv Lib.IntTypes.size_t Prims.op_LessThanOrEqual Lib.IntTypes.v Lib.IntTypes.U32 Lib.IntTypes.PUB Spec.Agile.AEAD.max_length Lib.Buffer.lbuffer Lib.IntTypes.uint8 Prims.op_Addition Lib.IntTypes.max_size_t Lib.IntTypes.size Hacl.Chacha20Poly1305_128.aead_encrypt Prims.unit Lib.Buffer.lbuffer_t Lib.Buffer.MUT Lib.IntTypes.int_t Lib.IntTypes.U8 Lib.IntTypes.SEC FStar.UInt32.uint_to_t FStar.UInt32.t Lib.Buffer.sub FStar.UInt32.__uint_to_t
module Hacl.HPKE.Interface.AEAD

open FStar.HyperStack
open FStar.HyperStack.All

open Lib.Buffer

friend Spec.Agile.AEAD

/// These two functions will never be extracted, they are only an interface
/// boundary for the tactic performing instantiations.
/// In other files, it is exposed as an assume val, but for AEAD, we need an fsti
/// since we need to friend Spec.Agile.AEAD to perform the instantiations below,
/// and assume val are forbidden in interface files
let aead_encrypt #cs = admit()
let aead_decrypt #cs = admit()

#set-options "--z3rlimit 60 --fuel 0 --ifuel 0"

inline_for_extraction noextract
let aead_encrypt_cp32 =
  fun _ key nonce alen aad len input output ->
    Hacl.Chacha20Poly1305_32.aead_encrypt key nonce alen aad len input (sub output 0ul len) (sub output len 16ul)

inline_for_extraction noextract
let aead_decrypt_cp32 =
  fun _ key nonce alen aad len input output ->
    Hacl.Chacha20Poly1305_32.aead_decrypt key nonce alen aad len input (sub output 0ul len) (sub output len 16ul)

inline_for_extraction noextract
val aead_encrypt_cp128 : aead_encrypt_st (S.Seal AEAD.CHACHA20_POLY1305)
Hacl.HPKE.Interface.AEAD.aead_encrypt_st (Spec.Agile.HPKE.Seal Spec.Agile.AEAD.CHACHA20_POLY1305)