val synth_keyShareEntry (r: (namedGroup * (LowParse.Spec.Bytes.parse_bounded_vlbytes_t 1 65535)))
    : Tot keyShareEntry
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) }
module MiTLS.Format.KeyShareEntry
open MiTLS

open MiTLS.Parsers.NamedGroup
open MiTLS.Format.UncompressedPointRepresentation

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


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