val create_device_from_serialized
  (#dc:dconfig) (dv:device dc) (entr:entropy) :
  Lemma
  // TODO: remove this precondition once we remove the precondition on the
  // length of the encrypted data
  (requires (
    Some? dv.dv_static_identity /\
    // The public key was computed from the private key
    dv.dv_static_identity == keypair_from_private (Some?.v dv.dv_static_identity).priv))
  (ensures (
    match serialize_device_secret dv entr with
    | None, _ -> None? dv.dv_sk \/ None? dv.dv_static_identity
    | Some enc_key, _ ->
      // TODO: we shouldn't have a precondition on the length of the encrypted data
      // given to the device
      Some? dv.dv_sk /\ Some? dv.dv_static_identity /\
      Seq.length enc_key = enc_private_key_with_nonce_size dc.dc_nc /\
      begin match create_device_from_secret dc dv.dv_pattern dv.dv_prologue dv.dv_info (Some?.v dv.dv_sk) (Some enc_key) with
      | None -> False
      | Some dv' ->
        dv' == { dv with dv_states_counter = 0; dv_peers = []; dv_peers_counter = 0; }
      end))
val create_device_from_serialized
  (#dc:dconfig) (dv:device dc) (entr:entropy) :
  Lemma
  // TODO: remove this precondition once we remove the precondition on the
  // length of the encrypted data
  (requires (
    Some? dv.dv_static_identity /\
    // The public key was computed from the private key
    dv.dv_static_identity == keypair_from_private (Some?.v dv.dv_static_identity).priv))
  (ensures (
    match serialize_device_secret dv entr with
    | None, _ -> None? dv.dv_sk \/ None? dv.dv_static_identity
    | Some enc_key, _ ->
      // TODO: we shouldn't have a precondition on the length of the encrypted data
      // given to the device
      Some? dv.dv_sk /\ Some? dv.dv_static_identity /\
      Seq.length enc_key = enc_private_key_with_nonce_size dc.dc_nc /\
      begin match create_device_from_secret dc dv.dv_pattern dv.dv_prologue dv.dv_info (Some?.v dv.dv_sk) (Some enc_key) with
      | None -> False
      | Some dv' ->
        dv' == { dv with dv_states_counter = 0; dv_peers = []; dv_peers_counter = 0; }
      end))
let create_device_from_serialized #dc dv entr =
  match dv.dv_sk, dv.dv_static_identity with
  | None, _ -> ()
  | _, None -> ()
  | Some sk, Some s ->
    let enc_s, entr' = serialize_bytes dc sk dv.dv_info s.priv entr in
    assert(Seq.length enc_s = enc_private_key_with_nonce_size dc.dc_nc);
    deserialize_serialize_bytes_eq dc sk dv.dv_info s.priv entr;
    assert(
      match Spec.Noise.API.Device.Definitions.deserialize_bytes dc sk dv.dv_info enc_s with
      | None  -> False
      | Some s' -> Mkkeypair?.priv s == s');
    let res = create_device_from_secret dc dv.dv_pattern dv.dv_prologue dv.dv_info sk (Some enc_s) in
    match res with
    | None -> assert(False)
    | Some dv' -> ()
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')

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

val create_device_from_serialized
  (#dc:dconfig) (dv:device dc) (entr:entropy) :
  Lemma
  // TODO: remove this precondition once we remove the precondition on the
  // length of the encrypted data
  (requires (
    Some? dv.dv_static_identity /\
    // The public key was computed from the private key
    dv.dv_static_identity == keypair_from_private (Some?.v dv.dv_static_identity).priv))
  (ensures (
    match serialize_device_secret dv entr with
    | None, _ -> None? dv.dv_sk \/ None? dv.dv_static_identity
    | Some enc_key, _ ->
      // TODO: we shouldn't have a precondition on the length of the encrypted data
      // given to the device
      Some? dv.dv_sk /\ Some? dv.dv_static_identity /\
      Seq.length enc_key = enc_private_key_with_nonce_size dc.dc_nc /\
      begin match create_device_from_secret dc dv.dv_pattern dv.dv_prologue dv.dv_info (Some?.v dv.dv_sk) (Some enc_key) with
      | None -> False
      | Some dv' ->
        dv' == { dv with dv_states_counter = 0; dv_peers = []; dv_peers_counter = 0; }
      end))
/
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 -> entr: Lib.RandomSequence.entropy
  -> FStar.Pervasives.Lemma
      (requires
        Some? (Mkdevice?.dv_static_identity dv) /\
        Mkdevice?.dv_static_identity dv ==
        Spec.Noise.Utils.keypair_from_private (Mkkeypair?.priv (Some?.v (Mkdevice?.dv_static_identity
                      dv))))
      (ensures
        ((match Spec.Noise.API.Device.Definitions.serialize_device_secret dv entr with
            | FStar.Pervasives.Native.Mktuple2 #_ #_ (FStar.Pervasives.Native.None #_) _ ->
              None? (Mkdevice?.dv_sk dv) \/ None? (Mkdevice?.dv_static_identity dv)
            | FStar.Pervasives.Native.Mktuple2 #_ #_ (FStar.Pervasives.Native.Some #_ enc_key) _ ->
              Some? (Mkdevice?.dv_sk dv) /\ Some? (Mkdevice?.dv_static_identity dv) /\
              FStar.Seq.Base.length enc_key =
              Spec.Noise.API.Device.Definitions.enc_private_key_with_nonce_size (Mkdconfig?.dc_nc dc
                ) /\
              (match
                  Spec.Noise.API.Device.Definitions.create_device_from_secret dc
                    (Mkdevice?.dv_pattern dv)
                    (Mkdevice?.dv_prologue dv)
                    (Mkdevice?.dv_info dv)
                    (Some?.v (Mkdevice?.dv_sk dv))
                    (FStar.Pervasives.Native.Some enc_key)
                with
                | FStar.Pervasives.Native.None #_ -> Prims.l_False
                | FStar.Pervasives.Native.Some #_ dv' ->
                  dv' ==
                  Spec.Noise.API.Device.Definitions.Mkdevice (Mkdevice?.dv_pattern dv)
                    (Mkdevice?.dv_info dv)
                    (Mkdevice?.dv_sk dv)
                    (Mkdevice?.dv_static_identity dv)
                    (Mkdevice?.dv_prologue dv)
                    0
                    []
                    0))
          <:
          Type0))
Spec.Noise.API.Device.Definitions.dconfig Spec.Noise.API.Device.Definitions.device Lib.RandomSequence.entropy FStar.Pervasives.Native.Mktuple2 FStar.Pervasives.Native.option Spec.Noise.CryptoPrimitives.aead_key Spec.Noise.CryptoPrimitives.keypair Spec.Noise.API.Device.Definitions.__proj__Mkdconfig__item__dc_nc Spec.Noise.API.Device.Definitions.__proj__Mkdevice__item__dv_sk Spec.Noise.API.Device.Definitions.__proj__Mkdevice__item__dv_static_identity Lib.ByteSequence.bytes Prims._assert Prims.l_False Prims.unit Spec.Noise.API.Device.Definitions.create_device_from_secret Spec.Noise.API.Device.Definitions.__proj__Mkdevice__item__dv_pattern Spec.Noise.API.Device.Definitions.__proj__Mkdevice__item__dv_prologue Spec.Noise.API.Device.Definitions.__proj__Mkdevice__item__dv_info FStar.Pervasives.Native.Some Spec.Noise.API.Device.Definitions.enc_private_key_with_nonce Spec.Noise.API.Device.Definitions.deserialize_bytes Prims.b2t Prims.op_Equality Prims.int Prims.op_Addition FStar.Seq.Base.length Lib.IntTypes.uint_t Lib.IntTypes.U8 Lib.IntTypes.SEC Spec.Noise.CryptoPrimitives.aead_tag_size Spec.Noise.CryptoPrimitives.aead_nonce_size Prims.eq2 Lib.Sequence.seq Prims.l_or Prims.nat Spec.Noise.CryptoPrimitives.private_key_size Spec.Noise.CryptoPrimitives.__proj__Mkkeypair__item__priv Spec.Noise.API.Device.Lemmas.deserialize_serialize_bytes_eq Spec.Noise.API.Device.Definitions.enc_private_key_with_nonce_size FStar.Pervasives.Native.tuple2 Lib.IntTypes.int_t Spec.Noise.API.Device.Definitions.serialize_bytes
let create_device_from_serialized #dc dv entr =
  
match dv.dv_sk, dv.dv_static_identity with
| None, _ -> ()
| _, None -> ()
| Some sk, Some s ->
  let enc_s, entr' = serialize_bytes dc sk dv.dv_info s.priv entr in
  assert (Seq.length enc_s = enc_private_key_with_nonce_size dc.dc_nc);
  deserialize_serialize_bytes_eq dc sk dv.dv_info s.priv entr;
  assert (match Spec.Noise.API.Device.Definitions.deserialize_bytes dc sk dv.dv_info enc_s with
      | None -> False
      | Some s' -> Mkkeypair?.priv s == s');
  let res = create_device_from_secret dc dv.dv_pattern dv.dv_prologue dv.dv_info sk (Some enc_s) in
  match res with
  | None -> assert (False)
  | Some dv' -> ()