val validate_ifthenelse
      (p: parse_ifthenelse_param)
      (vt: validator p.parse_ifthenelse_tag_parser)
      (test: test_ifthenelse_tag p)
      (vp: (b: bool -> Tot (validator (dsnd (p.parse_ifthenelse_payload_parser b)))))
    : Tot (validator (parse_ifthenelse p))
let validate_ifthenelse
  (p: parse_ifthenelse_param)
  (vt: validator p.parse_ifthenelse_tag_parser)
  (test: test_ifthenelse_tag p)
  (vp: (b: bool) -> Tot (validator (dsnd (p.parse_ifthenelse_payload_parser b))))
: Tot (validator (parse_ifthenelse p))
= fun #rrel #rel input pos ->
  let h = HST.get () in
  [@inline_let] let _ =
    Classical.move_requires (valid_ifthenelse_intro p h input) (uint64_to_uint32 pos);
    Classical.move_requires (valid_ifthenelse_elim p h input) (uint64_to_uint32 pos)
  in
  let pos_after_t = vt input pos in
  if is_error pos_after_t
  then pos_after_t
  else
    let b = test input (uint64_to_uint32 pos) in
    if b (* eta-expansion here *)
    then vp true input pos_after_t
    else vp false input pos_after_t
val validate_ifthenelse
      (p: parse_ifthenelse_param)
      (vt: validator p.parse_ifthenelse_tag_parser)
      (test: test_ifthenelse_tag p)
      (vp: (b: bool -> Tot (validator (dsnd (p.parse_ifthenelse_payload_parser b)))))
    : Tot (validator (parse_ifthenelse p))
let validate_ifthenelse
      (p: parse_ifthenelse_param)
      (vt: validator p.parse_ifthenelse_tag_parser)
      (test: test_ifthenelse_tag p)
      (vp: (b: bool -> Tot (validator (dsnd (p.parse_ifthenelse_payload_parser b)))))
    : Tot (validator (parse_ifthenelse p)) =
fun #rrel #rel input pos ->
  let h = HST.get () in
  [@@ inline_let ]let _ =
    Classical.move_requires (valid_ifthenelse_intro p h input) (uint64_to_uint32 pos);
    Classical.move_requires (valid_ifthenelse_elim p h input) (uint64_to_uint32 pos)
  in
  let pos_after_t = vt input pos in
  if is_error pos_after_t
  then pos_after_t
  else
    let b = test input (uint64_to_uint32 pos) in
    if b then vp true input pos_after_t else vp false input pos_after_t
LowParse.Low.IfThenElse.fst.checked
prims.fst.checked LowStar.Buffer.fst.checked LowParse.Spec.IfThenElse.fst.checked LowParse.Low.Combinators.fsti.checked FStar.UInt64.fsti.checked FStar.UInt32.fsti.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.IfThenElse.fst
LowParse.Spec.IfThenElse.parse_ifthenelse_param LowParse.Low.Base.validator LowParse.Spec.IfThenElse.__proj__Mkparse_ifthenelse_param__item__parse_ifthenelse_tag_kind 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.Low.IfThenElse.test_ifthenelse_tag Prims.bool Prims.__proj__Mkdtuple2__item___1 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 FStar.Pervasives.dsnd LowParse.Slice.srel LowParse.Bytes.byte LowParse.Slice.slice FStar.UInt64.t LowParse.Low.ErrorCode.is_error LowParse.Low.ErrorCode.uint64_to_uint32 Prims.unit FStar.Classical.move_requires FStar.UInt32.t LowParse.Low.Base.Spec.valid LowParse.Spec.IfThenElse.parse_ifthenelse_kind LowParse.Spec.IfThenElse.__proj__Mkparse_ifthenelse_param__item__parse_ifthenelse_t LowParse.Spec.IfThenElse.parse_ifthenelse Prims.l_and LowParse.Spec.IfThenElse.__proj__Mkparse_ifthenelse_param__item__parse_ifthenelse_tag_cond LowParse.Low.Base.Spec.contents LowParse.Low.Base.Spec.get_valid_pos LowParse.Low.Base.Spec.valid_content_pos LowParse.Spec.IfThenElse.__proj__Mkparse_ifthenelse_param__item__parse_ifthenelse_synth LowParse.Low.IfThenElse.valid_ifthenelse_elim LowParse.Low.IfThenElse.valid_ifthenelse_intro FStar.Monotonic.HyperStack.mem FStar.HyperStack.ST.get
module LowParse.Low.IfThenElse
include LowParse.Spec.IfThenElse
include LowParse.Low.Combinators

module U32 = FStar.UInt32
module HS = FStar.HyperStack
module HST = FStar.HyperStack.ST
module B = LowStar.Buffer
module Cast = FStar.Int.Cast
module U64 = FStar.UInt64

