val dstate_get_remote_static :
     #dc:dconfig
  -> st:dstate dc{dstate_is_handshake st} ->
  Tot (option (public_key dc.dc_nc))
val dstate_get_remote_static :
     #dc:dconfig
  -> st:dstate dc{dstate_is_handshake st} ->
  Tot (option (public_key dc.dc_nc))
let dstate_get_remote_static #dc dst = State.state_get_rs dst.dst_state
module Spec.Noise.API.DState.Definitions

open Lib.ByteSequence
open FStar.Mul
open FStar.List.Tot

friend Spec.Noise.Base.Definitions
module Base = Spec.Noise.Base.Definitions
module State = Spec.Noise.API.State.Definitions
friend Spec.Noise.API.State.Definitions
friend Spec.Noise.API.Device.Definitions
module M = Spec.Noise.Map
open Spec.Noise.API.MetaInfo

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

(*** API *)

let s_error_to_ds_error (e : State.s_error) : ds_error =
  match e with
  | State.Incorrect_transition -> Incorrect_transition
  | State.Premessage -> Premessage
  | State.No_key -> No_key
  | State.Already_key -> Already_key
  | State.Rs_not_valid -> Rs_rejected_by_policy
  | State.Input_size -> Input_size
  | State.DH_error -> DH_error
  | State.Decryption -> Decryption
  | State.Saturated_nonce -> Saturated_nonce

(*** Configuration *)

val apply_policy (dc : dconfig) :
  State.validation_function dc.dc_nc (device dc)
                            (option (peer_id & dc.dc_info))

let apply_policy dc dv rs =
  (* Lookup the associated peer *)
  match lookup_peer_by_static dv rs with
  | Some p ->
    (* There is a peer: nothing to validate *)
    Some (Some (p.p_id, p.p_info), p.p_psk)
  | None ->
    (* No peer: apply the policy *)
    if dc.dc_policy rs then
      (* Success *)
      Some (None, None)
    else
      (* Failure *)
      None

let dconfig_to_sconfig dc =
  {
    State.sc_config = dc.dc_nc;
    State.sc_vstate = device dc;
    State.sc_pinfo = option (peer_id & dc.dc_info);
    State.sc_validate = apply_policy dc;
  }

(*** DState *)

/// The dstate definition
// TODO: the implementation keeps the static keys even when in transport phase
noeq type dstate (dc : dconfig) = {
  dst_state : s:State.state (dconfig_to_sconfig dc){check_swf (State.state_get_pattern s)};
  dst_id : state_id;
  dst_info : dc.dc_info;
  dst_pid : option peer_id;
  dst_pinfo : option dc.dc_info;
}

let dstate_get_pattern #dc dst =
  State.state_get_pattern dst.dst_state

let dstate_get_status #dc dst =
  State.state_get_status dst.dst_state

let dstate_is_initiator #dc dst =
  State.state_is_initiator dst.dst_state

let dstate_is_handshake #dc dst =
  State.state_is_handshake dst.dst_state

let dstate_is_stuck #dc dst =
  let n = List.Tot.length (dstate_get_pattern #dc dst).messages in
  let status = dstate_get_status dst in
  let is_handshake_state = not (State.Transport? status) in
  if is_handshake_state then
    let step = match status with | State.Handshake_send i | State.Handshake_receive i -> i in
    step >= n + 1
  else false

let dstate_get_id #dc dst = dst.dst_id
let dstate_get_info #dc dst = dst.dst_info
let dstate_get_peer_id #dc dst = dst.dst_pid
let dstate_get_peer_info #dc dst = dst.dst_pinfo
/
Spec.Noise.Map.fst.checked Spec.Noise.Base.Definitions.fst.checked Spec.Noise.API.State.Definitions.fst.checked Spec.Noise.API.State.Definitions.fst.checked Spec.Noise.API.MetaInfo.fst.checked Spec.Noise.API.Device.Definitions.fst.checked prims.fst.checked Lib.ByteSequence.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.List.Tot.fst.checked
Spec.Noise.API.DState.Definitions.fst

    st:
      Spec.Noise.API.DState.Definitions.dstate dc
        {Spec.Noise.API.DState.Definitions.dstate_is_handshake st}
  -> FStar.Pervasives.Native.option (Spec.Noise.CryptoPrimitives.public_key (Mkdconfig?.dc_nc dc))
Spec.Noise.API.Device.Definitions.dconfig Spec.Noise.API.DState.Definitions.dstate Prims.b2t Spec.Noise.API.DState.Definitions.dstate_is_handshake Spec.Noise.API.State.Definitions.state_get_rs Spec.Noise.API.DState.Definitions.dconfig_to_sconfig Spec.Noise.API.DState.Definitions.__proj__Mkdstate__item__dst_state FStar.Pervasives.Native.option Spec.Noise.CryptoPrimitives.public_key Spec.Noise.API.Device.Definitions.__proj__Mkdconfig__item__dc_nc
let dstate_get_remote_static #dc dst =
  
State.state_get_rs dst.dst_state