val serialize_bytes (dc : dconfig) (sk : aead_key) (name : dc.dc_info)
                    (b : bytes{Seq.length b <= aead_max_input dc.dc_nc})
                    (entr : entropy) :
  bytes & entropy
val serialize_bytes (dc : dconfig) (sk : aead_key) (name : dc.dc_info)
                    (b : bytes{Seq.length b <= aead_max_input dc.dc_nc})
                    (entr : entropy) :
  bytes & entropy
let serialize_bytes dc sk name b entr =
  let n8, n, entr' = generate_random_nonce entr in
  let name_raw = dc.dc_info_to_bytes name in
  let c = aead_encrypt dc.dc_nc sk n name_raw b in
  let c = Seq.append n8 c in
  c, entr'
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
let device_get_static #dc dv = dv.dv_static_identity
let device_get_states_counter dv = dv.dv_states_counter
let device_get_peers_counter dv = dv.dv_peers_counter

(** Small helpers for serialization/deserialization *)

let bytes_to_nonce (n8 : lbytes aead_nonce_size) : aead_nonce =
  let nonce = uint_from_bytes_le #U64 n8 in
  UInt64.v (Lib.RawIntTypes.u64_to_UInt64 nonce)

let generate_random_nonce (entr : entropy) : lbytes aead_nonce_size & aead_nonce & entropy =
  // Generate some random bytes
  let entr', n8 = crypto_random entr aead_nonce_size in
  // Convert the bytes to a nonce
  n8, bytes_to_nonce n8, entr'

val serialize_bytes (dc : dconfig) (sk : aead_key) (name : dc.dc_info)
                    (b : bytes{Seq.length b <= aead_max_input dc.dc_nc})
                    (entr : entropy) :
  bytes & entropy
/
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

    dc: Spec.Noise.API.Device.Definitions.dconfig ->
    sk: Spec.Noise.CryptoPrimitives.aead_key ->
    name: Mkdconfig?.dc_info dc ->
    b:
      Lib.ByteSequence.bytes
        { FStar.Seq.Base.length b <=
          Spec.Noise.CryptoPrimitives.aead_max_input (Mkdconfig?.dc_nc dc) } ->
    entr: Lib.RandomSequence.entropy
  -> Lib.ByteSequence.bytes * Lib.RandomSequence.entropy
Spec.Noise.API.Device.Definitions.dconfig Spec.Noise.CryptoPrimitives.aead_key Spec.Noise.API.Device.Definitions.__proj__Mkdconfig__item__dc_info Lib.ByteSequence.bytes Prims.b2t Prims.op_LessThanOrEqual FStar.Seq.Base.length Lib.IntTypes.uint_t Lib.IntTypes.U8 Lib.IntTypes.SEC Spec.Noise.CryptoPrimitives.aead_max_input Spec.Noise.API.Device.Definitions.__proj__Mkdconfig__item__dc_nc Lib.RandomSequence.entropy Lib.ByteSequence.lbytes Spec.Noise.CryptoPrimitives.aead_nonce_size Spec.Noise.CryptoPrimitives.aead_nonce FStar.Pervasives.Native.Mktuple2 FStar.Seq.Base.seq Lib.IntTypes.int_t FStar.Seq.Base.append Lib.Sequence.seq Prims.eq2 Prims.int Lib.Sequence.length Prims.op_Addition Spec.Noise.CryptoPrimitives.aead_tag_size Spec.Noise.CryptoPrimitives.aead_encrypt Prims.pow2 Spec.Noise.API.Device.Definitions.__proj__Mkdconfig__item__dc_info_to_bytes FStar.Pervasives.Native.tuple2 FStar.Pervasives.Native.tuple3 Lib.Sequence.lseq Spec.Noise.API.Device.Definitions.generate_random_nonce
let serialize_bytes dc sk name b entr =
  
let n8, n, entr' = generate_random_nonce entr in
let name_raw = dc.dc_info_to_bytes name in
let c = aead_encrypt dc.dc_nc sk n name_raw b in
let c = Seq.append n8 c in
c, entr'