val is_supported_group : x: MiTLS.Parsers.NamedGroup.namedGroup -> Prims.bool
let is_supported_group x = List.Tot.mem x 
  [ Secp256r1; Secp384r1; Secp521r1; X25519; X448; 
    Ffdhe2048; Ffdhe3072; Ffdhe4096; Ffdhe6144; Ffdhe8192 ]
(**
An abstract interface for Diffie-Hellman operations

When the key extraction stack is idealized (ideal_KEF), this module
records the honesty of shares using two layers of types

[pre_share] is for syntactically valid shares (used in parsing modules);
[share] is for registered shares (for which is_honest is defined).
*)
module MiTLS.CommonDH
open MiTLS

open FStar.HyperStack
open FStar.Bytes
open FStar.Error
module Parse = MiTLS.Parse
open MiTLS.Parse
open MiTLS.TLSError
open FStar.HyperStack.ST

include MiTLS.Parsers.NamedGroup
module NGL = MiTLS.Parsers.NamedGroupList

let namedGroups = NGL.namedGroupList
let namedGroupList = NGL.namedGroupList

let namedGroupBytes x = namedGroup_serializer32 x
let parseNamedGroup x = namedGroup_parser32 x
let namedGroupsBytes x = NGL.namedGroupList_serializer32 x
let parseNamedGroups x = NGL.namedGroupList_parser32 x
/
prims.fst.checked MiTLS.TLSError.fst.checked MiTLS.Parsers.NamedGroupList.fsti.checked MiTLS.Parsers.NamedGroup.fsti.checked MiTLS.Parse.fst.checked MiTLS.Flags.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Error.fst.checked FStar.Bytes.fsti.checked
MiTLS.CommonDH.fsti
x: MiTLS.Parsers.NamedGroup.namedGroup -> Prims.bool
MiTLS.Parsers.NamedGroup.namedGroup FStar.List.Tot.Base.mem Prims.Cons MiTLS.Parsers.NamedGroup.Secp256r1 MiTLS.Parsers.NamedGroup.Secp384r1 MiTLS.Parsers.NamedGroup.Secp521r1 MiTLS.Parsers.NamedGroup.X25519 MiTLS.Parsers.NamedGroup.X448 MiTLS.Parsers.NamedGroup.Ffdhe2048 MiTLS.Parsers.NamedGroup.Ffdhe3072 MiTLS.Parsers.NamedGroup.Ffdhe4096 MiTLS.Parsers.NamedGroup.Ffdhe6144 MiTLS.Parsers.NamedGroup.Ffdhe8192 Prims.Nil Prims.bool
let is_supported_group x =
  
List.Tot.mem x
  [
    Secp256r1; Secp384r1; Secp521r1; X25519; X448; Ffdhe2048; Ffdhe3072; Ffdhe4096; Ffdhe6144;
    Ffdhe8192
  ]