val impls_params:config_impls_params Spec.Noise.Instances.wgc
val impls_params:config_impls_params Spec.Noise.Instances.wgc
let impls_params : config_impls_params Spec.Noise.Instances.wgc =
  ImplCFields.M51, ImplPolyFields.M32, ImplBlake2Core.M32
module Impl.Noise.Instances

open Lib.Buffer

module Spec = Spec.Noise.Instances
open Spec.Noise
open Impl.Noise.Extraction
open Impl.Noise.PatternMessages

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

#set-options "--z3rlimit 15 --fuel 0 --ifuel 0"
/
Spec.Noise.Instances.fst.checked Spec.Noise.fst.checked prims.fst.checked Lib.IntTypes.fsti.checked Lib.Buffer.fsti.checked Impl.Noise.PatternMessages.fst.checked Impl.Noise.Extraction.fst.checked Hacl.Impl.Poly1305.Fields.fst.checked Hacl.Impl.Curve25519.Fields.Core.fsti.checked Hacl.Impl.Blake2.Core.fsti.checked FStar.UInt32.fsti.checked FStar.Tactics.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked
Impl.Noise.Instances.fst
Impl.Noise.Extraction.config_impls_params Spec.Noise.Instances.wgc
FStar.Pervasives.Native.Mktuple3 Impl.Noise.CryptoPrimitives.dh_field_spec Spec.Noise.CryptoPrimitives.get_dh_alg Spec.Noise.Instances.wgc Impl.Noise.CryptoPrimitives.aead_field_spec Spec.Noise.CryptoPrimitives.get_aead_alg Impl.Noise.CryptoPrimitives.hash_field_spec Spec.Noise.CryptoPrimitives.get_hash_alg Hacl.Impl.Curve25519.Fields.Core.M51 Hacl.Impl.Poly1305.Fields.M32 Hacl.Impl.Blake2.Core.M32
let impls_params:config_impls_params Spec.Noise.Instances.wgc =
  
ImplCFields.M51, ImplPolyFields.M32, ImplBlake2Core.M32