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))
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
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))
/
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
dv: Spec.Noise.API.Device.Definitions.device dc -> id: Spec.Noise.API.Device.Definitions.peer_id
  -> FStar.Pervasives.Lemma
      (requires
        Spec.Noise.API.Device.Definitions.dv_peers_counter_invariant dv /\
        Spec.Noise.API.Device.Definitions.peers_pairwise_distinct_ids (Mkdevice?.dv_peers dv) /\
        Spec.Noise.API.Device.Definitions.peers_pairwise_distinct_statics (Mkdevice?.dv_peers dv))
      (ensures
        (let dv' = Spec.Noise.API.Device.Definitions.remove_peer dv id in
          Spec.Noise.API.Device.Definitions.dv_peers_counter_invariant dv' /\
          Spec.Noise.API.Device.Definitions.peers_pairwise_distinct_ids (Mkdevice?.dv_peers dv') /\
          Spec.Noise.API.Device.Definitions.peers_pairwise_distinct_statics (Mkdevice?.dv_peers dv')
        ))
Spec.Noise.API.Device.Definitions.dconfig Spec.Noise.API.Device.Definitions.device Spec.Noise.API.Device.Definitions.peer_id Spec.Noise.Map.filter_one_preserves_pairwise_rel Spec.Noise.API.Device.Definitions.peer Spec.Noise.API.Device.Definitions.peers_distinct_statics Spec.Noise.API.Device.Definitions.peer_has_not_id Spec.Noise.API.Device.Definitions.__proj__Mkdevice__item__dv_peers Prims.unit Spec.Noise.API.Device.Definitions.peers_distinct_ids Spec.Noise.Map.filter_one_preserves_for_all Spec.Noise.API.Device.Definitions.peer_has_smaller_id Spec.Noise.API.Device.Definitions.__proj__Mkdevice__item__dv_peers_counter
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