val apply_policy (idc: idconfig)
    : stateful_validation_state (idc_get_nc idc) (stateful_validation_info idc)
val apply_policy (idc: idconfig)
    : stateful_validation_state (idc_get_nc idc) (stateful_validation_info idc)
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)
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"
/
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.idconfig
  -> Impl.Noise.API.State.Base.stateful_validation_state (Impl.Noise.API.Device.idc_get_nc idc)
      (Impl.Noise.API.Device.stateful_validation_info idc)
Impl.Noise.API.Device.idconfig Impl.Noise.API.State.Base.Stateful_vstate Impl.Noise.API.Device.idc_get_nc Impl.Noise.API.Device.stateful_validation_info Impl.Noise.API.Device.apply_policy_stateful Impl.Noise.API.Device.idc_is_psk Spec.Noise.API.DState.Definitions.apply_policy Impl.Noise.API.Device.idc_get_dc Impl.Noise.Stateful.__proj__Stateful__item__s Prims.unit Impl.Noise.Types.public_key_t Impl.Noise.TypeOrUnit.preshared_key_t_or_unit Impl.Noise.API.Device.info_t Impl.Noise.API.Device.serialize_key_t Impl.Noise.TypeOrUnit.private_key_t_or_unit Impl.Noise.API.Device.device_has_s Impl.Noise.API.Device.idc_get_pattern Impl.Noise.TypeOrUnit.public_key_t_or_unit Impl.Noise.API.Device.hsized_buffer Impl.Noise.API.Device.state_id_t Impl.Noise.LinkedList.t Impl.Noise.API.Device.idc_stateful_peer_p Impl.Noise.API.Device.peer_id_t Impl.Noise.API.Device.idc_get_cstate_s Prims._assert Prims.b2t Prims.op_Negation Impl.Noise.Stateful.__proj__Stateful__item__t Impl.Noise.API.Device.raw_stateful_validation_info Impl.Noise.Stateful.__proj__Stateful_malloc_from_input_clone_copy__item__smficc_stateful FStar.Pervasives.Native.option Spec.Noise.CryptoPrimitives.preshared_key Prims.l_and Prims.eq2 Impl.Noise.Stateful.__proj__Stateful__item__v Impl.Noise.TypeOrUnit.lbuffer_or_unit_to_opt_lseq Lib.IntTypes.uint8 Impl.Noise.Types.preshared_key_vs FStar.Pervasives.Native.tuple2 Prims.l_False Spec.Noise.Map.lookup_pred_eq_lem Spec.Noise.API.Device.Definitions.peer Spec.Noise.API.Device.Definitions.raw_peer_has_s Impl.Noise.Types.get_config Spec.Noise.API.Device.Definitions.peer_has_s Prims.l_Forall Spec.Noise.API.Device.Definitions.raw_peer Prims.bool Prims.list Spec.Noise.API.Device.Definitions.peer_id Spec.Noise.API.Device.Definitions.__proj__Mkdconfig__item__dc_info Spec.Noise.API.DState.Lemmas.apply_policy_on_peers_spec Impl.Noise.API.State.Base.__proj__Stateful_vstate__item__validate_spec Impl.Noise.API.Device.raw_apply_policy Lib.Sequence.lseq Lib.IntTypes.int_t Lib.IntTypes.U8 Lib.IntTypes.SEC Lib.IntTypes.v Lib.IntTypes.U32 Lib.IntTypes.PUB Impl.Noise.Types.public_key_vs Lib.Buffer.as_seq Lib.Buffer.MUT Spec.Noise.Map.t Spec.Noise.API.Device.Definitions.__proj__Mkdevice__item__dv_peers Impl.Noise.LinkedList.dt_t Impl.Noise.LinkedList.v Impl.Noise.API.Device.device_s Impl.Noise.API.Device.device_t_v FStar.Monotonic.HyperStack.mem FStar.HyperStack.ST.get Impl.Noise.API.State.Base.__proj__Stateful_vstate__item__validate Impl.Noise.API.State.Base.stateful_peer_info Impl.Noise.API.Device.stateful_policy_function Impl.Noise.API.Device.idc_get_policy Meta.Noise.with_onorm Impl.Noise.API.Device.peers_have_s Impl.Noise.Stateful.stateful_malloc_from_input_clone_copy Impl.Noise.API.Device.idc_get_info Impl.Noise.API.Device.id_cl Impl.Noise.API.Device.idc_get_pid Impl.Noise.Types.iconfig Impl.Noise.API.State.Base.stateful_validation_state
let apply_policy (idc: idconfig)
    : stateful_validation_state (idc_get_nc idc) (stateful_validation_info idc) =
  
Stateful_vstate (apply_policy_stateful idc)
  (idc_is_psk idc)
  (apply_policy (idc_get_dc idc))
  (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
      (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 (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));
      b)