val device_get_states_counter : #dc:dconfig -> dv:device dc -> state_id
val device_get_states_counter : #dc:dconfig -> dv:device dc -> state_id
let device_get_states_counter dv = dv.dv_states_counter
module Spec.Noise.API.Device.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
open Spec.Noise.Utils
module M = Spec.Noise.Map

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

(*** Peer *)

noeq type raw_peer (nc : config) (info_ty : Type0) : Type0 = {
  p_id : peer_id; // identifier in the table
  p_info : info_ty; // meta-data provided by the end-user
  p_s : option (public_key nc);
  p_psk : option preshared_key;
}

let peer_get_id #dc p = p.p_id
let peer_get_info #dc p = p.p_info
let peer_get_static #dc p = p.p_s
let peer_get_psk #dc p = p.p_psk

let raw_peer_has_s (#nc : config) (#info_ty : Type0) (s : public_key nc) (p : raw_peer nc info_ty) :
  Tot bool =
  match p.p_s with
  | None -> false
  | Some k -> lbytes_eq k s

(*** Device *)
(* A device handles one static identity and one handshake pattern. The user
 * can of course use several devices at the same time.
 * Stores the list of peers.
 * Is used for example to lookup keys: when creating a state, we may not know
 * who we are talking to, once we know (i.e.: after having received a public
 * static key) we can lookup information like the psk associated to this peer. *)
// TODO: make the device parametric in the dconfig?

noeq type device (dc : dconfig) = {
  dv_pattern : wfs_handshake_pattern;
  dv_info : dc.dc_info; // TODO: rename to dv_name
  dv_sk : option aead_key;
  dv_static_identity : option (keypair dc.dc_nc);
  dv_prologue : hashable dc.dc_nc;
  dv_states_counter : state_id;
  dv_peers : M.t (peer dc);
  dv_peers_counter : peer_id;
}

let device_get_pattern dv = dv.dv_pattern
let device_get_peers dv = dv.dv_peers
let device_get_info dv = dv.dv_info
/
Spec.Noise.Utils.fst.checked 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 prims.fst.checked Lib.RawIntTypes.fsti.checked Lib.ByteSequence.fsti.checked FStar.UInt64.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.List.Tot.fst.checked
Spec.Noise.API.Device.Definitions.fst
dv: Spec.Noise.API.Device.Definitions.device dc -> Spec.Noise.API.Device.Definitions.state_id
Spec.Noise.API.Device.Definitions.dconfig Spec.Noise.API.Device.Definitions.device Spec.Noise.API.Device.Definitions.__proj__Mkdevice__item__dv_states_counter Spec.Noise.API.Device.Definitions.state_id
let device_get_states_counter dv =
  
dv.dv_states_counter