val receive_premessage_IKpsk2 : Impl.Noise.PatternMessages.Definitions.creceive_premessage_gen_st Impl.Noise.Instances.wg_inc
  Spec.Noise.Instances.pattern_IKpsk2
  false
  false
let receive_premessage_IKpsk2 =
  creceive_premessage hski Spec.pattern_IKpsk2 false false
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 *)
[@(Tactics.postprocess_with pp_hsk_def)]
let initialize_IKpsk2 =
  initialize hski Spec.pattern_IKpsk2

(* premessages *)
[@(Tactics.postprocess_with pp_hsk_def)]
let send_premessage_IKpsk2 =
  csend_premessage hski Spec.pattern_IKpsk2 false false
/
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.PatternMessages.Definitions.creceive_premessage_gen_st Impl.Noise.Instances.wg_inc
  Spec.Noise.Instances.pattern_IKpsk2
  false
  false
Impl.Noise.FlatStructures.handshake_state_t Impl.Noise.Instances.wg_inc Impl.Noise.PatternMessages.Definitions.premessage_t 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.CipherState.cipher_state_m Impl.Noise.Types.chaining_key_t Impl.Noise.Types.hash_t Impl.Noise.Types.opt_private_key_t Impl.Noise.Types.opt_public_key_t Impl.Noise.Types.opt_preshared_key_t Impl.Noise.Types.rtype Impl.Noise.HandshakeState.tokens_premessage_return_type FStar.Monotonic.HyperStack.mem FStar.HyperStack.ST.get Impl.Noise.Types.success FStar.Ghost.erased Spec.Noise.MetaInfo.meta_info FStar.Ghost.hide Spec.Noise.MetaInfo.receive_pretoken_update_smi Impl.Noise.HandshakeState.token_premessage_return_type Impl.Noise.HandshakeState.receive_premessage_token_m Impl.Noise.HandshakeState.ssdhi_get_ssi Impl.Noise.Instances.ssdhi Prims.unit Spec.Noise.Base.Lemmas.receive_premessage_tokens_unfold_lem Impl.Noise.Types.get_config Lib.Buffer.op_Brack_Lens_Access Lib.Buffer.MUT Lib.IntTypes.uint8 Impl.Noise.HandshakeState.premessage_vs FStar.Ghost.reveal Spec.Noise.Base.Definitions.handshake_state Impl.Noise.HandshakeState.eval_handshake_state_m Prims._assert Lib.Sequence.equal Lib.IntTypes.v Lib.IntTypes.U32 Lib.IntTypes.PUB Lib.Sequence.concat Impl.Noise.Types.public_key_vs Meta.Noise.with_norm Lib.IntTypes.size_t Lib.IntTypes.size FStar.Mul.op_Star FStar.List.Tot.Base.length Impl.Noise.Types.public_key_vsv Lib.Buffer.lbuffer_t Lib.IntTypes.int_t Lib.IntTypes.U8 Lib.IntTypes.SEC Lib.IntTypes.mk_int Prims.op_Multiply Lib.Buffer.sub FStar.UInt32.__uint_to_t Impl.Noise.FlatStructures.eval_handshake_state_eq Spec.Noise.MetaInfo.creceive_premessage_post_smi Impl.Noise.HandshakeState.hsm_disjoint Impl.Noise.PatternMessages.Definitions.premessage_vs Impl.Noise.FlatStructures.handshake_state_t_to_m_disjoint_impl Impl.Noise.HandshakeState.hsm_inv Impl.Noise.FlatStructures.handshake_state_t_to_m_impl_hsm_inv 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 Spec.Noise.MetaInfo.csend_creceive_cexchange_smi_consistent_lem Impl.Noise.PatternMessages.Definitions.wf_handshake_pattern_pre_length_lem Impl.Noise.PatternMessages.Definitions.creceive_premessage_pre_lem Prims.eq2 Prims.bool Spec.Noise.HandshakeFlags.__proj__Mkhandshake_state_flags__item__psk Spec.Noise.MetaInfo.__proj__Mkmeta_info__item__hsf Spec.Noise.MetaInfo.creceive_premessage_pre_smi
let receive_premessage_IKpsk2 =
  
creceive_premessage hski Spec.pattern_IKpsk2 false false