val mk_dstate_p_compute_next_message_len
  (#idc:valid_idc) (out : B.pointer size_t)
  (dst_p : dstate_p idc) (payload_len : size_t) :
  Stack bool
  (requires (fun h0 ->
    B.live h0 out /\
    dstate_p_invariant h0 dst_p))
  (ensures (fun h0 b h1 ->
    B.(modifies (loc_buffer out) h0 h1) /\
    begin
    let nc = idc_get_config idc in
    let pat = idc_get_pattern idc in
    let dst_v = dstate_p_v h0 dst_p in
    (**) normalize_term_spec(List.Tot.length pat.messages);
    if b then
      match dstate_get_status dst_v with
      | Spec.Noise.API.State.Handshake_receive step
      | Spec.Noise.API.State.Handshake_send step ->
        step < List.Tot.length pat.messages /\
        size_v (B.deref h1 out) =
          size_v payload_len + compute_message_length nc pat step
      | Spec.Noise.API.State.Transport ->
        size_v (B.deref h1 out) = size_v payload_len + aead_tag_vsv
    else True
    end))
val mk_dstate_p_compute_next_message_len
  (#idc:valid_idc) (out : B.pointer size_t)
  (dst_p : dstate_p idc) (payload_len : size_t) :
  Stack bool
  (requires (fun h0 ->
    B.live h0 out /\
    dstate_p_invariant h0 dst_p))
  (ensures (fun h0 b h1 ->
    B.(modifies (loc_buffer out) h0 h1) /\
    begin
    let nc = idc_get_config idc in
    let pat = idc_get_pattern idc in
    let dst_v = dstate_p_v h0 dst_p in
    (**) normalize_term_spec(List.Tot.length pat.messages);
    if b then
      match dstate_get_status dst_v with
      | Spec.Noise.API.State.Handshake_receive step
      | Spec.Noise.API.State.Handshake_send step ->
        step < List.Tot.length pat.messages /\
        size_v (B.deref h1 out) =
          size_v payload_len + compute_message_length nc pat step
      | Spec.Noise.API.State.Transport ->
        size_v (B.deref h1 out) = size_v payload_len + aead_tag_vsv
    else True
    end))
let mk_dstate_p_compute_next_message_len #idc out dst_p payload_len =
  let dst = B.index dst_p.stp 0ul in
  mk_dstate_t_compute_next_message_len #idc out dst payload_len
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) :
  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

[@@ noextract_to "krml"] noextract
val dstate_t_core_footprint (#idc : valid_idc) (st : dstate_t idc) : GTot B.loc
let dstate_t_core_footprint #idc st =
  let Mkgddstate_t initiator id info spriv spub pid pinfo dv st = gdestruct_dstate_t st in
  B.(loc_union (state_t_core_footprint st)
    (loc_union (idc_get_info_footprint info) (idc_get_info_footprint pinfo)))

[@@ noextract_to "krml"] noextract
val dstate_t_footprint (#idc : valid_idc) (st : dstate_t idc) : GTot B.loc
let dstate_t_footprint #idc st =
  let Mkgddstate_t initiator id info spriv spub pid pinfo dv st = gdestruct_dstate_t st in
  // The static keys footprint is actually already included in [state_t_footprint],
  // but as it is abstract, counting them twice makes reasoning easier.
  B.(loc_union (loc_union (state_t_footprint st)
               (loc_union (idc_get_info_footprint info) (idc_get_info_footprint pinfo)))
               (loc_union (lbuffer_or_unit_to_loc spriv) (lbuffer_or_unit_to_loc spub)))

[@@ noextract_to "krml"] noextract
val dstate_t_footprint_with_device (#idc : valid_idc) (dst : dstate_t idc) : GTot B.loc
let dstate_t_footprint_with_device #idc dst =
  let Mkgddstate_t initiator id info spriv spub pid pinfo dv st = gdestruct_dstate_t dst in
  B.(loc_union (dstate_t_footprint dst) (device_p_region_of dv))

[@@ noextract_to "krml"] inline_for_extraction noextract
val dstate_t_has_static (#idc : valid_idc) (st : dstate_t idc) : bool
let dstate_t_has_static #idc st =
  let initiator = dstate_t_is_initiator st in
  isc_get_s (idc_get_isc idc initiator)

[@@ noextract_to "krml"] noextract
val device_p_owns_dstate_t
  (#idc : valid_idc) (h : mem) (dvp : device_p idc) (st : dstate_t idc) : GTot Type0
let device_p_owns_dstate_t #idc h dvp dst =
  let Mkgddstate_t initiator id info spriv spub pid pinfo dvp' st = gdestruct_dstate_t dst in
  let dv = B.deref h dvp.dvp in
  let Mkdevice_t_raw dv_info dv_sk dv_spriv dv_spub prologue dv_scounter peers pcounter cstate = dv in
  dvp == dvp' /\
  begin
  if dstate_t_is_handshake dst && dstate_t_has_static dst then
    lbuffer_or_unit_to_opt_lseq h spriv == lbuffer_or_unit_to_opt_lseq h dv_spriv /\
    lbuffer_or_unit_to_opt_lseq h spub == lbuffer_or_unit_to_opt_lseq h dv_spub
  else True
  end

/// Internally, any dstate_t will always satisfy this invariant when given to or
/// returned by a function. The invariant revealed to the user is (very) slightly more
/// precise.
[@@ noextract_to "krml"] noextract
val dstate_t_invariant_core (#idc : valid_idc) (h : mem) (dst : dstate_t idc) : GTot Type0
let dstate_t_invariant_core #idc h dst =
  let Mkgddstate_t initiator id info spriv spub pid pinfo dvp st = gdestruct_dstate_t dst in
  let dv = B.deref h dvp.dvp in
  let Mkdevice_t_raw dv_info dv_sk dv_spriv dv_spub scounter prologue peers pcounter cstate = dv in
  device_p_invariant h dvp /\
  state_t_invariant h st /\
  lbuffer_or_unit_live h spriv /\
  lbuffer_or_unit_live h spub /\
  idc_get_info_invariant h info /\
  idc_get_info_invariant h pinfo /\

  lbuffer_or_unit_freeable spriv /\
  lbuffer_or_unit_freeable spub /\
  idc_get_info_freeable h info /\
  idc_get_info_freeable h pinfo /\

  begin
  let dvp_loc = device_p_region_of dvp in
  let st_loc = state_t_core_footprint st in
  let info_loc = info_footprint info in
  let pinfo_loc = peer_info_footprint pinfo in
  let spriv_loc = lbuffer_or_unit_to_loc spriv in
  let spub_loc = lbuffer_or_unit_to_loc spub in
  B.all_disjoint [dvp_loc; st_loc; info_loc; pinfo_loc; spriv_loc; spub_loc]
  end /\

  begin
  let pattern = idc_get_pattern idc in
  let n = List.Tot.length pattern.messages in
  if state_t_is_handshake st then
    let step = UInt32.v (state_t_handshake_get_step st) in
    let st_spriv, st_spub = state_t_handshake_get_static st in
    st_spriv == spriv /\ st_spub == spub
  else
    peer_id_is_some pid = knows_remote pattern initiator n
  end /\

  device_p_owns_dstate_t h dvp dst

[@@ noextract_to "krml"] noextract
val dstate_t_invariant (#idc : valid_idc) (h : mem) (dst : dstate_t idc) : GTot Type0
let dstate_t_invariant #idc h dst =
  dstate_t_invariant_core h dst /\

  begin
  let Mkgddstate_t initiator id info spriv spub pid pinfo dvp st = gdestruct_dstate_t dst in
  let pattern = idc_get_pattern idc in
  let n = List.Tot.length pattern.messages in
  if state_t_is_handshake st then
    let step = UInt32.v (state_t_handshake_get_step st) in
    (step <= n ==> (
      peer_id_is_some pid = knows_remote pattern initiator step))
  else
    peer_id_is_some pid = knows_remote pattern initiator n
  end

/// When we need to manipulate a state's step index, but there is no invariant to
/// assert it is bounded by the number of messages, we use min(step, number of messages).
/// This allows us to call functions which take a precondition on the step, without
/// carrying cumbersome preconditions everywhere (and in the end all this is hidden
/// from the user).
[@@ noextract_to "krml"] noextract
let get_bounded_step (#isc : isconfig) (#initiator : bool)
                     (st:State.state_t isc initiator{state_t_is_handshake st}) : nat =
  let pattern =  isc_get_pattern isc in
  let i = state_t_handshake_get_step st in
  let i = UInt32.v i in
  let n = List.Tot.length pattern.messages in
  if i > n then n else i  

[@@ noextract_to "krml"] noextract
val dstate_t_v_aux (#idc : valid_idc) (h : mem)
                   (initiator : bool)
                   (st:State.state_t (idc_get_isc idc initiator) initiator)
                   (id:dstate_id_t idc)
                   (info:info_t idc)
                   (pid:(idc_get_pid idc).id_t)
                   (pinfo:peer_info_t idc) :
  GTot (dstate_s idc)

let dstate_t_v_aux #idc h initiator st id info pid pinfo =
  let pattern = idc_get_pattern idc in
  let isc = idc_get_isc idc initiator in
  let id_v = dstate_id_v id in
  let info_v = idc_get_info_v h info in
  let pid_v = peer_id_opt_v pid in
  let pinfo_v = if Some? pid_v then Some (idc_get_info_v #idc h pinfo) else None in
  if state_t_is_handshake st then
    begin
    let i = get_bounded_step #isc #initiator st in
    let smi = isc_step_to_smi #initiator isc i in
    let st_v = handshake_state_t_v_with_smi h st smi in
    {
      dst_state = st_v;
      dst_id = id_v;
      dst_info = info_v;
      dst_pid = pid_v;
      dst_pinfo = pinfo_v;
    }
    end
  else
    let st_v = transport_state_t_v h st in
    {
      dst_state = st_v;
      dst_id = id_v;
      dst_info = info_v;
      dst_pid = pid_v;
      dst_pinfo = pinfo_v;
    }

[@@ noextract_to "krml"] noextract
val dstate_t_v (#idc : valid_idc) (h : mem) (st : dstate_t idc) : GTot (dstate_s idc)
let dstate_t_v #idc h st =
  let Mkgddstate_t initiator id info spriv spub pid pinfo dv st = gdestruct_dstate_t st in
  dstate_t_v_aux #idc h initiator st id info pid pinfo

// Sanity check
[@@ noextract_to "krml"] noextract
val dstate_t_is_handshake_lem (#idc : valid_idc) (st : dstate_t idc) (h : mem) :
  Lemma
  (requires (dstate_t_invariant h st))
  (ensures (
    let st_v = dstate_t_v h st in
    dstate_t_is_handshake st = dstate_is_handshake st_v))

let dstate_t_is_handshake_lem #idc st h = ()

[@@ noextract_to "krml"] noextract
val dstate_t_frame_invariant :
     #idc:valid_idc
  -> l:B.loc
  -> st:dstate_t idc
  -> h0:HS.mem
  -> h1:HS.mem ->
  Lemma
  (requires (
    dstate_t_invariant h0 st /\
    B.loc_disjoint l (dstate_t_footprint_with_device st) /\
    B.modifies l h0 h1))
  (ensures (
    dstate_t_invariant h1 st /\
    dstate_t_v h0 st == dstate_t_v h1 st))
  [SMTPat (dstate_t_invariant h1 st);
   SMTPat (B.modifies l h0 h1)]

let dstate_t_frame_invariant #idc l dst h0 h1 =
  let Mkgddstate_t initiator id info spriv spub pid pinfo dvp st = gdestruct_dstate_t dst in
  let pattern = idc_get_pattern idc in
  let isc = idc_get_isc idc initiator in
  info_frame_invariant l info h0 h1;
  info_frame_invariant l pinfo h0 h1;
  info_frame_freeable l info h0 h1;
  info_frame_freeable l pinfo h0 h1;
  device_p_frame_invariant l dvp h0 h1;
  if state_t_is_handshake st then
    begin
    let i = get_bounded_step #isc #initiator st in
    let smi = isc_step_to_smi isc i in
    handshake_state_t_frame_invariant #isc l #initiator st smi h0 h1
    end
  else
    begin
    state_t_footprint_inclusion_lem #isc #initiator st;
    transport_state_t_frame_invariant #isc l #initiator st h0 h1
    end

/// The finer frame invariant
[@@ noextract_to "krml"] noextract
val dstate_t_frame_invariant_update_device
  (#idc : valid_idc) (l : B.loc) (st : dstate_t idc) (dvp : device_p idc) (h0 h1 : mem) :
  Lemma
  (requires (
    B.loc_disjoint (dstate_t_footprint st) l /\
    B.modifies l h0 h1 /\
    device_p_only_changed_peers_or_counters dvp h0 h1 /\
    device_p_invariant h1 dvp /\
    dstate_t_invariant h0 st /\
    device_p_owns_dstate_t h0 dvp st))
  (ensures (
    dstate_t_invariant h1 st /\
    dstate_t_v h1 st == dstate_t_v h0 st /\
    device_p_owns_dstate_t h1 dvp st))
    [SMTPat (dstate_t_invariant h1 st);
     SMTPat (device_p_owns_dstate_t h0 dvp st);
     SMTPat (B.modifies l h0 h1)]

let dstate_t_frame_invariant_update_device #idc l dst dvp0 h0 h1 =
  let Mkgddstate_t initiator id info spriv spub pid pinfo dvp st = gdestruct_dstate_t dst in
  let pattern = idc_get_pattern idc in
  let isc = idc_get_isc idc initiator in
  info_frame_invariant l info h0 h1;
  info_frame_invariant l pinfo h0 h1;
  info_frame_freeable l info h0 h1;
  info_frame_freeable l pinfo h0 h1;
  if state_t_is_handshake st then
    begin
    let i = get_bounded_step #isc #initiator st in
    let smi = isc_step_to_smi isc i in
    handshake_state_t_frame_invariant #isc l #initiator st smi h0 h1
    end
  else
    begin
    state_t_footprint_inclusion_lem #isc #initiator st;
    transport_state_t_frame_invariant #isc l #initiator st h0 h1
    end

[@@ noextract_to "krml"] noextract
val dstate_p_core_footprint (#idc : valid_idc) (h : mem) (stp : dstate_p idc) : GTot B.loc
let dstate_p_core_footprint #idc h stp =
  let st = B.deref h stp.stp in
  B.(loc_union (loc_addr_of_buffer stp.stp) (dstate_t_core_footprint st))

[@@ noextract_to "krml"] noextract
val dstate_p_footprint (#idc : valid_idc) (h : mem) (stp : dstate_p idc) : GTot B.loc
let dstate_p_footprint #idc h stp =
  let st = B.deref h stp.stp in
  B.(loc_union (loc_addr_of_buffer stp.stp) (dstate_t_footprint st))

[@@ noextract_to "krml"] noextract
val dstate_p_footprint_with_device (#idc : valid_idc) (h : mem) (stp : dstate_p idc) : GTot B.loc
let dstate_p_footprint_with_device #idc h stp =
  let st = B.deref h stp.stp in
  B.(loc_union (loc_addr_of_buffer stp.stp) (dstate_t_footprint_with_device st))

let dstate_p_rid_of (#idc : valid_idc) (stp : dstate_p idc) :
  GTot HS.rid =
  stp.stp_r

let dstate_p_v #idc h stp =
  let st = B.deref h stp.stp in
  dstate_t_v h st

[@@ noextract_to "krml"] inline_for_extraction noextract
val dstate_t_is_stuck (#idc : valid_idc) (st : dstate_t idc) : bool
let dstate_t_is_stuck #idc st =
  [@inline_let] let n = with_onorm(List.Tot.length (idc_get_pattern idc).messages) in
  [@inline_let] let is_handshake_state = dstate_t_is_handshake st in
  is_handshake_state && UInt32.gte (dstate_t_handshake_get_step st) (size (n + 1))

[@@ noextract_to "krml"] noextract
val dstate_t_is_stuck_lem (#idc : valid_idc) (st : dstate_t idc) (h : mem) :
  Lemma
  (requires (dstate_t_invariant h st))
  (ensures (
    let st_v = dstate_t_v h st in
    dstate_t_is_stuck st = dstate_is_stuck st_v))

let dstate_t_is_stuck_lem #idc st h = ()

let dstate_p_g_handshake_get_static #idc h stp =
  let st = B.deref h stp.stp in
  dstate_t_g_handshake_get_static st

// Sanity check
[@@ noextract_to "krml"] noextract
let dstate_p_g_is_initiator_lem (#idc : valid_idc) (stp : dstate_p idc) (h : mem) :
  Lemma (
    let st = B.deref h stp.stp in
    dstate_p_g_is_initiator h stp = dstate_t_is_initiator st) = ()

// Sanity check
[@@ noextract_to "krml"] noextract
let dstate_p_g_is_handshake_lem (#idc : valid_idc) (stp : dstate_p idc) (h : mem) :
  Lemma (
    let st = B.deref h stp.stp in
    dstate_p_g_is_handshake h stp = dstate_t_is_handshake st) = ()

let dstate_p_invariant #idc h stp =
  let st = B.deref h stp.stp in

  // Parent region: used to make the footprint independent from the memory snapshot
  // If dvp.dvp_r <> FStar.Monotonic.HyperHeap.root, we can use:
  // * [ST.recall_region]
  // * [FStar.Monotonic.HyperStack.eternal_disjoint_from_tip]
  // to show that the region is disjoint from the stack.
  // This won't appear on the user side: at allocation time, we use the trick
  // of allocating a new region inside the region the user provides for heap
  // allocation, and allocate the new state in this new region.
  ST.is_eternal_region stp.stp_r /\
  ST.is_eternal_region stp.stp_r_split /\
  ST.is_eternal_region stp.stp_r_pid /\
  stp.stp_r <> root /\
  stp.stp_r_split <> root /\
  stp.stp_r_pid <> root /\

  // We don't need (and can't have) precise relations between regions
  region_includes_region stp.stp_r stp.stp_r_split /\
  region_includes_region stp.stp_r stp.stp_r_pid /\

  B.live h stp.stp /\
  B.freeable stp.stp /\

  region_includes stp.stp_r (dstate_t_footprint st) /\
  region_includes stp.stp_r (B.loc_addr_of_buffer stp.stp) /\

  begin
  let ptr_loc = B.loc_addr_of_buffer stp.stp in
  let st_loc = dstate_t_footprint_with_device st in
  let r_split =
    if dstate_p_g_is_handshake h stp then region_to_loc stp.stp_r_split else B.loc_none in
  let r_pid = region_to_loc stp.stp_r_pid in
  B.all_disjoint [ptr_loc; st_loc; r_split; r_pid]
  end /\

  B.loc_disjoint (device_p_region_of (dstate_p_g_get_device h stp)) (dstate_p_region_of stp) /\

  dstate_t_invariant h st

let dstate_p_live #idc h stp =
  B.live h stp.stp /\
  begin
  if dstate_p_g_is_null stp then True
  else dstate_p_invariant h stp
  end

let dstate_p_is_null #idc stp =
  is_null #MUT #_ stp.stp

let dstate_p_recall_region #idc stp =
  (**) let h0 = ST.get () in
  recall_region stp.stp_r;
  // We could use a pattern instead, but it would be cumbersome
  if IndefiniteDescription.strong_excluded_middle (is_stack_region (get_tip h0)) then
    eternal_disjoint_from_tip h0 stp.stp_r
  else ()

let dstate_p_is_stuck #idc st =
  let st = B.index st.stp 0ul in
  dstate_t_is_stuck st

// Sanity check
[@@ noextract_to "krml"] noextract
let dstate_t_p_owns_dstate_p_lem
  (#idc : valid_idc) (h : mem) (stp : dstate_p idc) :
  Lemma (
    let st = B.deref h stp.stp in
    dstate_p_g_has_static h stp = dstate_t_has_static st) = ()

let device_p_owns_dstate_p
  (#idc : valid_idc) (h : mem) (dvp : device_p idc) (stp : dstate_p idc) : GTot Type0 =
  dstate_p_g_get_device h stp == dvp /\
  begin
  if dstate_p_g_is_handshake h stp && dstate_p_g_has_static h stp then
    let spriv, spub = dstate_p_g_handshake_get_static h stp in
    let dv_spriv, dv_spub = device_p_g_get_static h dvp in
    lbuffer_or_unit_to_opt_lseq h spriv == lbuffer_or_unit_to_opt_lseq h dv_spriv /\
    lbuffer_or_unit_to_opt_lseq h spub == lbuffer_or_unit_to_opt_lseq h dv_spub
  else
    True
  end

// Sanity check
[@@ noextract_to "krml"] noextract
let device_p_owns_dstate_p_lem
  (#idc : valid_idc) (h : mem) (dvp : device_p idc) (dstp : dstate_p idc) :
  Lemma (
    let dst = B.deref h dstp.stp in
    device_p_owns_dstate_p h dvp dstp <==> device_p_owns_dstate_t h dvp dst) = ()

let dstate_p_invariant_get_device #idc h stp = ()

let dstate_p_invariant_live_lem #idc h stp = ()

let dstate_p_frame_invariant #idc l stp h0 h1 =
  let st = B.deref h0 stp.stp in
  dstate_t_frame_invariant l st h0 h1

let dstate_p_frame_invariant_update_device #idc l stp dvp h0 h1 =
  let st = B.deref h0 stp.stp in
  dstate_t_frame_invariant_update_device l st dvp h0 h1

let dstate_p_or_null_frame_invariant #idc l stp dvp h0 h1 =
  if dstate_p_g_is_null stp then ()
  else
    let st = B.deref h0 stp.stp in
    dstate_t_frame_invariant l st h0 h1

let dstate_p_or_null_frame_invariant_update_device #idc l stp dvp h0 h1 =
  if dstate_p_g_is_null stp then ()
  else
    let st = B.deref h0 stp.stp in
    dstate_t_frame_invariant_update_device l st dvp h0 h1

#push-options "--fuel 1"
let idc_pattern_length_not_zero (idc : valid_idc) :
  Lemma(List.Tot.length (idc_get_pattern idc).messages > 0) = ()
#push-options

[@@ noextract_to "krml"] noextract
let dstate_t_handshake_shared_props_base
  (#idc : valid_idc)
  (h1 h2 : mem)
  (dst1 : dstate_t idc{dstate_t_is_handshake dst1})
  (dst2 : dstate_t idc) :
  GTot Type0 =
  let initiator = dstate_t_is_initiator dst1 in
  let isc = idc_get_isc idc initiator in
  let Mkgddstate_t initiator1 id1 info1 spriv1 spub1 pid1 pinfo1 dv1 st1 = gdestruct_dstate_t dst1 in
  let Mkgddstate_t initiator2 id2 info2 spriv2 spub2 pid2 pinfo2 dv2 st2 = gdestruct_dstate_t dst2 in
  initiator1 = initiator2 /\
  dv1 == dv2 /\
  device_p_get_cstate h1 dv1 == device_p_get_cstate h2 dv2 /\
  id1 == id2 /\
  info1 == info2 /\
  // TODO: Is the peer info footprint equality really necessary?
//  peer_info_footprint pinfo1 == peer_info_footprint pinfo2 /\
  pinfo1 == pinfo2
  // The core footprint and the keys will be taken care of by the additional requirements

[@@ noextract_to "krml"] noextract
let dstate_t_handshake_no_split_shared_props
  (#idc : valid_idc)
  (h1 h2 : mem)
  (dst1 : dstate_t idc{dstate_t_is_handshake dst1})
  (dst2 : dstate_t idc{dstate_t_is_handshake dst2}) :
  GTot Type0 =
  let initiator = dstate_t_is_initiator dst1 in
  let isc = idc_get_isc idc initiator in
  dstate_t_handshake_shared_props_base h1 h2 dst1 dst2 /\
  state_t_handshake_shared_props #isc #initiator (dstate_t_get_state dst1) (dstate_t_get_state dst2)

[@@ noextract_to "krml"] noextract
let dstate_t_handshake_shared_props
  (#idc : valid_idc)
  (r : rid) // some dynamic allocations might have happened because of split
  (h1 h2 : mem)
  (dst1 : dstate_t idc{dstate_t_is_handshake dst1})
  (dst2 : dstate_t idc) :
  GTot Type0 =
  let initiator = dstate_t_is_initiator dst1 in
  let isc = idc_get_isc idc initiator in
  dstate_t_handshake_shared_props_base h1 h2 dst1 dst2 /\
   begin
   if dstate_t_is_handshake dst2 then
     state_t_handshake_shared_props #isc #initiator (dstate_t_get_state dst1) (dstate_t_get_state dst2)
   else
     B.(loc_includes (loc_union (region_to_loc r) (dstate_t_footprint dst1))
                     (dstate_t_footprint dst2))
   end

[@@ noextract_to "krml"] noextract
let dstate_p_handshake_shared_props
  (#idc : valid_idc)
  (h1 h2 : mem)
  (dstp1 : dstate_p idc{dstate_p_g_is_handshake h1 dstp1})
  (dstp2 : dstate_p idc) :
  GTot Type0 =
  let dst1 = B.deref h1 dstp1.stp in
  let dst2 = B.deref h2 dstp2.stp in
  dstp1.stp_r == dstp2.stp_r /\
  dstate_t_handshake_shared_props dstp1.stp_r h1 h2 dst1 dst2

let dstate_p_g_get_device_disjoint_regions #idc stp h0 = ()

(**** Utilities *)
let mk_dstate_p_get_status #idc dst_p =
  let dst = B.index dst_p.stp 0ul in
  match dst with
  | DS_Initiator st _ _ _ _ _ _ _ ->
    begin match st with
    | IMS_Handshake step _ _ _ _ _ _ _ _ _ _ ->
      if FStar.UInt32.(step %^ 2ul) = 0ul then Handshake_write
      else Handshake_read
    | IMS_Transport _ _ _ _ _ _ -> Transport
    end
  | DS_Responder st _ _ _ _ _ _ _ ->
    begin match st with
    | IMS_Handshake step _ _ _ _ _ _ _ _ _ _ ->
      if FStar.UInt32.(step %^ 2ul) = 0ul then Handshake_read
      else Handshake_write
    | IMS_Transport _ _ _ _ _ _ -> Transport
    end

// Given a payload length, return the length of the next message to receive/send.
// If we are in the handshake phase, it depends on the current step.
// In transport phase, it is always payload_len + aead_tag (note that the state
// can't necessarily send/receive a message).
[@@ noextract_to "krml"] inline_for_extraction noextract
val mk_dstate_t_compute_next_message_len
  (#idc:valid_idc) (out : B.pointer size_t)
  (dst : dstate_t idc) (payload_len : size_t) :
  Stack bool
  (requires (fun h0 ->
    B.live h0 out /\
    dstate_t_invariant h0 dst))
  (ensures (fun h0 b h1 ->
    B.(modifies (loc_buffer out) h0 h1) /\
    begin
    let nc = idc_get_config idc in
    let pat = idc_get_pattern idc in
    let dst_v = dstate_t_v h0 dst in
    (**) normalize_term_spec(List.Tot.length pat.messages);
    if b then
      match dstate_get_status dst_v with
      | Spec.Noise.API.State.Handshake_receive step
      | Spec.Noise.API.State.Handshake_send step ->
        step < List.Tot.length pat.messages /\
        size_v (B.deref h1 out) =
          size_v payload_len + compute_message_length nc pat step
      | Spec.Noise.API.State.Transport ->
        size_v (B.deref h1 out) = size_v payload_len + aead_tag_vsv
    else True
    end))

let mk_dstate_t_compute_next_message_len #idc out dst payload_len =
  (**) normalize_term_spec(List.Tot.length (idc_get_pattern idc).messages);
  match dst with
  | DS_Initiator st _ _ _ _ _ _ _ ->
    mk_state_t_compute_next_message_len st payload_len out
  | DS_Responder st _ _ _ _ _ _ _ ->
    mk_state_t_compute_next_message_len st payload_len out
/
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

    out: LowStar.Buffer.pointer Lib.IntTypes.size_t ->
    dst_p: Impl.Noise.API.DState.dstate_p idc ->
    payload_len: Lib.IntTypes.size_t
  -> FStar.HyperStack.ST.Stack Prims.bool
Impl.Noise.API.Device.valid_idc LowStar.Buffer.pointer Lib.IntTypes.size_t Impl.Noise.API.DState.dstate_p Impl.Noise.API.DState.mk_dstate_t_compute_next_message_len Prims.bool Impl.Noise.API.DState.dstate_t LowStar.Monotonic.Buffer.index LowStar.Buffer.trivial_preorder Impl.Noise.API.DState.__proj__Mkdstate_p_or_null_raw__item__stp FStar.UInt32.__uint_to_t
let mk_dstate_p_compute_next_message_len #idc out dst_p payload_len =
  
let dst = B.index dst_p.stp 0ul in
mk_dstate_t_compute_next_message_len #idc out dst payload_len