let valid_ifthenelse_intro
  (p: parse_ifthenelse_param)
  (h: HS.mem)
  (#rrel #rel: _)
  (sl: slice rrel rel)
  (pos: U32.t)
: Lemma
  (requires (
    valid p.parse_ifthenelse_tag_parser h sl pos /\ (
    let t = contents p.parse_ifthenelse_tag_parser h sl pos in
    let pos_after_t = get_valid_pos p.parse_ifthenelse_tag_parser h sl pos in
    let b = p.parse_ifthenelse_tag_cond t in
    valid (dsnd (p.parse_ifthenelse_payload_parser b)) h sl pos_after_t
  )))
  (ensures (
    valid p.parse_ifthenelse_tag_parser h sl pos /\ (
    let t = contents p.parse_ifthenelse_tag_parser h sl pos in
    let b = p.parse_ifthenelse_tag_cond t in
    let pos_after_t = get_valid_pos p.parse_ifthenelse_tag_parser h sl pos in
    valid (dsnd (p.parse_ifthenelse_payload_parser b)) h sl pos_after_t /\
    valid_content_pos
      (parse_ifthenelse p) h sl pos
      (p.parse_ifthenelse_synth
        t
        (contents (dsnd (p.parse_ifthenelse_payload_parser b)) h sl pos_after_t)
      )
      (get_valid_pos (dsnd (p.parse_ifthenelse_payload_parser b)) h sl pos_after_t)
  )))
= valid_facts (parse_ifthenelse p) h sl pos;
  valid_facts p.parse_ifthenelse_tag_parser h sl pos;
  let pos_after_t = get_valid_pos p.parse_ifthenelse_tag_parser h sl pos in
  let t = contents p.parse_ifthenelse_tag_parser h sl pos in
  let b = p.parse_ifthenelse_tag_cond t in
  valid_facts (dsnd (p.parse_ifthenelse_payload_parser b)) h sl pos_after_t;
  parse_ifthenelse_eq p (bytes_of_slice_from h sl pos)

let valid_ifthenelse_elim
  (p: parse_ifthenelse_param)
  (h: HS.mem)
  (#rrel #rel: _)
  (sl: slice rrel rel)
  (pos: U32.t)
: Lemma
  (requires (valid (parse_ifthenelse p) h sl pos))
  (ensures (
    valid p.parse_ifthenelse_tag_parser h sl pos /\ (
    let t = contents p.parse_ifthenelse_tag_parser h sl pos in
    let pos_after_t = get_valid_pos p.parse_ifthenelse_tag_parser h sl pos in
    let b = p.parse_ifthenelse_tag_cond t in
    valid (dsnd (p.parse_ifthenelse_payload_parser b)) h sl pos_after_t /\
    valid_content_pos
      (parse_ifthenelse p) h sl pos
      (p.parse_ifthenelse_synth
        t
        (contents (dsnd (p.parse_ifthenelse_payload_parser b)) h sl pos_after_t)
      )
      (get_valid_pos (dsnd (p.parse_ifthenelse_payload_parser b)) h sl pos_after_t)
  )))
= valid_facts (parse_ifthenelse p) h sl pos;
  parse_ifthenelse_eq p (bytes_of_slice_from h sl pos);
  valid_facts p.parse_ifthenelse_tag_parser h sl pos;
  let pos_after_t = get_valid_pos p.parse_ifthenelse_tag_parser h sl pos in
  let t = contents p.parse_ifthenelse_tag_parser h sl pos in
  let b = p.parse_ifthenelse_tag_cond t in
  valid_facts (dsnd (p.parse_ifthenelse_payload_parser b)) h sl pos_after_t

inline_for_extraction
type test_ifthenelse_tag
  (p: parse_ifthenelse_param)
= (#rrel: _) -> (#rel: _) ->
  (input: slice rrel rel) ->
  (pos: U32.t) ->
  HST.Stack bool
  (requires (fun h -> valid p.parse_ifthenelse_tag_parser h input pos))
  (ensures (fun h res h' ->
    B.modifies B.loc_none h h' /\
    res == p.parse_ifthenelse_tag_cond (contents p.parse_ifthenelse_tag_parser h input pos)
  ))

inline_for_extraction
let validate_ifthenelse
  (p: parse_ifthenelse_param)
  (vt: validator p.parse_ifthenelse_tag_parser)
  (test: test_ifthenelse_tag p)
  (vp: (b: bool) -> Tot (validator (dsnd (p.parse_ifthenelse_payload_parser b))))
val validate_ifthenelse
      (p: parse_ifthenelse_param)
      (vt: validator p.parse_ifthenelse_tag_parser)
      (test: test_ifthenelse_tag p)
      (vp: (b: bool -> Tot (validator (dsnd (p.parse_ifthenelse_payload_parser b)))))
    : Tot (validator (parse_ifthenelse p))

    p: LowParse.Spec.IfThenElse.parse_ifthenelse_param ->
    vt: LowParse.Low.Base.validator (Mkparse_ifthenelse_param?.parse_ifthenelse_tag_parser p) ->
    test: LowParse.Low.IfThenElse.test_ifthenelse_tag p ->
    vp:
      (b: Prims.bool
          -> LowParse.Low.Base.validator (FStar.Pervasives.dsnd (Mkparse_ifthenelse_param?.parse_ifthenelse_payload_parser
                      p
                      b)))
  -> LowParse.Low.Base.validator (LowParse.Spec.IfThenElse.parse_ifthenelse p)