val size32_sum_cases_aux
      (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)))))
      (sc32: (x: sum_key t -> Tot (size32 (sc x))))
      (k: sum_key t)
    : Tot (size32 (serialize_sum_cases t pc sc k))
let size32_sum_cases_aux
  (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)))))
  (sc32: ((x: sum_key t) -> Tot (size32 (sc x))))
  (k: sum_key t)
: Tot (size32 (serialize_sum_cases t pc sc k))
= fun input ->
  [@inline_let] let _ =
    Classical.forall_intro (parse_sum_cases_eq' t pc k);
    synth_sum_case_injective t k;
    synth_sum_case_inverse t k
  in
  size32_synth
    _
    (synth_sum_case t k)
    _
    (sc32 k)
    (synth_sum_case_recip t k)
    (fun x -> synth_sum_case_recip t k x)
    ()
    input
val size32_sum_cases_aux
      (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)))))
      (sc32: (x: sum_key t -> Tot (size32 (sc x))))
      (k: sum_key t)
    : Tot (size32 (serialize_sum_cases t pc sc k))
let size32_sum_cases_aux
      (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)))))
      (sc32: (x: sum_key t -> Tot (size32 (sc x))))
      (k: sum_key t)
    : Tot (size32 (serialize_sum_cases t pc sc k)) =
fun input ->
  [@@ inline_let ]let _ =
    Classical.forall_intro (parse_sum_cases_eq' t pc k);
    synth_sum_case_injective t k;
    synth_sum_case_inverse t k
  in
  size32_synth _
    (synth_sum_case t k)
    _
    (sc32 k)
    (synth_sum_case_recip t k)
    (fun x -> synth_sum_case_recip t k x)
    ()
    input
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.Spec.Base.serializer Prims.__proj__Mkdtuple2__item___1 FStar.Pervasives.dsnd LowParse.SLow.Base.size32 LowParse.Spec.Sum.sum_cases LowParse.SLow.Combinators.size32_synth LowParse.Spec.Sum.synth_sum_case LowParse.Spec.Sum.synth_sum_case_recip Prims.eq2 Prims.unit LowParse.Spec.Sum.synth_sum_case_inverse LowParse.Spec.Sum.synth_sum_case_injective FStar.Classical.forall_intro LowParse.Bytes.bytes FStar.Pervasives.Native.option FStar.Pervasives.Native.tuple2 LowParse.Spec.Base.consumed_length LowParse.Spec.Base.parse LowParse.Spec.Sum.parse_sum_cases LowParse.Spec.Sum.parse_sum_cases' LowParse.Spec.Sum.parse_sum_cases_eq' FStar.UInt32.t LowParse.SLow.Base.size32_postcond LowParse.Spec.Sum.weaken_parse_cases_kind LowParse.Spec.Sum.serialize_sum_cases
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)
: 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 } ))

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)))))
  (destr: dep_enum_destr (sum_enum t) (parse32_sum_cases_t t pc))
  (k: sum_key t)
: Tot (parser32 (parse_sum_cases t pc k))
= destr
    _
    (parse32_sum_cases_t_if t pc)
    (fun _ _ -> ())
    (fun _ _ _ _ -> ())
    (parse32_sum_cases_aux t pc pc32)
    k

