val serialize32_ifthenelse
      (#p: parse_ifthenelse_param)
      (s:
          serialize_ifthenelse_param p
            { let tk = p.parse_ifthenelse_tag_kind in
              tk.parser_kind_subkind == Some ParserStrong /\ Some? tk.parser_kind_high /\
              Some? (dfst (p.parse_ifthenelse_payload_parser true)).parser_kind_high /\
              Some? (dfst (p.parse_ifthenelse_payload_parser false)).parser_kind_high /\
              Some?.v tk.parser_kind_high +
              Some?.v (dfst (p.parse_ifthenelse_payload_parser true)).parser_kind_high <
              4294967296 /\
              Some?.v tk.parser_kind_high +
              Some?.v (dfst (p.parse_ifthenelse_payload_parser false)).parser_kind_high <
              4294967296 })
      (st32: serializer32 s.serialize_ifthenelse_tag_serializer)
      (syntt:
          (x: p.parse_ifthenelse_t
              -> Tot (t: p.parse_ifthenelse_tag_t{t == dfst (s.serialize_ifthenelse_synth_recip x)})
          ))
      (b32: (t: p.parse_ifthenelse_tag_t -> Tot (b: bool{b == p.parse_ifthenelse_tag_cond t})))
      (syntp:
          (
                b: bool ->
                x:
                  p.parse_ifthenelse_t
                    {b == p.parse_ifthenelse_tag_cond (dfst (s.serialize_ifthenelse_synth_recip x))}
              -> Tot
                (pl:
                  p.parse_ifthenelse_payload_t b {pl == dsnd (s.serialize_ifthenelse_synth_recip x)}
                )))
      (sp32: (b: bool -> Tot (serializer32 (s.serialize_ifthenelse_payload_serializer b))))
    : Tot (serializer32 (serialize_ifthenelse s))
let serialize32_ifthenelse
  (#p: parse_ifthenelse_param)
  (s: serialize_ifthenelse_param p {
    let tk = p.parse_ifthenelse_tag_kind in
    tk.parser_kind_subkind == Some ParserStrong /\
    Some? tk.parser_kind_high /\
    Some? (dfst (p.parse_ifthenelse_payload_parser true)).parser_kind_high /\
    Some? (dfst (p.parse_ifthenelse_payload_parser false)).parser_kind_high /\
    Some?.v tk.parser_kind_high + Some?.v (dfst (p.parse_ifthenelse_payload_parser true)).parser_kind_high < 4294967296 /\
    Some?.v tk.parser_kind_high + Some?.v (dfst (p.parse_ifthenelse_payload_parser false)).parser_kind_high < 4294967296
  })
  (st32: serializer32 s.serialize_ifthenelse_tag_serializer)
  (syntt: (x: p.parse_ifthenelse_t) -> Tot (t: p.parse_ifthenelse_tag_t { t == dfst (s.serialize_ifthenelse_synth_recip x) } ))
  (b32: (t: p.parse_ifthenelse_tag_t) -> Tot (b: bool { b == p.parse_ifthenelse_tag_cond t } ))
  (syntp: (b: bool) -> (x: p.parse_ifthenelse_t { b == p.parse_ifthenelse_tag_cond (dfst (s.serialize_ifthenelse_synth_recip x)) } ) -> Tot (pl: p.parse_ifthenelse_payload_t b { pl == dsnd (s.serialize_ifthenelse_synth_recip x) } ))
  (sp32: (b: bool) -> Tot (serializer32 (s.serialize_ifthenelse_payload_serializer b)))
: Tot (serializer32 (serialize_ifthenelse s))
= fun (input: p.parse_ifthenelse_t) -> ((
    let t = syntt input in
    let st = st32 t in
    let b = b32 t in
    if b
    then
      let y = syntp true input in
      B32.append st (sp32 true y)
    else
      let y = syntp false input in
      B32.append st (sp32 false y)
  ) <: (res: _ { serializer32_correct (serialize_ifthenelse s) input res }))
val serialize32_ifthenelse
      (#p: parse_ifthenelse_param)
      (s:
          serialize_ifthenelse_param p
            { let tk = p.parse_ifthenelse_tag_kind in
              tk.parser_kind_subkind == Some ParserStrong /\ Some? tk.parser_kind_high /\
              Some? (dfst (p.parse_ifthenelse_payload_parser true)).parser_kind_high /\
              Some? (dfst (p.parse_ifthenelse_payload_parser false)).parser_kind_high /\
              Some?.v tk.parser_kind_high +
              Some?.v (dfst (p.parse_ifthenelse_payload_parser true)).parser_kind_high <
              4294967296 /\
              Some?.v tk.parser_kind_high +
              Some?.v (dfst (p.parse_ifthenelse_payload_parser false)).parser_kind_high <
              4294967296 })
      (st32: serializer32 s.serialize_ifthenelse_tag_serializer)
      (syntt:
          (x: p.parse_ifthenelse_t
              -> Tot (t: p.parse_ifthenelse_tag_t{t == dfst (s.serialize_ifthenelse_synth_recip x)})
          ))
      (b32: (t: p.parse_ifthenelse_tag_t -> Tot (b: bool{b == p.parse_ifthenelse_tag_cond t})))
      (syntp:
          (
                b: bool ->
                x:
                  p.parse_ifthenelse_t
                    {b == p.parse_ifthenelse_tag_cond (dfst (s.serialize_ifthenelse_synth_recip x))}
              -> Tot
                (pl:
                  p.parse_ifthenelse_payload_t b {pl == dsnd (s.serialize_ifthenelse_synth_recip x)}
                )))
      (sp32: (b: bool -> Tot (serializer32 (s.serialize_ifthenelse_payload_serializer b))))
    : Tot (serializer32 (serialize_ifthenelse s))
let serialize32_ifthenelse
      (#p: parse_ifthenelse_param)
      (s:
          serialize_ifthenelse_param p
            { let tk = p.parse_ifthenelse_tag_kind in
              tk.parser_kind_subkind == Some ParserStrong /\ Some? tk.parser_kind_high /\
              Some? (dfst (p.parse_ifthenelse_payload_parser true)).parser_kind_high /\
              Some? (dfst (p.parse_ifthenelse_payload_parser false)).parser_kind_high /\
              Some?.v tk.parser_kind_high +
              Some?.v (dfst (p.parse_ifthenelse_payload_parser true)).parser_kind_high <
              4294967296 /\
              Some?.v tk.parser_kind_high +
              Some?.v (dfst (p.parse_ifthenelse_payload_parser false)).parser_kind_high <
              4294967296 })
      (st32: serializer32 s.serialize_ifthenelse_tag_serializer)
      (syntt:
          (x: p.parse_ifthenelse_t
              -> Tot (t: p.parse_ifthenelse_tag_t{t == dfst (s.serialize_ifthenelse_synth_recip x)})
          ))
      (b32: (t: p.parse_ifthenelse_tag_t -> Tot (b: bool{b == p.parse_ifthenelse_tag_cond t})))
      (syntp:
          (
                b: bool ->
                x:
                  p.parse_ifthenelse_t
                    {b == p.parse_ifthenelse_tag_cond (dfst (s.serialize_ifthenelse_synth_recip x))}
              -> Tot
                (pl:
                  p.parse_ifthenelse_payload_t b {pl == dsnd (s.serialize_ifthenelse_synth_recip x)}
                )))
      (sp32: (b: bool -> Tot (serializer32 (s.serialize_ifthenelse_payload_serializer b))))
    : Tot (serializer32 (serialize_ifthenelse s)) =
fun (input: p.parse_ifthenelse_t) ->
  ((let t = syntt input in
      let st = st32 t in
      let b = b32 t in
      if b
      then
        let y = syntp true input in
        B32.append st (sp32 true y)
      else
        let y = syntp false input in
        B32.append st (sp32 false y))
    <:
    (res: _{serializer32_correct (serialize_ifthenelse s) input res}))
LowParse.SLow.IfThenElse.fst.checked
prims.fst.checked LowParse.Spec.IfThenElse.fst.checked LowParse.SLow.Combinators.fst.checked LowParse.Bytes32.fst.checked FStar.UInt32.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked
LowParse.SLow.IfThenElse.fst
LowParse.Spec.IfThenElse.parse_ifthenelse_param LowParse.Spec.IfThenElse.serialize_ifthenelse_param Prims.l_and Prims.eq2 FStar.Pervasives.Native.option LowParse.Spec.Base.parser_subkind LowParse.Spec.Base.__proj__Mkparser_kind'__item__parser_kind_subkind FStar.Pervasives.Native.Some LowParse.Spec.Base.ParserStrong Prims.b2t FStar.Pervasives.Native.uu___is_Some Prims.nat LowParse.Spec.Base.__proj__Mkparser_kind'__item__parser_kind_high FStar.Pervasives.dfst LowParse.Spec.Base.parser_kind LowParse.Spec.Base.parser LowParse.Spec.IfThenElse.__proj__Mkparse_ifthenelse_param__item__parse_ifthenelse_payload_t LowParse.Spec.IfThenElse.__proj__Mkparse_ifthenelse_param__item__parse_ifthenelse_payload_parser Prims.op_LessThan Prims.op_Addition FStar.Pervasives.Native.__proj__Some__item__v LowParse.Spec.IfThenElse.__proj__Mkparse_ifthenelse_param__item__parse_ifthenelse_tag_kind LowParse.SLow.Base.serializer32 LowParse.Spec.IfThenElse.__proj__Mkparse_ifthenelse_param__item__parse_ifthenelse_tag_t LowParse.Spec.IfThenElse.__proj__Mkparse_ifthenelse_param__item__parse_ifthenelse_tag_parser LowParse.Spec.IfThenElse.__proj__Mkserialize_ifthenelse_param__item__serialize_ifthenelse_tag_serializer LowParse.Spec.IfThenElse.__proj__Mkparse_ifthenelse_param__item__parse_ifthenelse_t LowParse.Spec.IfThenElse.__proj__Mkparse_ifthenelse_param__item__parse_ifthenelse_tag_cond LowParse.Spec.IfThenElse.__proj__Mkserialize_ifthenelse_param__item__serialize_ifthenelse_synth_recip Prims.bool FStar.Pervasives.dsnd Prims.__proj__Mkdtuple2__item___1 LowParse.Spec.IfThenElse.__proj__Mkserialize_ifthenelse_param__item__serialize_ifthenelse_payload_serializer FStar.Bytes.append LowParse.SLow.Base.bytes32 LowParse.SLow.Base.serializer32_correct LowParse.Spec.IfThenElse.parse_ifthenelse_kind LowParse.Spec.IfThenElse.parse_ifthenelse LowParse.Spec.IfThenElse.serialize_ifthenelse
module LowParse.SLow.IfThenElse
include LowParse.Spec.IfThenElse
include LowParse.SLow.Combinators

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

inline_for_extraction
let parse32_ifthenelse
  (p: parse_ifthenelse_param)
  (pt32: parser32 p.parse_ifthenelse_tag_parser)
  (b32: (t: p.parse_ifthenelse_tag_t) -> Tot (b: bool { b == p.parse_ifthenelse_tag_cond t } ))
  (pp32: (b: bool) -> Tot (parser32 (dsnd (p.parse_ifthenelse_payload_parser b))))
  (synt: (b: bool) -> (t: p.parse_ifthenelse_tag_t { b == p.parse_ifthenelse_tag_cond t } ) -> (pl: p.parse_ifthenelse_payload_t b) -> Tot (y: p.parse_ifthenelse_t { y == p.parse_ifthenelse_synth t pl } ))
: Tot (parser32 (parse_ifthenelse p))
= fun input ->
  ((
    [@inline_let]
    let _ = parse_ifthenelse_eq p (B32.reveal input) in
    match pt32 input with
    | None -> None
    | Some (t, consumed_t) ->
      let b = b32 t in
      let input' = B32.slice input consumed_t (B32.len input) in
      if b
      then
        match pp32 true input' with
        | None -> None
        | Some (pl, consumed_pl) ->
          Some (synt true t pl, consumed_t `U32.add` consumed_pl)
      else
        match pp32 false input' with
        | None -> None
        | Some (pl, consumed_pl) ->
          Some (synt false t pl, consumed_t `U32.add` consumed_pl)
  ) <: (res: _ { parser32_correct (parse_ifthenelse p) input res } )
  )

inline_for_extraction
let serialize32_ifthenelse
  (#p: parse_ifthenelse_param)
  (s: serialize_ifthenelse_param p {
    let tk = p.parse_ifthenelse_tag_kind in
    tk.parser_kind_subkind == Some ParserStrong /\
    Some? tk.parser_kind_high /\
    Some? (dfst (p.parse_ifthenelse_payload_parser true)).parser_kind_high /\
    Some? (dfst (p.parse_ifthenelse_payload_parser false)).parser_kind_high /\
    Some?.v tk.parser_kind_high + Some?.v (dfst (p.parse_ifthenelse_payload_parser true)).parser_kind_high < 4294967296 /\
    Some?.v tk.parser_kind_high + Some?.v (dfst (p.parse_ifthenelse_payload_parser false)).parser_kind_high < 4294967296
  })
  (st32: serializer32 s.serialize_ifthenelse_tag_serializer)
  (syntt: (x: p.parse_ifthenelse_t) -> Tot (t: p.parse_ifthenelse_tag_t { t == dfst (s.serialize_ifthenelse_synth_recip x) } ))
  (b32: (t: p.parse_ifthenelse_tag_t) -> Tot (b: bool { b == p.parse_ifthenelse_tag_cond t } ))
  (syntp: (b: bool) -> (x: p.parse_ifthenelse_t { b == p.parse_ifthenelse_tag_cond (dfst (s.serialize_ifthenelse_synth_recip x)) } ) -> Tot (pl: p.parse_ifthenelse_payload_t b { pl == dsnd (s.serialize_ifthenelse_synth_recip x) } ))
  (sp32: (b: bool) -> Tot (serializer32 (s.serialize_ifthenelse_payload_serializer b)))
val serialize32_ifthenelse
      (#p: parse_ifthenelse_param)
      (s:
          serialize_ifthenelse_param p
            { let tk = p.parse_ifthenelse_tag_kind in
              tk.parser_kind_subkind == Some ParserStrong /\ Some? tk.parser_kind_high /\
              Some? (dfst (p.parse_ifthenelse_payload_parser true)).parser_kind_high /\
              Some? (dfst (p.parse_ifthenelse_payload_parser false)).parser_kind_high /\
              Some?.v tk.parser_kind_high +
              Some?.v (dfst (p.parse_ifthenelse_payload_parser true)).parser_kind_high <
              4294967296 /\
              Some?.v tk.parser_kind_high +
              Some?.v (dfst (p.parse_ifthenelse_payload_parser false)).parser_kind_high <
              4294967296 })
      (st32: serializer32 s.serialize_ifthenelse_tag_serializer)
      (syntt:
          (x: p.parse_ifthenelse_t
              -> Tot (t: p.parse_ifthenelse_tag_t{t == dfst (s.serialize_ifthenelse_synth_recip x)})
          ))
      (b32: (t: p.parse_ifthenelse_tag_t -> Tot (b: bool{b == p.parse_ifthenelse_tag_cond t})))
      (syntp:
          (
                b: bool ->
                x:
                  p.parse_ifthenelse_t
                    {b == p.parse_ifthenelse_tag_cond (dfst (s.serialize_ifthenelse_synth_recip x))}
              -> Tot
                (pl:
                  p.parse_ifthenelse_payload_t b {pl == dsnd (s.serialize_ifthenelse_synth_recip x)}
                )))
      (sp32: (b: bool -> Tot (serializer32 (s.serialize_ifthenelse_payload_serializer b))))
    : Tot (serializer32 (serialize_ifthenelse s))

    s:
      LowParse.Spec.IfThenElse.serialize_ifthenelse_param p
        { let tk = Mkparse_ifthenelse_param?.parse_ifthenelse_tag_kind p in
          Mkparser_kind'?.parser_kind_subkind tk ==
          FStar.Pervasives.Native.Some LowParse.Spec.Base.ParserStrong /\
          Some? (Mkparser_kind'?.parser_kind_high tk) /\
          Some? (Mkparser_kind'?.parser_kind_high (FStar.Pervasives.dfst (Mkparse_ifthenelse_param?.parse_ifthenelse_payload_parser
                        p
                        true))) /\
          Some? (Mkparser_kind'?.parser_kind_high (FStar.Pervasives.dfst (Mkparse_ifthenelse_param?.parse_ifthenelse_payload_parser
                        p
                        false))) /\
          Some?.v (Mkparser_kind'?.parser_kind_high tk) +
          Some?.v (Mkparser_kind'?.parser_kind_high (FStar.Pervasives.dfst (Mkparse_ifthenelse_param?.parse_ifthenelse_payload_parser
                        p
                        true))) <
          4294967296 /\
          Some?.v (Mkparser_kind'?.parser_kind_high tk) +
          Some?.v (Mkparser_kind'?.parser_kind_high (FStar.Pervasives.dfst (Mkparse_ifthenelse_param?.parse_ifthenelse_payload_parser
                        p
                        false))) <
          4294967296 } ->
    st32:
      LowParse.SLow.Base.serializer32 (Mkserialize_ifthenelse_param?.serialize_ifthenelse_tag_serializer
            s) ->
    syntt:
      (x: Mkparse_ifthenelse_param?.parse_ifthenelse_t p
          -> t:
            Mkparse_ifthenelse_param?.parse_ifthenelse_tag_t p
              { t ==
                FStar.Pervasives.dfst (Mkserialize_ifthenelse_param?.serialize_ifthenelse_synth_recip
                      s
                      x) }) ->
    b32:
      (t: Mkparse_ifthenelse_param?.parse_ifthenelse_tag_t p
          -> b: Prims.bool{b == Mkparse_ifthenelse_param?.parse_ifthenelse_tag_cond p t}) ->
    syntp:
      (
            b: Prims.bool ->
            x:
              Mkparse_ifthenelse_param?.parse_ifthenelse_t p
                { b ==
                  Mkparse_ifthenelse_param?.parse_ifthenelse_tag_cond p
                    (FStar.Pervasives.dfst (Mkserialize_ifthenelse_param?.serialize_ifthenelse_synth_recip
                            s
                            x)) }
          -> pl:
            Mkparse_ifthenelse_param?.parse_ifthenelse_payload_t p b
              { pl ==
                FStar.Pervasives.dsnd (Mkserialize_ifthenelse_param?.serialize_ifthenelse_synth_recip
                      s
                      x) }) ->
    sp32:
      (b: Prims.bool
          -> LowParse.SLow.Base.serializer32 (Mkserialize_ifthenelse_param?.serialize_ifthenelse_payload_serializer
                  s
                  b))
  -> LowParse.SLow.Base.serializer32 (LowParse.Spec.IfThenElse.serialize_ifthenelse s)