val send_message_E_m_:send_message_token_m_impl E
val send_message_E_m_:send_message_token_m_impl E
let send_message_E_m_ : send_message_token_m_impl E =
  fun #nc ssdhi smi initiator is_psk st out ->
    send_message_E_m #nc (ssdhi_get_ssi ssdhi) smi initiator is_psk st out
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

noextract
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


inline_for_extraction noextract
val send_message_S_m :
  #nc : iconfig ->
  ssi : ss_impls nc ->
  smi : meta_info ->
  initiator : bool ->
  is_psk : bool ->
  st : valid_send_token_hsm nc is_psk S smi ->
  out : lbuffer uint8 (size (opt_encrypt_size smi.hsf.sk (public_key_vsv nc))) ->
  Stack (rtype (send_token_return_type smi is_psk S))
  (requires (fun h -> hsm_inv h st smi /\ live h out /\ hsm_disjoint st out /\
                    (**) smi.hsf.s == true (**) /\
                    smi.nonce < saturated_nonce_value /\
                    (smi.hsf.sk ==> get_aead_pre nc) /\
                    get_hash_pre nc))
  (ensures (
    send_message_token_no_fail_post smi (send_token_update_smi is_psk S smi)
                                    initiator is_psk S st out))

#push-options "--z3rlimit 50"
let send_message_S_m #nc ssi smi initiator is_psk st out =
  [@inline_let] let s_pub = kpm_get_pub (hsm_get_static st) in
  [@inline_let] let sym_st = hsm_get_sym_state st in
  (**) hash_max_input_norm_lem (get_config nc);
  ssi_get_encrypt_and_hash ssi smi.hsf.sk (public_key_vs nc) s_pub out sym_st
                           (uint smi.nonce)
#pop-options


inline_for_extraction noextract
val send_message_E_m :
  #nc : iconfig ->
  ssi : ss_impls nc ->
  smi : meta_info ->
  initiator : bool ->
  is_psk : bool ->
  st : valid_send_token_hsm nc is_psk E smi ->
  out : public_key_t nc ->
  Stack (rtype (send_token_return_type smi is_psk E))
  (requires (fun h -> hsm_inv h st smi /\ live h out /\ hsm_disjoint st out /\
                    (**) smi.hsf.e == true (**) /\ get_hash_pre nc))
  (ensures (
    send_message_token_no_fail_post smi (send_token_update_smi is_psk E smi)
                                    initiator is_psk E st out))

#push-options "--z3rlimit 50"
let send_message_E_m #nc ssi smi initiator is_psk st out =
  (**) let h0 = HST.get () in
  [@inline_let] let e_pub = kpm_get_pub (hsm_get_ephemeral st) in
  [@inline_let] let sym_st = hsm_get_sym_state st in
  (**) hash_max_input_norm_lem (get_config nc);
  ssi_get_mix_hash ssi smi.hsf.sk (public_key_vs nc) e_pub sym_st smi.nonce;
  if is_psk then
    ssi_get_mix_key ssi smi.hsf.sk e_pub sym_st smi.nonce;
    begin
    update_sub out 0ul (public_key_vs nc) e_pub;
    (**) let h1 = HST.get () in
    (**) assert(ssm_modifies1 sym_st out h0 h1);
    let r3 = success (send_token_return_type smi is_psk E) in
    (**) assert(
    (**)   let smi0 = smi in
    (**)   let smi1 = send_token_update_smi is_psk E smi in
    (**)   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 E st0_v in
    (**)   match to_prim_error_code r3, 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);
    r3
    end
#pop-options

inline_for_extraction noextract
val send_message_SS_m :
  #nc : iconfig ->
  ssdhi : ssdh_impls nc ->
  smi : meta_info ->
  initiator : bool ->
  is_psk : bool ->
  st : valid_send_token_hsm nc is_psk SS smi ->
  Stack (rtype (send_token_return_type smi is_psk SS))
  (requires (fun h -> hsm_inv h st smi /\ (**) smi.hsf.s == true /\ smi.hsf.rs == true (**) /\
                    get_dh_pre nc /\ get_hash_pre nc))
  (ensures (send_message_token_DH_post smi initiator is_psk SS st))

let send_message_SS_m #nc ssdhi smi initiator is_psk st =
  [@inline_let] let priv = hsm_get_static st in
  [@inline_let] let pub = hsm_get_remote_static st in
  ssdhi_get_dh_update ssdhi BS.lbytes_empty smi priv pub st


inline_for_extraction noextract
val send_message_EE_m :
  #nc : iconfig ->
  ssdhi : ssdh_impls nc ->
  smi : meta_info ->
  initiator : bool ->
  is_psk : bool ->
  st : valid_send_token_hsm nc is_psk EE smi ->
  Stack (rtype (send_token_return_type smi is_psk EE))
  (requires (fun h -> hsm_inv h st smi /\ (**) smi.hsf.e == true /\ smi.hsf.re == true (**) /\
                    get_dh_pre nc /\ get_hash_pre nc))
  (ensures (send_message_token_DH_post smi initiator is_psk EE st))

let send_message_EE_m #nc ssdhi smi initiator is_psk st =
  [@inline_let] let priv = hsm_get_ephemeral st in
  [@inline_let] let pub = hsm_get_remote_ephemeral st in
  ssdhi_get_dh_update ssdhi BS.lbytes_empty smi priv pub st


