val dstate_get_pattern : #dc:dconfig -> dstate dc -> wfs_handshake_pattern
val dstate_get_pattern : #dc:dconfig -> dstate dc -> wfs_handshake_pattern
let dstate_get_pattern #dc dst =
  State.state_get_pattern 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;
}
/
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
dst: Spec.Noise.API.DState.Definitions.dstate dc -> Spec.Noise.SPatterns.wfs_handshake_pattern
Spec.Noise.API.Device.Definitions.dconfig Spec.Noise.API.DState.Definitions.dstate Spec.Noise.API.State.Definitions.state_get_pattern Spec.Noise.API.DState.Definitions.dconfig_to_sconfig Spec.Noise.API.DState.Definitions.__proj__Mkdstate__item__dst_state Spec.Noise.SPatterns.wfs_handshake_pattern
let dstate_get_pattern #dc dst =
  
State.state_get_pattern dst.dst_state