val deserialize_serialize_bytes_eq
  (dc : dconfig) (sk : aead_key) (name : dc.dc_info)
  (b : bytes{Seq.length b <= aead_max_input dc.dc_nc})
  (entr : entropy) :
    Lemma (
      let c, _ = serialize_bytes dc sk name b entr in
      // Note: doesn't work if we write an equality without the match
      match deserialize_bytes dc sk name c with
      | None -> False
      | Some b' -> b == b')
val deserialize_serialize_bytes_eq
  (dc : dconfig) (sk : aead_key) (name : dc.dc_info)
  (b : bytes{Seq.length b <= aead_max_input dc.dc_nc})
  (entr : entropy) :
    Lemma (
      let c, _ = serialize_bytes dc sk name b entr in
      // Note: doesn't work if we write an equality without the match
      match deserialize_bytes dc sk name c with
      | None -> False
      | Some b' -> b == b')
let deserialize_serialize_bytes_eq 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 c0 = aead_encrypt dc.dc_nc sk n name_raw b in
  let c1 = Seq.append n8 c0 in
  let n8', c' = Seq.split c1 aead_nonce_size in
  let n' = bytes_to_nonce n8' in
  assert(Seq.equal n8' n8);
  assert(n' = n);
  assert(Seq.equal c' c0);
  Spec.Noise.CryptoPrimitives.aead_correctness dc.dc_nc sk n name_raw b
module Spec.Noise.API.Device.Lemmas

open Lib.ByteSequence
open Spec.Noise.API.State.Definitions
module State = Spec.Noise.API.State.Definitions
open Spec.Noise.API.Device.Definitions
friend Spec.Noise.API.Device.Definitions
module M = Spec.Noise.Map
open Spec.Noise.CryptoPrimitives
open FStar.List.Tot
open Spec.Noise.Utils

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

(*** Invariant preservation *)
(**** Add peer *)
val add_peer_get_distinct_ids_lem :
     #dc:dconfig
  -> dv:device dc
  -> pinfo:dc.dc_info
  -> rs:option (public_key dc.dc_nc)
  -> psk:option preshared_key ->
  Lemma
  (requires
    dv_peers_counter_invariant dv /\
    peers_pairwise_distinct_ids dv.dv_peers)
  (ensures (
    match add_peer_get dv pinfo rs psk with
    | None -> True
    | Some (p, dv') ->
      dv_peers_counter_invariant dv' /\
      peers_pairwise_distinct_ids dv'.dv_peers))

#push-options "--fuel 1"
let add_peer_get_distinct_ids_lem #dc dv pinfo rs psk =
  match add_peer_get dv pinfo rs psk with
  | None -> ()
  | Some (p, dv') ->
    for_all_mem (peer_has_smaller_id dv.dv_peers_counter) dv.dv_peers;
    for_all_mem (peer_has_smaller_id dv'.dv_peers_counter) dv.dv_peers;
    assert(dv_peers_counter_invariant dv');
    for_all_mem (peers_distinct_ids p) dv.dv_peers
#pop-options

val add_peer_get_distinct_statics_lem :
     #dc:dconfig
  -> dv:device dc
  -> pinfo:dc.dc_info
  -> rs:option (public_key dc.dc_nc)
  -> psk:option preshared_key ->
  Lemma
  (requires
    peers_pairwise_distinct_statics dv.dv_peers)
  (ensures (
    match add_peer_get dv pinfo rs psk with
    | None -> True
    | Some (p, dv') ->
      peers_pairwise_distinct_statics dv'.dv_peers))

#push-options "--fuel 1 --ifuel 1"
let add_peer_get_distinct_statics_lem #dc dv pinfo rs psk =
  match add_peer_get dv pinfo rs psk with
  | None -> ()
  | Some (p, dv') ->
    match rs with
    | None ->
      M.forall_implies_list_for_all (peers_distinct_statics p) dv.dv_peers
    | Some rs ->
      M.tryFind_not_is_for_all_lem (peer_has_s rs)
                                   peers_distinct_statics
                                   p dv.dv_peers
#pop-options

val add_peer_get_invariant_preservation_lem :
     #dc:dconfig
  -> dv:device dc
  -> pinfo:dc.dc_info
  -> rs:option (public_key dc.dc_nc)
  -> psk:option preshared_key ->
  Lemma
  (requires
    dv_peers_counter_invariant dv /\
    peers_pairwise_distinct_ids dv.dv_peers /\
    peers_pairwise_distinct_statics dv.dv_peers)
  (ensures (
    match add_peer_get dv pinfo rs psk with
    | None -> True
    | Some (p, dv') ->
      dv_peers_counter_invariant dv' /\
      peers_pairwise_distinct_ids dv'.dv_peers /\
      peers_pairwise_distinct_statics dv'.dv_peers))

let add_peer_get_invariant_preservation_lem #dc dv pinfo rs psk =
  add_peer_get_distinct_ids_lem #dc dv pinfo rs psk;
  add_peer_get_distinct_statics_lem #dc dv pinfo rs psk

(**** Remove peer *)

val remove_peer_invariant_lem :
     #dc:dconfig
  -> dv:device dc
  -> id:peer_id ->
  Lemma
  (requires
    dv_peers_counter_invariant dv /\
    peers_pairwise_distinct_ids dv.dv_peers /\
    peers_pairwise_distinct_statics dv.dv_peers)
  (ensures (
    let dv' = remove_peer dv id in
    dv_peers_counter_invariant dv' /\
    peers_pairwise_distinct_ids dv'.dv_peers /\
    peers_pairwise_distinct_statics dv'.dv_peers))

let remove_peer_invariant_lem #dc dv id =
  M.filter_one_preserves_for_all (peer_has_smaller_id dv.dv_peers_counter) (peer_has_not_id id) dv.dv_peers;
  M.filter_one_preserves_pairwise_rel peers_distinct_ids (peer_has_not_id id) dv.dv_peers;
  M.filter_one_preserves_pairwise_rel peers_distinct_statics (peer_has_not_id id) dv.dv_peers


(*** Misc *)
val lookup_peer_by_id_same_id :
     #dc:dconfig
  -> dv:device dc
  -> id:peer_id ->
  Lemma (
    match lookup_peer_by_id dv id with
    | None -> True
    | Some p -> p.p_id = id)

let lookup_peer_by_id_same_id #dc dv id =
  M.tryFind_lem (peer_has_id id) dv.dv_peers

val lookup_peer_by_static_same_static :
     #dc:dconfig
  -> dv:device dc
  -> s : public_key dc.dc_nc ->
  Lemma(
    match lookup_peer_by_static dv s with
    | None -> True
    | Some p -> Some? p.p_s /\ Some?.v p.p_s == s)

let lookup_peer_by_static_same_static #dc dv s =
  M.tryFind_lem (peer_has_s s) dv.dv_peers

(*** Serialization/deserialization *)

open Lib.RandomSequence

val deserialize_serialize_bytes_eq
  (dc : dconfig) (sk : aead_key) (name : dc.dc_info)
  (b : bytes{Seq.length b <= aead_max_input dc.dc_nc})
  (entr : entropy) :
    Lemma (
      let c, _ = serialize_bytes dc sk name b entr in
      // Note: doesn't work if we write an equality without the match
      match deserialize_bytes dc sk name c with
      | None -> False
      | Some b' -> b == b')
/
Spec.Noise.Utils.fst.checked Spec.Noise.Map.fst.checked Spec.Noise.CryptoPrimitives.fsti.checked Spec.Noise.API.State.Definitions.fsti.checked Spec.Noise.API.Device.Definitions.fst.checked Spec.Noise.API.Device.Definitions.fst.checked prims.fst.checked Lib.RandomSequence.fsti.checked Lib.ByteSequence.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked
Spec.Noise.API.Device.Lemmas.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
  -> FStar.Pervasives.Lemma
    (ensures
      (let _ = Spec.Noise.API.Device.Definitions.serialize_bytes dc sk name b entr in
        (let FStar.Pervasives.Native.Mktuple2 #_ #_ c _ = _ in
          (match Spec.Noise.API.Device.Definitions.deserialize_bytes dc sk name c with
            | FStar.Pervasives.Native.None #_ -> Prims.l_False
            | FStar.Pervasives.Native.Some #_ b' -> b == b')
          <:
          Type0)
        <:
        Type0))
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.Seq.Base.seq Spec.Noise.CryptoPrimitives.aead_correctness Prims.unit Prims._assert FStar.Seq.Base.equal Prims.op_Equality Spec.Noise.API.Device.Definitions.bytes_to_nonce FStar.Pervasives.Native.tuple2 Lib.IntTypes.int_t FStar.Seq.Properties.split 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.tuple3 Lib.Sequence.lseq Spec.Noise.API.Device.Definitions.generate_random_nonce
let deserialize_serialize_bytes_eq 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 c0 = aead_encrypt dc.dc_nc sk n name_raw b in
let c1 = Seq.append n8 c0 in
let n8', c' = Seq.split c1 aead_nonce_size in
let n' = bytes_to_nonce n8' in
assert (Seq.equal n8' n8);
assert (n' = n);
assert (Seq.equal c' c0);
Spec.Noise.CryptoPrimitives.aead_correctness dc.dc_nc sk n name_raw b