inline_for_extraction
let parse32_sum'
  (#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)))))
  (destr: enum_destr_t (option (sum_type t * U32.t)) (sum_enum t))
  (input: B32.bytes)
: Pure (option (sum_type t * U32.t))
  (requires True)
  (ensures (fun res -> res == parse32_sum_aux t p p32 pc pc32 input))
= [@inline_let]
  let res : option (sum_type t * U32.t) =
    //NS: hoist nested match
    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
        destr
          (eq2 #(option (sum_type t * U32.t))) (default_if _)
          (fun _ -> ()) (fun _ _ _ -> ())
          (fun k ->
            //NS: hoist nested match
            let pcases2 = parse32_sum_cases' t pc pc32 k input_k in
            match pcases2 with
            | None -> None
            | Some (x, consumed_x) ->
              Some ((x <: sum_type t), consumed_k `U32.add` consumed_x)
          )
          k
  in
  res

inline_for_extraction
let parse32_sum
  (#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)))))
  (destr: enum_destr_t (option (sum_type t * U32.t)) (sum_enum t))
: Tot (parser32 (parse_sum t p pc))
= fun input ->
  (parse32_sum' t p p32 pc pc32 destr input <: (res: option (sum_type t * U32.t) { parser32_correct (parse_sum t p pc) input res } ))

inline_for_extraction
let parse32_sum2
  (#kt: parser_kind)
  (t: sum)
  (p: parser kt (sum_repr_type t))
  (p32: parser32 p)
  (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)))))
  (destr: enum_destr_t (option (sum_type t * U32.t)) (sum_enum t))
  (f: maybe_enum_key_of_repr'_t (sum_enum t))
: Tot (parser32 (parse_sum t p pc))
= parse32_sum t p (parse32_enum_key p32 (sum_enum t) f) pc pc32 destr

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)
: GTot Type0
= True

inline_for_extraction
let serialize32_sum_cases_t_if
  (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 (if_combinator _ (serialize32_sum_cases_t_eq t sc k))
= fun cond (sv_true: (cond_true cond -> Tot (serialize32_sum_cases_t t sc k))) (sv_false: (cond_false cond -> Tot (serialize32_sum_cases_t t sc k))) input ->
  if cond
  then (sv_true () input <: (res: _ { serializer32_correct (serialize_sum_cases t pc sc k) input res } ))
  else (sv_false () input <: (res: _ { serializer32_correct (serialize_sum_cases t pc sc k) input res } ))

inline_for_extraction
let serialize32_sum_cases_aux
  (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)))))
  (sc32: ((x: sum_key t) -> Tot (serializer32 (sc x))))
  (k: sum_key t)
: Tot (serializer32 (serialize_sum_cases t pc sc k))
= fun input ->
  [@inline_let] let _ =
    Classical.forall_intro (parse_sum_cases_eq' t pc k);
    synth_sum_case_injective t k;
    synth_sum_case_inverse t k
  in
  serialize32_synth
    _
    (synth_sum_case t k)
    _
    (sc32 k)
    (synth_sum_case_recip t k)
    (fun x -> synth_sum_case_recip t k x)
    ()
    input

inline_for_extraction
let serialize32_sum_cases
  (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)))))
  (sc32: ((x: sum_key t) -> Tot (serializer32 (sc x))))
  (destr: dep_enum_destr (sum_enum t) (serialize32_sum_cases_t t sc))
  (k: sum_key t)
: Tot (serializer32 (serialize_sum_cases t pc sc k))
= destr
    _
    (serialize32_sum_cases_t_if t sc)
    (fun _ _ -> ())
    (fun _ _ _ _ -> ())
    (serialize32_sum_cases_aux t sc sc32)
    k

