val aaead_encrypt :
     a:aead_alg
  -> aead_key
  -> aead_nonce
  -> aad:bytes{length aad <= aaead_max_input a}
  -> msg:bytes{length msg <= aaead_max_input a} ->
  Tot (r:bytes{length r == length msg + aead_tag_size})
val aaead_encrypt :
     a:aead_alg
  -> aead_key
  -> aead_nonce
  -> aad:bytes{length aad <= aaead_max_input a}
  -> msg:bytes{length msg <= aaead_max_input a} ->
  Tot (r:bytes{length r == length msg + aead_tag_size})
let aaead_encrypt a k n aad msg =
  match a with
  | AES256_GCM ->
    (* We encode the nonce as BIG endian *)
    let n8 = uint_to_bytes_be (u64 n) in
    AEAD.encrypt #AES256_GCM k n8 aad msg
  | CHACHA20_POLY1305 ->
    (* We encode the nonce as LITTLE endian *)
    let n8 = uint_to_bytes_le (u64 n) in
    let n12 = (create 4 (u8 0)) @| n8 in
    AEAD.encrypt #CHACHA20_POLY1305 k n12 aad msg
module Spec.Noise.CryptoPrimitives

open Lib.IntTypes
open Lib.Sequence
open Lib.ByteSequence
module S = Lib.Sequence
open FStar.Seq

#set-options "--z3rlimit 15 --fuel 0 --ifuel 1"

/// DH : we support Curve25519
// Remark: Noise also supports Curve448
module DH = Spec.Agile.DH
open Spec.Agile.DH

/// AEAD : we support AES256 GCM and Chacha20Poly1305
module AEAD = Spec.Agile.AEAD
open Spec.Agile.AEAD

/// Hash : we support SHA2 256, SHA2 512 and Blake2
module Hash = Spec.Agile.Hash
open Spec.Agile.Hash
module HMAC = Spec.Agile.HMAC
open Spec.Agile.HMAC
module HKDF = Spec.Agile.HKDF
open Spec.Agile.HKDF

(* We reopen ByteSequence because [lbytes] is redefined there many times in HACL,
 * and sometimes doesn't have exactly the same definition. *)
open Lib.ByteSequence

open FStar.Mul

friend Spec.Agile.HKDF

/// For .fsti/.fst alignment purposes
let _align_beg = ()

(*** DH *)

let adh #a = DH.dh a

(*** AEAD *)
/
Spec.Agile.HMAC.fsti.checked Spec.Agile.HKDF.fst.checked Spec.Agile.HKDF.fst.checked Spec.Agile.Hash.fsti.checked Spec.Agile.DH.fst.checked Spec.Agile.AEAD.fsti.checked prims.fst.checked Lib.Sequence.fsti.checked Lib.IntTypes.fsti.checked Lib.ByteSequence.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked
Spec.Noise.CryptoPrimitives.fst

    a: Spec.Noise.CryptoPrimitives.aead_alg ->
    k: Spec.Noise.CryptoPrimitives.aead_key ->
    n: Spec.Noise.CryptoPrimitives.aead_nonce ->
    aad:
      Lib.ByteSequence.bytes
        {FStar.Seq.Base.length aad <= Spec.Noise.CryptoPrimitives.aaead_max_input a} ->
    msg:
      Lib.ByteSequence.bytes
        {FStar.Seq.Base.length msg <= Spec.Noise.CryptoPrimitives.aaead_max_input a}
  -> r:
    Lib.ByteSequence.bytes
      { FStar.Seq.Base.length r ==
        FStar.Seq.Base.length msg + Spec.Noise.CryptoPrimitives.aead_tag_size }
Spec.Noise.CryptoPrimitives.aead_alg Spec.Noise.CryptoPrimitives.aead_key Spec.Noise.CryptoPrimitives.aead_nonce Lib.ByteSequence.bytes Prims.b2t Prims.op_LessThanOrEqual FStar.Seq.Base.length Lib.IntTypes.uint_t Lib.IntTypes.U8 Lib.IntTypes.SEC Spec.Noise.CryptoPrimitives.aaead_max_input Spec.Agile.AEAD.encrypt Spec.Agile.AEAD.AES256_GCM Lib.Sequence.lseq Lib.IntTypes.int_t Lib.ByteSequence.uint_to_bytes_be Lib.IntTypes.U64 Lib.IntTypes.u64 Spec.Agile.AEAD.CHACHA20_POLY1305 FStar.Seq.Base.seq FStar.Seq.Base.op_At_Bar FStar.Seq.Base.create Lib.IntTypes.u8 Lib.ByteSequence.uint_to_bytes_le Prims.eq2 Prims.int Prims.op_Addition Spec.Noise.CryptoPrimitives.aead_tag_size
let aaead_encrypt a k n aad msg =
  
match a with
| AES256_GCM ->
  let n8 = uint_to_bytes_be (u64 n) in
  AEAD.encrypt #AES256_GCM k n8 aad msg
| CHACHA20_POLY1305 ->
  let n8 = uint_to_bytes_le (u64 n) in
  let n12 = (create 4 (u8 0)) @| n8 in
  AEAD.encrypt #CHACHA20_POLY1305 k n12 aad msg