val cipherSuite_jumper:LL.jumper cipherSuite_parser
let cipherSuite_jumper: LL.jumper cipherSuite_parser = LL.jump_constant_size cipherSuite_parser 2ul ()
val cipherSuite_jumper:LL.jumper cipherSuite_parser
let cipherSuite_jumper:LL.jumper cipherSuite_parser =
LL.jump_constant_size cipherSuite_parser 2ul ()
Parsers.CipherSuite.fsti.checked
prims.fst.checked LowStar.Buffer.fst.checked LowParse.Spec.Base.fsti.checked LowParse.Spec.AllIntegers.fst.checked LowParse.SLow.Base.fst.checked LowParse.Low.Base.fst.checked FStar.UInt8.fsti.checked FStar.UInt64.fsti.checked FStar.UInt32.fsti.checked FStar.UInt16.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Bytes.fsti.checked
Parsers.CipherSuite.fsti
LowParse.Low.Base.jump_constant_size Parsers.CipherSuite.cipherSuite_parser_kind Parsers.CipherSuite.cipherSuite Parsers.CipherSuite.cipherSuite_parser FStar.UInt32.__uint_to_t
module Parsers.CipherSuite

(* This file has been automatically generated by EverParse. *)
open FStar.Bytes
module U8 = FStar.UInt8
module U16 = FStar.UInt16
module U32 = FStar.UInt32
module U64 = FStar.UInt64
module LP = LowParse.Spec.Base
module LS = LowParse.SLow.Base
module LSZ = LowParse.SLow.Base
module LPI = LowParse.Spec.AllIntegers
module LL = LowParse.Low.Base
module L = FStar.List.Tot
module B = LowStar.Buffer
module BY = FStar.Bytes
module HS = FStar.HyperStack
module HST = FStar.HyperStack.ST


