val nc:config
val nc:config
let nc : config = DH_Curve25519, CHACHA20_POLY1305, Hash.Blake2S
/// This module defines a configuration and specializes the protocol functions for
/// this configuration.

module Impl.Noise.API.Instances.Common_25519_ChaChaPoly_BLAKE2s
open Impl.Noise.Extraction
open Meta.Noise
open FStar.Tactics
open Spec.Noise.CryptoPrimitives
open Impl.Noise.CryptoPrimitives

module DH = Spec.Agile.DH
open Spec.Agile.DH

module AEAD = Spec.Agile.AEAD
open Spec.Agile.AEAD

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

module T = FStar.Tactics
open Impl.Noise.API.Instances.Common

#set-options "--z3rlimit 50 --fuel 0 --ifuel 0"
/
Spec.Noise.CryptoPrimitives.fsti.checked Spec.Agile.HMAC.fsti.checked Spec.Agile.HKDF.fsti.checked Spec.Agile.Hash.fsti.checked Spec.Agile.DH.fst.checked Spec.Agile.AEAD.fsti.checked prims.fst.checked Meta.Noise.fsti.checked Impl.Noise.Extraction.fst.checked Impl.Noise.CryptoPrimitives.fsti.checked Impl.Noise.API.Instances.Common.fst.checked FStar.Tactics.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked
Impl.Noise.API.Instances.Common_25519_ChaChaPoly_BLAKE2s.fst
Spec.Noise.CryptoPrimitives.config
FStar.Pervasives.Native.Mktuple3 Spec.Noise.CryptoPrimitives.dh_alg Spec.Noise.CryptoPrimitives.aead_alg Spec.Noise.CryptoPrimitives.hash_alg Spec.Agile.DH.DH_Curve25519 Spec.Agile.AEAD.CHACHA20_POLY1305 Spec.Hash.Definitions.Blake2S
let nc:config =
  
DH_Curve25519, CHACHA20_POLY1305, Hash.Blake2S