val as_supportedNamedGroups (xs: namedGroups)
    : Pure supportedNamedGroups
      (requires
        (b2t (norm [
                  primops;
                  iota;
                  zeta;
                  delta_only [`%List.Tot.for_all; `%is_supported_group; `%List.Tot.mem]
                ]
                (List.Tot.for_all is_supported_group xs))))
      (ensures (fun x -> True))
val as_supportedNamedGroups (xs: namedGroups)
    : Pure supportedNamedGroups
      (requires
        (b2t (norm [
                  primops;
                  iota;
                  zeta;
                  delta_only [`%List.Tot.for_all; `%is_supported_group; `%List.Tot.mem]
                ]
                (List.Tot.for_all is_supported_group xs))))
      (ensures (fun x -> True))
let as_supportedNamedGroups
  (xs:namedGroups)
  : Pure supportedNamedGroups
    (requires (b2t (norm [primops; iota; zeta; delta_only [`%List.Tot.for_all; `%is_supported_group; `%List.Tot.mem]]
                                     (List.Tot.for_all is_supported_group xs))))
    (ensures (fun x -> True))
  = xs
(**
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

// was "valid", not "supported"; should probably be defined from the crypto provider.
let is_supported_group x = List.Tot.mem x 
  [ Secp256r1; Secp384r1; Secp521r1; X25519; X448; 
    Ffdhe2048; Ffdhe3072; Ffdhe4096; Ffdhe6144; Ffdhe8192 ]
type supportedNamedGroup = x:namedGroup{is_supported_group x}
type supportedNamedGroups = xs:namedGroups{List.Tot.for_all is_supported_group xs}
/
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
xs: MiTLS.CommonDH.namedGroups -> Prims.Pure MiTLS.CommonDH.supportedNamedGroups
MiTLS.CommonDH.namedGroups MiTLS.CommonDH.supportedNamedGroups Prims.b2t FStar.Pervasives.norm Prims.Cons FStar.Pervasives.norm_step FStar.Pervasives.primops FStar.Pervasives.iota FStar.Pervasives.zeta FStar.Pervasives.delta_only Prims.string Prims.Nil Prims.bool FStar.List.Tot.Base.for_all MiTLS.Parsers.NamedGroup.namedGroup MiTLS.CommonDH.is_supported_group Prims.l_True
let as_supportedNamedGroups (xs: namedGroups)
    : Pure supportedNamedGroups
      (requires
        (b2t (norm [
                  primops;
                  iota;
                  zeta;
                  delta_only [`%List.Tot.for_all; `%is_supported_group; `%List.Tot.mem]
                ]
                (List.Tot.for_all is_supported_group xs))))
      (ensures (fun x -> True)) =
  
xs