let serialize32_sum_aux
  (#kt: parser_kind)
  (t: sum)
  (#p: parser kt (sum_repr_type t))
  (s: serializer p)
  (s32: serializer32 (serialize_enum_key _ s (sum_enum t)))
  (#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)))))
  (sc32: ((x: sum_key t) -> Tot (serializer32 (sc x))))
  (u: squash (serializer32_sum_gen_precond kt (weaken_parse_cases_kind t pc)))
: GTot (serializer32 (serialize_sum t s sc))
= fun x ->
  serialize_sum_eq t s sc x;
  let tg = sum_tag_of_data t x in
  let s1 = s32 tg in
  let s2 = sc32 tg (synth_sum_case_recip t tg x) in
  let res = s1 `B32.b32append` s2 in
  (res <: (res: B32.bytes { serializer32_correct (serialize_sum t s sc) x res } ))

inline_for_extraction
let serialize32_sum_destr_codom
  (t: sum)
  (k: sum_key t)
: Tot Type
= refine_with_tag (sum_tag_of_data t) k -> Tot B32.bytes

module T = FStar.Tactics

let serialize32_sum_destr_eq
  (t: sum)
  (k: sum_key t)
: Tot (serialize32_sum_destr_codom t k -> serialize32_sum_destr_codom t k -> GTot Type0)
= _ by (T.apply (`feq); T.apply (`eq2))

let serialize32_sum_destr_trans
  (t: sum)
  (k: sum_key t)
: Tot (r_transitive_t _ (serialize32_sum_destr_eq t k))
= feq_trans _ _ (eq2 #_)

inline_for_extraction
let serialize32_sum_destr_if
  (t: sum)
  (k: sum_key t)
: Tot (if_combinator _ (serialize32_sum_destr_eq t k))
= // _ by (T.apply (`fif); T.fail "abc")
  fif _ _ _ (default_if _) 

#set-options "--z3rlimit 32"

inline_for_extraction
let serialize32_sum
  (#kt: parser_kind)
  (t: sum)
  (#p: parser kt (sum_repr_type t))
  (s: serializer p)
  (s32: serializer32 (serialize_enum_key _ s (sum_enum t)))
  (#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)))))
  (sc32: ((x: sum_key t) -> Tot (serializer32 (sc x))))
  (destr: dep_enum_destr (sum_enum t) (serialize32_sum_destr_codom t))
  (u: squash (serializer32_sum_gen_precond kt (weaken_parse_cases_kind t pc)))
: Tot (serializer32 (serialize_sum t s sc))
= fun x ->
  [@inline_let]
  let _ = serialize_sum_eq t s sc x in
  let tg = sum_tag_of_data t x in
  let s1 = s32 tg in
  [@inline_let]
  let phi tg x = sc32 tg (synth_sum_case_recip t tg x) in
  [@inline_let]
  let phi'tg = destr
    (serialize32_sum_destr_eq t)
    (serialize32_sum_destr_if t)
    (fun _ _ -> ())
    (serialize32_sum_destr_trans t)
    phi
    tg
  in
  let s2 = phi'tg x in
  [@inline_let]
  let _ =
    let phitg = phi tg in
    feq_elim _ _ (eq2 #_) phitg phi'tg x
  in
  let res = s1 `B32.b32append` s2 in
  (res <: (res: B32.bytes { serializer32_correct (serialize_sum t s sc) x res } ))

#reset-options

inline_for_extraction
let serialize32_sum2
  (#kt: parser_kind)
  (t: sum)
  (#p: parser kt (sum_repr_type t))
  (s: serializer p)
  (s32: serializer32 s)
  (#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)))))
  (sc32: ((x: sum_key t) -> Tot (serializer32 (sc x))))
  (destr: dep_enum_destr (sum_enum t) (serialize32_sum_destr_codom t))
  (f: enum_repr_of_key'_t (sum_enum t))
  (u: squash (serializer32_sum_gen_precond kt (weaken_parse_cases_kind t pc)))
: Tot (serializer32 (serialize_sum t s sc))
= serialize32_sum t s (serialize32_enum_key s32 (sum_enum t) f) sc sc32 destr u

inline_for_extraction
let size32_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
= size32 (serialize_sum_cases t pc sc k)

let size32_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: size32_sum_cases_t t sc k)
: GTot Type0
= True

inline_for_extraction
let size32_sum_cases_t_if
  (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 (if_combinator _ (size32_sum_cases_t_eq t sc k))
= fun cond (sv_true: (cond_true cond -> Tot (size32_sum_cases_t t sc k))) (sv_false: (cond_false cond -> Tot (size32_sum_cases_t t sc k))) input ->
  if cond
  then (sv_true () input <: (res: _ { size32_postcond (serialize_sum_cases t pc sc k) input res } ))
  else (sv_false () input <: (res: _ { size32_postcond (serialize_sum_cases t pc sc k) input res } ))

inline_for_extraction
let size32_sum_cases_aux
  (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)))))
  (sc32: ((x: sum_key t) -> Tot (size32 (sc x))))
  (k: sum_key t)
val size32_sum_cases_aux
      (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)))))
      (sc32: (x: sum_key t -> Tot (size32 (sc x))))
      (k: sum_key t)
    : Tot (size32 (serialize_sum_cases t pc sc k))

    t: LowParse.Spec.Sum.sum ->
    sc:
      (x: LowParse.Spec.Sum.sum_key t
          -> LowParse.Spec.Base.serializer (FStar.Pervasives.dsnd (pc x))) ->
    sc32: (x: LowParse.Spec.Sum.sum_key t -> LowParse.SLow.Base.size32 (sc x)) ->
    k: LowParse.Spec.Sum.sum_key t
  -> LowParse.SLow.Base.size32 (LowParse.Spec.Sum.serialize_sum_cases t pc sc k)