val handshake_read_no_split_certify_static :
     #dc:dconfig
  -> cst:dc.dc_cert_state
  -> dv:device dc
  -> st:State.state (dconfig_to_sconfig dc){check_swf (State.state_get_pattern st)}
  -> dst_id:state_id
  -> dst_info:dc.dc_info
  -> payload:hashable dc.dc_nc ->
  Pure (ds_result (device dc & bytes & dstate dc))
  (requires (State.state_is_handshake st))
  (ensures (fun r -> True))
val handshake_read_no_split_certify_static :
     #dc:dconfig
  -> cst:dc.dc_cert_state
  -> dv:device dc
  -> st:State.state (dconfig_to_sconfig dc){check_swf (State.state_get_pattern st)}
  -> dst_id:state_id
  -> dst_info:dc.dc_info
  -> payload:hashable dc.dc_nc ->
  Pure (ds_result (device dc & bytes & dstate dc))
  (requires (State.state_is_handshake st))
  (ensures (fun r -> True))
let handshake_read_no_split_certify_static #dc cst dv st dst_id dst_info payload =
  let hs_st = State.IS_Handshake?.st st.State.st_hs_state in
  let rs = hs_st.remote_static in
  match rs with
  | None -> Fail No_key (* can't happen *)
  | Some rs ->
    match dc.dc_certification cst rs payload with
    | None -> Fail Rs_not_certified
    | Some pinfo ->
      (* We received a valid static key for a new peer: add it to the device *)
      match add_peer_get dv pinfo (Some rs) hs_st.preshared with
      | None -> Fail Peer_conflict
      | Some (p, dv') ->
        let dst = {
          dst_state = st;
          dst_id = dst_id;
          dst_info = dst_info;
          dst_pid = Some p.p_id;
          dst_pinfo = Some pinfo
        } in
        Res (dv', payload, dst)
module Spec.Noise.API.DState.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
open Spec.Noise.API.Device.Lemmas
friend Spec.Noise.API.Device.Lemmas
open Spec.Noise.API.DState.Definitions
friend Spec.Noise.API.DState.Definitions
module M = Spec.Noise.Map
open Spec.Noise.SPatterns
open Spec.Noise.CryptoPrimitives
open FStar.List.Tot

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

open Spec.Noise.Base
open Spec.Noise.API.DState.Definitions

/// Some helpers to split handshake_read into smaller functions - it is too
/// big to be implemented in one block without the proofs exploding.

(* We received a message and the current patter *)
val handshake_read_no_split_certify_static :
     #dc:dconfig
  -> cst:dc.dc_cert_state
  -> dv:device dc
  -> st:State.state (dconfig_to_sconfig dc){check_swf (State.state_get_pattern st)}
  -> dst_id:state_id
  -> dst_info:dc.dc_info
  -> payload:hashable dc.dc_nc ->
  Pure (ds_result (device dc & bytes & dstate dc))
  (requires (State.state_is_handshake st))
  (ensures (fun r -> True))
/
Spec.Noise.SPatterns.fst.checked Spec.Noise.Map.fst.checked Spec.Noise.CryptoPrimitives.fsti.checked Spec.Noise.Base.fst.checked Spec.Noise.API.State.Definitions.fsti.checked Spec.Noise.API.DState.Definitions.fst.checked Spec.Noise.API.DState.Definitions.fst.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 prims.fst.checked Lib.ByteSequence.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked
Spec.Noise.API.DState.Lemmas.fst

    cst: Mkdconfig?.dc_cert_state dc ->
    dv: Spec.Noise.API.Device.Definitions.device dc ->
    st:
      Spec.Noise.API.State.Definitions.state (Spec.Noise.API.DState.Definitions.dconfig_to_sconfig dc
          ) {Spec.Noise.SPatterns.check_swf (Spec.Noise.API.State.Definitions.state_get_pattern st)} ->
    dst_id: Spec.Noise.API.Device.Definitions.state_id ->
    dst_info: Mkdconfig?.dc_info dc ->
    payload: Spec.Noise.CryptoPrimitives.hashable (Mkdconfig?.dc_nc dc)
  -> Prims.Pure
    (Spec.Noise.API.DState.Definitions.ds_result ((Spec.Noise.API.Device.Definitions.device dc *
          Lib.ByteSequence.bytes) *
          Spec.Noise.API.DState.Definitions.dstate dc))
Spec.Noise.API.Device.Definitions.dconfig Spec.Noise.API.Device.Definitions.__proj__Mkdconfig__item__dc_cert_state Spec.Noise.API.Device.Definitions.device Spec.Noise.API.State.Definitions.state Spec.Noise.API.DState.Definitions.dconfig_to_sconfig Prims.b2t Spec.Noise.SPatterns.check_swf Spec.Noise.API.State.Definitions.state_get_pattern Spec.Noise.API.Device.Definitions.state_id Spec.Noise.API.Device.Definitions.__proj__Mkdconfig__item__dc_info Spec.Noise.CryptoPrimitives.hashable Spec.Noise.API.Device.Definitions.__proj__Mkdconfig__item__dc_nc Spec.Noise.Base.Definitions.Fail FStar.Pervasives.Native.tuple3 Lib.ByteSequence.bytes Spec.Noise.API.DState.Definitions.dstate Spec.Noise.API.DState.Definitions.ds_error Spec.Noise.API.DState.Definitions.No_key Spec.Noise.CryptoPrimitives.public_key Spec.Noise.API.State.Definitions.sc_get_config Spec.Noise.API.Device.Definitions.__proj__Mkdconfig__item__dc_certification Spec.Noise.API.DState.Definitions.Rs_not_certified Spec.Noise.API.Device.Definitions.add_peer_get FStar.Pervasives.Native.Some Spec.Noise.Base.Definitions.__proj__Mkhandshake_state__item__preshared Spec.Noise.API.DState.Definitions.Peer_conflict Spec.Noise.API.Device.Definitions.peer Spec.Noise.Base.Definitions.Res FStar.Pervasives.Native.Mktuple3 Spec.Noise.API.DState.Definitions.Mkdstate Spec.Noise.API.Device.Definitions.peer_id Spec.Noise.API.Device.Definitions.__proj__Mkraw_peer__item__p_id Spec.Noise.API.DState.Definitions.ds_result FStar.Pervasives.Native.option Spec.Noise.Base.Definitions.__proj__Mkhandshake_state__item__remote_static Spec.Noise.Base.Definitions.handshake_state Spec.Noise.API.State.Definitions.__proj__IS_Handshake__item__st Spec.Noise.API.State.Definitions.__proj__Mkstate__item__st_hs_state
let handshake_read_no_split_certify_static #dc cst dv st dst_id dst_info payload =
  
let hs_st = State.IS_Handshake?.st st.State.st_hs_state in
let rs = hs_st.remote_static in
match rs with
| None -> Fail No_key
| Some rs ->
  match dc.dc_certification cst rs payload with
  | None -> Fail Rs_not_certified
  | Some pinfo ->
    match add_peer_get dv pinfo (Some rs) hs_st.preshared with
    | None -> Fail Peer_conflict
    | Some (p, dv') ->
      let dst =
        {
          dst_state = st;
          dst_id = dst_id;
          dst_info = dst_info;
          dst_pid = Some p.p_id;
          dst_pinfo = Some pinfo
        }
      in
      Res (dv', payload, dst)