val 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))))
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)
val 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))))
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)
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 FStar.Monotonic.HyperStack.mem LowParse.Slice.srel LowParse.Bytes.byte LowParse.Slice.slice FStar.UInt32.t LowParse.Spec.IfThenElse.parse_ifthenelse_eq LowParse.Slice.bytes_of_slice_from Prims.unit LowParse.Low.Base.Spec.valid_facts 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 Prims.bool LowParse.Spec.IfThenElse.__proj__Mkparse_ifthenelse_param__item__parse_ifthenelse_tag_cond LowParse.Spec.IfThenElse.__proj__Mkparse_ifthenelse_param__item__parse_ifthenelse_tag_t LowParse.Low.Base.Spec.contents LowParse.Spec.IfThenElse.__proj__Mkparse_ifthenelse_param__item__parse_ifthenelse_tag_kind LowParse.Spec.IfThenElse.__proj__Mkparse_ifthenelse_param__item__parse_ifthenelse_tag_parser LowParse.Low.Base.Spec.get_valid_pos 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.Low.Base.Spec.valid Prims.squash LowParse.Low.Base.Spec.valid_content_pos LowParse.Spec.IfThenElse.__proj__Mkparse_ifthenelse_param__item__parse_ifthenelse_synth Prims.Nil FStar.Pervasives.pattern
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)
val 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))))

    p: LowParse.Spec.IfThenElse.parse_ifthenelse_param ->
    h: FStar.Monotonic.HyperStack.mem ->
    sl: LowParse.Slice.slice rrel rel ->
    pos: FStar.UInt32.t
  -> FStar.Pervasives.Lemma
      (requires
        LowParse.Low.Base.Spec.valid (Mkparse_ifthenelse_param?.parse_ifthenelse_tag_parser p)
          h
          sl
          pos /\
        (let t =
            LowParse.Low.Base.Spec.contents (Mkparse_ifthenelse_param?.parse_ifthenelse_tag_parser p
              )
              h
              sl
              pos
          in
          let pos_after_t =
            LowParse.Low.Base.Spec.get_valid_pos (Mkparse_ifthenelse_param?.parse_ifthenelse_tag_parser
                  p)
              h
              sl
              pos
          in
          let b = Mkparse_ifthenelse_param?.parse_ifthenelse_tag_cond p t in
          LowParse.Low.Base.Spec.valid (FStar.Pervasives.dsnd (Mkparse_ifthenelse_param?.parse_ifthenelse_payload_parser
                    p
                    b))
            h
            sl
            pos_after_t))
      (ensures
        LowParse.Low.Base.Spec.valid (Mkparse_ifthenelse_param?.parse_ifthenelse_tag_parser p)
          h
          sl
          pos /\
        (let t =
            LowParse.Low.Base.Spec.contents (Mkparse_ifthenelse_param?.parse_ifthenelse_tag_parser p
              )
              h
              sl
              pos
          in
          let b = Mkparse_ifthenelse_param?.parse_ifthenelse_tag_cond p t in
          let pos_after_t =
            LowParse.Low.Base.Spec.get_valid_pos (Mkparse_ifthenelse_param?.parse_ifthenelse_tag_parser
                  p)
              h
              sl
              pos
          in
          LowParse.Low.Base.Spec.valid (FStar.Pervasives.dsnd (Mkparse_ifthenelse_param?.parse_ifthenelse_payload_parser
                    p
                    b))
            h
            sl
            pos_after_t /\
          LowParse.Low.Base.Spec.valid_content_pos (LowParse.Spec.IfThenElse.parse_ifthenelse p)
            h
            sl
            pos
            (Mkparse_ifthenelse_param?.parse_ifthenelse_synth p
                t
                (LowParse.Low.Base.Spec.contents (FStar.Pervasives.dsnd (Mkparse_ifthenelse_param?.parse_ifthenelse_payload_parser
                            p
                            b))
                    h
                    sl
                    pos_after_t))
            (LowParse.Low.Base.Spec.get_valid_pos (FStar.Pervasives.dsnd (Mkparse_ifthenelse_param?.parse_ifthenelse_payload_parser
                        p
                        b))
                h
                sl
                pos_after_t)))