let cipherSuite_repr = U16.t
inline_for_extraction let cipherSuite_repr_eq (x1 x2: cipherSuite_repr) : Tot bool = (x1 = x2)
let known_cipherSuite_repr (v:U16.t) : bool = v `cipherSuite_repr_eq` 0us || (v `cipherSuite_repr_eq` 1us || (v `cipherSuite_repr_eq` 2us || (v `cipherSuite_repr_eq` 4us || (v `cipherSuite_repr_eq` 5us || (v `cipherSuite_repr_eq` 10us || (v `cipherSuite_repr_eq` 19us || (v `cipherSuite_repr_eq` 22us || (v `cipherSuite_repr_eq` 24us || (v `cipherSuite_repr_eq` 27us || (v `cipherSuite_repr_eq` 47us || (v `cipherSuite_repr_eq` 50us || (v `cipherSuite_repr_eq` 51us || (v `cipherSuite_repr_eq` 52us || (v `cipherSuite_repr_eq` 53us || (v `cipherSuite_repr_eq` 56us || (v `cipherSuite_repr_eq` 57us || (v `cipherSuite_repr_eq` 58us || (v `cipherSuite_repr_eq` 59us || (v `cipherSuite_repr_eq` 60us || (v `cipherSuite_repr_eq` 61us || (v `cipherSuite_repr_eq` 64us || (v `cipherSuite_repr_eq` 103us || (v `cipherSuite_repr_eq` 106us || (v `cipherSuite_repr_eq` 107us || (v `cipherSuite_repr_eq` 108us || (v `cipherSuite_repr_eq` 109us || (v `cipherSuite_repr_eq` 156us || (v `cipherSuite_repr_eq` 157us || (v `cipherSuite_repr_eq` 158us || (v `cipherSuite_repr_eq` 159us || (v `cipherSuite_repr_eq` 160us || (v `cipherSuite_repr_eq` 161us || (v `cipherSuite_repr_eq` 162us || (v `cipherSuite_repr_eq` 163us || (v `cipherSuite_repr_eq` 164us || (v `cipherSuite_repr_eq` 165us || (v `cipherSuite_repr_eq` 166us || (v `cipherSuite_repr_eq` 167us || (v `cipherSuite_repr_eq` 4865us || (v `cipherSuite_repr_eq` 4866us || (v `cipherSuite_repr_eq` 4867us || (v `cipherSuite_repr_eq` 4868us || (v `cipherSuite_repr_eq` 4869us || (v `cipherSuite_repr_eq` 49169us || (v `cipherSuite_repr_eq` 49170us || (v `cipherSuite_repr_eq` 49171us || (v `cipherSuite_repr_eq` 49172us || (v `cipherSuite_repr_eq` 49191us || (v `cipherSuite_repr_eq` 49192us || (v `cipherSuite_repr_eq` 49195us || (v `cipherSuite_repr_eq` 49196us || (v `cipherSuite_repr_eq` 49199us || (v `cipherSuite_repr_eq` 49200us || (v `cipherSuite_repr_eq` 52392us || (v `cipherSuite_repr_eq` 52393us || (v `cipherSuite_repr_eq` 52394us || (v `cipherSuite_repr_eq` 52395us || (v `cipherSuite_repr_eq` 52396us || (v `cipherSuite_repr_eq` 52397us || (false))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

type cipherSuite =
  | TLS_NULL_WITH_NULL_NULL
  | TLS_RSA_WITH_NULL_MD5
  | TLS_RSA_WITH_NULL_SHA
  | TLS_RSA_WITH_RC4_128_MD5
  | TLS_RSA_WITH_RC4_128_SHA
  | TLS_RSA_WITH_3DES_EDE_CBC_SHA
  | TLS_DHE_DSS_WITH_3DES_EDE_CBC_SHA
  | TLS_DHE_RSA_WITH_3DES_EDE_CBC_SHA
  | TLS_DH_anon_WITH_RC4_128_MD5
  | TLS_DH_anon_WITH_3DES_EDE_CBC_SHA
  | TLS_RSA_WITH_AES_128_CBC_SHA
  | TLS_DHE_DSS_WITH_AES_128_CBC_SHA
  | TLS_DHE_RSA_WITH_AES_128_CBC_SHA
  | TLS_DH_anon_WITH_AES_128_CBC_SHA
  | TLS_RSA_WITH_AES_256_CBC_SHA
  | TLS_DHE_DSS_WITH_AES_256_CBC_SHA
  | TLS_DHE_RSA_WITH_AES_256_CBC_SHA
  | TLS_DH_anon_WITH_AES_256_CBC_SHA
  | TLS_RSA_WITH_NULL_SHA256
  | TLS_RSA_WITH_AES_128_CBC_SHA256
  | TLS_RSA_WITH_AES_256_CBC_SHA256
  | TLS_DHE_DSS_WITH_AES_128_CBC_SHA256
  | TLS_DHE_RSA_WITH_AES_128_CBC_SHA256
  | TLS_DHE_DSS_WITH_AES_256_CBC_SHA256
  | TLS_DHE_RSA_WITH_AES_256_CBC_SHA256
  | TLS_DH_anon_WITH_AES_128_CBC_SHA256
  | TLS_DH_anon_WITH_AES_256_CBC_SHA256
  | TLS_RSA_WITH_AES_128_GCM_SHA256
  | TLS_RSA_WITH_AES_256_GCM_SHA384
  | TLS_DHE_RSA_WITH_AES_128_GCM_SHA256
  | TLS_DHE_RSA_WITH_AES_256_GCM_SHA384
  | TLS_DH_RSA_WITH_AES_128_GCM_SHA256
  | TLS_DH_RSA_WITH_AES_256_GCM_SHA384
  | TLS_DHE_DSS_WITH_AES_128_GCM_SHA256
  | TLS_DHE_DSS_WITH_AES_256_GCM_SHA384
  | TLS_DH_DSS_WITH_AES_128_GCM_SHA256
  | TLS_DH_DSS_WITH_AES_256_GCM_SHA384
  | TLS_DH_anon_WITH_AES_128_GCM_SHA256
  | TLS_DH_anon_WITH_AES_256_GCM_SHA384
  | TLS_AES_128_GCM_SHA256
  | TLS_AES_256_GCM_SHA384
  | TLS_CHACHA20_POLY1305_SHA256
  | TLS_AES_128_CCM_SHA256
  | TLS_AES_128_CCM_8_SHA256
  | TLS_ECDHE_RSA_WITH_RC4_128_SHA
  | TLS_ECDHE_RSA_WITH_3DES_EDE_CBC_SHA
  | TLS_ECDHE_RSA_WITH_AES_128_CBC_SHA
  | TLS_ECDHE_RSA_WITH_AES_256_CBC_SHA
  | TLS_ECDHE_RSA_WITH_AES_128_CBC_SHA256
  | TLS_ECDHE_RSA_WITH_AES_256_CBC_SHA384
  | TLS_ECDHE_ECDSA_WITH_AES_128_GCM_SHA256
  | TLS_ECDHE_ECDSA_WITH_AES_256_GCM_SHA384
  | TLS_ECDHE_RSA_WITH_AES_128_GCM_SHA256
  | TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384
  | TLS_ECDHE_RSA_WITH_CHACHA20_POLY1305_SHA256
  | TLS_ECDHE_ECDSA_WITH_CHACHA20_POLY1305_SHA256
  | TLS_DHE_RSA_WITH_CHACHA20_POLY1305_SHA256
  | TLS_PSK_WITH_CHACHA20_POLY1305_SHA256
  | TLS_ECDHE_PSK_WITH_CHACHA20_POLY1305_SHA256
  | TLS_DHE_PSK_WITH_CHACHA20_POLY1305_SHA256
  | Unknown_cipherSuite of (v:U16.t{not (known_cipherSuite_repr v)})

let string_of_cipherSuite = function
  | TLS_NULL_WITH_NULL_NULL -> "TLS_NULL_WITH_NULL_NULL"
  | TLS_RSA_WITH_NULL_MD5 -> "TLS_RSA_WITH_NULL_MD5"
  | TLS_RSA_WITH_NULL_SHA -> "TLS_RSA_WITH_NULL_SHA"
  | TLS_RSA_WITH_RC4_128_MD5 -> "TLS_RSA_WITH_RC4_128_MD5"
  | TLS_RSA_WITH_RC4_128_SHA -> "TLS_RSA_WITH_RC4_128_SHA"
  | TLS_RSA_WITH_3DES_EDE_CBC_SHA -> "TLS_RSA_WITH_3DES_EDE_CBC_SHA"
  | TLS_DHE_DSS_WITH_3DES_EDE_CBC_SHA -> "TLS_DHE_DSS_WITH_3DES_EDE_CBC_SHA"
  | TLS_DHE_RSA_WITH_3DES_EDE_CBC_SHA -> "TLS_DHE_RSA_WITH_3DES_EDE_CBC_SHA"
  | TLS_DH_anon_WITH_RC4_128_MD5 -> "TLS_DH_anon_WITH_RC4_128_MD5"
  | TLS_DH_anon_WITH_3DES_EDE_CBC_SHA -> "TLS_DH_anon_WITH_3DES_EDE_CBC_SHA"
  | TLS_RSA_WITH_AES_128_CBC_SHA -> "TLS_RSA_WITH_AES_128_CBC_SHA"
  | TLS_DHE_DSS_WITH_AES_128_CBC_SHA -> "TLS_DHE_DSS_WITH_AES_128_CBC_SHA"
  | TLS_DHE_RSA_WITH_AES_128_CBC_SHA -> "TLS_DHE_RSA_WITH_AES_128_CBC_SHA"
  | TLS_DH_anon_WITH_AES_128_CBC_SHA -> "TLS_DH_anon_WITH_AES_128_CBC_SHA"
  | TLS_RSA_WITH_AES_256_CBC_SHA -> "TLS_RSA_WITH_AES_256_CBC_SHA"
  | TLS_DHE_DSS_WITH_AES_256_CBC_SHA -> "TLS_DHE_DSS_WITH_AES_256_CBC_SHA"
  | TLS_DHE_RSA_WITH_AES_256_CBC_SHA -> "TLS_DHE_RSA_WITH_AES_256_CBC_SHA"
  | TLS_DH_anon_WITH_AES_256_CBC_SHA -> "TLS_DH_anon_WITH_AES_256_CBC_SHA"
  | TLS_RSA_WITH_NULL_SHA256 -> "TLS_RSA_WITH_NULL_SHA256"
  | TLS_RSA_WITH_AES_128_CBC_SHA256 -> "TLS_RSA_WITH_AES_128_CBC_SHA256"
  | TLS_RSA_WITH_AES_256_CBC_SHA256 -> "TLS_RSA_WITH_AES_256_CBC_SHA256"
  | TLS_DHE_DSS_WITH_AES_128_CBC_SHA256 -> "TLS_DHE_DSS_WITH_AES_128_CBC_SHA256"
  | TLS_DHE_RSA_WITH_AES_128_CBC_SHA256 -> "TLS_DHE_RSA_WITH_AES_128_CBC_SHA256"
  | TLS_DHE_DSS_WITH_AES_256_CBC_SHA256 -> "TLS_DHE_DSS_WITH_AES_256_CBC_SHA256"
  | TLS_DHE_RSA_WITH_AES_256_CBC_SHA256 -> "TLS_DHE_RSA_WITH_AES_256_CBC_SHA256"
  | TLS_DH_anon_WITH_AES_128_CBC_SHA256 -> "TLS_DH_anon_WITH_AES_128_CBC_SHA256"
  | TLS_DH_anon_WITH_AES_256_CBC_SHA256 -> "TLS_DH_anon_WITH_AES_256_CBC_SHA256"
  | TLS_RSA_WITH_AES_128_GCM_SHA256 -> "TLS_RSA_WITH_AES_128_GCM_SHA256"
  | TLS_RSA_WITH_AES_256_GCM_SHA384 -> "TLS_RSA_WITH_AES_256_GCM_SHA384"
  | TLS_DHE_RSA_WITH_AES_128_GCM_SHA256 -> "TLS_DHE_RSA_WITH_AES_128_GCM_SHA256"
  | TLS_DHE_RSA_WITH_AES_256_GCM_SHA384 -> "TLS_DHE_RSA_WITH_AES_256_GCM_SHA384"
  | TLS_DH_RSA_WITH_AES_128_GCM_SHA256 -> "TLS_DH_RSA_WITH_AES_128_GCM_SHA256"
  | TLS_DH_RSA_WITH_AES_256_GCM_SHA384 -> "TLS_DH_RSA_WITH_AES_256_GCM_SHA384"
  | TLS_DHE_DSS_WITH_AES_128_GCM_SHA256 -> "TLS_DHE_DSS_WITH_AES_128_GCM_SHA256"
  | TLS_DHE_DSS_WITH_AES_256_GCM_SHA384 -> "TLS_DHE_DSS_WITH_AES_256_GCM_SHA384"
  | TLS_DH_DSS_WITH_AES_128_GCM_SHA256 -> "TLS_DH_DSS_WITH_AES_128_GCM_SHA256"
  | TLS_DH_DSS_WITH_AES_256_GCM_SHA384 -> "TLS_DH_DSS_WITH_AES_256_GCM_SHA384"
  | TLS_DH_anon_WITH_AES_128_GCM_SHA256 -> "TLS_DH_anon_WITH_AES_128_GCM_SHA256"
  | TLS_DH_anon_WITH_AES_256_GCM_SHA384 -> "TLS_DH_anon_WITH_AES_256_GCM_SHA384"
  | TLS_AES_128_GCM_SHA256 -> "TLS_AES_128_GCM_SHA256"
  | TLS_AES_256_GCM_SHA384 -> "TLS_AES_256_GCM_SHA384"
  | TLS_CHACHA20_POLY1305_SHA256 -> "TLS_CHACHA20_POLY1305_SHA256"
  | TLS_AES_128_CCM_SHA256 -> "TLS_AES_128_CCM_SHA256"
  | TLS_AES_128_CCM_8_SHA256 -> "TLS_AES_128_CCM_8_SHA256"
  | TLS_ECDHE_RSA_WITH_RC4_128_SHA -> "TLS_ECDHE_RSA_WITH_RC4_128_SHA"
  | TLS_ECDHE_RSA_WITH_3DES_EDE_CBC_SHA -> "TLS_ECDHE_RSA_WITH_3DES_EDE_CBC_SHA"
  | TLS_ECDHE_RSA_WITH_AES_128_CBC_SHA -> "TLS_ECDHE_RSA_WITH_AES_128_CBC_SHA"
  | TLS_ECDHE_RSA_WITH_AES_256_CBC_SHA -> "TLS_ECDHE_RSA_WITH_AES_256_CBC_SHA"
  | TLS_ECDHE_RSA_WITH_AES_128_CBC_SHA256 -> "TLS_ECDHE_RSA_WITH_AES_128_CBC_SHA256"
  | TLS_ECDHE_RSA_WITH_AES_256_CBC_SHA384 -> "TLS_ECDHE_RSA_WITH_AES_256_CBC_SHA384"
  | TLS_ECDHE_ECDSA_WITH_AES_128_GCM_SHA256 -> "TLS_ECDHE_ECDSA_WITH_AES_128_GCM_SHA256"
  | TLS_ECDHE_ECDSA_WITH_AES_256_GCM_SHA384 -> "TLS_ECDHE_ECDSA_WITH_AES_256_GCM_SHA384"
  | TLS_ECDHE_RSA_WITH_AES_128_GCM_SHA256 -> "TLS_ECDHE_RSA_WITH_AES_128_GCM_SHA256"
  | TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384 -> "TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384"
  | TLS_ECDHE_RSA_WITH_CHACHA20_POLY1305_SHA256 -> "TLS_ECDHE_RSA_WITH_CHACHA20_POLY1305_SHA256"
  | TLS_ECDHE_ECDSA_WITH_CHACHA20_POLY1305_SHA256 -> "TLS_ECDHE_ECDSA_WITH_CHACHA20_POLY1305_SHA256"
  | TLS_DHE_RSA_WITH_CHACHA20_POLY1305_SHA256 -> "TLS_DHE_RSA_WITH_CHACHA20_POLY1305_SHA256"
  | TLS_PSK_WITH_CHACHA20_POLY1305_SHA256 -> "TLS_PSK_WITH_CHACHA20_POLY1305_SHA256"
  | TLS_ECDHE_PSK_WITH_CHACHA20_POLY1305_SHA256 -> "TLS_ECDHE_PSK_WITH_CHACHA20_POLY1305_SHA256"
  | TLS_DHE_PSK_WITH_CHACHA20_POLY1305_SHA256 -> "TLS_DHE_PSK_WITH_CHACHA20_POLY1305_SHA256"
  | Unknown_cipherSuite _ -> "Unknown_cipherSuite"

inline_for_extraction noextract let cipherSuite_parser_kind = LP.strong_parser_kind 2 2 (Some LP.ParserKindMetadataTotal)

noextract val cipherSuite_parser: LP.parser cipherSuite_parser_kind cipherSuite

noextract val cipherSuite_serializer: LP.serializer cipherSuite_parser

noextract val cipherSuite_bytesize (x:cipherSuite) : GTot nat

noextract val cipherSuite_bytesize_eq (x:cipherSuite) : Lemma (cipherSuite_bytesize x == Seq.length (LP.serialize cipherSuite_serializer x))

val cipherSuite_parser32: LS.parser32 cipherSuite_parser

val cipherSuite_serializer32: LS.serializer32 cipherSuite_serializer

val cipherSuite_size32: LSZ.size32 cipherSuite_serializer

let cipherSuite_validator: LL.validator cipherSuite_parser = LL.validate_total_constant_size cipherSuite_parser 2uL ()
val cipherSuite_jumper:LL.jumper cipherSuite_parser
LowParse.Low.Base.jumper Parsers.CipherSuite.cipherSuite_parser