val handshake_pattern_is_valid (pattern: handshake_pattern) : Tot bool
val handshake_pattern_is_valid (pattern: handshake_pattern) : Tot bool
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
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 *)
/
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
pattern: Spec.Noise.Base.Definitions.handshake_pattern -> Prims.bool
Spec.Noise.Base.Definitions.handshake_pattern Prims.op_AmpAmp Prims.op_BarBar Prims.op_Equality FStar.Pervasives.Native.option Prims.list Spec.Noise.Base.Definitions.premessage_token Spec.Noise.Base.Definitions.__proj__Mkhandshake_pattern__item__premessage_ir FStar.Pervasives.Native.None FStar.Pervasives.Native.Some Prims.Cons Spec.Noise.Base.Definitions.PS Prims.Nil Spec.Noise.Base.Definitions.__proj__Mkhandshake_pattern__item__premessage_ri Prims.uu___is_Cons Spec.Noise.Base.Definitions.message_token Spec.Noise.Base.Definitions.__proj__Mkhandshake_pattern__item__messages Prims.bool
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