val synth_keyShareEntry (r: (namedGroup * (LowParse.Spec.Bytes.parse_bounded_vlbytes_t 1 65535)))
    : Tot keyShareEntry
let synth_keyShareEntry (r:namedGroup * (LowParse.Spec.Bytes.parse_bounded_vlbytes_t 1 65535)): Tot keyShareEntry = { group=(fst r); key_exchange=(snd r) }
val synth_keyShareEntry (r: (namedGroup * (LowParse.Spec.Bytes.parse_bounded_vlbytes_t 1 65535)))
    : Tot keyShareEntry
let synth_keyShareEntry (r: namedGroup * (LowParse.Spec.Bytes.parse_bounded_vlbytes_t 1 65535))
    : Tot keyShareEntry =
{ group = (fst r); key_exchange = (snd r) }
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
FStar.Pervasives.Native.tuple2 Parsers.NamedGroup.namedGroup LowParse.Spec.Bytes.parse_bounded_vlbytes_t Format.KeyShareEntry.MkkeyShareEntry FStar.Pervasives.Native.fst FStar.Pervasives.Native.snd Format.KeyShareEntry.keyShareEntry
module Format.KeyShareEntry

open Parsers.NamedGroup
open Format.UncompressedPointRepresentation

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


(* Parsers, validators *)
val synth_keyShareEntry (r: (namedGroup * (LowParse.Spec.Bytes.parse_bounded_vlbytes_t 1 65535)))
    : Tot keyShareEntry
r: (Parsers.NamedGroup.namedGroup * LowParse.Spec.Bytes.parse_bounded_vlbytes_t 1 65535)
  -> Format.KeyShareEntry.keyShareEntry