val dstate_t_get_pid (#idc : valid_idc) (dst : dstate_t idc) :
  Tot (idc_get_pid idc).id_t
val dstate_t_get_pid (#idc : valid_idc) (dst : dstate_t idc) :
  Tot (idc_get_pid idc).id_t
let dstate_t_get_pid #idc dst =
  match dst with
  | DS_Initiator st id info spriv spub pid pinfo dv -> pid
  | DS_Responder st id info spriv spub pid pinfo dv -> pid
module Impl.Noise.API.DState

open FStar.Mul
open FStar.HyperStack
open FStar.HyperStack.ST

open Lib.RawIntTypes
open Lib.IntTypes

open Lib.Sequence
module S = Lib.Sequence
module L = FStar.List
module Seq = FStar.Seq

open Lib.Buffer
open LowStar.BufferOps

module B = LowStar.Buffer
module BS = Lib.ByteSequence
module HS = FStar.HyperStack
module ST = FStar.HyperStack.ST
module G = FStar.Ghost

open Spec.Noise.API.State.Definitions
friend Spec.Noise.API.State.Definitions
open Spec.Noise.API.State

module M = Spec.Noise.Map
module SSpec = Spec.Noise.API.State.Definitions

open Spec.Noise.API.Device.Definitions
friend Spec.Noise.API.Device.Definitions
open Spec.Noise.API.Device.Lemmas
friend Spec.Noise.API.Device.Lemmas
module DSpec = Spec.Noise.API.Device

open Spec.Noise.API.DState.Definitions
friend Spec.Noise.API.DState.Definitions
open Spec.Noise.API.DState.Lemmas
friend Spec.Noise.API.DState.Lemmas
module Spec = Spec.Noise.API.DState

open Impl.Noise.Types
open Impl.Noise.HandshakeState
open Impl.Noise.SendReceive
open Impl.Noise.RecursiveMessages
open Impl.Noise.API.State
module State = Impl.Noise.API.State
open Impl.Noise.API.Device
friend Impl.Noise.API.Device
open Impl.Noise.SymmetricState
open Impl.Noise.HandshakeState
open Impl.Noise.BufferEquality
open Impl.Noise.TypeOrUnit
open Impl.Noise.Allocate
open Spec.Noise

module LL = Impl.Noise.LinkedList
module St = Impl.Noise.Stateful

open Lib.Memzero0

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

let _align_fsti = ()

(*** Configuration, policy *)

#push-options "--ifuel 1"
[@@ noextract_to "krml"] inline_for_extraction noextract
let apply_policy (idc : idconfig) :
  stateful_validation_state (idc_get_nc idc) (stateful_validation_info idc) =

Stateful_vstate

  (* vst *)
  (apply_policy_stateful idc)

  (* recv_psk *)
  (idc_is_psk idc)

  (* validate_spec *)
  // Don't do eta-expansion, because otherwise we need functional extensionality
  // later on to prove equalities with other functions.
  (apply_policy (idc_get_dc idc))

  // validate
  (fun dv rs pinfo psk ->
   (**) let h0 = ST.get () in
   [@inline_let]
   let Mkdevice_t_raw info sk spriv spub prlg scounter peers pcounter cert = dv in
   [@inline_let] let nc = idc_get_nc idc in
   [@inline_let] let id_cl = idc_get_pid idc in
   [@inline_let] let peer_info = idc_get_info idc in
   [@inline_let] let has_s = with_onorm(peers_have_s (idc_get_pattern idc)) in
   [@inline_let] let has_psk = with_onorm(idc_is_psk idc) in
   [@inline_let] let policy = idc_get_policy idc in
   [@inline_let] let vpinfo_st = stateful_validation_info idc in

   let b =
   (raw_apply_policy nc id_cl peer_info has_s has_psk policy).validate peers rs pinfo psk in
   (**) let h1 = ST.get () in
   begin
   (**) let dv_v0 = device_t_v h0 dv in
   (**) let dv_v1 = device_t_v h1 dv in
   (**) let peers_v0 = dv_v0.DSpec.dv_peers in
   (**) let peers_v1 = LL.v h1 peers in
   (**) let peers_v1' = dv_v1.DSpec.dv_peers in
   (**) let rs_v = as_seq h0 rs in
   (**) let res_v = (raw_apply_policy nc id_cl peer_info has_s has_psk policy).validate_spec peers_v0 rs_v in
   (**) let res_v' = apply_policy_on_peers_spec (idc_get_dc idc) peers_v0 rs_v in
   (**) assert(peers_v1 == peers_v1');
   (**) assert(forall p. raw_peer_has_s #(get_config nc) #(peer_info.St.smficc_stateful.St.t ()) rs_v p ==
   (**)        DSpec.peer_has_s #(idc_get_dc idc) rs_v p);
   (**) M.lookup_pred_eq_lem (raw_peer_has_s #(get_config nc) #(peer_info.St.smficc_stateful.St.t ()) rs_v)
   (**)                      (DSpec.peer_has_s #(idc_get_dc idc) rs_v) peers_v0;
   (**) assert(res_v == res_v');
   (**) assert(
   (**)   begin
   (**)   match res_v with
   (**)   | None  -> not b
   (**)   | Some (pinfo_v, psk_v) ->
   (**)     b /\
   (**)     pinfo_v ==
   (**)     (raw_stateful_validation_info id_cl peer_info.St.smficc_stateful).St.v () h1 pinfo /\
   (**)     psk_v == lbuffer_or_unit_to_opt_lseq h1 psk
   (**)   | _ -> False
   (**)   end)
   end;   
   b)
#pop-options


#push-options "--fuel 1"
let idc_pre_receives_rs_lem (idc : valid_idc) (initiator : bool) :
  Lemma (
    let hsk = idc_get_pattern idc in
    let pre = get_receive_pre hsk initiator in
    (pre_receives_rs hsk initiator <==> Some? pre)) = ()
#pop-options

let idc_get_isc idc initiator =
  match idc () with Mkidconfig_raw nc dc pat sid pid info policy cert srlz ->
  [@inline_let] let sc_info = stateful_validation_info idc in
  [@inline_let] let peers_have_s = with_onorm(peers_have_s pat) in
  [@inline_let] let is_psk = with_onorm(idc_is_psk idc) in
  [@inline_let] let ks = with_onorm(key_slots_from_pattern initiator pat) in
  [@inline_let] let info_st = info.St.smficc_stateful in
  [@inline_let] let sc = dconfig_to_sconfig dc in
  [@inline_let] let isc =
  {
    isc_nc = nc;
    isc_sc = sc;
    isc_pattern = pat;
    isc_ks = ks;
    isc_pinfo = sc_info;
    isc_lookups_psk = idc_is_psk idc;
  } in
  (**) assert(not (isc_lookups_psk isc) || is_psk);
  (**) assert(not (lookups_psk pat initiator) || isc_lookups_psk isc);
  (**) assert(handshake_pattern_is_valid (isc_get_pattern isc));
  (**) assert(check_pattern (isc_get_pattern isc));
  (**) assert(isc_is_valid initiator isc);
  isc

let idc_get_resp_isc_is_valid (idc : valid_idc) = ()

let idc_get_validate idc initiator =
  apply_policy idc


(*** DState *)
(**** Definitions *)

/// TODO: A state doesn't necessarily need to keep a device as parameter. However,
/// implemeting this makes it difficult to make it work with the spec. A possibility
/// would be to carry around an option device, rather than a device.

/// We have to create one constructor for the initiator and one constructor for
/// the responder, because the types extracted for [state_t] will not be the same.
[@CAbstractStruct]
noeq type dstate_t_raw
  (id_t info_t
   istate_t ispriv_t ispub_t ipid_t ipinfo_t idv_t
   rstate_t rspriv_t rspub_t rpid_t rpinfo_t rdv_t : Type0) =
| DS_Initiator :
     state:istate_t
  -> id:id_t
  -> info:info_t
  -> spriv:ispriv_t
  -> spub:ispub_t
  -> pid:ipid_t
  -> pinfo:ipinfo_t
  -> dv:idv_t
  -> dstate_t_raw id_t info_t istate_t ispriv_t ispub_t ipid_t ipinfo_t idv_t
                  rstate_t rspriv_t rspub_t rpid_t rpinfo_t rdv_t
| DS_Responder :
     state:rstate_t
  -> id:id_t
  -> info:info_t
  -> spriv:rspriv_t
  -> spub:rspub_t
  -> pid:rpid_t
  -> pinfo:rpinfo_t
  -> dv:rdv_t
  -> dstate_t_raw id_t info_t istate_t ispriv_t ispub_t ipid_t ipinfo_t idv_t
                  rstate_t rspriv_t rspub_t rpid_t rpinfo_t rdv_t

[@@ noextract_to "krml"] inline_for_extraction noextract
type dstate_t (idc : valid_idc) =
  dstate_t_raw 
    (dstate_id_t idc)
    (info_t idc)
    (State.state_t (idc_get_init_isc idc) true)
    (sprivate_key_t idc true) // For now, we copy the keys inside the state. TODO: share them with the device
    (spublic_key_t idc true)
    (peer_id_opt_t idc) //(idc_get_pid idc).id_t // We don't use [peer_id_t]: [pid] might be the 'none' value
    (peer_info_t idc)
    (device_p idc)
    (State.state_t (idc_get_resp_isc idc) false)
    (sprivate_key_t idc false) // For now, we copy the keys inside the state. TODO: share them with the device
    (spublic_key_t idc false)
    (peer_id_opt_t idc) //(idc_get_pid idc).id_t // Might be the 'none' value
    (peer_info_t idc)
    (device_p idc)

[@@ noextract_to "krml"] noextract
let invert_dstate_t (idc : valid_idc) :
  Lemma
  (inversion (dstate_t idc))
  [SMTPat (dstate_t idc)] =
  allow_inversion (dstate_t idc)

noeq type dstate_p_or_null_raw (dstate_t : Type0) = {
  stp : B.pointer_or_null dstate_t;
  stp_r : HS.rid;
  // Region in which to perform the split allocations
  stp_r_split : HS.rid;
  // Region in which to allocate the pid pointers
  stp_r_pid : HS.rid;
}

[@@ noextract_to "krml"] inline_for_extraction noextract
type dstate_p_or_null (idc : valid_idc) =
  dstate_p_or_null_raw (dstate_t idc)

let dstate_p_g_is_null #idc stp = B.g_is_null stp.stp

/// A small utility to factorize the proofs and the helpers.
/// Note that we can't extract it because [isconfig] can't be extracted.
/// The first 'd' stands for 'destructed'.

inline_for_extraction noextract noeq
type gddstate_t (idc : valid_idc) = {
  gdds_initiator : bool;
  gdds_id:dstate_id_t idc;
  gdds_info:info_t idc;
  gdds_spriv:sprivate_key_t idc gdds_initiator;
  gdds_spub:spublic_key_t idc gdds_initiator;
  gdds_pid : (idc_get_pid idc).id_t;
  gdds_pinfo : peer_info_t idc;
  gdds_dv : device_p idc;
  gdds_st : state_t (idc_get_isc idc gdds_initiator) gdds_initiator;
}

inline_for_extraction noextract noeq
type ddstate_t (idc : valid_idc) (initiator : bool) = {
  dds_id:dstate_id_t idc;
  dds_info:info_t idc;
  dds_spriv:sprivate_key_t idc initiator;
  dds_spub:spublic_key_t idc initiator;
  dds_pid : (idc_get_pid idc).id_t;
  dds_pinfo : peer_info_t idc;
  dds_dv : device_p idc;
  dds_st : state_t (idc_get_isc idc initiator) initiator;
}

[@@ noextract_to "krml"] inline_for_extraction noextract
val gdestruct_dstate_t (#idc : valid_idc) (st : dstate_t idc) : GTot (gddstate_t idc)
let gdestruct_dstate_t #idc st =
  match st with
  | DS_Initiator st id info spriv spub pid pinfo dv ->
    { gdds_initiator = true; gdds_id = id; gdds_info = info;
      gdds_st = st; gdds_spriv = spriv; gdds_spub = spub;
      gdds_pid = pid; gdds_pinfo = pinfo; gdds_dv = dv }
  | DS_Responder st id info spriv spub pid pinfo dv ->
    { gdds_initiator = false; gdds_id = id; gdds_info = info;
      gdds_st = st; gdds_spriv = spriv; gdds_spub = spub;
      gdds_pid = pid; gdds_pinfo = pinfo; gdds_dv = dv }

[@@ noextract_to "krml"] inline_for_extraction noextract
val dstate_t_is_initiator :
     #idc:valid_idc
  -> st:dstate_t idc
  -> bool
let dstate_t_is_initiator #idc st =
  DS_Initiator? st

[@@ noextract_to "krml"] inline_for_extraction noextract
val destruct_dstate_t (#idc : valid_idc) (initiator : bool)
                      (st : dstate_t idc{initiator = dstate_t_is_initiator st}) :
    ddstate_t idc initiator
let destruct_dstate_t #idc initiator st =
  match st with
  | DS_Initiator st id info spriv spub pid pinfo dv ->
    { dds_st = st; dds_id = id; dds_info = info;
      dds_spriv = spriv; dds_spub = spub;
      dds_pid = pid; dds_pinfo = pinfo; dds_dv = dv }
  | DS_Responder st id info spriv spub pid pinfo dv ->
    { dds_st = st; dds_id = id; dds_info = info;
      dds_spriv = spriv; dds_spub = spub;
      dds_pid = pid; dds_pinfo = pinfo; dds_dv = dv }

[@@ noextract_to "krml"] inline_for_extraction noextract
val dstate_t_is_handshake (#idc : valid_idc) (st : dstate_t idc) : bool
let dstate_t_is_handshake #idc st =
  match st with
  | DS_Initiator st id info spriv spub pid pinfo dv -> state_t_is_handshake st
  | DS_Responder st id info spriv spub pid pinfo dv -> state_t_is_handshake st

[@@ noextract_to "krml"] inline_for_extraction noextract
let dstate_t_is_transport (#idc : valid_idc) (st : dstate_t idc) : GTot bool =
  not (dstate_t_is_handshake st)

[@@ noextract_to "krml"] inline_for_extraction noextract
val dstate_t_handshake_get_step :
     #idc:valid_idc
  -> st:dstate_t idc{dstate_t_is_handshake st}
  -> UInt32.t
let dstate_t_handshake_get_step #idc st =
  match st with
  | DS_Initiator st id info spriv spub pid pinfo dv -> state_t_handshake_get_step st
  | DS_Responder st id info spriv spub pid pinfo dv -> state_t_handshake_get_step st

[@@ noextract_to "krml"] inline_for_extraction noextract
val dstate_t_handshake_get_step_v :
     #idc:valid_idc
  -> st:dstate_t idc{dstate_t_is_handshake st}
  -> nat
let dstate_t_handshake_get_step_v #idc st =
  UInt32.v (dstate_t_handshake_get_step st)

let mk_dstate_p_null (idc : valid_idc) : stp:dstate_p_or_null idc{dstate_p_g_is_null stp} =
  { stp = B.null; stp_r = root; stp_r_split = root; stp_r_pid = root; }

[@@ noextract_to "krml"] noextract
val dstate_t_g_handshake_get_static :
     #idc:valid_idc
  -> st:dstate_t idc{dstate_t_is_handshake st}
  -> GTot (
       let initiator = dstate_t_is_initiator st in
       sprivate_key_t idc initiator & spublic_key_t idc initiator)

let dstate_t_g_handshake_get_static #idc st =
  match st with
  | DS_Initiator st id info spriv spub pid pinfo dv -> (spriv, spub)
  | DS_Responder st id info spriv spub pid pinfo dv -> (spriv, spub)

[@@ noextract_to "krml"] inline_for_extraction noextract
val dstate_t_get_device (#idc : valid_idc) (dst : dstate_t idc) : GTot (device_p idc)
let dstate_t_get_device #idc dst =
  let Mkgddstate_t initiator id info spriv spub pid pinfo dv st = gdestruct_dstate_t dst in
  dv

[@@ noextract_to "krml"] noextract
val dstate_t_get_state (#idc : valid_idc) (dst : dstate_t idc) :
  GTot (state_t (idc_get_isc idc (dstate_t_is_initiator dst)) (dstate_t_is_initiator dst))
let dstate_t_get_state #idc dst =
  let Mkgddstate_t initiator id info spriv spub pid pinfo dv st = gdestruct_dstate_t dst in
  st

let dstate_p_g_get_device #idc h dst_p =
  let dst = B.deref h dst_p.stp in
  dstate_t_get_device #idc dst

[@@ noextract_to "krml"] inline_for_extraction noextract
val dstate_t_get_pid (#idc : valid_idc) (dst : dstate_t idc) :
/
Spec.Noise.Map.fst.checked Spec.Noise.API.State.Definitions.fst.checked Spec.Noise.API.State.Definitions.fst.checked Spec.Noise.API.State.fsti.checked Spec.Noise.API.DState.Lemmas.fst.checked Spec.Noise.API.DState.Lemmas.fst.checked Spec.Noise.API.DState.Definitions.fst.checked Spec.Noise.API.DState.Definitions.fst.checked Spec.Noise.API.DState.fsti.checked Spec.Noise.API.Device.Lemmas.fst.checked Spec.Noise.API.Device.Lemmas.fst.checked Spec.Noise.API.Device.Definitions.fst.checked Spec.Noise.API.Device.Definitions.fst.checked Spec.Noise.API.Device.fsti.checked Spec.Noise.fst.checked prims.fst.checked LowStar.Monotonic.Buffer.fsti.checked LowStar.BufferOps.fst.checked LowStar.Buffer.fst.checked Lib.Sequence.fsti.checked Lib.RawIntTypes.fsti.checked Lib.Memzero0.fsti.checked Lib.IntTypes.fsti.checked Lib.ByteSequence.fsti.checked Lib.Buffer.fsti.checked Impl.Noise.Types.fst.checked Impl.Noise.TypeOrUnit.fsti.checked Impl.Noise.SymmetricState.fsti.checked Impl.Noise.Stateful.fst.checked Impl.Noise.SendReceive.fsti.checked Impl.Noise.RecursiveMessages.fst.checked Impl.Noise.LinkedList.fsti.checked Impl.Noise.HandshakeState.fsti.checked Impl.Noise.BufferEquality.fst.checked Impl.Noise.API.State.fst.checked Impl.Noise.API.Device.fst.checked Impl.Noise.API.Device.fst.checked Impl.Noise.Allocate.fst.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.List.Tot.fst.checked FStar.List.fst.checked FStar.IndefiniteDescription.fsti.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Ghost.fsti.checked
Impl.Noise.API.DState.fst
dst: Impl.Noise.API.DState.dstate_t idc -> Mkid_cl?.id_t (Impl.Noise.API.Device.idc_get_pid idc)
Impl.Noise.API.Device.valid_idc Impl.Noise.API.DState.dstate_t Impl.Noise.API.State.Base.state_t Impl.Noise.API.DState.idc_get_init_isc Impl.Noise.API.DState.dstate_id_t Impl.Noise.API.Device.info_t Impl.Noise.API.DState.sprivate_key_t Impl.Noise.API.DState.spublic_key_t Impl.Noise.API.Device.peer_id_opt_t Impl.Noise.API.Device.peer_info_t Impl.Noise.API.Device.device_p Impl.Noise.API.DState.idc_get_resp_isc Impl.Noise.API.Device.__proj__Mkid_cl__item__id_t Impl.Noise.API.Device.idc_get_pid
let dstate_t_get_pid #idc dst =
  
match dst with
| DS_Initiator st id info spriv spub pid pinfo dv -> pid
| DS_Responder st id info spriv spub pid pinfo dv -> pid