val serialize32_sum_cases_t_eq
      (t: sum)
      (#pc: (x: sum_key t -> Tot (k: parser_kind & parser k (sum_type_of_tag t x))))
      (sc: (x: sum_key t -> Tot (serializer (dsnd (pc x)))))
      (k: sum_key t)
      (x y: serialize32_sum_cases_t t sc k)
    : GTot Type0
let serialize32_sum_cases_t_eq
  (t: sum)
  (#pc: ((x: sum_key t) -> Tot (k: parser_kind & parser k (sum_type_of_tag t x))))
  (sc: ((x: sum_key t) -> Tot (serializer (dsnd (pc x)))))
  (k: sum_key t)
  (x y: serialize32_sum_cases_t t sc k)
: GTot Type0
= True
val serialize32_sum_cases_t_eq
      (t: sum)
      (#pc: (x: sum_key t -> Tot (k: parser_kind & parser k (sum_type_of_tag t x))))
      (sc: (x: sum_key t -> Tot (serializer (dsnd (pc x)))))
      (k: sum_key t)
      (x y: serialize32_sum_cases_t t sc k)
    : GTot Type0
let serialize32_sum_cases_t_eq
      (t: sum)
      (#pc: (x: sum_key t -> Tot (k: parser_kind & parser k (sum_type_of_tag t x))))
      (sc: (x: sum_key t -> Tot (serializer (dsnd (pc x)))))
      (k: sum_key t)
      (x y: serialize32_sum_cases_t t sc k)
    : GTot Type0 =
True
LowParse.Low.Sum.fst.checked
prims.fst.checked LowStar.Buffer.fst.checked LowParse.Spec.Sum.fst.checked LowParse.Low.Enum.fst.checked FStar.UInt64.fsti.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Int.Cast.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Classical.fsti.checked
LowParse.Low.Sum.fst
LowParse.Spec.Sum.sum LowParse.Spec.Sum.sum_key Prims.dtuple2 LowParse.Spec.Base.parser_kind LowParse.Spec.Base.parser LowParse.Spec.Sum.sum_type_of_tag LowParse.Spec.Base.serializer Prims.__proj__Mkdtuple2__item___1 FStar.Pervasives.dsnd LowParse.Low.Sum.serialize32_sum_cases_t Prims.l_True
module LowParse.Low.Sum
include LowParse.Low.Enum
include LowParse.Spec.Sum

module U32 = FStar.UInt32
module HST = FStar.HyperStack.ST
module B = LowStar.Buffer
module Cast = FStar.Int.Cast
module U64 = FStar.UInt64

inline_for_extraction
let validate_sum_cases_aux
  (t: sum)
  (pc: ((x: sum_key t) -> Tot (k: parser_kind & parser k (sum_type_of_tag t x))))
  (vc: ((x: sum_key t) -> Tot (validator (dsnd (pc x)))))
  (k: sum_key t)
: Tot (validator (parse_sum_cases t pc k))
= [@inline_let]
  let _ = synth_sum_case_injective t k in
  validate_synth
    (validate_weaken
      (weaken_parse_cases_kind t pc)
      (vc k)
      ()
    )
    (synth_sum_case t k)
    ()

inline_for_extraction
let validate_sum_cases_t
  (t: sum)
  (pc: ((x: sum_key t) -> Tot (k: parser_kind & parser k (sum_type_of_tag t x))))
  (k: sum_key t)
: Tot Type
= validator (parse_sum_cases t pc k)

let validate_sum_cases_t_eq
  (t: sum)
  (pc: ((x: sum_key t) -> Tot (k: parser_kind & parser k (sum_type_of_tag t x))))
  (k: sum_key t)
  (x y : validate_sum_cases_t t pc k)
: GTot Type0
= True

inline_for_extraction
let validate_sum_cases_t_if
  (t: sum)
  (pc: ((x: sum_key t) -> Tot (k: parser_kind & parser k (sum_type_of_tag t x))))
  (k: sum_key t)
: Tot (if_combinator _ (validate_sum_cases_t_eq t pc k))
= fun cond (sv_true: cond_true cond -> Tot (validate_sum_cases_t t pc k)) (sv_false: cond_false cond -> Tot (validate_sum_cases_t t pc k)) #rrel #rel input pos ->
  if cond
  then sv_true () input pos
  else sv_false () input pos

inline_for_extraction
let validate_sum_cases 
  (t: sum)
  (pc: ((x: sum_key t) -> Tot (k: parser_kind & parser k (sum_type_of_tag t x))))
  (vc: ((x: sum_key t) -> Tot (validator (dsnd (pc x)))))
  (destr: dep_enum_destr (sum_enum t) (validate_sum_cases_t t pc))
  (k: sum_key t)
: Tot (validator (parse_sum_cases t pc k))
= destr
    _
    (validate_sum_cases_t_if t pc)
    (fun _ _ -> ())
    (fun _ _ _ _ -> ())
    (validate_sum_cases_aux t pc vc)
    k

inline_for_extraction
let validate_sum_aux_payload_t
  (t: sum)
  (pc: ((x: sum_key t) -> Tot (k: parser_kind & parser k (sum_type_of_tag t x))))
  (k: maybe_enum_key (sum_enum t))
: Tot Type
= (#rrel: _) -> (#rel: _) ->
  (input: slice rrel rel) ->
  (pos: U64.t) ->
  HST.Stack U64.t
  (requires (fun h -> live_slice h input /\ U64.v pos <= U32.v input.len))
  (ensures (fun h res h' ->
    B.modifies B.loc_none h h' /\ (
    match k with
    | Unknown _ -> is_error res
    | Known k' ->
      if is_success res
      then
        valid_pos (dsnd (pc k')) h input (uint64_to_uint32 pos) (uint64_to_uint32 res)
      else
        (~ (valid (dsnd (pc k')) h input (uint64_to_uint32 pos)))
  )))

let validate_sum_aux_payload_eq
  (t: sum)
  (pc: ((x: sum_key t) -> Tot (k: parser_kind & parser k (sum_type_of_tag t x))))
  (k: maybe_enum_key (sum_enum t))
: Tot (validate_sum_aux_payload_t t pc k -> validate_sum_aux_payload_t t pc k -> GTot Type0)
= fun _ _ -> True

inline_for_extraction
let validate_sum_aux_payload_if'
  (t: sum)
  (pc: ((x: sum_key t) -> Tot (k: parser_kind & parser k (sum_type_of_tag t x))))
  (k: maybe_enum_key (sum_enum t))
  (cond: bool)
  (ift: ((cond_true cond) -> Tot (validate_sum_aux_payload_t t pc k)))
  (iff: ((cond_false cond) -> Tot (validate_sum_aux_payload_t t pc k)))
: Tot (validate_sum_aux_payload_t t pc k)
= fun #rrel #rel input pos ->
  if cond
  then begin
    (ift () <: validate_sum_aux_payload_t t pc k) input pos
  end else
    (iff () <: validate_sum_aux_payload_t t pc k) input pos

inline_for_extraction
let validate_sum_aux_payload_if
  (t: sum)
  (pc: ((x: sum_key t) -> Tot (k: parser_kind & parser k (sum_type_of_tag t x))))
  (k: maybe_enum_key (sum_enum t))
: Tot (if_combinator _ (validate_sum_aux_payload_eq t pc k))
= validate_sum_aux_payload_if' t pc k

#push-options "--z3rlimit 64 --z3cliopt smt.arith.nl=false --using_facts_from '* -FStar.Int.Cast -LowParse.BitFields'"

// --query_stats  --smtencoding.elim_box true --smtencoding.l_arith_repr native --z3refresh"

inline_for_extraction
let validate_sum_aux
  (t: sum)
  (#kt: parser_kind)
  (#p: parser kt (sum_repr_type t))
  (v: validator p)
  (p32: leaf_reader p)
  (pc: ((x: sum_key t) -> Tot (k: parser_kind & parser k (sum_type_of_tag t x))))
  (v_payload: ((k: sum_repr_type t)) -> Tot (validate_sum_aux_payload_t t pc (maybe_enum_key_of_repr (sum_enum t) k)))
: Tot (validator (parse_sum t p pc))
= fun #rrel #rel input pos ->
  let h = HST.get () in
  [@inline_let]
  let _ = parse_sum_eq'' t p pc (bytes_of_slice_from h input (uint64_to_uint32 pos)) in
  [@inline_let]
  let _ = valid_facts (parse_sum t p pc) h input (uint64_to_uint32 pos) in
  [@inline_let]
  let _ = valid_facts p h input (uint64_to_uint32 pos) in
  let len_after_tag = v input pos in
  if is_error len_after_tag
  then len_after_tag
  else begin
    let h1 = HST.get () in
    let k' = p32 input (uint64_to_uint32 pos) in
    [@inline_let]
    let _ =
      match maybe_enum_key_of_repr (sum_enum t) k' with
      | Known k -> valid_facts (dsnd (pc k)) h input (uint64_to_uint32 len_after_tag)
      | _ -> ()
    in
    v_payload k' input len_after_tag
  end

#pop-options

inline_for_extraction
let validate_sum_aux_payload'
  (t: sum)
  (pc: ((x: sum_key t) -> Tot (k: parser_kind & parser k (sum_type_of_tag t x))))
  (pc32: ((x: sum_key t) -> Tot (validator (dsnd (pc x)))))
  (k: maybe_enum_key (sum_enum t))
: Tot (validate_sum_aux_payload_t t pc k)
= fun #rrel #rel input pos ->
    match k with
    | Known k ->
      [@inline_let]
      let _ = synth_sum_case_injective t k in
      pc32 k input pos
      // validate_synth (pc32 k) (synth_sum_case t k) () input pos
    | _ -> validator_error_generic

inline_for_extraction
let validate_sum_aux_payload
  (t: sum)
  (pc: ((x: sum_key t) -> Tot (k: parser_kind & parser k (sum_type_of_tag t x))))
  (pc32: ((x: sum_key t) -> Tot (validator (dsnd (pc x)))))
  (destr: dep_maybe_enum_destr_t (sum_enum t) (validate_sum_aux_payload_t t pc))
  (k: sum_repr_type t)
: Tot (validate_sum_aux_payload_t t pc (maybe_enum_key_of_repr (sum_enum t) k))
= destr (validate_sum_aux_payload_eq t pc) (validate_sum_aux_payload_if t pc) (fun _ _ -> ()) (fun _ _ _ _ -> ()) (validate_sum_aux_payload' t pc pc32) k

inline_for_extraction
let validate_sum
  (t: sum)
  (#kt: parser_kind)
  (#p: parser kt (sum_repr_type t))
  (v: validator p)
  (p32: leaf_reader p)
  (pc: ((x: sum_key t) -> Tot (k: parser_kind & parser k (sum_type_of_tag t x))))
  (pc32: ((x: sum_key t) -> Tot (validator (dsnd (pc x)))))
  (destr: dep_maybe_enum_destr_t (sum_enum t) (validate_sum_aux_payload_t t pc))
: Tot (validator (parse_sum t p pc))
= validate_sum_aux t v p32 pc (validate_sum_aux_payload t pc pc32 destr)

module HS = FStar.HyperStack

#push-options "--z3rlimit 256 --z3cliopt smt.arith.nl=false --initial_ifuel 8 --max_ifuel 8 --initial_fuel 2 --max_fuel 2"
#restart-solver

let valid_sum_intro
  (h: HS.mem)
  (t: sum)
  (#kt: parser_kind)
  (p: parser kt (sum_repr_type t))
  (pc: ((x: sum_key t) -> Tot (k: parser_kind & parser k (sum_type_of_tag t x))))
  (#rrel #rel: _)
  (input: slice rrel rel)
  (pos: U32.t)
: Lemma
  (requires (
    valid (parse_enum_key p (sum_enum t)) h input pos /\ (
    let k = contents (parse_enum_key p (sum_enum t)) h input pos in
    valid (dsnd (pc k)) h input (get_valid_pos (parse_enum_key p (sum_enum t)) h input pos)
  )))
  (ensures (
    let k = contents (parse_enum_key p (sum_enum t)) h input pos in
    let pos_payload = get_valid_pos (parse_enum_key p (sum_enum t)) h input pos in
    valid_content_pos
      (parse_sum t p pc) h input pos
      (synth_sum_case t k (contents (dsnd (pc k)) h input pos_payload))
      (get_valid_pos (dsnd (pc k)) h input pos_payload)
  ))
= valid_facts (parse_enum_key p (sum_enum t)) h input pos;
  let k = contents (parse_enum_key p (sum_enum t)) h input pos in
  let pos_payload = get_valid_pos (parse_enum_key p (sum_enum t)) h input pos in
  valid_facts (dsnd (pc k)) h input pos_payload;
  valid_facts (parse_sum t p pc) h input pos;
  parse_sum_eq t p pc (bytes_of_slice_from h input pos)

#pop-options

inline_for_extraction
let finalize_sum_case
  (t: sum)
  (#kt: parser_kind)
  (#p: parser kt (sum_repr_type t))
  (s: serializer p)
  (w: leaf_writer_strong s)
  (pc: ((x: sum_key t) -> Tot (k: parser_kind & parser k (sum_type_of_tag t x))))
  (destr: enum_repr_of_key'_t (sum_enum t))
  (k: sum_key t)
  (#rrel #rel: _)
  (input: slice rrel rel)
  (pos: U32.t)
: HST.Stack unit
  (requires (fun h ->
    let len_tag = serialized_length (serialize_enum_key _ s (sum_enum t)) k in
    U32.v pos + len_tag < 4294967296 /\ (
    let pos_payload = pos `U32.add` U32.uint_to_t len_tag in
    valid (dsnd (pc k)) h input pos_payload /\
    writable input.base (U32.v pos) (U32.v pos_payload) h
  )))
  (ensures (fun h _ h' ->
    let len_tag = serialized_length (serialize_enum_key _ s (sum_enum t)) k in
    let pos_payload = pos `U32.add` U32.uint_to_t len_tag in
    B.modifies (loc_slice_from_to input pos pos_payload) h h' /\
    valid_content_pos (parse_sum t p pc) h' input pos (synth_sum_case t k (contents (dsnd (pc k)) h input pos_payload)) (get_valid_pos (dsnd (pc k)) h input pos_payload)
  ))
= let pos1 = write_enum_key w (sum_enum t) destr k input pos in
  let h = HST.get () in
  [@inline_let]
  let _ = valid_sum_intro h t p pc input pos in
  ()

inline_for_extraction
let jump_sum_cases_aux
  (t: sum)
  (pc: ((x: sum_key t) -> Tot (k: parser_kind & parser k (sum_type_of_tag t x))))
  (vc: ((x: sum_key t) -> Tot (jumper (dsnd (pc x)))))
  (k: sum_key t)
: Tot (jumper (parse_sum_cases t pc k))
= [@inline_let]
  let _ = synth_sum_case_injective t k in
  jump_synth
    (jump_weaken
      (weaken_parse_cases_kind t pc)
      (vc k)
      ()
    )
    (synth_sum_case t k)
    ()

inline_for_extraction
let jump_sum_cases_t
  (t: sum)
  (pc: ((x: sum_key t) -> Tot (k: parser_kind & parser k (sum_type_of_tag t x))))
  (k: sum_key t)
: Tot Type
= jumper (parse_sum_cases t pc k)

let jump_sum_cases_t_eq
  (t: sum)
  (pc: ((x: sum_key t) -> Tot (k: parser_kind & parser k (sum_type_of_tag t x))))
  (k: sum_key t)
  (x y : jump_sum_cases_t t pc k)
: GTot Type0
= True

inline_for_extraction
let jump_sum_cases_t_if
  (t: sum)
  (pc: ((x: sum_key t) -> Tot (k: parser_kind & parser k (sum_type_of_tag t x))))
  (k: sum_key t)
: Tot (if_combinator _ (jump_sum_cases_t_eq t pc k))
= fun cond (sv_true: cond_true cond -> Tot (jump_sum_cases_t t pc k)) (sv_false: cond_false cond -> Tot (jump_sum_cases_t t pc k)) #rrel #rel input pos ->
  if cond
  then sv_true () input pos
  else sv_false () input pos

inline_for_extraction
let jump_sum_cases 
  (t: sum)
  (pc: ((x: sum_key t) -> Tot (k: parser_kind & parser k (sum_type_of_tag t x))))
  (vc: ((x: sum_key t) -> Tot (jumper (dsnd (pc x)))))
  (destr: dep_enum_destr (sum_enum t) (jump_sum_cases_t t pc))
  (k: sum_key t)
: Tot (jumper (parse_sum_cases t pc k))
= destr
    _
    (jump_sum_cases_t_if t pc)
    (fun _ _ -> ())
    (fun _ _ _ _ -> ())
    (jump_sum_cases_aux t pc vc)
    k

inline_for_extraction
let jump_sum_aux_payload_t
  (t: sum)
  (pc: ((x: sum_key t) -> Tot (k: parser_kind & parser k (sum_type_of_tag t x))))
  (k: maybe_enum_key (sum_enum t))
: Tot Type
= (#rrel: _) -> (#rel: _) ->
  (input: slice rrel rel) ->
  (pos: U32.t) ->
  HST.Stack U32.t
  (requires (fun h -> live_slice h input /\ U32.v pos <= U32.v input.len /\ (
    match k with
    | Unknown _ -> False
    | Known k' -> valid (dsnd (pc k')) h input pos
  )))
  (ensures (fun h res h' ->
    B.modifies B.loc_none h h' /\ (
    match k with
    | Unknown _ -> False
    | Known k' ->
      valid_pos (dsnd (pc k')) h input pos res
  )))

let jump_sum_aux_payload_eq
  (t: sum)
  (pc: ((x: sum_key t) -> Tot (k: parser_kind & parser k (sum_type_of_tag t x))))
  (k: maybe_enum_key (sum_enum t))
: Tot (jump_sum_aux_payload_t t pc k -> jump_sum_aux_payload_t t pc k -> GTot Type0)
= fun _ _ -> True

inline_for_extraction
let jump_sum_aux_payload_if'
  (t: sum)
  (pc: ((x: sum_key t) -> Tot (k: parser_kind & parser k (sum_type_of_tag t x))))
  (k: maybe_enum_key (sum_enum t))
  (cond: bool)
  (ift: ((cond_true cond) -> Tot (jump_sum_aux_payload_t t pc k)))
  (iff: ((cond_false cond) -> Tot (jump_sum_aux_payload_t t pc k)))
: Tot (jump_sum_aux_payload_t t pc k)
= fun #rrel #rel input pos ->
  if cond
  then begin
    (ift () <: jump_sum_aux_payload_t t pc k) input pos
  end else
    (iff () <: jump_sum_aux_payload_t t pc k) input pos

inline_for_extraction
let jump_sum_aux_payload_if
  (t: sum)
  (pc: ((x: sum_key t) -> Tot (k: parser_kind & parser k (sum_type_of_tag t x))))
  (k: maybe_enum_key (sum_enum t))
: Tot (if_combinator _ (jump_sum_aux_payload_eq t pc k))
= jump_sum_aux_payload_if' t pc k

let parse_sum_eq3
  (#kt: parser_kind)
  (t: sum)
  (p: parser kt (sum_repr_type t))
  (pc: ((x: sum_key t) -> Tot (k: parser_kind & parser k (sum_type_of_tag t x))))
  (input: bytes)
  (k' : sum_repr_type t)
  (consumed_k: consumed_length input)
: Lemma
  (requires (Some? (parse (parse_sum t p pc) input) /\ parse p input == Some (k', consumed_k)))
  (ensures (
    let input_k = Seq.slice input consumed_k (Seq.length input) in
    let k = maybe_enum_key_of_repr (sum_enum t) k' in
    begin match k with
    | Known k ->
      Some? (parse (dsnd (pc k)) input_k)
    | _ -> False
    end
  ))
= parse_sum_eq'' t p pc input

let parse_sum_eq4
  (#kt: parser_kind)
  (t: sum)
  (p: parser kt (sum_repr_type t))
  (pc: ((x: sum_key t) -> Tot (k: parser_kind & parser k (sum_type_of_tag t x))))
  (input: bytes)
  (k' : sum_repr_type t)
  (consumed_k: consumed_length input)
  (consumed_payload: nat)
: Lemma
  (requires (Some? (parse (parse_sum t p pc) input) /\ parse p input == Some (k', consumed_k) /\ (
    let input_k = Seq.slice input consumed_k (Seq.length input) in
    let k = maybe_enum_key_of_repr (sum_enum t) k' in
    begin match k with
    | Known k ->
      Some? (parse (dsnd (pc k)) input_k) /\ (
      let Some (_, consumed_payload') = parse (dsnd (pc k)) input_k in
      consumed_payload' == consumed_payload
      )
    | _ -> False
    end
  )))
  (ensures (
      let Some (_, consumed) = parse (parse_sum t p pc) input in
      consumed == consumed_k + consumed_payload
  ))
= parse_sum_eq'' t p pc input

#push-options "--z3rlimit 16"

let valid_sum_elim
  (h: HS.mem)
  (t: sum)
  (#kt: parser_kind)
  (p: parser kt (sum_repr_type t))
  (pc: ((x: sum_key t) -> Tot (k: parser_kind & parser k (sum_type_of_tag t x))))
  (#rrel: _) (#rel: _)
  (input: slice rrel rel)
  (pos: U32.t)
: Lemma
  (requires (
    valid (parse_sum t p pc) h input pos
  ))
  (ensures (
    valid p h input pos /\ (
    let pos_payload = get_valid_pos p h input pos in
    let k' = maybe_enum_key_of_repr (sum_enum t) (contents p h input pos) in
    match k' with
    | Known k ->
      k == sum_tag_of_data t (contents (parse_sum t p pc) h input pos) /\
      valid (dsnd (pc k)) h input pos_payload /\
      valid_pos
        (parse_sum t p pc) h input pos
        (get_valid_pos (dsnd (pc k)) h input pos_payload)
    | _ -> False
  )))
= let sinput = bytes_of_slice_from h input pos in
  let _ = parse_sum_eq'' t p pc sinput in
  [@inline_let]
  let _ = valid_facts (parse_sum t p pc) h input pos in
  let Some (k', consumed_k) = parse p sinput in
  let pos_after_tag = U32.uint_to_t (U32.v pos + consumed_k) in
  [@inline_let]
  let _ = valid_facts p h input pos in
  assert (valid_content_pos p h input pos k' pos_after_tag);
  match maybe_enum_key_of_repr (sum_enum t) k' with
  | Known k -> valid_facts (dsnd (pc k)) h input pos_after_tag
  | _ -> ()

#pop-options

let valid_sum_elim_tag
  (h: HS.mem)
  (t: sum)
  (#kt: parser_kind)
  (p: parser kt (sum_repr_type t))
  (pc: ((x: sum_key t) -> Tot (k: parser_kind & parser k (sum_type_of_tag t x))))
  (#rrel #rel: _)
  (input: slice rrel rel)
  (pos: U32.t)
: Lemma
  (requires (
    valid (parse_sum t p pc) h input pos
  ))
  (ensures (
    valid (parse_enum_key p (sum_enum t)) h input pos /\
    contents (parse_enum_key p (sum_enum t)) h input pos == sum_tag_of_data t (contents (parse_sum t p pc) h input pos)
  ))
= let _ = parse_sum_eq' t p pc (bytes_of_slice_from h input pos) in
  let _ = valid_facts (parse_sum t p pc) h input pos in
  let _ = valid_facts (parse_enum_key p (sum_enum t)) h input pos in
  ()

inline_for_extraction
let read_sum_tag
  (t: sum)
  (#kt: parser_kind)
  (#p: parser kt (sum_repr_type t))
  (p32: leaf_reader p)
  (destr: dep_maybe_enum_destr_t (sum_enum t) (read_enum_key_t (sum_enum t)))
  (pc: ((x: sum_key t) -> Tot (k: parser_kind & parser k (sum_type_of_tag t x))))
  (#rrel #rel: _)
  (input: slice rrel rel)
  (pos: U32.t)
: HST.Stack (sum_key t)
  (requires (fun h ->
    valid (parse_sum t p pc) h input pos
  ))
  (ensures (fun h res h' ->
    B.modifies B.loc_none h h' /\
    res == sum_tag_of_data t (contents (parse_sum t p pc) h input pos)
  ))
= let h = HST.get () in
  [@inline_let] let _ = valid_sum_elim_tag h t p pc input pos in
  read_enum_key p32 (sum_enum t) destr input pos

inline_for_extraction
let jump_sum_aux
  (t: sum)
  (#kt: parser_kind)
  (#p: parser kt (sum_repr_type t))
  (v: jumper p)
  (p32: leaf_reader p)
  (pc: ((x: sum_key t) -> Tot (k: parser_kind & parser k (sum_type_of_tag t x))))
  (v_payload: ((k: sum_repr_type t)) -> Tot (jump_sum_aux_payload_t t pc (maybe_enum_key_of_repr (sum_enum t) k)))
: Tot (jumper (parse_sum t p pc))
= fun #rrel #rel input pos ->
  let h = HST.get () in
  [@inline_let]
  let _ = valid_sum_elim h t p pc input pos in
  let pos_after_tag = v input pos in
  let k' = p32 input pos in
  v_payload k' input pos_after_tag

inline_for_extraction
let jump_sum_aux_payload'
  (t: sum)
  (pc: ((x: sum_key t) -> Tot (k: parser_kind & parser k (sum_type_of_tag t x))))
  (pc32: ((x: sum_key t) -> Tot (jumper (dsnd (pc x)))))
  (k: maybe_enum_key (sum_enum t))
: Tot (jump_sum_aux_payload_t t pc k)
= fun #rrel #rel input pos ->
    match k with
    | Known k ->
      [@inline_let]
      let _ = synth_sum_case_injective t k in
      pc32 k input pos
    | _ -> 0ul // dummy, but we MUST NOT remove this branch, otherwise extraction fails

inline_for_extraction
let jump_sum_aux_payload
  (t: sum)
  (pc: ((x: sum_key t) -> Tot (k: parser_kind & parser k (sum_type_of_tag t x))))
  (pc32: ((x: sum_key t) -> Tot (jumper (dsnd (pc x)))))
  (destr: dep_maybe_enum_destr_t (sum_enum t) (jump_sum_aux_payload_t t pc))
  (k: sum_repr_type t)
: Tot (jump_sum_aux_payload_t t pc (maybe_enum_key_of_repr (sum_enum t) k))
= destr (jump_sum_aux_payload_eq t pc) (jump_sum_aux_payload_if t pc) (fun _ _ -> ()) (fun _ _ _ _ -> ()) (jump_sum_aux_payload' t pc pc32) k

inline_for_extraction
let jump_sum
  (t: sum)
  (#kt: parser_kind)
  (#p: parser kt (sum_repr_type t))
  (v: jumper p)
  (p32: leaf_reader p)
  (pc: ((x: sum_key t) -> Tot (k: parser_kind & parser k (sum_type_of_tag t x))))
  (pc32: ((x: sum_key t) -> Tot (jumper (dsnd (pc x)))))
  (destr: dep_maybe_enum_destr_t (sum_enum t) (jump_sum_aux_payload_t t pc))
: Tot (jumper (parse_sum t p pc))
= jump_sum_aux t v p32 pc (jump_sum_aux_payload t pc pc32 destr)

inline_for_extraction
let read_sum_cases'
  (t: sum)
  (pc: ((x: sum_key t) -> Tot (k: parser_kind & parser k (sum_type_of_tag t x))))
  (pc32: ((x: sum_key t) -> Tot (leaf_reader (dsnd (pc x)))))
  (k: sum_key t)
: Tot (leaf_reader (parse_sum_cases' t pc k))
= [@inline_let]
  let _ = synth_sum_case_injective t k in
        read_synth'
            (dsnd (pc k))
            (synth_sum_case t k)
            (pc32 k)
            ()

inline_for_extraction
let read_sum_cases_t
  (t: sum)
  (pc: ((x: sum_key t) -> Tot (k: parser_kind & parser k (sum_type_of_tag t x))))
  (k: sum_key t)
: Tot Type
= leaf_reader (parse_sum_cases' t pc k)

let read_sum_cases_t_eq
  (t: sum)
  (pc: ((x: sum_key t) -> Tot (k: parser_kind & parser k (sum_type_of_tag t x))))
  (k: sum_key t)
  (x y : read_sum_cases_t t pc k)
: GTot Type0
= True

inline_for_extraction
let read_sum_cases_t_if
  (t: sum)
  (pc: ((x: sum_key t) -> Tot (k: parser_kind & parser k (sum_type_of_tag t x))))
  (k: sum_key t)
: Tot (if_combinator _ (read_sum_cases_t_eq t pc k))
= fun cond (sv_true: cond_true cond -> Tot (read_sum_cases_t t pc k)) (sv_false: cond_false cond -> Tot (read_sum_cases_t t pc k)) #_ #_ input pos ->
  if cond
  then (sv_true () input pos)
  else (sv_false () input pos)

inline_for_extraction
let read_sum_cases 
  (t: sum)
  (pc: ((x: sum_key t) -> Tot (k: parser_kind & parser k (sum_type_of_tag t x))))
  (pc32: ((x: sum_key t) -> Tot (leaf_reader (dsnd (pc x)))))
  (destr: dep_enum_destr (sum_enum t) (read_sum_cases_t t pc))
  (k: sum_key t)
: Tot (leaf_reader (parse_sum_cases' t pc k))
= destr
    _
    (read_sum_cases_t_if t pc)
    (fun _ _ -> ())
    (fun _ _ _ _ -> ())
    (read_sum_cases' t pc pc32)
    k

#push-options "--z3rlimit 32"

inline_for_extraction
let read_sum
  (#kt: parser_kind)
  (t: sum)
  (p: parser kt (sum_repr_type t))
  (p32: leaf_reader (parse_enum_key p (sum_enum t)))
  (j: jumper p)
  (pc: ((x: sum_key t) -> Tot (k: parser_kind & parser k (sum_type_of_tag t x))))
  (pc32: ((x: sum_key t) -> Tot (leaf_reader (dsnd (pc x)))))
  (destr: dep_enum_destr (sum_enum t) (read_sum_cases_t t pc))
: Tot (leaf_reader (parse_sum t p pc))
=
  fun #_ #_ input pos ->
    let h = HST.get () in
    valid_facts (parse_sum t p pc) h input pos;
    parse_sum_eq' t p pc (bytes_of_slice_from h input pos);
    valid_facts (parse_enum_key p (sum_enum t)) h input pos;
    let k = p32 input pos in
    let pos' = jump_enum_key j (sum_enum t) input pos in
    valid_facts (parse_sum_cases' t pc k) h input pos' ;
    read_sum_cases t pc pc32 destr k input pos'

#pop-options

inline_for_extraction
let serialize32_sum_cases_t
  (t: sum)
  (#pc: ((x: sum_key t) -> Tot (k: parser_kind & parser k (sum_type_of_tag t x))))
  (sc: ((x: sum_key t) -> Tot (serializer (dsnd (pc x)))))
  (k: sum_key t)
: Tot Type
= serializer32 (serialize_sum_cases t pc sc k)

let serialize32_sum_cases_t_eq
  (t: sum)
  (#pc: ((x: sum_key t) -> Tot (k: parser_kind & parser k (sum_type_of_tag t x))))
  (sc: ((x: sum_key t) -> Tot (serializer (dsnd (pc x)))))
  (k: sum_key t)
  (x y: serialize32_sum_cases_t t sc k)
val serialize32_sum_cases_t_eq
      (t: sum)
      (#pc: (x: sum_key t -> Tot (k: parser_kind & parser k (sum_type_of_tag t x))))
      (sc: (x: sum_key t -> Tot (serializer (dsnd (pc x)))))
      (k: sum_key t)
      (x y: serialize32_sum_cases_t t sc k)
    : GTot Type0

    t: LowParse.Spec.Sum.sum ->
    sc:
      (x: LowParse.Spec.Sum.sum_key t
          -> LowParse.Spec.Base.serializer (FStar.Pervasives.dsnd (pc x))) ->
    k: LowParse.Spec.Sum.sum_key t ->
    x: LowParse.Low.Sum.serialize32_sum_cases_t t sc k ->
    y: LowParse.Low.Sum.serialize32_sum_cases_t t sc k
  -> Prims.GTot Type0