val keyShareEntry_serializer32: LP.serializer32 keyShareEntry_serializer
val keyShareEntry_serializer32: LP.serializer32 keyShareEntry_serializer
let keyShareEntry_serializer32: LP.serializer32 keyShareEntry_serializer =
  lemma_synth_keyShareEntry_is_injective ();
  lemma_synth_keyShareEntry_of_unsynth_keyShareEntry ();
  assert_norm (keyShareEntry_parser_kind' == keyShareEntry_parser_kind);
  LP.serialize32_synth
    (LP.nondep_then namedGroup_parser (LP.parse_bounded_vlbytes 1 65535))
    synth_keyShareEntry
    (LP.serialize_nondep_then namedGroup_serializer
                              (LP.serialize_bounded_vlbytes 1 65535))
    (LP.serialize32_nondep_then namedGroup_serializer32
                              (LP.serialize32_bounded_vlbytes 1 65535))
    unsynth_keyShareEntry
    (fun x -> unsynth_keyShareEntry x)
    ()
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) }

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

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))
    ()
    

(* Serialization *)

#reset-options "--using_facts_from '* -LowParse -FStar.Reflection -FStar.Tactics'"
let lemma_synth_keyShareEntry_of_unsynth_keyShareEntry () 
  : Lemma (LP.synth_inverse synth_keyShareEntry unsynth_keyShareEntry)
  = LP.synth_inverse_intro synth_keyShareEntry unsynth_keyShareEntry
#reset-options

#reset-options "--using_facts_from '* -FStar.Reflection -FStar.Tactics'"
let keyShareEntry_serializer =
  lemma_synth_keyShareEntry_is_injective ();
  lemma_synth_keyShareEntry_of_unsynth_keyShareEntry ();
  assert_norm (keyShareEntry_parser_kind' == keyShareEntry_parser_kind);
  LP.serialize_synth
    _
    synth_keyShareEntry
    (LP.serialize_nondep_then namedGroup_serializer
                              (LP.serialize_bounded_vlbytes 1 65535))
    unsynth_keyShareEntry
    ()
/
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
LowParse.SLow.Base.serializer32 MiTLS.Format.KeyShareEntry.keyShareEntry_serializer
LowParse.SLow.Combinators.serialize32_synth LowParse.Spec.Combinators.and_then_kind MiTLS.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 MiTLS.Parsers.NamedGroup.namedGroup LowParse.Spec.Bytes.parse_bounded_vlbytes_t MiTLS.Format.KeyShareEntry.keyShareEntry LowParse.Spec.Combinators.nondep_then MiTLS.Parsers.NamedGroup.namedGroup_parser LowParse.Spec.Bytes.parse_bounded_vlbytes MiTLS.Format.KeyShareEntry.synth_keyShareEntry LowParse.Spec.Combinators.serialize_nondep_then MiTLS.Parsers.NamedGroup.namedGroup_serializer LowParse.Spec.Bytes.serialize_bounded_vlbytes LowParse.SLow.Combinators.serialize32_nondep_then MiTLS.Parsers.NamedGroup.namedGroup_serializer32 LowParse.SLow.Bytes.serialize32_bounded_vlbytes MiTLS.Format.KeyShareEntry.unsynth_keyShareEntry Prims.eq2 Prims.unit FStar.Pervasives.assert_norm LowParse.Spec.Base.parser_kind MiTLS.Format.KeyShareEntry.keyShareEntry_parser_kind' MiTLS.Format.KeyShareEntry.keyShareEntry_parser_kind MiTLS.Format.KeyShareEntry.lemma_synth_keyShareEntry_of_unsynth_keyShareEntry MiTLS.Format.KeyShareEntry.lemma_synth_keyShareEntry_is_injective LowParse.SLow.Base.serializer32 MiTLS.Format.KeyShareEntry.keyShareEntry_parser MiTLS.Format.KeyShareEntry.keyShareEntry_serializer
let keyShareEntry_serializer32:LP.serializer32 keyShareEntry_serializer =
  
lemma_synth_keyShareEntry_is_injective ();
lemma_synth_keyShareEntry_of_unsynth_keyShareEntry ();
assert_norm (keyShareEntry_parser_kind' == keyShareEntry_parser_kind);
LP.serialize32_synth (LP.nondep_then namedGroup_parser (LP.parse_bounded_vlbytes 1 65535))
  synth_keyShareEntry
  (LP.serialize_nondep_then namedGroup_serializer (LP.serialize_bounded_vlbytes 1 65535))
  (LP.serialize32_nondep_then namedGroup_serializer32 (LP.serialize32_bounded_vlbytes 1 65535))
  unsynth_keyShareEntry
  (fun x -> unsynth_keyShareEntry x)
  ()