val generate_hski_declaration (debug: bool) (nc ssdhi: term) (hski_name: string) : Tac sigelt
val generate_hski_declaration (debug: bool) (nc ssdhi: term) (hski_name: string) : Tac sigelt
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
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"
/
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

    debug: Prims.bool ->
    nc: FStar.Stubs.Reflection.Types.term ->
    ssdhi: FStar.Stubs.Reflection.Types.term ->
    hski_name: Prims.string
  -> FStar.Tactics.Effect.Tac FStar.Stubs.Reflection.Types.sigelt
Prims.bool FStar.Stubs.Reflection.Types.term Prims.string FStar.Stubs.Reflection.Types.sigelt Prims.unit Impl.Noise.Extraction.print_declaration FStar.Stubs.Reflection.V1.Builtins.set_sigelt_attrs Prims.Cons Prims.Nil FStar.Stubs.Reflection.V1.Builtins.set_sigelt_quals FStar.Stubs.Reflection.V1.Data.qualifier FStar.Stubs.Reflection.V1.Data.NoExtract FStar.Stubs.Reflection.V1.Data.Inline_for_extraction FStar.Stubs.Reflection.V1.Builtins.pack_sigelt FStar.Stubs.Reflection.V1.Data.sigelt_view FStar.Stubs.Reflection.V1.Data.Sg_Let FStar.Stubs.Reflection.Types.letbinding FStar.Stubs.Reflection.V1.Builtins.pack_lb FStar.Stubs.Reflection.V1.Data.Mklb_view FStar.Stubs.Reflection.V1.Data.univ_name FStar.Pervasives.Native.option FStar.Pervasives.Native.Some FStar.Stubs.Reflection.Types.fv Impl.Noise.Extraction.make_cur_module_fv
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