val aead_encrypt:
  k:lbuffer uint8 32ul -> // key
  n:lbuffer uint8 12ul -> // nonce
  aadlen:size_t ->
  aad:lbuffer uint8 aadlen ->
  (mlen:size_t{v mlen + 16 <= max_size_t /\ v aadlen + v mlen / 64 <= max_size_t}) ->
  m:lbuffer uint8 mlen -> // input: plaintext
  cipher:lbuffer uint8 mlen -> // output: buffer for cipher + mac
  tag:lbuffer uint8 16ul -> // output: buffer for cipher + mac
  Stack unit
    (requires (fun h ->
      disjoint k cipher /\ disjoint n cipher /\
      disjoint k tag /\ disjoint n tag /\
      disjoint cipher tag /\
      eq_or_disjoint m cipher /\
      disjoint aad cipher /\
      live h k /\ live h n /\ live h aad /\ live h m /\ live h cipher /\ live h tag))
    (ensures  (fun h0 _ h1 -> modifies (loc cipher |+| loc tag) h0 h1 /\
      Seq.equal
        (Seq.concat (as_seq h1 cipher) (as_seq h1 tag))
        (Spec.aead_encrypt (as_seq h0 k) (as_seq h0 n) (as_seq h0 m) (as_seq h0 aad))))
let aead_encrypt k n aadlen aad mlen m cipher tag =
  let vec256 = EverCrypt.AutoConfig2.has_vec256 () in
  let vec128 = EverCrypt.AutoConfig2.has_vec128 () in
  if EverCrypt.TargetConfig.hacl_can_compile_vec256 && vec256 then begin
    LowStar.Ignore.ignore vec128;
    Hacl.Chacha20Poly1305_256.aead_encrypt k n aadlen aad mlen m cipher tag
  end else if EverCrypt.TargetConfig.hacl_can_compile_vec128 && vec128 then begin
    LowStar.Ignore.ignore vec256;
    Hacl.Chacha20Poly1305_128.aead_encrypt k n aadlen aad mlen m cipher tag

  end else begin
    LowStar.Ignore.ignore vec128;
    LowStar.Ignore.ignore vec256;
    Hacl.Chacha20Poly1305_32.aead_encrypt k n aadlen aad mlen m cipher tag
  end
val aead_encrypt:
  k:lbuffer uint8 32ul -> // key
  n:lbuffer uint8 12ul -> // nonce
  aadlen:size_t ->
  aad:lbuffer uint8 aadlen ->
  (mlen:size_t{v mlen + 16 <= max_size_t /\ v aadlen + v mlen / 64 <= max_size_t}) ->
  m:lbuffer uint8 mlen -> // input: plaintext
  cipher:lbuffer uint8 mlen -> // output: buffer for cipher + mac
  tag:lbuffer uint8 16ul -> // output: buffer for cipher + mac
  Stack unit
    (requires (fun h ->
      disjoint k cipher /\ disjoint n cipher /\
      disjoint k tag /\ disjoint n tag /\
      disjoint cipher tag /\
      eq_or_disjoint m cipher /\
      disjoint aad cipher /\
      live h k /\ live h n /\ live h aad /\ live h m /\ live h cipher /\ live h tag))
    (ensures  (fun h0 _ h1 -> modifies (loc cipher |+| loc tag) h0 h1 /\
      Seq.equal
        (Seq.concat (as_seq h1 cipher) (as_seq h1 tag))
        (Spec.aead_encrypt (as_seq h0 k) (as_seq h0 n) (as_seq h0 m) (as_seq h0 aad))))
let aead_encrypt k n aadlen aad mlen m cipher tag =
let vec256 = EverCrypt.AutoConfig2.has_vec256 () in
let vec128 = EverCrypt.AutoConfig2.has_vec128 () in
if EverCrypt.TargetConfig.hacl_can_compile_vec256 && vec256
then
  (LowStar.Ignore.ignore vec128;
    Hacl.Chacha20Poly1305_256.aead_encrypt k n aadlen aad mlen m cipher tag)
else
  if EverCrypt.TargetConfig.hacl_can_compile_vec128 && vec128
  then
    (LowStar.Ignore.ignore vec256;
      Hacl.Chacha20Poly1305_128.aead_encrypt k n aadlen aad mlen m cipher tag)
  else
    (LowStar.Ignore.ignore vec128;
      LowStar.Ignore.ignore vec256;
      Hacl.Chacha20Poly1305_32.aead_encrypt k n aadlen aad mlen m cipher tag)
