val consume_initiation_IKpsk2 : payload_out: Lib.Buffer.lbuffer Lib.IntTypes.uint8 12ul ->
    st: Impl.Noise.FlatStructures.handshake_state_t Impl.Noise.Instances.wg_inc ->
    input:
      Impl.Noise.PatternMessages.Definitions.pat_message_t Impl.Noise.Instances.wg_inc
        Spec.Noise.Instances.pattern_IKpsk2
        (Lib.IntTypes.size_v 12ul)
        0
  -> FStar.HyperStack.ST.Stack
    (Impl.Noise.Types.rtype (Impl.Noise.PatternMessages.Definitions.creceive_message_return_type Impl.Noise.Instances.wg_inc
            Spec.Noise.Instances.pattern_IKpsk2
            0
            false))
let consume_initiation_IKpsk2 =
  creceive_message hski Spec.pattern_IKpsk2 0 false 12ul
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

[@(Tactics.postprocess_with pp_hsk_def)]
let receive_premessage_IKpsk2 =
  creceive_premessage hski Spec.pattern_IKpsk2 false false

(* messages *)
[@(Tactics.postprocess_with pp_hsk_def)]
let create_initiation_IKpsk2 =
  csend_message hski Spec.pattern_IKpsk2 0 false 12ul
/
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

    payload_out: Lib.Buffer.lbuffer Lib.IntTypes.uint8 12ul ->
    st: Impl.Noise.FlatStructures.handshake_state_t Impl.Noise.Instances.wg_inc ->
    input:
      Impl.Noise.PatternMessages.Definitions.pat_message_t Impl.Noise.Instances.wg_inc
        Spec.Noise.Instances.pattern_IKpsk2
        (Lib.IntTypes.size_v 12ul)
        0
  -> FStar.HyperStack.ST.Stack
    (Impl.Noise.Types.rtype (Impl.Noise.PatternMessages.Definitions.creceive_message_return_type Impl.Noise.Instances.wg_inc
            Spec.Noise.Instances.pattern_IKpsk2
            0
            false))
