val unsynth_keyShareEntry (e: keyShareEntry)
    : Tot (namedGroup * (LowParse.Spec.Bytes.parse_bounded_vlbytes_t 1 65535))
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
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 *)

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) }
/
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
e: MiTLS.Format.KeyShareEntry.keyShareEntry
  -> MiTLS.Parsers.NamedGroup.namedGroup * LowParse.Spec.Bytes.parse_bounded_vlbytes_t 1 65535
MiTLS.Format.KeyShareEntry.keyShareEntry FStar.Pervasives.Native.Mktuple2 MiTLS.Parsers.NamedGroup.namedGroup LowParse.Spec.Bytes.parse_bounded_vlbytes_t MiTLS.Format.KeyShareEntry.__proj__MkkeyShareEntry__item__group MiTLS.Format.KeyShareEntry.__proj__MkkeyShareEntry__item__key_exchange FStar.Pervasives.Native.tuple2
let unsynth_keyShareEntry (e: keyShareEntry)
    : Tot (namedGroup * (LowParse.Spec.Bytes.parse_bounded_vlbytes_t 1 65535)) =
  
e.group, e.key_exchange