val lemma_synth_keyShareEntry_of_unsynth_keyShareEntry: Prims.unit
  -> Lemma (LP.synth_inverse synth_keyShareEntry unsynth_keyShareEntry)
let lemma_synth_keyShareEntry_of_unsynth_keyShareEntry () 
  : Lemma (LP.synth_inverse synth_keyShareEntry unsynth_keyShareEntry)
  = LP.synth_inverse_intro synth_keyShareEntry unsynth_keyShareEntry
val lemma_synth_keyShareEntry_of_unsynth_keyShareEntry: Prims.unit
  -> Lemma (LP.synth_inverse synth_keyShareEntry unsynth_keyShareEntry)
let lemma_synth_keyShareEntry_of_unsynth_keyShareEntry ()
    : Lemma (LP.synth_inverse synth_keyShareEntry unsynth_keyShareEntry) =
LP.synth_inverse_intro synth_keyShareEntry unsynth_keyShareEntry
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
Prims.unit LowParse.Spec.Combinators.synth_inverse_intro FStar.Pervasives.Native.tuple2 Parsers.NamedGroup.namedGroup LowParse.Spec.Bytes.parse_bounded_vlbytes_t Format.KeyShareEntry.keyShareEntry Format.KeyShareEntry.synth_keyShareEntry Format.KeyShareEntry.unsynth_keyShareEntry Prims.l_True Prims.squash LowParse.Spec.Combinators.synth_inverse Prims.Nil FStar.Pervasives.pattern
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

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 ()
val lemma_synth_keyShareEntry_of_unsynth_keyShareEntry: Prims.unit
  -> Lemma (LP.synth_inverse synth_keyShareEntry unsynth_keyShareEntry)
_: Prims.unit
  -> FStar.Pervasives.Lemma
    (ensures
      LowParse.Spec.Combinators.synth_inverse Format.KeyShareEntry.synth_keyShareEntry
        Format.KeyShareEntry.unsynth_keyShareEntry)