val impls_params:config_impls_params nc
val impls_params:config_impls_params nc
let impls_params : config_impls_params nc = impls_params nc
/// 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"

inline_for_extraction noextract
let nc : config = DH_Curve25519, CHACHA20_POLY1305, Hash.Blake2S

[@@ T.postprocess_with (fun () -> T.norm [delta; zeta; iota; primops]; T.trefl())]
/
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
Impl.Noise.Extraction.config_impls_params Impl.Noise.API.Instances.Common_25519_ChaChaPoly_BLAKE2s.nc

FStar.Pervasives.Native.Mktuple3 Hacl.Impl.Curve25519.Fields.Core.field_spec Hacl.Impl.Poly1305.Fields.field_spec Hacl.Impl.Blake2.Core.m_spec Prims.eq2 Prims.bool FStar.Pervasives.Native.Mktuple2 Spec.Hash.Definitions.hash_alg Spec.Hash.Definitions.Blake2S FStar.Pervasives.Native.tuple2 Hacl.Impl.Curve25519.Fields.Core.M51 Hacl.Impl.Poly1305.Fields.M32 Hacl.Impl.Blake2.Core.M32
let impls_params:config_impls_params nc =
  
impls_params nc