val create_response1_XX : Impl.Noise.PatternMessages.Definitions.csend_message_gen_st Impl.Noise.Instances.wg_inc
  Spec.Noise.Instances.pattern_XX
  1
  false
let create_response1_XX =
  csend_message hski Spec.pattern_XX 1 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

[@(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

[@(Tactics.postprocess_with pp_hsk_def)]
let consume_initiation_IKpsk2 =
  creceive_message hski Spec.pattern_IKpsk2 0 false 12ul

// TODO: the normalize_term in cset_psk_st doesn't work anymore. Fix that.
// Maybe start by investigating while the following doesn't normalize here:
// [> let x = chskf_check_is_psk (convert_pattern Spec.pattern_IKpsk2)
// (note that it normalizes in Impl.Noise.PatternMessages.Definitions.fst...)
[@@ noextract_to "krml"] noextract
let _convert_pattern (x : wf_handshake_pattern) : handshake_pattern = x

(* set the PSK just before the response message *)
[@(Tactics.postprocess_with pp_hsk_def)]
let cset_psk_IKpsk2 =
  // TODO: remove those once the normalization is fixed
  (**) normalize_term_spec(chskf_check_is_psk (_convert_pattern Spec.pattern_IKpsk2));
  (**) normalize_term_spec(chskf_check_is_psk (Spec.pattern_IKpsk2));
  cset_psk hski Spec.pattern_IKpsk2 1

[@(Tactics.postprocess_with pp_hsk_def)]
let create_response_IKpsk2 =
  csend_message hski Spec.pattern_IKpsk2 1 true 0ul (null Lib.IntTypes.uint8)

[@(Tactics.postprocess_with pp_hsk_def)]
let consume_response_IKpsk2 =
  creceive_message hski Spec.pattern_IKpsk2 1 true 0ul (null Lib.IntTypes.uint8)

(*** XX *)
(* initialization *)
[@(Tactics.postprocess_with pp_hsk_def)]
let initialize_XX =
  initialize hski Spec.pattern_XX

(* messages *)
[@(Tactics.postprocess_with pp_hsk_def)]
let create_initiation_XX =
  csend_message hski Spec.pattern_XX 0 false

[@(Tactics.postprocess_with pp_hsk_def)]
let consume_initiation_XX =
  creceive_message hski Spec.pattern_XX 0 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.csend_message_gen_st Impl.Noise.Instances.wg_inc
  Spec.Noise.Instances.pattern_XX
  1
  false
Impl.Noise.Types.plain_message_len_t Impl.Noise.Instances.wg_inc Prims.b2t Prims.op_LessThanOrEqual Prims.op_Addition FStar.UInt32.v Lib.IntTypes.max_size_t Lib.Buffer.lbuffer Lib.IntTypes.uint8 Impl.Noise.FlatStructures.handshake_state_t 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 Prims.Cons Spec.Noise.Base.Definitions.message_token Spec.Noise.Base.Definitions.E Prims.Nil Spec.Noise.Base.Definitions.EE Spec.Noise.Base.Definitions.S Spec.Noise.Base.Definitions.ES Spec.Noise.Base.Definitions.SE 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_csend_message_rtype Impl.Noise.Types.rtype Impl.Noise.PatternMessages.Definitions.csend_message_return_type FStar.Monotonic.HyperStack.mem FStar.HyperStack.ST.get Impl.Noise.SendReceive.send_message_return_type Prims.op_Negation Impl.Noise.Types.is_success Impl.Noise.SendReceive.send_tokens_return_type Prims.bool Impl.Noise.SendReceive.encrypt_hash_rtype_to_message_payload Impl.Noise.Types.encrypt_hash_return_type Impl.Noise.SymmetricState.ssi_get_encrypt_and_hash Impl.Noise.HandshakeState.ssdhi_get_ssi Impl.Noise.Instances.ssdhi Lib.IntTypes.uint Lib.IntTypes.U64 Lib.IntTypes.PUB Prims.unit Prims._assert FStar.Pervasives.Native.Mktuple2 Impl.Noise.Types.error_code Spec.Noise.Base.Definitions.result FStar.Pervasives.Native.tuple2 Lib.ByteSequence.bytes Spec.Noise.Base.Definitions.handshake_state Impl.Noise.Types.get_config Spec.Noise.Base.Definitions.error Impl.Noise.Types.to_prim_error_code Spec.Noise.Base.Definitions.send_message_tokens FStar.Ghost.reveal Prims.l_and Prims.eq2 Impl.Noise.HandshakeState.eval_handshake_state_m Prims.nat Lib.Buffer.length Lib.Buffer.MUT Lib.Sequence.length Lib.IntTypes.uint_t Lib.IntTypes.U8 Lib.IntTypes.SEC Lib.Sequence.equal Lib.IntTypes.v Lib.IntTypes.U32 Lib.Buffer.op_Brack_Lens_Access Prims.l_False Spec.Noise.Base.Lemmas.send_message_tokens_with_payload_unfold_lem Impl.Noise.SendReceive.send_token_return_type Impl.Noise.SendReceive.tokens_message_rtype_add_token Impl.Noise.SendReceive.token_message_rtype_to_tokens Impl.Noise.SendReceive.send_message_token_m Spec.Noise.Base.Lemmas.send_message_tokens_one_token_lem FStar.Ghost.erased FStar.Ghost.hide Impl.Noise.SendReceive.send_message_tokens_pre Impl.Noise.SendReceive.send_message_token_post Impl.Noise.Types.success Spec.Noise.MetaInfo.greater_smi Spec.Noise.MetaInfo.send_token_update_smi Lib.Buffer.lbuffer_t Lib.IntTypes.int_t Lib.Buffer.sub Prims.int Prims.op_Subtraction Lib.IntTypes.op_Subtraction_Bang Spec.Noise.Base.Lemmas.send_message_tokens_unfold_lem Impl.Noise.SendReceive.send_message_token_pre FStar.UInt32.__uint_to_t Impl.Noise.SendReceive.token_message_vs Prims.l_or Lib.IntTypes.range Prims.op_GreaterThanOrEqual Spec.Noise.Lengths.opt_encrypt_size Prims.op_LessThan Spec.Noise.Base.Definitions.saturated_nonce_value Spec.Noise.WellFormedness.tokens_update_nonce_not_saturated Spec.Noise.HandshakeFlags.handshake_state_flags Spec.Noise.MetaInfo.__proj__Mkmeta_info__item__hsf Spec.Noise.MetaInfo.meta_info Spec.Noise.MetaInfo.__proj__Mkmeta_info__item__nonce Spec.Noise.HandshakeFlags.__proj__Mkhandshake_state_flags__item__sk Spec.Noise.MetaInfo.send_message_update_smi Spec.Noise.HandshakeFlags.tokens_update_sym_key_flag Meta.Noise.with_norm Spec.Noise.MetaInfo.send_tokens_update_smi Impl.Noise.SymmetricState.symmetric_state_m Impl.Noise.HandshakeState.hsm_get_sym_state Lib.Sequence.concat Lib.IntTypes.size Spec.Noise.Lengths.tokens_message_size Impl.Noise.SendReceive.tokens_message_vsv Impl.Noise.FlatStructures.eval_handshake_state_eq Spec.Noise.MetaInfo.csend_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.csend_message_pre_post_smi_lem Impl.Noise.PatternMessages.Definitions.csend_message_pre_lem Lib.IntTypes.size_t Prims.op_Equality Spec.Noise.Base.Definitions.check_hsk_is_psk Spec.Noise.HandshakeFlags.chskf_check_is_psk Spec.Noise.Base.Definitions.is_even Spec.Noise.MetaInfo.csend_message_pre_smi
let create_response1_XX =
  
csend_message hski Spec.pattern_XX 1 false