inline_for_extraction noextract
val send_message_SE_m :
  #nc : iconfig ->
  ssdhi : ssdh_impls nc ->
  smi : meta_info ->
  initiator : bool ->
  is_psk : bool ->
  st : valid_send_token_hsm nc is_psk SE smi ->
  Stack (rtype (send_token_return_type smi is_psk SE))
  (requires (fun h -> hsm_inv h st smi /\
                    (**)
                    (if initiator then smi.hsf.s == true /\ smi.hsf.re == true
                                  else smi.hsf.e == true /\ smi.hsf.rs == true)
                    (**) /\
                    get_dh_pre nc /\ get_hash_pre nc))
  (ensures (send_message_token_DH_post smi initiator is_psk SE st))

let send_message_SE_m #nc ssdhi smi initiator is_psk st =
  [@inline_let] let priv = if initiator then hsm_get_static st
                                        else hsm_get_ephemeral st in
  [@inline_let] let pub = if initiator then hsm_get_remote_ephemeral st
                                       else hsm_get_remote_static st in
  ssdhi_get_dh_update ssdhi BS.lbytes_empty smi priv pub st


inline_for_extraction noextract
val send_message_ES_m :
  #nc : iconfig ->
  ssdhi : ssdh_impls nc ->
  smi : meta_info ->
  initiator : bool ->
  is_psk : bool ->
  st : valid_send_token_hsm nc is_psk ES smi ->
  Stack (rtype (send_token_return_type smi is_psk ES))
  (requires (fun h -> hsm_inv h st smi /\
                    (**)
                    (if initiator then smi.hsf.e == true /\ smi.hsf.rs == true
                                  else smi.hsf.s == true /\ smi.hsf.re == true)
                    (**) /\
                    get_dh_pre nc /\ get_hash_pre nc))
  (ensures (send_message_token_DH_post smi initiator is_psk ES st))

let send_message_ES_m #nc ssdhi smi initiator is_psk st =
  [@inline_let] let priv = if initiator then hsm_get_ephemeral st
                                        else hsm_get_static st in
  [@inline_let] let pub = if initiator then hsm_get_remote_static st
                                       else hsm_get_remote_ephemeral st in
  ssdhi_get_dh_update ssdhi BS.lbytes_empty smi priv pub st

#push-options "--ifuel 1"
inline_for_extraction noextract
val send_message_PSK_m :
  #nc : iconfig ->
  ssi : ss_impls nc ->
  smi : meta_info ->
  initiator : bool ->
  st : valid_send_token_hsm nc true PSK smi ->
  Stack (rtype (send_token_return_type smi true PSK))
  (requires (fun h -> hsm_inv h st smi /\ (**) smi.hsf.psk == true (**) /\
                    get_hash_pre nc))
  (ensures (send_message_token_no_fail_post smi (**) (send_token_update_smi true PSK smi) (**)
                                            initiator true PSK st null))
#pop-options

let send_message_PSK_m #nc ssi smi initiator st =
  [@inline_let] let psk = hsm_get_preshared st in
  [@inline_let] let sym_st = hsm_get_sym_state st in
  (**) hash_max_input_norm_lem (get_config nc);
  ssi_get_mix_key_and_hash ssi smi.hsf.sk psk sym_st smi.nonce

/// Some intermediate step: replace the specific preconditions/postconditions of the individual
/// [send_message] functions with the general ones. If we don't do this intermediate step,
/// the proofs explode.

/// Rk.: this intermediate post is maybe not necessary any more...

type send_message_token_m_impl (tk : message_token) =
     #nc : iconfig
  -> ssdhi : ssdh_impls nc
  -> smi : meta_info
  -> initiator : bool
  -> is_psk : bool
  -> st : valid_send_token_hsm nc is_psk tk smi
  -> out : token_message_t nc smi tk ->
  Stack (rtype (send_token_return_type smi is_psk tk))
  (requires (send_message_token_pre smi initiator is_psk tk st out))
  (ensures (send_message_token_post smi initiator is_psk tk st out))

inline_for_extraction noextract
let send_message_S_m_ : send_message_token_m_impl S =
  fun #nc ssdhi smi initiator is_psk st out ->
    send_message_S_m #nc (ssdhi_get_ssi ssdhi) smi initiator is_psk st out
/
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
Impl.Noise.SendReceive.send_message_token_m_impl Spec.Noise.Base.Definitions.E
Impl.Noise.Types.iconfig Impl.Noise.HandshakeState.ssdh_impls Spec.Noise.MetaInfo.meta_info Prims.bool Impl.Noise.HandshakeState.valid_send_token_hsm Spec.Noise.Base.Definitions.E Impl.Noise.SendReceive.token_message_t Impl.Noise.SendReceive.send_message_E_m Impl.Noise.HandshakeState.ssdhi_get_ssi Impl.Noise.Types.rtype Impl.Noise.SendReceive.send_token_return_type
let send_message_E_m_:send_message_token_m_impl E =
  
fun #nc ssdhi smi initiator is_psk st out ->
  send_message_E_m #nc (ssdhi_get_ssi ssdhi) smi initiator is_psk st out