val raw_peer_has_s (#nc: config) (#info_ty: Type0) (s: public_key nc) (p: raw_peer nc info_ty)
    : Tot bool
val raw_peer_has_s (#nc: config) (#info_ty: Type0) (s: public_key nc) (p: raw_peer nc info_ty)
    : Tot bool
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
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
/
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

    s: Spec.Noise.CryptoPrimitives.public_key nc ->
    p: Spec.Noise.API.Device.Definitions.raw_peer nc info_ty
  -> Prims.bool
Spec.Noise.CryptoPrimitives.config Spec.Noise.CryptoPrimitives.public_key Spec.Noise.API.Device.Definitions.raw_peer Spec.Noise.API.Device.Definitions.__proj__Mkraw_peer__item__p_s Lib.ByteSequence.lbytes_eq Spec.Noise.CryptoPrimitives.public_key_size Prims.bool
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