val compile_hski_from_ssdhi (#nc: iconfig) (ssdhi: ssdh_impls nc)
    : Tot (handshake_functions_impls nc)
val compile_hski_from_ssdhi (#nc: iconfig) (ssdhi: ssdh_impls nc)
    : Tot (handshake_functions_impls nc)
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
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"
/
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
ssdhi: Impl.Noise.HandshakeState.ssdh_impls nc
  -> Impl.Noise.PatternMessages.Definitions.handshake_functions_impls nc
Impl.Noise.Types.iconfig Impl.Noise.HandshakeState.ssdh_impls Impl.Noise.PatternMessages.Definitions.compile_handshake_functions_impls Impl.Noise.PatternMessages.Definitions.hs_impls Impl.Noise.PatternMessages.Definitions.compile_hs_impls Impl.Noise.PatternMessages.Definitions.handshake_functions_impls
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