EverCrypt.Chacha20Poly1305.fst.checked
Spec.Chacha20Poly1305.fst.checked prims.fst.checked LowStar.Ignore.fsti.checked Lib.Sequence.fsti.checked Lib.IntTypes.fsti.checked Lib.ByteBuffer.fsti.checked Lib.Buffer.fsti.checked Hacl.Chacha20Poly1305_32.fst.checked Hacl.Chacha20Poly1305_256.fst.checked Hacl.Chacha20Poly1305_128.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.All.fst.checked FStar.HyperStack.fst.checked EverCrypt.TargetConfig.fsti.checked EverCrypt.AutoConfig2.fsti.checked
EverCrypt.Chacha20Poly1305.fst
Lib.Buffer.lbuffer Lib.IntTypes.uint8 FStar.UInt32.__uint_to_t Lib.IntTypes.size_t Prims.l_and Prims.b2t Prims.op_LessThanOrEqual Prims.op_Addition Lib.IntTypes.v Lib.IntTypes.U32 Lib.IntTypes.PUB Lib.IntTypes.max_size_t Prims.op_Division Prims.op_AmpAmp EverCrypt.TargetConfig.hacl_can_compile_vec256 Hacl.Chacha20Poly1305_256.aead_encrypt Prims.unit LowStar.Ignore.ignore Prims.bool EverCrypt.TargetConfig.hacl_can_compile_vec128 Hacl.Chacha20Poly1305_128.aead_encrypt Hacl.Chacha20Poly1305_32.aead_encrypt EverCrypt.AutoConfig2.has_vec128 EverCrypt.AutoConfig2.has_vec256
module EverCrypt.Chacha20Poly1305

module ST = FStar.HyperStack.ST
open FStar.HyperStack
open FStar.HyperStack.All
open Lib.IntTypes
open Lib.Buffer
open Lib.ByteBuffer
module Seq = Lib.Sequence
open FStar.Mul

module Spec = Spec.Chacha20Poly1305

#set-options "--max_fuel 0 --max_ifuel 0 --z3rlimit 20"
val aead_encrypt:
  k:lbuffer uint8 32ul -> // key
  n:lbuffer uint8 12ul -> // nonce
  aadlen:size_t ->
  aad:lbuffer uint8 aadlen ->
  (mlen:size_t{v mlen + 16 <= max_size_t /\ v aadlen + v mlen / 64 <= max_size_t}) ->
  m:lbuffer uint8 mlen -> // input: plaintext
  cipher:lbuffer uint8 mlen -> // output: buffer for cipher + mac
  tag:lbuffer uint8 16ul -> // output: buffer for cipher + mac
  Stack unit
    (requires (fun h ->
      disjoint k cipher /\ disjoint n cipher /\
      disjoint k tag /\ disjoint n tag /\
      disjoint cipher tag /\
      eq_or_disjoint m cipher /\
      disjoint aad cipher /\
      live h k /\ live h n /\ live h aad /\ live h m /\ live h cipher /\ live h tag))
    (ensures  (fun h0 _ h1 -> modifies (loc cipher |+| loc tag) h0 h1 /\
      Seq.equal
        (Seq.concat (as_seq h1 cipher) (as_seq h1 tag))
        (Spec.aead_encrypt (as_seq h0 k) (as_seq h0 n) (as_seq h0 m) (as_seq h0 aad))))

    k: Lib.Buffer.lbuffer Lib.IntTypes.uint8 32ul ->
    n: Lib.Buffer.lbuffer Lib.IntTypes.uint8 12ul ->
    aadlen: Lib.IntTypes.size_t ->
    aad: Lib.Buffer.lbuffer Lib.IntTypes.uint8 aadlen ->
    mlen:
      Lib.IntTypes.size_t
        { Lib.IntTypes.v mlen + 16 <= Lib.IntTypes.max_size_t /\
          Lib.IntTypes.v aadlen + Lib.IntTypes.v mlen / 64 <= Lib.IntTypes.max_size_t } ->
    m: Lib.Buffer.lbuffer Lib.IntTypes.uint8 mlen ->
    cipher: Lib.Buffer.lbuffer Lib.IntTypes.uint8 mlen ->
    tag: Lib.Buffer.lbuffer Lib.IntTypes.uint8 16ul
  -> FStar.HyperStack.ST.Stack Prims.unit