val aaead_decrypt :
     a:aead_alg
  -> aead_key
  -> aead_nonce
  -> aad:bytes{length aad <= aaead_max_input a}
  -> cipher:bytes{length cipher >= aead_tag_size /\
                  length cipher <= aaead_max_input a + aead_tag_size} ->
  Tot (option (r:bytes{length r + aead_tag_size == length cipher}))
val aaead_decrypt :
     a:aead_alg
  -> aead_key
  -> aead_nonce
  -> aad:bytes{length aad <= aaead_max_input a}
  -> cipher:bytes{length cipher >= aead_tag_size /\
                  length cipher <= aaead_max_input a + aead_tag_size} ->
  Tot (option (r:bytes{length r + aead_tag_size == length cipher}))
let aaead_decrypt a k n aad cipher =
  match a with
  | AES256_GCM ->
    (* We encode the nonce as BIG endian *)
    let n8 = uint_to_bytes_be (u64 n) in
    AEAD.decrypt #AES256_GCM k n8 aad cipher
  | 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.decrypt #CHACHA20_POLY1305 k n12 aad cipher
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 *)

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
/
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} ->
    cipher:
      Lib.ByteSequence.bytes
        { FStar.Seq.Base.length cipher >= Spec.Noise.CryptoPrimitives.aead_tag_size /\
          FStar.Seq.Base.length cipher <=
          Spec.Noise.CryptoPrimitives.aaead_max_input a + Spec.Noise.CryptoPrimitives.aead_tag_size
        }
  -> FStar.Pervasives.Native.option (r:
        Lib.ByteSequence.bytes
          { FStar.Seq.Base.length r + Spec.Noise.CryptoPrimitives.aead_tag_size ==
            FStar.Seq.Base.length cipher })
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 Prims.l_and Prims.op_GreaterThanOrEqual Spec.Noise.CryptoPrimitives.aead_tag_size Prims.op_Addition Spec.Agile.AEAD.decrypt 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 FStar.Pervasives.Native.option Prims.eq2 Prims.int
let aaead_decrypt a k n aad cipher =
  
match a with
| AES256_GCM ->
  let n8 = uint_to_bytes_be (u64 n) in
  AEAD.decrypt #AES256_GCM k n8 aad cipher
| CHACHA20_POLY1305 ->
  let n8 = uint_to_bytes_le (u64 n) in
  let n12 = (create 4 (u8 0)) @| n8 in
  AEAD.decrypt #CHACHA20_POLY1305 k n12 aad cipher