val hkdf : hkdf_s
val hkdf : hkdf_s
let hkdf #nc ck k =
  let const1 = create 1 (u8 0x1) in
  let const2 = create 1 (u8 0x2) in
  let const3 = create 1 (u8 0x3) in
  let extracted = hmac nc ck k in
  let first = hmac nc extracted const1 in
  let second = hmac nc extracted (Seq.append first const2) in
  let third = hmac nc extracted (Seq.append second const3) in
  first, second, third
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

(*** Hash *)
let ado_hash a input =
  Hash.hash a input

(*** HMAC *)
let ahmac a =
  fun key data ->
  (**) ahash_max_input_norm_lem a;
  HMAC.hmac a key data
/
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
Spec.Noise.CryptoPrimitives.hkdf_s
Spec.Noise.CryptoPrimitives.config Spec.Noise.CryptoPrimitives.hash Lib.ByteSequence.bytes Prims.l_or Prims.b2t Prims.op_Equality Prims.int FStar.Seq.Base.length Lib.IntTypes.uint_t Lib.IntTypes.U8 Lib.IntTypes.SEC Prims.nat Spec.Noise.CryptoPrimitives.public_key_size FStar.Pervasives.Native.Mktuple3 Lib.Sequence.lseq Lib.IntTypes.int_t Spec.Noise.CryptoPrimitives.ahash_size Spec.Noise.CryptoPrimitives.get_hash_alg Spec.Noise.CryptoPrimitives.hmac FStar.Seq.Base.append FStar.Seq.Base.seq FStar.Seq.Base.create Lib.IntTypes.u8 FStar.Pervasives.Native.tuple3
let hkdf #nc ck k =
  
let const1 = create 1 (u8 0x1) in
let const2 = create 1 (u8 0x2) in
let const3 = create 1 (u8 0x3) in
let extracted = hmac nc ck k in
let first = hmac nc extracted const1 in
let second = hmac nc extracted (Seq.append first const2) in
let third = hmac nc extracted (Seq.append second const3) in
first, second, third