val 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)
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
val 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)
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
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.Enum.maybe_enum_key LowParse.Spec.Sum.sum_key_type LowParse.Spec.Sum.sum_repr_type LowParse.Spec.Sum.sum_enum LowParse.Low.Sum.validate_sum_aux_payload_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))
val 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)

    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))) ->
    k: LowParse.Spec.Enum.maybe_enum_key (LowParse.Spec.Sum.sum_enum t) ->
    _: LowParse.Low.Sum.validate_sum_aux_payload_t t pc k ->
    _: LowParse.Low.Sum.validate_sum_aux_payload_t t pc k
  -> Prims.GTot Type0