val isc_get_sc (isc: isconfig)
    : Tot
    (sc:
      sconfig
        {isc_get_config isc == sc_get_config sc /\ (isc_get_pinfo isc).St.t () == sc_get_pinfo sc})
val isc_get_sc (isc: isconfig)
    : Tot
    (sc:
      sconfig
        {isc_get_config isc == sc_get_config sc /\ (isc_get_pinfo isc).St.t () == sc_get_pinfo sc})
let isc_get_sc : isc:isconfig ->
  Tot (sc:sconfig{isc_get_config isc == sc_get_config sc /\
                  (isc_get_pinfo isc).St.t () == sc_get_pinfo sc}) =
  fun isc -> match isc with Mkisconfig nc sc pat ks pi lpsk -> sc
module Impl.Noise.API.State.Base

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 LB = Lib.Buffer
module B = LowStar.Buffer
module HS = FStar.HyperStack
module ST = FStar.HyperStack.ST
module G = FStar.Ghost

open Spec.Noise
open Spec.Noise.API
open Spec.Noise.API.State.Definitions
open Spec.Noise.API.State.Lemmas
module Spec = Spec.Noise.API.State
open Spec.Noise.API.MetaInfo

open Impl.Noise.Types
open Impl.Noise.CipherState
open Impl.Noise.HKDF
open Impl.Noise.SymmetricState
open Impl.Noise.HandshakeState
open Impl.Noise.SendReceive
open Impl.Noise.RecursivePremessages
open Impl.Noise.RecursiveMessages
open Impl.Noise.FlatStructures
open Impl.Noise.CryptoPrimitives
open Impl.Noise.TypeOrUnit
open Impl.Noise.Allocate

module UInt64 = FStar.UInt64

open Meta.Noise

module Streaming = Hacl.Streaming.Interface
module St = Impl.Noise.Stateful

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

/// In the specification, we use different types to encode the error codes for
/// the different levels of the API. In the implementation, to prevent useless
/// conversions and in order not to clutter the code, we use one type [error_code],
/// which is the union of all the possible errors.
/// However, we define some refined types to implement the spec error codes as subsets
/// of this low-level error-code. Below is the refinement for [s_error_code].
[@@ noextract_to "krml"] inline_for_extraction noextract
type s_error_code_or_success =
  e:error_code{
    (**) let _ = allow_inversion error_code in
    match e with
    | CSuccess
    | CIncorrect_transition
    | CPremessage
    | CNo_key
    | CAlready_key
    | CRs_rejected_by_policy -> True
    | CRs_not_certified -> False
    | CAlready_peer -> False
    | CPeer_conflict -> False
    | CUnknown_peer_id -> False
    | CInput_size
    | CDH_error
    | CDecrypt_error
    | CSaturated_nonce -> True
    | CEphemeral_generation -> False
    | CSecurity_level -> False
  }

[@@ noextract_to "krml"] inline_for_extraction noextract
type s_error_code =
  e:s_error_code_or_success{e <> CSuccess}

[@@ noextract_to "krml"] noextract
let s_error_code_v (e : s_error_code) : Spec.s_error =
  match e with
  | CIncorrect_transition -> Incorrect_transition
  | CPremessage -> Premessage
  | CNo_key -> No_key
  | CAlready_key -> Already_key
  | CRs_rejected_by_policy -> Rs_not_valid
  | CInput_size -> Input_size
  | CDH_error -> DH_error
  | CDecrypt_error -> Decryption
  | CSaturated_nonce -> Saturated_nonce

[@@ noextract_to "krml"] inline_for_extraction noextract
let s_result_code a = result a s_error_code

(*** Type definitions *)

[@@ noextract_to "krml"] inline_for_extraction noextract
let handshake_pattern_is_valid (pattern : handshake_pattern) : Tot bool =
  (pattern.premessage_ir = None || pattern.premessage_ir = Some [PS]) &&
  (pattern.premessage_ri = None || pattern.premessage_ri = Some [PS]) &&
  Cons? pattern.messages

