val idc_get_isc (idc : valid_idc) (initiator : bool) :
  isc:valid_isc initiator{
   isc_get_nc isc == idc_get_nc idc /\
   isc_get_sc isc == dconfig_to_sconfig (idc_get_dc idc) /\
   isc_get_pattern isc == idc_get_pattern idc /\
   isc_get_ks isc == idc_get_ks idc initiator
  }
val idc_get_isc (idc : valid_idc) (initiator : bool) :
  isc:valid_isc initiator{
   isc_get_nc isc == idc_get_nc idc /\
   isc_get_sc isc == dconfig_to_sconfig (idc_get_dc idc) /\
   isc_get_pattern isc == idc_get_pattern idc /\
   isc_get_ks isc == idc_get_ks idc initiator
  }
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
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
/
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
idc: Impl.Noise.API.Device.valid_idc -> initiator: Prims.bool
  -> isc:
    Impl.Noise.API.State.StateMachine.valid_isc initiator
      { Impl.Noise.API.State.Base.isc_get_nc isc == Impl.Noise.API.Device.idc_get_nc idc /\
        Impl.Noise.API.State.Base.isc_get_sc isc ==
        Spec.Noise.API.DState.Definitions.dconfig_to_sconfig (Impl.Noise.API.Device.idc_get_dc idc) /\
        Impl.Noise.API.State.Base.isc_get_pattern isc == Impl.Noise.API.Device.idc_get_pattern idc /\
        Impl.Noise.API.State.Base.isc_get_ks isc == Impl.Noise.API.DState.idc_get_ks idc initiator }
Impl.Noise.API.Device.valid_idc Prims.bool Impl.Noise.Types.iconfig Spec.Noise.API.Device.Definitions.dconfig Prims.b2t Prims.op_Equality Spec.Noise.CryptoPrimitives.config Spec.Noise.API.Device.Definitions.__proj__Mkdconfig__item__dc_nc Impl.Noise.Types.get_config Spec.Noise.SPatterns.wfs_handshake_pattern Impl.Noise.API.Device.id_cl Impl.Noise.Stateful.stateful_malloc_from_input_clone_copy Prims.unit Prims.l_and Prims.eq2 Impl.Noise.Stateful.__proj__Stateful__item__t Impl.Noise.Stateful.__proj__Stateful_malloc_from_input_clone_copy__item__smficc_stateful Spec.Noise.API.Device.Definitions.__proj__Mkdconfig__item__dc_info Lib.ByteSequence.bytes Prims.op_LessThanOrEqual FStar.Seq.Base.length Lib.IntTypes.uint_t Lib.IntTypes.U8 Lib.IntTypes.SEC Prims.pow2 Impl.Noise.Stateful.__proj__Stateful_malloc_from_input_clone_copy__item__smficc_to_bytes_seq Spec.Noise.API.Device.Definitions.__proj__Mkdconfig__item__dc_info_to_bytes Impl.Noise.API.Device.stateful_policy_function Meta.Noise.with_onorm Spec.Noise.Base.Definitions.check_hsk_is_psk Spec.Noise.CryptoPrimitives.public_key Impl.Noise.API.Device.__proj__Stateful_policy_function__item__apply_policy_spec Spec.Noise.API.Device.Definitions.__proj__Mkdconfig__item__dc_policy Impl.Noise.API.Device.stateful_certification_state Impl.Noise.API.Device.__proj__Stateful_cstate__item__cstate Spec.Noise.API.Device.Definitions.__proj__Mkdconfig__item__dc_cert_state Spec.Noise.API.Device.Definitions.certification_function Impl.Noise.API.Device.__proj__Stateful_cstate__item__certify_spec Spec.Noise.API.Device.Definitions.__proj__Mkdconfig__item__dc_certification Prims._assert Impl.Noise.API.State.StateMachine.isc_is_valid Impl.Noise.API.Device.check_pattern Impl.Noise.API.State.Base.isc_get_pattern Impl.Noise.API.State.Base.handshake_pattern_is_valid Prims.op_BarBar Prims.op_Negation Spec.Noise.API.MetaInfo.lookups_psk Impl.Noise.API.State.Base.isc_lookups_psk Impl.Noise.API.State.Base.isconfig Impl.Noise.API.State.Base.Mkisconfig Impl.Noise.API.Device.idc_is_psk Spec.Noise.API.State.Definitions.sconfig Spec.Noise.API.DState.Definitions.dconfig_to_sconfig Impl.Noise.Stateful.stateful Prims.l_Forall Impl.Noise.Stateful.__proj__Stateful_malloc_from_input_clone_copy__item__smficc_input Spec.Noise.API.MetaInfo.key_slots Spec.Noise.API.MetaInfo.key_slots_from_pattern Impl.Noise.API.Device.peers_have_s Impl.Noise.API.State.Base.stateful_peer_info Impl.Noise.API.Device.stateful_validation_info Impl.Noise.API.State.StateMachine.valid_isc Impl.Noise.API.State.Base.isc_get_nc Impl.Noise.API.Device.idc_get_nc Impl.Noise.API.State.Base.isc_get_sc Impl.Noise.API.Device.idc_get_dc Spec.Noise.WellFormedness.wf_handshake_pattern Impl.Noise.API.Device.idc_get_pattern Impl.Noise.API.State.Base.isc_get_ks Impl.Noise.API.DState.idc_get_ks
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