val initialize_handshake_state_m (#nc : iconfig) (ssi : ss_impls nc) :
  initialize_handshake_state_st nc
val initialize_handshake_state_m (#nc : iconfig) (ssi : ss_impls nc) :
  initialize_handshake_state_st nc
let initialize_handshake_state_m
  #nc ssi pname_len pname prlg_len prlg
  #s_b spriv spub #e_b epriv epub #rs_b rs #re_b re #psk_b psk st =
  [@inline_let] let st_sym_state = hsm_get_sym_state st in
  [@inline_let] let st_static = hsm_get_static st in
  [@inline_let] let st_ephemeral = hsm_get_ephemeral st in
  [@inline_let] let st_remote_static = hsm_get_remote_static st in
  [@inline_let] let st_remote_ephemeral = hsm_get_remote_ephemeral st in
  [@inline_let] let st_preshared = hsm_get_preshared st in
  (**) let h0 = HST.get () in
  (**) let pname_v : Ghost.erased _ = h0.[|pname|] in
  (**) let prologue_v : Ghost.erased _ = h0.[|prlg|] in
  let _ = ssi_get_initialize_symmetric ssi pname_len pname st_sym_state in
  (**) let h1 = HST.get () in
  let _ = ssi_get_mix_hash ssi false prlg_len prlg st_sym_state 0 in
  (**) let h2 = HST.get () in
  (**) assert(ssm_modifies0 st_sym_state h0 h2);
  (**) assert(
  (**)   let sym_st1 = Spec.initialize_symmetric pname_v in
  (**)   let sym_st2 = Spec.mix_hash prologue_v sym_st1 in
  (**)   sym_st2 == eval_symmetric_state_m h2 st_sym_state false 0);
  update_keypair_opt st_static spriv spub;
  update_keypair_opt st_ephemeral epriv epub;
  update_sub_opt st_remote_static rs;
  update_sub_opt st_remote_ephemeral re;
  update_sub_opt st_preshared psk;
  (**) let hf = HST.get () in
  (**) assert(hsm_modifies0 st h0 hf);
  success hash_return_type
module Impl.Noise.HandshakeState

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
open Lib.ByteSequence

module B = LowStar.Buffer
open Lib.Buffer
open Lib.ByteBuffer

open LowStar.BufferOps

module Spec = Spec.Noise
open Spec.Noise
open Meta.Noise
open Impl.Noise.Types
open Impl.Noise.CipherState
open Impl.Noise.HKDF
open Impl.Noise.SymmetricState
open Impl.Noise.TypeOrUnit

friend Spec.Noise.Base.Definitions

#set-options "--z3rlimit 25 --fuel 0 --ifuel 1"

(* Align the .fst and the .fsti *)
let _align_beg = ()

(*** Initialization *)
// TODO: move. Note that there are functions with the same name in Impl.Noise.Types (those from Impl.Noise.Types will be removed)
inline_for_extraction noextract
val update_sub_opt :
  #a : Type0 ->
  (* Warning: len must be valid for extraction *)
  #len : size_t ->
  #b : bool ->
  dst : lbuffer_or_null a len ->
  src : type_or_unit (lbuffer a len) b ->
  Stack unit
  (requires (fun h ->
    live h dst /\ lbuffer_or_unit_live h src /\
    B.(loc_disjoint (loc_buffer (dst <: buffer a)) (lbuffer_or_unit_loc src)) /\
    (b ==> not (g_is_null dst))))
  (ensures (fun h0 _ h1 ->
    (if not b then modifies0 h0 h1 else modifies1 dst h0 h1) /\
    (if not b then
      (if g_is_null dst then True else h1.[|dst <: lbuffer_t MUT a len|] `S.equal`
                                    h0.[|dst <: lbuffer_t MUT a len|])
     else h1.[|dst <: lbuffer_t MUT a len|] `S.equal` lbuffer_or_unit_to_seq h0 src)))
let update_sub_opt #a #len #b dst src =
  if b then update_sub (dst <: lbuffer_t MUT a len) 0ul len (src <: lbuffer_t MUT a len)
  else ()

inline_for_extraction noextract
val update_keypair_opt :
  #nc : iconfig ->
  #b : bool ->
  dst : keypair_m nc ->
  src_priv : private_key_t_or_unit nc b ->
  src_pub : public_key_t_or_unit nc b ->
  Stack unit
  (requires (fun h ->
    live_kpm h dst /\
    lbuffer_or_unit_live h src_priv /\ lbuffer_or_unit_live h src_pub /\
    disjoint_kpm dst /\
    kpm_loc_disjoint dst (B.loc_union (lbuffer_or_unit_loc src_priv)
                                      (lbuffer_or_unit_loc src_pub)) /\
    ((g_is_null (kpm_get_priv dst) || g_is_null (kpm_get_pub dst)) ==> not b)
    ))
  (ensures (fun h0 _ h1 ->
    (if not b then modifies0 h0 h1
     else modifies (B.loc_union (loc (kpm_get_priv dst)) (loc (kpm_get_pub dst))) h0 h1) /\
    begin
    if b
    then eval_keypair_m h1 dst == Some?.v (keys_t_or_unit_to_keypair h0 src_priv src_pub)
    else True
    end))

let update_keypair_opt #nc #b dst src_priv src_pub =
  if b then
    begin
    update_sub ((kpm_get_priv dst) <: private_key_t nc) 0ul (private_key_vs nc)
               (src_priv <: private_key_t nc);
    update_sub ((kpm_get_pub dst) <: public_key_t nc) 0ul (public_key_vs nc)
               (src_pub <: public_key_t nc)
    end
  else ()
/
Spec.Noise.Base.Definitions.fst.checked Spec.Noise.fst.checked prims.fst.checked Meta.Noise.fsti.checked LowStar.BufferOps.fst.checked LowStar.Buffer.fst.checked Lib.Sequence.fsti.checked Lib.RawIntTypes.fsti.checked Lib.Memzero0.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.TypeOrUnit.fsti.checked Impl.Noise.SymmetricState.fsti.checked Impl.Noise.HKDF.fsti.checked Impl.Noise.CipherState.fsti.checked FStar.UInt32.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Ghost.fsti.checked
Impl.Noise.HandshakeState.fst
ssi: Impl.Noise.SymmetricState.ss_impls nc
  -> Impl.Noise.HandshakeState.initialize_handshake_state_st nc
Impl.Noise.Types.iconfig Impl.Noise.SymmetricState.ss_impls Impl.Noise.Types.hashable_size_t Impl.Noise.Types.hashable_t Prims.bool Impl.Noise.TypeOrUnit.private_key_t_or_unit Impl.Noise.TypeOrUnit.public_key_t_or_unit Impl.Noise.TypeOrUnit.preshared_key_t_or_unit Impl.Noise.HandshakeState.handshake_state_m Impl.Noise.Types.success Impl.Noise.Types.hash_return_type Prims.unit Prims._assert Impl.Noise.HandshakeState.hsm_modifies0 Impl.Noise.Types.rtype FStar.Monotonic.HyperStack.mem FStar.HyperStack.ST.get Impl.Noise.HandshakeState.update_sub_opt Lib.IntTypes.uint8 Impl.Noise.Types.preshared_key_vs Impl.Noise.Types.public_key_vs Impl.Noise.HandshakeState.update_keypair_opt Prims.eq2 Spec.Noise.Base.Definitions.symmetric_state Impl.Noise.Types.get_config Impl.Noise.SymmetricState.eval_symmetric_state_m Spec.Noise.Base.Definitions.mix_hash FStar.Ghost.reveal Spec.Noise.CryptoPrimitives.hashable Spec.Noise.Base.Definitions.initialize_symmetric Impl.Noise.SymmetricState.ssm_modifies0 Impl.Noise.SymmetricState.ssi_get_mix_hash FStar.Ghost.hide Prims.nat Impl.Noise.SymmetricState.ssi_get_initialize_symmetric FStar.Ghost.erased Lib.Buffer.op_Brack_Lens_Access Lib.Buffer.MUT Impl.Noise.Types.opt_preshared_key_t Impl.Noise.HandshakeState.hsm_get_preshared Impl.Noise.Types.opt_public_key_t Impl.Noise.HandshakeState.hsm_get_remote_ephemeral Impl.Noise.HandshakeState.hsm_get_remote_static Impl.Noise.Types.keypair_m Impl.Noise.HandshakeState.hsm_get_ephemeral Impl.Noise.HandshakeState.hsm_get_static Impl.Noise.SymmetricState.symmetric_state_m Impl.Noise.HandshakeState.hsm_get_sym_state
let initialize_handshake_state_m
      #nc
      ssi
      pname_len
      pname
      prlg_len
      prlg
      #s_b
      spriv
      spub
      #e_b
      epriv
      epub
      #rs_b
      rs
      #re_b
      re
      #psk_b
      psk
      st
     =
  
[@@ inline_let ]let st_sym_state = hsm_get_sym_state st in
[@@ inline_let ]let st_static = hsm_get_static st in
[@@ inline_let ]let st_ephemeral = hsm_get_ephemeral st in
[@@ inline_let ]let st_remote_static = hsm_get_remote_static st in
[@@ inline_let ]let st_remote_ephemeral = hsm_get_remote_ephemeral st in
[@@ inline_let ]let st_preshared = hsm_get_preshared st in
let h0 = HST.get () in
let pname_v:Ghost.erased _ = h0.[| pname |] in
let prologue_v:Ghost.erased _ = h0.[| prlg |] in
let _ = ssi_get_initialize_symmetric ssi pname_len pname st_sym_state in
let h1 = HST.get () in
let _ = ssi_get_mix_hash ssi false prlg_len prlg st_sym_state 0 in
let h2 = HST.get () in
assert (ssm_modifies0 st_sym_state h0 h2);
assert (let sym_st1 = Spec.initialize_symmetric pname_v in
    let sym_st2 = Spec.mix_hash prologue_v sym_st1 in
    sym_st2 == eval_symmetric_state_m h2 st_sym_state false 0);
update_keypair_opt st_static spriv spub;
update_keypair_opt st_ephemeral epriv epub;
update_sub_opt st_remote_static rs;
update_sub_opt st_remote_ephemeral re;
update_sub_opt st_preshared psk;
let hf = HST.get () in
assert (hsm_modifies0 st h0 hf);
success hash_return_type