val peer_get_info : #dc:dconfig -> p:peer dc -> dc.dc_info
val peer_get_info : #dc:dconfig -> p:peer dc -> dc.dc_info
let peer_get_info #dc p = p.p_info
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;
}
/
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
p: Spec.Noise.API.Device.Definitions.peer dc -> Mkdconfig?.dc_info dc
Spec.Noise.API.Device.Definitions.dconfig Spec.Noise.API.Device.Definitions.peer Spec.Noise.API.Device.Definitions.__proj__Mkraw_peer__item__p_info Spec.Noise.API.Device.Definitions.__proj__Mkdconfig__item__dc_nc Spec.Noise.API.Device.Definitions.__proj__Mkdconfig__item__dc_info
let peer_get_info #dc p =
  
p.p_info