val 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))
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
val 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))
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
    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
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.Base.parser_kind LowParse.Spec.Base.parser LowParse.Spec.Sum.sum_repr_type LowParse.Low.Base.validator LowParse.Low.Base.leaf_reader LowParse.Spec.Sum.sum_key Prims.dtuple2 LowParse.Spec.Sum.sum_type_of_tag LowParse.Low.Sum.validate_sum_aux_payload_t LowParse.Spec.Enum.maybe_enum_key_of_repr LowParse.Spec.Sum.sum_key_type LowParse.Spec.Sum.sum_enum LowParse.Slice.srel LowParse.Bytes.byte LowParse.Slice.slice FStar.UInt64.t LowParse.Low.ErrorCode.is_error Prims.bool Prims.unit LowParse.Spec.Enum.enum_key LowParse.Low.Base.Spec.valid_facts Prims.__proj__Mkdtuple2__item___1 FStar.Pervasives.dsnd LowParse.Low.ErrorCode.uint64_to_uint32 LowParse.Spec.Enum.maybe_enum_key FStar.Monotonic.HyperStack.mem FStar.HyperStack.ST.get LowParse.Spec.Sum.parse_sum_kind LowParse.Spec.Sum.sum_type LowParse.Spec.Sum.parse_sum LowParse.Spec.Sum.parse_sum_eq'' LowParse.Slice.bytes_of_slice_from
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)))
val 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))

    t: LowParse.Spec.Sum.sum ->
    v: LowParse.Low.Base.validator p ->
    p32: LowParse.Low.Base.leaf_reader p ->
    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))) ->
    v_payload:
      (k: LowParse.Spec.Sum.sum_repr_type t
          -> LowParse.Low.Sum.validate_sum_aux_payload_t t
              pc
              (LowParse.Spec.Enum.maybe_enum_key_of_repr (LowParse.Spec.Sum.sum_enum t) k))
  -> LowParse.Low.Base.validator (LowParse.Spec.Sum.parse_sum t p pc)