Lib.Buffer.lbuffer Lib.IntTypes.uint8 FStar.UInt32.__uint_to_t Impl.Noise.FlatStructures.handshake_state_t Impl.Noise.Instances.wg_inc Impl.Noise.PatternMessages.Definitions.pat_message_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 Lib.IntTypes.size_v 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.PatternMessages.Definitions.to_creceive_message_rtype Impl.Noise.Types.rtype Impl.Noise.PatternMessages.Definitions.creceive_message_return_type FStar.Monotonic.HyperStack.mem FStar.HyperStack.ST.get Impl.Noise.SendReceive.receive_message_return_type Meta.Noise.convert_subtype Prims.op_Negation Impl.Noise.Types.is_success Impl.Noise.SendReceive.receive_tokens_return_type Prims.bool Impl.Noise.SendReceive.message_return_type Prims.b2t Prims.op_Equality Impl.Noise.Types.prim_error_code Impl.Noise.Types.to_prim_error_code Impl.Noise.Types.decrypt_hash_return_type Spec.Noise.HandshakeFlags.__proj__Mkhandshake_state_flags__item__sk Spec.Noise.MetaInfo.__proj__Mkmeta_info__item__hsf Spec.Noise.MetaInfo.receive_tokens_update_smi Impl.Noise.SendReceive.decrypt_hash_rtype_convert_sk Impl.Noise.SendReceive.decrypt_hash_rtype_to_message_payload FStar.Ghost.erased Spec.Noise.Base.Definitions.handshake_state Impl.Noise.Types.get_config FStar.Ghost.hide Impl.Noise.HandshakeState.eval_handshake_state_m Impl.Noise.SymmetricState.ssi_get_decrypt_and_hash Impl.Noise.HandshakeState.ssdhi_get_ssi Impl.Noise.Instances.ssdhi Lib.IntTypes.uint Lib.IntTypes.U64 Lib.IntTypes.PUB Spec.Noise.MetaInfo.__proj__Mkmeta_info__item__nonce Prims.unit Spec.Noise.Lengths.receive_message_tokens_nout_with_payload_unfold_lem Lib.IntTypes.v Lib.IntTypes.U32 Lib.IntTypes.size Lib.Buffer.op_Brack_Lens_Access Lib.Buffer.MUT FStar.Ghost.reveal Prims._assert FStar.Pervasives.Native.Mktuple2 Impl.Noise.Types.error_code Spec.Noise.Base.Definitions.result Spec.Noise.Base.Definitions.error Spec.Noise.Base.Definitions.eresult Prims.l_True Prims.eq2 FStar.Pervasives.Native.tuple2 Prims.l_False Spec.Noise.Lengths.receive_message_tokens_nout Impl.Noise.SendReceive.receive_token_return_type Impl.Noise.SendReceive.tokens_message_rtype_add_token Impl.Noise.RecursiveMessages.receive_message_tokens_nout_m_Cons_Nil_ Impl.Noise.SendReceive.receive_message_token_m Impl.Noise.SendReceive.receive_message_tokens_nout_pre Impl.Noise.SendReceive.receive_message_token_post_ Impl.Noise.Types.success Spec.Noise.MetaInfo.greater_smi Spec.Noise.MetaInfo.receive_token_update_smi Lib.Buffer.lbuffer_t Lib.IntTypes.int_t Lib.IntTypes.U8 Lib.IntTypes.SEC Lib.Buffer.sub Prims.int Prims.op_Subtraction Lib.IntTypes.op_Subtraction_Bang Impl.Noise.SendReceive.token_message_rtype_to_tokens Spec.Noise.Lengths.receive_message_tokens_nout_unfold_lem Impl.Noise.SendReceive.receive_message_token_m_ Impl.Noise.SendReceive.receive_message_token_pre_ Impl.Noise.SendReceive.token_message_vs Prims.l_and Spec.Noise.HandshakeFlags.handshake_state_flags Spec.Noise.MetaInfo.meta_info Prims.op_Addition Spec.Noise.MetaInfo.receive_message_update_smi Prims.op_LessThan Spec.Noise.Base.Definitions.saturated_nonce_value Spec.Noise.WellFormedness.tokens_update_nonce_not_saturated Spec.Noise.HandshakeFlags.tokens_update_sym_key_flag Spec.Noise.MetaInfo.updt_sk_consistent_with_receive_tokens_update_smi Meta.Noise.with_norm Impl.Noise.SymmetricState.symmetric_state_m Impl.Noise.HandshakeState.hsm_get_sym_state Lib.Sequence.equal Lib.Sequence.concat Lib.IntTypes.mk_int Prims.nat Spec.Noise.Lengths.opt_encrypt_size Prims.op_BarBar Spec.Noise.Lengths.tokens_message_size Impl.Noise.SendReceive.tokens_message_vsv Impl.Noise.FlatStructures.eval_handshake_state_eq Spec.Noise.MetaInfo.creceive_message_post_smi Impl.Noise.HandshakeState.hsm_disjoint Impl.Noise.FlatStructures.handshake_state_t_to_m_disjoint_impl Impl.Noise.PatternMessages.Definitions.pat_message_vs 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.Types.keypair_m FStar.Pervasives.Native.Mktuple3 Impl.Noise.FlatStructures.handshake_state_t_to_m Impl.Noise.PatternMessages.Definitions.creceive_message_pre_post_smi_lem Impl.Noise.PatternMessages.Definitions.creceive_message_pre_lem Lib.IntTypes.size_t Spec.Noise.Base.Definitions.check_hsk_is_psk Spec.Noise.HandshakeFlags.chskf_check_is_psk Spec.Noise.Base.Definitions.is_even Spec.Noise.MetaInfo.creceive_message_pre_smi
let consume_initiation_IKpsk2 =
  
creceive_message hski Spec.pattern_IKpsk2 0 false 12ul