val send_message_token_DH_post
      (#nc: iconfig)
      (smi: meta_info)
      (initiator is_psk: bool)
      (tk: message_token)
      (st: valid_hsm nc (smi_set_sk true smi))
      (h0: mem)
      (r: rtype (send_token_return_type smi is_psk tk))
      (h1: mem)
    : Type0
val send_message_token_DH_post
      (#nc: iconfig)
      (smi: meta_info)
      (initiator is_psk: bool)
      (tk: message_token)
      (st: valid_hsm nc (smi_set_sk true smi))
      (h0: mem)
      (r: rtype (send_token_return_type smi is_psk tk))
      (h1: mem)
    : Type0
let send_message_token_DH_post
    (#nc : iconfig)
    (smi : meta_info)
    (initiator : bool)
    (is_psk : bool)
    (tk : message_token)
    (st : valid_hsm nc (smi_set_sk true smi))
    (h0 : mem) (r : rtype (send_token_return_type smi is_psk tk))
    (h1 : mem) : Type0 =
  ssm_modifies0 (hsm_get_sym_state st) h0 h1 /\
  begin
  let st0_v = eval_handshake_state_m h0 st smi in
  let st1_v = eval_handshake_state_m h1 st (smi_init_sk smi) in
  let r_v = Spec.send_message_token initiator is_psk tk st0_v in
  match to_prim_error_code r, r_v with
  | CSuccess, Res (cipher_v, st1'_v) ->
    st1_v == st1'_v /\ S.length cipher_v == 0 /\ cipher_v `S.equal` BS.lbytes_empty
  | CDH_error, Fail DH -> True
  | _ -> False
  end
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"

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

let smi_init_sk (smi : meta_info) : Tot meta_info =
  smi_opt_init_sk true smi

(*** Send message token(s) *)
(**** send_message_token *)
noextract
let send_message_token_no_fail_post
    (#nc : iconfig)
    (smi0 : meta_info)
    (smi1 : meta_info{less_than smi0 smi1})
    (initiator : bool)
    (is_psk : bool)
    (tk : message_token)
    (st : valid_hsm nc smi1)
    (out : token_message_t nc smi0 tk)
    (h0 : mem) (r : rtype (send_token_return_type smi0 is_psk tk))
    (h1 : mem) : Type0 =
  ssm_modifies1 (hsm_get_sym_state st) out h0 h1 /\
  begin
  let st0_v = eval_handshake_state_m h0 st smi0 in
  let st1_v = eval_handshake_state_m h1 st smi1 in
  let r_v = Spec.send_message_token initiator is_psk tk st0_v in
  match to_prim_error_code r, r_v with
  | CSuccess, Res (cipher_v, st1'_v) ->
    st1_v == st1'_v /\ S.length cipher_v == length out /\
    cipher_v `S.equal` h1.[|out|]
  | _ -> False
  end
/
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

    smi: Spec.Noise.MetaInfo.meta_info ->
    initiator: Prims.bool ->
    is_psk: Prims.bool ->
    tk: Spec.Noise.Base.Definitions.message_token ->
    st: Impl.Noise.HandshakeState.valid_hsm nc (Spec.Noise.MetaInfo.smi_set_sk true smi) ->
    h0: FStar.Monotonic.HyperStack.mem ->
    r: Impl.Noise.Types.rtype (Impl.Noise.SendReceive.send_token_return_type smi is_psk tk) ->
    h1: FStar.Monotonic.HyperStack.mem
  -> Type0
Impl.Noise.Types.iconfig Spec.Noise.MetaInfo.meta_info Prims.bool Spec.Noise.Base.Definitions.message_token Impl.Noise.HandshakeState.valid_hsm Spec.Noise.MetaInfo.smi_set_sk FStar.Monotonic.HyperStack.mem Impl.Noise.Types.rtype Impl.Noise.SendReceive.send_token_return_type Prims.l_and Impl.Noise.SymmetricState.ssm_modifies0 Impl.Noise.HandshakeState.hsm_get_sym_state FStar.Pervasives.Native.Mktuple2 Impl.Noise.Types.error_code Spec.Noise.Base.Definitions.result FStar.Pervasives.Native.tuple2 Lib.ByteSequence.bytes Spec.Noise.Base.Definitions.handshake_state Impl.Noise.Types.get_config Spec.Noise.Base.Definitions.error Impl.Noise.Types.to_prim_error_code Prims.eq2 Prims.int Lib.Sequence.length Lib.IntTypes.uint_t Lib.IntTypes.U8 Lib.IntTypes.SEC Lib.Sequence.equal Lib.IntTypes.int_t Lib.ByteSequence.lbytes_empty Prims.l_True Prims.l_False Prims.logical Spec.Noise.Base.Definitions.eresult Lib.Sequence.seq Spec.Noise.Base.Definitions.send_message_token FStar.Pervasives.Native.uu___is_Some Spec.Noise.CryptoPrimitives.aead_key Spec.Noise.Base.Definitions.__proj__Mkcipher_state__item__k Spec.Noise.Base.Definitions.__proj__Mksymmetric_state__item__c_state Spec.Noise.Base.Definitions.__proj__Mkhandshake_state__item__sym_state Spec.Noise.HandshakeFlags.__proj__Mkhandshake_state_flags__item__sk Spec.Noise.MetaInfo.__proj__Mkmeta_info__item__hsf Impl.Noise.SendReceive.smi_init_sk Spec.Noise.CryptoPrimitives.keypair Spec.Noise.Base.Definitions.__proj__Mkhandshake_state__item__static Spec.Noise.HandshakeFlags.__proj__Mkhandshake_state_flags__item__s Spec.Noise.Base.Definitions.__proj__Mkhandshake_state__item__ephemeral Spec.Noise.HandshakeFlags.__proj__Mkhandshake_state_flags__item__e Spec.Noise.CryptoPrimitives.public_key Spec.Noise.Base.Definitions.__proj__Mkhandshake_state__item__remote_static Spec.Noise.HandshakeFlags.__proj__Mkhandshake_state_flags__item__rs Spec.Noise.Base.Definitions.__proj__Mkhandshake_state__item__remote_ephemeral Spec.Noise.HandshakeFlags.__proj__Mkhandshake_state_flags__item__re Spec.Noise.CryptoPrimitives.preshared_key Spec.Noise.Base.Definitions.__proj__Mkhandshake_state__item__preshared Spec.Noise.HandshakeFlags.__proj__Mkhandshake_state_flags__item__psk Impl.Noise.HandshakeState.eval_handshake_state_m
let send_message_token_DH_post
      (#nc: iconfig)
      (smi: meta_info)
      (initiator is_psk: bool)
      (tk: message_token)
      (st: valid_hsm nc (smi_set_sk true smi))
      (h0: mem)
      (r: rtype (send_token_return_type smi is_psk tk))
      (h1: mem)
    : Type0 =
  
ssm_modifies0 (hsm_get_sym_state st) h0 h1 /\
(let st0_v = eval_handshake_state_m h0 st smi in
  let st1_v = eval_handshake_state_m h1 st (smi_init_sk smi) in
  let r_v = Spec.send_message_token initiator is_psk tk st0_v in
  match to_prim_error_code r, r_v with
  | CSuccess, Res (cipher_v, st1'_v) ->
    st1_v == st1'_v /\ S.length cipher_v == 0 /\ cipher_v `S.equal` BS.lbytes_empty
  | CDH_error, Fail DH -> True
  | _ -> False)