val aead_decrypt:
  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 -> // output: buffer for decrypted plaintext
  c:lbuffer uint8 mlen -> // input: cipher
  mac:lbuffer uint8 16ul -> // input: mac
  Stack UInt32.t
    (requires (fun h ->
      eq_or_disjoint m c /\
      live h k /\ live h n /\ live h aad /\ live h m /\ live h c /\ live h mac))
    (ensures  (fun h0 z h1 -> modifies (loc m) h0 h1 /\
      (let plain = Spec.aead_decrypt (as_seq h0 k) (as_seq h0 n) (as_seq h0 c) (as_seq h0 mac) (as_seq h0 aad) in
      match z with
      | 0ul -> Some? plain /\ as_seq h1 m == Some?.v plain // decryption succeeded
      | 1ul -> None? plain
      | _ -> false)  // decryption failed
      )
    )
let aead_decrypt 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_decrypt 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_decrypt k n aadlen aad mlen m cipher tag

  end else begin
    LowStar.Ignore.ignore vec128;
    LowStar.Ignore.ignore vec256;
    Hacl.Chacha20Poly1305_32.aead_decrypt k n aadlen aad mlen m cipher tag
  end
val aead_decrypt:
  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 -> // output: buffer for decrypted plaintext
  c:lbuffer uint8 mlen -> // input: cipher
  mac:lbuffer uint8 16ul -> // input: mac
  Stack UInt32.t
    (requires (fun h ->
      eq_or_disjoint m c /\
      live h k /\ live h n /\ live h aad /\ live h m /\ live h c /\ live h mac))
    (ensures  (fun h0 z h1 -> modifies (loc m) h0 h1 /\
      (let plain = Spec.aead_decrypt (as_seq h0 k) (as_seq h0 n) (as_seq h0 c) (as_seq h0 mac) (as_seq h0 aad) in
      match z with
      | 0ul -> Some? plain /\ as_seq h1 m == Some?.v plain // decryption succeeded
      | 1ul -> None? plain
      | _ -> false)  // decryption failed
      )
    )
let aead_decrypt 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_decrypt 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_decrypt k n aadlen aad mlen m cipher tag)
  else
    (LowStar.Ignore.ignore vec128;
      LowStar.Ignore.ignore vec256;
      Hacl.Chacha20Poly1305_32.aead_decrypt 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_decrypt FStar.UInt32.t Prims.unit LowStar.Ignore.ignore Prims.bool EverCrypt.TargetConfig.hacl_can_compile_vec128 Hacl.Chacha20Poly1305_128.aead_decrypt Hacl.Chacha20Poly1305_32.aead_decrypt 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"

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_decrypt:
  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 -> // output: buffer for decrypted plaintext
  c:lbuffer uint8 mlen -> // input: cipher
  mac:lbuffer uint8 16ul -> // input: mac
  Stack UInt32.t
    (requires (fun h ->
      eq_or_disjoint m c /\
      live h k /\ live h n /\ live h aad /\ live h m /\ live h c /\ live h mac))
    (ensures  (fun h0 z h1 -> modifies (loc m) h0 h1 /\
      (let plain = Spec.aead_decrypt (as_seq h0 k) (as_seq h0 n) (as_seq h0 c) (as_seq h0 mac) (as_seq h0 aad) in
      match z with
      | 0ul -> Some? plain /\ as_seq h1 m == Some?.v plain // decryption succeeded
      | 1ul -> None? plain
      | _ -> false)  // decryption failed
      )
    )

    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 ->
    c: Lib.Buffer.lbuffer Lib.IntTypes.uint8 mlen ->
    mac: Lib.Buffer.lbuffer Lib.IntTypes.uint8 16ul
  -> FStar.HyperStack.ST.Stack FStar.UInt32.t