[@@ noextract_to "krml"] inline_for_extraction noextract
type stateful_peer_info = St.stateful unit//Streaming.stateful unit

[@@ noextract_to "krml"] inline_for_extraction noextract
noeq type stateful_validation_state (nc : iconfig)
                                    (peer_info : stateful_peer_info) =
| Stateful_vstate:

  vst : St.stateful unit ->

  recv_psk: bool ->

  // Pure operations
  validate_spec : validation_function (get_config nc) (vst.St.t ()) (peer_info.St.t ()) ->

  // Stateful operations
  validate: (
    state:vst.St.s () ->
    rs:public_key_t nc ->
    pinfo:(peer_info.St.s ()) -> // TODO: move to return value?
    psk:preshared_key_t_or_unit recv_psk ->
    ST bool
    (requires (fun h0 ->
      vst.St.invariant h0 state /\
      live h0 rs /\
      peer_info.St.invariant h0 pinfo /\
      lbuffer_or_unit_live h0 psk /\
      
      begin
      let state_loc = vst.St.footprint state in
      let rs_loc = B.loc_buffer (rs <: buffer uint8) in
      let pinfo_loc = peer_info.St.footprint pinfo in
      let psk_loc = if recv_psk then B.loc_buffer (psk <: buffer uint8) else B.loc_none in
      B.all_disjoint [state_loc; rs_loc; pinfo_loc; psk_loc]
      end
      ))
    (ensures (fun h0 res h1 ->
      let psk_loc = if recv_psk then B.loc_buffer (psk <: buffer uint8) else B.loc_none in
      // Note that the validation state CAN'T be modified. Allowing the validation
      // state to be modified makes things a lot more complex, because we can't
      // exactly link the spec to the implementation (because of the static analyses),
      // meaning we later on have trouble linking the updated validation state to the
      // original one in case of failure.
      B.(modifies (loc_union (peer_info.St.footprint pinfo) psk_loc) h0 h1) /\
    
      vst.St.invariant h1 state /\
      peer_info.St.invariant h1 pinfo /\
      lbuffer_or_unit_live h1 psk /\

      peer_info.St.footprint pinfo == peer_info.St.footprint pinfo /\
      (peer_info.St.freeable h0 pinfo ==> peer_info.St.freeable h1 pinfo) /\
      
      begin
      let state_v0 = vst.St.v () h0 state in
      let rs_v = B.as_seq h0 (rs <: buffer uint8) in
      let res_v = validate_spec state_v0 rs_v in
      begin match res_v with
      | None -> not res
      | Some (pinfo_v, psk_v) ->
        res /\
        pinfo_v == peer_info.St.v () h1 pinfo /\
        psk_v == lbuffer_or_unit_to_opt_lseq h1 psk
      end
      end /\
      
      True))) ->

  stateful_validation_state nc peer_info

