val namedGroup_validator:LL.validator namedGroup_parser
let namedGroup_validator: LL.validator namedGroup_parser = LL.validate_total_constant_size namedGroup_parser 2uL ()
val namedGroup_validator:LL.validator namedGroup_parser
let namedGroup_validator:LL.validator namedGroup_parser =
LL.validate_total_constant_size namedGroup_parser 2uL ()
Parsers.NamedGroup.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.NamedGroup.fsti
LowParse.Low.Base.validate_total_constant_size Parsers.NamedGroup.namedGroup_parser_kind Parsers.NamedGroup.namedGroup Parsers.NamedGroup.namedGroup_parser FStar.UInt64.__uint_to_t
module Parsers.NamedGroup

(* 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 namedGroup_repr = U16.t
inline_for_extraction let namedGroup_repr_eq (x1 x2: namedGroup_repr) : Tot bool = (x1 = x2)
let known_namedGroup_repr (v:U16.t) : bool = v `namedGroup_repr_eq` 6us || (v `namedGroup_repr_eq` 7us || (v `namedGroup_repr_eq` 8us || (v `namedGroup_repr_eq` 9us || (v `namedGroup_repr_eq` 10us || (v `namedGroup_repr_eq` 11us || (v `namedGroup_repr_eq` 12us || (v `namedGroup_repr_eq` 13us || (v `namedGroup_repr_eq` 14us || (v `namedGroup_repr_eq` 20us || (v `namedGroup_repr_eq` 21us || (v `namedGroup_repr_eq` 22us || (v `namedGroup_repr_eq` 23us || (v `namedGroup_repr_eq` 24us || (v `namedGroup_repr_eq` 25us || (v `namedGroup_repr_eq` 29us || (v `namedGroup_repr_eq` 30us || (v `namedGroup_repr_eq` 256us || (v `namedGroup_repr_eq` 257us || (v `namedGroup_repr_eq` 258us || (v `namedGroup_repr_eq` 259us || (v `namedGroup_repr_eq` 260us || (false))))))))))))))))))))))

type namedGroup =
  | Sect233k1
  | Sect233r1
  | Sect239k1
  | Sect283k1
  | Sect283r1
  | Sect409k1
  | Sect409r1
  | Sect571k1
  | Sect571r1
  | Secp224k1
  | Secp224r1
  | Secp256k1
  | Secp256r1
  | Secp384r1
  | Secp521r1
  | X25519
  | X448
  | Ffdhe2048
  | Ffdhe3072
  | Ffdhe4096
  | Ffdhe6144
  | Ffdhe8192
  | Unknown_namedGroup of (v:U16.t{not (known_namedGroup_repr v)})

let string_of_namedGroup = function
  | Sect233k1 -> "sect233k1"
  | Sect233r1 -> "sect233r1"
  | Sect239k1 -> "sect239k1"
  | Sect283k1 -> "sect283k1"
  | Sect283r1 -> "sect283r1"
  | Sect409k1 -> "sect409k1"
  | Sect409r1 -> "sect409r1"
  | Sect571k1 -> "sect571k1"
  | Sect571r1 -> "sect571r1"
  | Secp224k1 -> "secp224k1"
  | Secp224r1 -> "secp224r1"
  | Secp256k1 -> "secp256k1"
  | Secp256r1 -> "secp256r1"
  | Secp384r1 -> "secp384r1"
  | Secp521r1 -> "secp521r1"
  | X25519 -> "x25519"
  | X448 -> "x448"
  | Ffdhe2048 -> "ffdhe2048"
  | Ffdhe3072 -> "ffdhe3072"
  | Ffdhe4096 -> "ffdhe4096"
  | Ffdhe6144 -> "ffdhe6144"
  | Ffdhe8192 -> "ffdhe8192"
  | Unknown_namedGroup _ -> "Unknown_namedGroup"

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

noextract val namedGroup_parser: LP.parser namedGroup_parser_kind namedGroup

noextract val namedGroup_serializer: LP.serializer namedGroup_parser

noextract val namedGroup_bytesize (x:namedGroup) : GTot nat

noextract val namedGroup_bytesize_eq (x:namedGroup) : Lemma (namedGroup_bytesize x == Seq.length (LP.serialize namedGroup_serializer x))

val namedGroup_parser32: LS.parser32 namedGroup_parser

val namedGroup_serializer32: LS.serializer32 namedGroup_serializer

val namedGroup_size32: LSZ.size32 namedGroup_serializer
val namedGroup_validator:LL.validator namedGroup_parser
LowParse.Low.Base.validator Parsers.NamedGroup.namedGroup_parser