val adh :
     #a:dh_alg
  -> aprivate_key a
  -> apublic_key a ->
  Tot (option (apublic_key a))
val adh :
     #a:dh_alg
  -> aprivate_key a
  -> apublic_key a ->
  Tot (option (apublic_key a))
let adh #a = DH.dh a
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 *)
/
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.aprivate_key a -> _: Spec.Noise.CryptoPrimitives.apublic_key a
  -> FStar.Pervasives.Native.option (Spec.Noise.CryptoPrimitives.apublic_key a)
Spec.Noise.CryptoPrimitives.dh_alg Spec.Agile.DH.dh Spec.Noise.CryptoPrimitives.aprivate_key Spec.Noise.CryptoPrimitives.apublic_key FStar.Pervasives.Native.option
let adh #a =
  
DH.dh a