val smi_opt_init_sk (b: bool) (smi: meta_info) : Tot meta_info
val smi_opt_init_sk (b: bool) (smi: meta_info) : Tot meta_info
let smi_opt_init_sk (b : bool) (smi : meta_info) : Tot meta_info =
  if b then { smi with hsf = { smi.hsf with sk = true }; nonce = 0} else smi
module Impl.Noise.SendReceive

open FStar.Mul
module HS = FStar.HyperStack
open FStar.HyperStack
open FStar.HyperStack.ST

open Lib.RawIntTypes
open Lib.IntTypes

module HST = FStar.HyperStack.ST
open Lib.Sequence
module S = Lib.Sequence
module SB = FStar.Seq.Base
module L = FStar.List
module Seq = FStar.Seq

module B = LowStar.Buffer
module BS = Lib.ByteSequence
module LB = Lib.Buffer
open Lib.Buffer
module BB = Lib.ByteBuffer
open Lib.ByteBuffer

open LowStar.BufferOps

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

friend Spec.Noise.Base.Definitions
friend Spec.Noise.Lengths

(* In order to prevent issues with the interleaving of the .fsti:
 * for the parameters we set the maximum values of the options used in the
 * .fsti *)
#set-options "--z3rlimit 25 --fuel 1 --ifuel 1"
/
Spec.Noise.Lengths.fst.checked Spec.Noise.Base.Definitions.fst.checked Spec.Noise.fst.checked prims.fst.checked LowStar.BufferOps.fst.checked LowStar.Buffer.fst.checked Lib.Sequence.fsti.checked Lib.RawIntTypes.fsti.checked Lib.IntTypes.fsti.checked Lib.ByteSequence.fsti.checked Lib.ByteBuffer.fsti.checked Lib.Buffer.fsti.checked Impl.Noise.Types.fst.checked Impl.Noise.SymmetricState.fsti.checked Impl.Noise.HKDF.fsti.checked Impl.Noise.HandshakeState.fsti.checked Impl.Noise.CipherState.fsti.checked FStar.UInt32.fsti.checked FStar.Seq.Base.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.List.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked
Impl.Noise.SendReceive.fst
b: Prims.bool -> smi: Spec.Noise.MetaInfo.meta_info -> Spec.Noise.MetaInfo.meta_info
Prims.bool Spec.Noise.MetaInfo.meta_info Spec.Noise.MetaInfo.Mkmeta_info Spec.Noise.HandshakeFlags.Mkhandshake_state_flags Spec.Noise.HandshakeFlags.__proj__Mkhandshake_state_flags__item__s Spec.Noise.HandshakeFlags.__proj__Mkhandshake_state_flags__item__e Spec.Noise.HandshakeFlags.__proj__Mkhandshake_state_flags__item__rs Spec.Noise.HandshakeFlags.__proj__Mkhandshake_state_flags__item__re Spec.Noise.HandshakeFlags.__proj__Mkhandshake_state_flags__item__psk Spec.Noise.HandshakeFlags.handshake_state_flags Spec.Noise.MetaInfo.__proj__Mkmeta_info__item__hsf
let smi_opt_init_sk (b: bool) (smi: meta_info) : Tot meta_info =
  
if b then { smi with hsf = { smi.hsf with sk = true }; nonce = 0 } else smi