[@@ noextract_to "krml"] inline_for_extraction noextract
let vst_s (#nc : iconfig) (#peer_info : stateful_peer_info)
          (vst : stateful_validation_state nc peer_info) : Type0 =
  vst.vst.St.s ()

[@@ noextract_to "krml"] inline_for_extraction noextract
let vst_t (#nc : iconfig) (#peer_info : stateful_peer_info)
          (vst : stateful_validation_state nc peer_info) : Type0 =
  vst.vst.St.t ()

[@@ noextract_to "krml"] inline_for_extraction noextract
let vst_footprint (#nc : iconfig) (#peer_info : stateful_peer_info)
                  (#vst : stateful_validation_state nc peer_info)
                  (st : vst_s vst) =
  vst.vst.St.footprint st

[@@ noextract_to "krml"] inline_for_extraction noextract
let vst_freeable (#nc : iconfig) (#peer_info : stateful_peer_info)
                 (#vst : stateful_validation_state nc peer_info)
                 (h : mem)
                 (st : vst_s vst) =
  vst.vst.St.freeable h st

[@@ noextract_to "krml"] inline_for_extraction noextract
let vst_invariant (#nc : iconfig) (#peer_info : stateful_peer_info)
                  (#vst : stateful_validation_state nc peer_info)
                  (h : mem)
                  (st : vst_s vst) =
  vst.vst.St.invariant h st

/// Configurations
[@@ noextract_to "krml"] inline_for_extraction noextract
noeq type isconfig : Type u#1 = {
  isc_nc : iconfig;
  isc_sc : sc:sconfig{sc_get_config sc = get_config isc_nc};
  isc_pattern : wf_handshake_pattern; // TODO: in the spec, stored directly in the state
  isc_ks : key_slots;
  isc_pinfo : pi:stateful_peer_info{pi.St.t () == sc_get_pinfo isc_sc};
  isc_lookups_psk : bool;
}

[@@ noextract_to "krml"] inline_for_extraction noextract
let isc_get_nc : isconfig -> Tot iconfig =
  fun isc -> match isc with Mkisconfig nc sc pat ks pi lpsk -> nc
[@@ noextract_to "krml"] inline_for_extraction noextract
let isc_get_config (isc : isconfig) = get_config (isc_get_nc isc)
[@@ noextract_to "krml"] inline_for_extraction noextract
let isc_get_pinfo : isconfig -> Tot stateful_peer_info =
  fun isc -> match isc with Mkisconfig nc sc pat ks pi lpsk -> pi
/
Spec.Noise.API.State.Lemmas.fsti.checked Spec.Noise.API.State.Definitions.fsti.checked Spec.Noise.API.State.fsti.checked Spec.Noise.API.MetaInfo.fst.checked Spec.Noise.fst.checked prims.fst.checked Meta.Noise.fsti.checked LowStar.BufferOps.fst.checked LowStar.Buffer.fst.checked Lib.Sequence.fsti.checked Lib.RawIntTypes.fsti.checked Lib.IntTypes.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.RecursivePremessages.fst.checked Impl.Noise.RecursiveMessages.fst.checked Impl.Noise.HKDF.fsti.checked Impl.Noise.HandshakeState.fsti.checked Impl.Noise.FlatStructures.fst.checked Impl.Noise.CryptoPrimitives.fsti.checked Impl.Noise.CipherState.fsti.checked Impl.Noise.Allocate.fst.checked Hacl.Streaming.Interface.fsti.checked FStar.UInt64.fsti.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.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Ghost.fsti.checked
Impl.Noise.API.State.Base.fsti
isc: Impl.Noise.API.State.Base.isconfig
  -> sc:
    Spec.Noise.API.State.Definitions.sconfig
      { Impl.Noise.API.State.Base.isc_get_config isc ==
        Spec.Noise.API.State.Definitions.sc_get_config sc /\
        Stateful?.t (Impl.Noise.API.State.Base.isc_get_pinfo isc) () ==
        Spec.Noise.API.State.Definitions.sc_get_pinfo sc }
Impl.Noise.API.State.Base.isconfig Impl.Noise.Types.iconfig Spec.Noise.API.State.Definitions.sconfig Prims.b2t Prims.op_Equality Spec.Noise.CryptoPrimitives.config Spec.Noise.API.State.Definitions.sc_get_config Impl.Noise.Types.get_config Spec.Noise.WellFormedness.wf_handshake_pattern Spec.Noise.API.MetaInfo.key_slots Impl.Noise.API.State.Base.stateful_peer_info Prims.eq2 Impl.Noise.Stateful.__proj__Stateful__item__t Prims.unit Spec.Noise.API.State.Definitions.sc_get_pinfo Prims.bool Prims.l_and Impl.Noise.API.State.Base.isc_get_config Impl.Noise.API.State.Base.isc_get_pinfo
let isc_get_sc: isc: isconfig
  -> Tot
    (sc:
      sconfig
        {isc_get_config isc == sc_get_config sc /\ (isc_get_pinfo isc).St.t () == sc_get_pinfo sc}) =
  
function | Mkisconfig nc sc pat ks pi lpsk -> sc