val vst_invariant : h: FStar.Monotonic.HyperStack.mem -> st: Impl.Noise.API.State.Base.vst_s vst -> Type0
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
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
/
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
h: FStar.Monotonic.HyperStack.mem -> st: Impl.Noise.API.State.Base.vst_s vst -> Type0
Impl.Noise.Types.iconfig Impl.Noise.API.State.Base.stateful_peer_info Impl.Noise.API.State.Base.stateful_validation_state FStar.Monotonic.HyperStack.mem Impl.Noise.API.State.Base.vst_s Impl.Noise.Stateful.__proj__Stateful__item__invariant Prims.unit Impl.Noise.API.State.Base.__proj__Stateful_vstate__item__vst
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