val parse32_sum_cases_aux
      (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 (parser32 (dsnd (pc x)))))
      (k: sum_key t)
    : Tot (parser32 (parse_sum_cases t pc k))
let parse32_sum_cases_aux
  (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 (parser32 (dsnd (pc x)))))
  (k: sum_key t)
: Tot (parser32 (parse_sum_cases t pc k))
= fun (input: B32.bytes) ->
  [@inline_let] let _ = parse_sum_cases_eq' t pc k (B32.reveal input) in
  (parse32_sum_cases' t pc pc32 k input <: (res: _ { parser32_correct (parse_sum_cases t pc k) input res } ))
val parse32_sum_cases_aux
      (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 (parser32 (dsnd (pc x)))))
      (k: sum_key t)
    : Tot (parser32 (parse_sum_cases t pc k))
let parse32_sum_cases_aux
      (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 (parser32 (dsnd (pc x)))))
      (k: sum_key t)
    : Tot (parser32 (parse_sum_cases t pc k)) =
fun (input: B32.bytes) ->
  [@@ inline_let ]let _ = parse_sum_cases_eq' t pc k (B32.reveal input) in
  (parse32_sum_cases' t pc pc32 k input
    <:
    (res: _{parser32_correct (parse_sum_cases t pc k) input res}))
LowParse.SLow.Sum.fst.checked
prims.fst.checked LowParse.Spec.Sum.fst.checked LowParse.SLow.Enum.fst.checked LowParse.Bytes32.fst.checked FStar.UInt32.fsti.checked FStar.Tactics.Effect.fsti.checked FStar.Tactics.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Classical.fsti.checked
LowParse.SLow.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.SLow.Base.parser32 Prims.__proj__Mkdtuple2__item___1 FStar.Pervasives.dsnd FStar.Bytes.bytes LowParse.SLow.Sum.parse32_sum_cases' FStar.Pervasives.Native.option FStar.Pervasives.Native.tuple2 LowParse.Spec.Sum.sum_cases FStar.UInt32.t LowParse.SLow.Base.parser32_correct LowParse.Spec.Sum.weaken_parse_cases_kind LowParse.Spec.Sum.parse_sum_cases Prims.unit LowParse.Spec.Sum.parse_sum_cases_eq' FStar.Bytes.reveal
module LowParse.SLow.Sum
include LowParse.Spec.Sum
include LowParse.SLow.Enum

module B32 = LowParse.Bytes32
module U32 = FStar.UInt32

let serializer32_sum_gen_precond
  (kt: parser_kind)
  (k: parser_kind)
: GTot Type0
= kt.parser_kind_subkind == Some ParserStrong /\
  Some? kt.parser_kind_high /\
  Some? k.parser_kind_high /\ (
  let (Some vt) = kt.parser_kind_high in
  let (Some v) = k.parser_kind_high in
  vt + v < 4294967296
  )

inline_for_extraction
let parse32_sum_t (t: sum) : Tot Type =
  bytes32 -> Tot (option (sum_type t * U32.t))

let parse32_sum_eq (t: sum) : Tot (parse32_sum_t t -> parse32_sum_t t -> GTot Type0) =
  feq _ _ (eq2 #_)

inline_for_extraction
let parse32_sum_if (t: sum) : Tot (if_combinator _ (parse32_sum_eq t)) =
  fif _ _ _ (default_if _)

let parse32_sum_eq_refl (t: sum) : Tot (r_reflexive_t _ (parse32_sum_eq t)) =
  fun _ -> ()

let parse32_sum_eq_trans (t: sum) : Tot (r_transitive_t _ (parse32_sum_eq t)) = feq_trans _ _ (eq2 #_)

inline_for_extraction
let parse32_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 (parser32 (dsnd (pc x)))))
  (k: sum_key t)
: Tot (parser32 (parse_sum_cases' t pc k))
= [@inline_let]
  let _ = synth_sum_case_injective t k in
        parse32_synth'
            (dsnd (pc k))
            (synth_sum_case t k)
            (pc32 k)
            ()

let parse32_sum_aux
  (#kt: parser_kind)
  (t: sum)
  (p: parser kt (sum_repr_type t))
  (p32: parser32 (parse_enum_key p (sum_enum t)))
  (pc: ((x: sum_key t) -> Tot (k: parser_kind & parser k (sum_type_of_tag t x))))
  (pc32: ((x: sum_key t) -> Tot (parser32 (dsnd (pc x)))))
: GTot (parser32 (parse_sum t p pc))
= fun input ->
  parse_sum_eq' t p pc (B32.reveal input);
  [@inline_let]
  let res : option (sum_type t * U32.t) =
    //NS: hoist nested match
    //we do not expect the case analysis to
    //on `p32 input` to reduce; hoist it for more efficient
    //normalization.
    //Note, in some simple cases, e.g., parsing raw enums
    //this r the pcases below maybe statically evaluated
    //to a `Some v`; this forgoes reduction in those simple
    //cases for more efficient extraction in more complex
    //common cases
    let pi = p32 input in
    match pi with
    | None -> None
    | Some (k, consumed_k) ->
        let input_k = B32.b32slice input consumed_k (B32.len input) in
        //NS: hoist nested match
        let pcases1 = parse32_sum_cases' t pc pc32 k input_k in
        match pcases1 with
        | None -> None
        | Some (x, consumed_x) ->
          Some ((x <: sum_type t), consumed_k `U32.add` consumed_x)
  in
  (res <: (res: option (sum_type t * U32.t) { parser32_correct (parse_sum t p pc) input res } ))

inline_for_extraction
let parse32_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
= parser32 (parse_sum_cases t pc k)

let parse32_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 : parse32_sum_cases_t t pc k)
: GTot Type0
= True

inline_for_extraction
let parse32_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 _ (parse32_sum_cases_t_eq t pc k))
= fun cond (sv_true: cond_true cond -> Tot (parse32_sum_cases_t t pc k)) (sv_false: cond_false cond -> Tot (parse32_sum_cases_t t pc k)) input ->
  if cond
  then (sv_true () input <: (res: _ { parser32_correct (parse_sum_cases t pc k) input res}))
  else (sv_false () input <: (res: _ {parser32_correct (parse_sum_cases t pc k) input res}))

inline_for_extraction
let parse32_sum_cases_aux
  (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 (parser32 (dsnd (pc x)))))
  (k: sum_key t)
val parse32_sum_cases_aux
      (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 (parser32 (dsnd (pc x)))))
      (k: sum_key t)
    : Tot (parser32 (parse_sum_cases t pc k))

    t: LowParse.Spec.Sum.sum ->
    pc:
      (x: LowParse.Spec.Sum.sum_key t
          -> Prims.dtuple2 LowParse.Spec.Base.parser_kind
              (fun k -> LowParse.Spec.Base.parser k (LowParse.Spec.Sum.sum_type_of_tag t x))) ->
    pc32:
      (x: LowParse.Spec.Sum.sum_key t -> LowParse.SLow.Base.parser32 (FStar.Pervasives.dsnd (pc x))) ->
    k: LowParse.Spec.Sum.sum_key t
  -> LowParse.SLow.Base.parser32 (LowParse.Spec.Sum.parse_sum_cases t pc k)