val impls_params (c: config) : config_impls_params c
val impls_params (c: config) : config_impls_params c
let impls_params (c : config) : config_impls_params c =
  dh_alg_to_field (get_dh_alg c),
  aead_alg_to_field (get_aead_alg c),
  hash_alg_to_field (get_hash_alg c)
/// This module provides common definitions used for the instantiations of
/// the Noise API

module Impl.Noise.API.Instances.Common
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

#set-options "--z3rlimit 50 --fuel 0 --ifuel 1"

module ImplCFields = Hacl.Impl.Curve25519.Fields.Core
module ImplPolyFields = Hacl.Impl.Poly1305.Fields
module ImplBlake2Core = Hacl.Impl.Blake2.Core

let dh_alg_to_field (a : dh_alg) : dh_field_spec a =
  match a with
  | DH_Curve25519 -> ImplCFields.M51

let aead_alg_to_field (a : aead_alg) : aead_field_spec a =
  match a with
  | AES256_GCM -> ()
  | CHACHA20_POLY1305 -> ImplPolyFields.M32

let hash_alg_to_field (a : Spec.Noise.CryptoPrimitives.hash_alg) : hash_field_spec a =
  match a with
  | SHA2_256 | SHA2_512 -> ()
  | Hash.Blake2S -> ImplBlake2Core.M32
  | Hash.Blake2B -> ImplBlake2Core.M32
/
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.RecursiveMessages.fst.checked Impl.Noise.Extraction.fst.checked Impl.Noise.CryptoPrimitives.fsti.checked Impl.Noise.API.State.StateMachine.fst.checked Impl.Noise.API.DState.fsti.checked Hacl.Impl.Poly1305.Fields.fst.checked Hacl.Impl.Curve25519.Fields.Core.fsti.checked Hacl.Impl.Blake2.Core.fsti.checked FStar.Tactics.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked
Impl.Noise.API.Instances.Common.fst
c: Spec.Noise.CryptoPrimitives.config -> Impl.Noise.Extraction.config_impls_params c
Spec.Noise.CryptoPrimitives.config FStar.Pervasives.Native.Mktuple3 Impl.Noise.CryptoPrimitives.dh_field_spec Spec.Noise.CryptoPrimitives.get_dh_alg Impl.Noise.CryptoPrimitives.aead_field_spec Spec.Noise.CryptoPrimitives.get_aead_alg Impl.Noise.CryptoPrimitives.hash_field_spec Spec.Noise.CryptoPrimitives.get_hash_alg Impl.Noise.API.Instances.Common.dh_alg_to_field Impl.Noise.API.Instances.Common.aead_alg_to_field Impl.Noise.API.Instances.Common.hash_alg_to_field Impl.Noise.Extraction.config_impls_params
let impls_params (c: config) : config_impls_params c =
  
dh_alg_to_field (get_dh_alg c),
aead_alg_to_field (get_aead_alg c),
hash_alg_to_field (get_hash_alg c)