val unsynth_keyShareEntry (e: keyShareEntry)
    : Tot (namedGroup * (LowParse.Spec.Bytes.parse_bounded_vlbytes_t 1 65535))
let unsynth_keyShareEntry (e:keyShareEntry): Tot (namedGroup * (LowParse.Spec.Bytes.parse_bounded_vlbytes_t 1 65535)) = e.group, e.key_exchange
val unsynth_keyShareEntry (e: keyShareEntry)
    : Tot (namedGroup * (LowParse.Spec.Bytes.parse_bounded_vlbytes_t 1 65535))
let unsynth_keyShareEntry (e: keyShareEntry)
    : Tot (namedGroup * (LowParse.Spec.Bytes.parse_bounded_vlbytes_t 1 65535)) =
e.group, e.key_exchange
Format.KeyShareEntry.fst.checked
prims.fst.checked Parsers.NamedGroup.fsti.checked LowParse.Spec.Bytes.fst.checked LowParse.SLow.fst.checked FStar.UInt32.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Bytes.fsti.checked Format.UncompressedPointRepresentation.fsti.checked
Format.KeyShareEntry.fst
Format.KeyShareEntry.keyShareEntry FStar.Pervasives.Native.Mktuple2 Parsers.NamedGroup.namedGroup LowParse.Spec.Bytes.parse_bounded_vlbytes_t Format.KeyShareEntry.__proj__MkkeyShareEntry__item__group Format.KeyShareEntry.__proj__MkkeyShareEntry__item__key_exchange FStar.Pervasives.Native.tuple2
module Format.KeyShareEntry

open Parsers.NamedGroup
open Format.UncompressedPointRepresentation

module B = FStar.Bytes
module LP = LowParse.SLow
module U32 = FStar.UInt32


(* Parsers, validators *)

inline_for_extraction
let synth_keyShareEntry (r:namedGroup * (LowParse.Spec.Bytes.parse_bounded_vlbytes_t 1 65535)): Tot keyShareEntry = { group=(fst r); key_exchange=(snd r) }
val unsynth_keyShareEntry (e: keyShareEntry)
    : Tot (namedGroup * (LowParse.Spec.Bytes.parse_bounded_vlbytes_t 1 65535))
e: Format.KeyShareEntry.keyShareEntry
  -> Parsers.NamedGroup.namedGroup * LowParse.Spec.Bytes.parse_bounded_vlbytes_t 1 65535