val namedGroupBytes : x: MiTLS.Parsers.NamedGroup.namedGroup
  -> res:
    LowParse.SLow.Base.bytes32
      {LowParse.SLow.Base.serializer32_correct MiTLS.Parsers.NamedGroup.namedGroup_serializer x res}
let namedGroupBytes x = namedGroup_serializer32 x
(**
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
/
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
  -> res:
    LowParse.SLow.Base.bytes32
      {LowParse.SLow.Base.serializer32_correct MiTLS.Parsers.NamedGroup.namedGroup_serializer x res}
MiTLS.Parsers.NamedGroup.namedGroup MiTLS.Parsers.NamedGroup.namedGroup_serializer32 LowParse.SLow.Base.bytes32 LowParse.SLow.Base.serializer32_correct MiTLS.Parsers.NamedGroup.namedGroup_parser_kind MiTLS.Parsers.NamedGroup.namedGroup_parser MiTLS.Parsers.NamedGroup.namedGroup_serializer
let namedGroupBytes x =
  
namedGroup_serializer32 x