val cimpl_m_ids : Prims.list Prims.string
let cimpl_m_ids = [
  `%initialize_m;
  `%initialize_from_lists_m;
  `%csend_premessage_m;
  `%creceive_premessage_m;
  `%csend_message_m;
  `%creceive_message_m
]
module Impl.Noise.PatternMessages.Tactics

module Spec = Spec.Noise
open Spec.Noise
open Impl.Noise.Types
open Impl.Noise.CipherState
open Impl.Noise.HKDF
open Impl.Noise.SymmetricState
open Impl.Noise.HandshakeState
open Impl.Noise.SendReceive
open Impl.Noise.RecursivePremessages
open Impl.Noise.RecursiveMessages
open Impl.Noise.FlatStructures
open Impl.Noise.CryptoPrimitives
open Impl.Noise.PatternMessages.Definitions
open Impl.Noise.Extraction

module T = FStar.Tactics
open FStar.Tactics
open FStar.String

#set-options "--z3rlimit 15 --fuel 0 --ifuel 0"

inline_for_extraction noextract
let compile_hski_from_ssdhi (#nc : iconfig) (ssdhi : ssdh_impls nc) :
  Tot (handshake_functions_impls nc) =
  [@inline_let] let hsi = compile_hs_impls ssdhi in
  compile_handshake_functions_impls hsi

#push-options "--ifuel 1"
inline_for_extraction noextract
let generate_hski_declaration (debug : bool) (nc ssdhi : term) (hski_name : string) :
  Tac sigelt =
  let body = `compile_hski_from_ssdhi (`#ssdhi) in
  let ty = `handshake_functions_impls (`#nc) in
  let name = make_cur_module_fv hski_name in
  let params = Some hski_name in
  let lb = pack_lb ({ lb_fv = name; lb_us = []; lb_typ = ty; lb_def = body }) in
  let sg = Sg_Let false [lb] in
  let decl : sigelt = pack_sigelt sg in
  let decl = set_sigelt_quals [ NoExtract; Inline_for_extraction ] decl in
  let decl = set_sigelt_attrs [ `(noextract_to "krml") ] decl in
  if debug then print_declaration sg;
  decl
#pop-options

/// The function to be used by the user to generate the declarations of the "basic"
/// Noise functions, used to generate the send/receive (pre) message functions.
noextract
let generate_pattern_declarations
  (debug : bool)
  (#nc : config)
  (impls_params : config_impls_params nc)
  (extract_params : extract_decls_params)
  (iconfig_name handshake_function_impl_name : string) :
  Tac decls =
  let dl, qnc, qssdhi =
    generate_config_declarations debug #nc impls_params extract_params iconfig_name
  in
  let hski_decl =
    generate_hski_declaration debug qnc qssdhi handshake_function_impl_name in
  List.append dl [hski_decl]

(** For debugging [generate_config_declarations]:

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; hski]
(generate_config_declarations true impls_params debug_extract_decls_params "iwgc" "hski")

*)

(**** Normalization *)

let handshake_functions_impls_id = `%handshake_functions_impls

let cimpl_st_ids = [
  `%initialize_st;
  `%initialize_from_lists_st;
  `%csend_premessage_st;
  `%creceive_premessage_st;
  `%csend_message_st;
  `%creceive_message_st;
]
/
Spec.Noise.fst.checked prims.fst.checked Impl.Noise.Types.fst.checked Impl.Noise.SymmetricState.fsti.checked Impl.Noise.SendReceive.fsti.checked Impl.Noise.RecursivePremessages.fst.checked Impl.Noise.RecursiveMessages.fst.checked Impl.Noise.PatternMessages.Definitions.fst.checked Impl.Noise.HKDF.fsti.checked Impl.Noise.HandshakeState.fsti.checked Impl.Noise.FlatStructures.fst.checked Impl.Noise.Extraction.fst.checked Impl.Noise.CryptoPrimitives.fsti.checked Impl.Noise.CipherState.fsti.checked FStar.Tactics.fst.checked FStar.String.fsti.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked FStar.List.fst.checked
Impl.Noise.PatternMessages.Tactics.fst
Prims.list Prims.string
Prims.Cons Prims.string Prims.Nil
let cimpl_m_ids =
  
[
  `%initialize_m;
  `%initialize_from_lists_m;
  `%csend_premessage_m;
  `%creceive_premessage_m;
  `%csend_message_m;
  `%creceive_message_m
]