val 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
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
val 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
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
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.Low.Sum.jump_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)
val 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

    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.Sum.sum_key t ->
    x: LowParse.Low.Sum.jump_sum_cases_t t pc k ->
    y: LowParse.Low.Sum.jump_sum_cases_t t pc k
  -> Prims.GTot Type0