val ado_hash :
     a:hash_alg
  -> input:bytes{length input <= ahash_max_input a} ->
  Tot (ahash a)
val ado_hash :
     a:hash_alg
  -> input:bytes{length input <= ahash_max_input a} ->
  Tot (ahash a)
let ado_hash a input =
  Hash.hash a input
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

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

let aaead_correctness a k n aad msg =
  match a with
  | AES256_GCM ->
    let n8 = uint_to_bytes_be (u64 n) in
    AEAD.correctness #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.correctness #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.hash_alg ->
    input:
      Lib.ByteSequence.bytes
        {FStar.Seq.Base.length input <= Spec.Noise.CryptoPrimitives.ahash_max_input a}
  -> Spec.Noise.CryptoPrimitives.ahash a
Spec.Noise.CryptoPrimitives.hash_alg 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.ahash_max_input Spec.Agile.Hash.hash Spec.Noise.CryptoPrimitives.ahash
let ado_hash a input =
  
Hash.hash a input