val keyShareEntry_parser32: LP.parser32 keyShareEntry_parser
let keyShareEntry_parser32 =
  lemma_synth_keyShareEntry_is_injective ();
  assert_norm (keyShareEntry_parser_kind' == keyShareEntry_parser_kind);
  LP.parse32_synth
    _
    synth_keyShareEntry
    (fun x -> synth_keyShareEntry x)
    (LP.parse32_nondep_then namedGroup_parser32 (LP.parse32_bounded_vlbytes 1 1ul 65535 65535ul))
    ()
val keyShareEntry_parser32: LP.parser32 keyShareEntry_parser
let keyShareEntry_parser32 =
lemma_synth_keyShareEntry_is_injective ();
assert_norm (keyShareEntry_parser_kind' == keyShareEntry_parser_kind);
LP.parse32_synth _
  synth_keyShareEntry
  (fun x -> synth_keyShareEntry x)
  (LP.parse32_nondep_then namedGroup_parser32 (LP.parse32_bounded_vlbytes 1 1ul 65535 65535ul))
  ()
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
LowParse.SLow.Combinators.parse32_synth LowParse.Spec.Combinators.and_then_kind Parsers.NamedGroup.namedGroup_parser_kind LowParse.Spec.VLData.parse_bounded_vldata_strong_kind LowParse.Spec.BoundedInt.log256' LowParse.Spec.Bytes.parse_all_bytes_kind FStar.Pervasives.Native.tuple2 Parsers.NamedGroup.namedGroup LowParse.Spec.Bytes.parse_bounded_vlbytes_t Format.KeyShareEntry.keyShareEntry LowParse.Spec.Combinators.nondep_then Parsers.NamedGroup.namedGroup_parser LowParse.Spec.Bytes.parse_bounded_vlbytes Format.KeyShareEntry.synth_keyShareEntry Prims.eq2 LowParse.SLow.Combinators.parse32_nondep_then Parsers.NamedGroup.namedGroup_parser32 LowParse.SLow.Bytes.parse32_bounded_vlbytes FStar.UInt32.__uint_to_t Prims.unit FStar.Pervasives.assert_norm LowParse.Spec.Base.parser_kind Format.KeyShareEntry.keyShareEntry_parser_kind' Format.KeyShareEntry.keyShareEntry_parser_kind Format.KeyShareEntry.lemma_synth_keyShareEntry_is_injective
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) }

inline_for_extraction
let unsynth_keyShareEntry (e:keyShareEntry): Tot (namedGroup * (LowParse.Spec.Bytes.parse_bounded_vlbytes_t 1 65535)) = e.group, e.key_exchange

#reset-options "--using_facts_from '* -LowParse -FStar.Reflection -FStar.Tactics'"
let lemma_synth_keyShareEntry_is_injective () 
  : Lemma (LP.synth_injective synth_keyShareEntry) 
  = LP.synth_injective_intro synth_keyShareEntry
#reset-options

inline_for_extraction
let keyShareEntry_parser_kind' =
  LP.and_then_kind namedGroup_parser_kind (LP.parse_bounded_vlbytes_kind 1 65535)

let keyShareEntry_parser_kind_metadata = keyShareEntry_parser_kind'.LP.parser_kind_metadata

#reset-options "--using_facts_from '* -FStar.Reflection -FStar.Tactics'"

let keyShareEntry_parser =
  lemma_synth_keyShareEntry_is_injective ();
  assert_norm (keyShareEntry_parser_kind' == keyShareEntry_parser_kind);
  LP.parse_synth 
    (namedGroup_parser `LP.nondep_then` (LP.parse_bounded_vlbytes 1 65535))
    synth_keyShareEntry
val keyShareEntry_parser32: LP.parser32 keyShareEntry_parser
LowParse.SLow.Base.parser32 Format.KeyShareEntry.keyShareEntry_parser