val initialize_IKpsk2 : initiator: FStar.Ghost.erased Prims.bool ->
    pname_len: Impl.Noise.Types.hashable_size_t Impl.Noise.Instances.wg_inc ->
    protocol_name: Impl.Noise.Types.hashable_t Impl.Noise.Instances.wg_inc pname_len ->
    prlg_len: Impl.Noise.Types.hashable_size_t Impl.Noise.Instances.wg_inc ->
    prologue: Impl.Noise.Types.hashable_t Impl.Noise.Instances.wg_inc prlg_len ->
    spriv: Impl.Noise.Types.opt_private_key_t Impl.Noise.Instances.wg_inc ->
    spub: Impl.Noise.Types.opt_public_key_t Impl.Noise.Instances.wg_inc ->
    epriv: Impl.Noise.Types.opt_private_key_t Impl.Noise.Instances.wg_inc ->
    epub: Impl.Noise.Types.opt_public_key_t Impl.Noise.Instances.wg_inc ->
    psk: Impl.Noise.Types.opt_preshared_key_t ->
    st: Impl.Noise.FlatStructures.handshake_state_t Impl.Noise.Instances.wg_inc
  -> FStar.HyperStack.ST.Stack (Impl.Noise.Types.rtype Impl.Noise.Types.hash_return_type)
let initialize_IKpsk2 =
  initialize hski Spec.pattern_IKpsk2
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"

inline_for_extraction noextract
let impls_params : config_impls_params Spec.Noise.Instances.wgc =
  ImplCFields.M51, ImplPolyFields.M32, ImplBlake2Core.M32

%splice[dh; aead_encrypt; aead_decrypt; hash; aead_encrypt; aead_decrypt; wg_inc; hski]
(generate_pattern_declarations true impls_params default_extract_decls_params "wg_inc" "hski")

(*** IKpsk2 *)
(**** General functions *)
(* initialization *)
/
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

    initiator: FStar.Ghost.erased Prims.bool ->
    pname_len: Impl.Noise.Types.hashable_size_t Impl.Noise.Instances.wg_inc ->
    protocol_name: Impl.Noise.Types.hashable_t Impl.Noise.Instances.wg_inc pname_len ->
    prlg_len: Impl.Noise.Types.hashable_size_t Impl.Noise.Instances.wg_inc ->
    prologue: Impl.Noise.Types.hashable_t Impl.Noise.Instances.wg_inc prlg_len ->
    spriv: Impl.Noise.Types.opt_private_key_t Impl.Noise.Instances.wg_inc ->
    spub: Impl.Noise.Types.opt_public_key_t Impl.Noise.Instances.wg_inc ->
    epriv: Impl.Noise.Types.opt_private_key_t Impl.Noise.Instances.wg_inc ->
    epub: Impl.Noise.Types.opt_public_key_t Impl.Noise.Instances.wg_inc ->
    psk: Impl.Noise.Types.opt_preshared_key_t ->
    st: Impl.Noise.FlatStructures.handshake_state_t Impl.Noise.Instances.wg_inc
  -> FStar.HyperStack.ST.Stack (Impl.Noise.Types.rtype Impl.Noise.Types.hash_return_type)
FStar.Ghost.erased Prims.bool Impl.Noise.Types.hashable_size_t Impl.Noise.Instances.wg_inc Impl.Noise.Types.hashable_t Impl.Noise.Types.opt_private_key_t Impl.Noise.Types.opt_public_key_t Impl.Noise.Types.opt_preshared_key_t Impl.Noise.FlatStructures.handshake_state_t Impl.Noise.CipherState.cipher_state_m Impl.Noise.Types.chaining_key_t Impl.Noise.Types.hash_t Impl.Noise.HandshakeState.initialize_handshake_state_m Impl.Noise.HandshakeState.ssdhi_get_ssi Impl.Noise.Instances.ssdhi Prims.op_Negation Impl.Noise.Types.rtype Impl.Noise.Types.hash_return_type Impl.Noise.TypeOrUnit.preshared_key_t_or_unit Impl.Noise.Types.is_null Lib.Buffer.MUT Lib.IntTypes.uint8 Impl.Noise.TypeOrUnit.public_key_t_or_unit Impl.Noise.TypeOrUnit.private_key_t_or_unit Prims.unit Spec.Noise.Base.Lemmas.initialize_unfold_lem Impl.Noise.Types.get_config Lib.Buffer.op_Brack_Lens_Access Impl.Noise.FlatStructures.eval_opt_split_keypair Impl.Noise.Types.eval_opt_preshared_key Impl.Noise.FlatStructures.eval_handshake_state_eq FStar.Ghost.reveal Spec.Noise.MetaInfo.meta_info Prims._assert Impl.Noise.HandshakeState.hsm_inv Impl.Noise.FlatStructures.handshake_state_t_to_m_impl_hsm_inv FStar.Ghost.hide Spec.Noise.MetaInfo.initialize_post_smi Spec.Noise.Base.Definitions.Mkhandshake_pattern FStar.Pervasives.Native.None Prims.list Spec.Noise.Base.Definitions.premessage_token FStar.Pervasives.Native.Some Prims.Cons Spec.Noise.Base.Definitions.PS Prims.Nil Spec.Noise.Base.Definitions.message_token Spec.Noise.Base.Definitions.E Spec.Noise.Base.Definitions.ES Spec.Noise.Base.Definitions.S Spec.Noise.Base.Definitions.SS Spec.Noise.Base.Definitions.EE Spec.Noise.Base.Definitions.SE Spec.Noise.Base.Definitions.PSK Impl.Noise.Types.g_is_null Impl.Noise.HandshakeState.handshake_state_m FStar.Pervasives.Native.Mktuple6 Impl.Noise.SymmetricState.symmetric_state_m Impl.Noise.Types.keypair_m FStar.Pervasives.Native.Mktuple3 FStar.Pervasives.Native.Mktuple2 Impl.Noise.FlatStructures.handshake_state_t_to_m Prims.l_and Prims.eq2 Spec.Noise.HandshakeFlags.handshake_state_flags Prims.nat FStar.Monotonic.HyperStack.mem FStar.HyperStack.ST.get
let initialize_IKpsk2 =
  
initialize hski Spec.pattern_IKpsk2