val valid_bounded_vlgen
      (vmin: der_length_t)
      (vmax: der_length_t{vmin <= vmax /\ vmax < 4294967296})
      (#sk: parser_kind)
      (pk: parser sk (bounded_int32 (vmin) (vmax)))
      (#k: parser_kind)
      (#t: Type)
      (#p: parser k t)
      (s: serializer p)
      (#rrel #rel: _)
      (input: slice rrel rel)
      (pos: U32.t)
      (h: HS.mem)
    : Lemma
      (requires
        (valid pk h input pos /\
          (let pos1 = get_valid_pos pk h input pos in
            let len = contents pk h input pos in
            U32.v pos1 + U32.v len < 4294967296 /\ valid_exact p h input pos1 (pos1 `U32.add` len)))
      )
      (ensures
        (valid pk h input pos /\
          (let pos1 = get_valid_pos pk h input pos in
            let len = contents pk h input pos in
            U32.v pos1 + U32.v len < 4294967296 /\ valid_exact p h input pos1 (pos1 `U32.add` len) /\
            (let x = contents_exact p h input pos1 (pos1 `U32.add` len) in
              Seq.length (serialize s x) == U32.v len /\
              valid_content_pos (parse_bounded_vlgen vmin vmax pk s)
                h
                input
                pos
                x
                (pos1 `U32.add` len)))))
let valid_bounded_vlgen
  (vmin: der_length_t)
  (vmax: der_length_t { vmin <= vmax /\ vmax < 4294967296 } )
  (#sk: parser_kind)
  (pk: parser sk (bounded_int32 (vmin) (vmax)))
  (#k: parser_kind)
  (#t: Type)
  (#p: parser k t)
  (s: serializer p)
  #rrel #rel
  (input: slice rrel rel)
  (pos: U32.t)
  (h: HS.mem)
: Lemma
  (requires (
    valid pk h input pos /\ (
    let pos1 = get_valid_pos pk h input pos in
    let len = contents pk h input pos in
    U32.v pos1 + U32.v len < 4294967296 /\
    valid_exact p h input pos1 (pos1 `U32.add` len)
  )))
  (ensures (
    valid pk h input pos /\ (
    let pos1 = get_valid_pos pk h input pos in
    let len = contents pk h input pos in
    U32.v pos1 + U32.v len < 4294967296 /\
    valid_exact p h input pos1 (pos1 `U32.add` len) /\ (
    let x = contents_exact p h input pos1 (pos1 `U32.add` len) in
    Seq.length (serialize s x) == U32.v len /\
    valid_content_pos (parse_bounded_vlgen vmin vmax pk s) h input pos x (pos1 `U32.add` len)
  ))))
= valid_facts (parse_bounded_vlgen (vmin) (vmax) pk s) h input pos;
  parse_bounded_vlgen_unfold (vmin) (vmax) pk s (bytes_of_slice_from h input pos);
  valid_facts pk h input pos;
  let pos1 = get_valid_pos pk h input pos in
  let len = contents pk h input pos in
  let pos2 = pos1 `U32.add` len in
  let x = contents_exact p h input pos1 pos2 in
  valid_fldata_gen p (U32.v len) input pos1 h;
  serialized_length_eq s x;
  valid_exact_serialize s h input pos1 pos2
val valid_bounded_vlgen
      (vmin: der_length_t)
      (vmax: der_length_t{vmin <= vmax /\ vmax < 4294967296})
      (#sk: parser_kind)
      (pk: parser sk (bounded_int32 (vmin) (vmax)))
      (#k: parser_kind)
      (#t: Type)
      (#p: parser k t)
      (s: serializer p)
      (#rrel #rel: _)
      (input: slice rrel rel)
      (pos: U32.t)
      (h: HS.mem)
    : Lemma
      (requires
        (valid pk h input pos /\
          (let pos1 = get_valid_pos pk h input pos in
            let len = contents pk h input pos in
            U32.v pos1 + U32.v len < 4294967296 /\ valid_exact p h input pos1 (pos1 `U32.add` len)))
      )
      (ensures
        (valid pk h input pos /\
          (let pos1 = get_valid_pos pk h input pos in
            let len = contents pk h input pos in
            U32.v pos1 + U32.v len < 4294967296 /\ valid_exact p h input pos1 (pos1 `U32.add` len) /\
            (let x = contents_exact p h input pos1 (pos1 `U32.add` len) in
              Seq.length (serialize s x) == U32.v len /\
              valid_content_pos (parse_bounded_vlgen vmin vmax pk s)
                h
                input
                pos
                x
                (pos1 `U32.add` len)))))
let valid_bounded_vlgen
      (vmin: der_length_t)
      (vmax: der_length_t{vmin <= vmax /\ vmax < 4294967296})
      (#sk: parser_kind)
      (pk: parser sk (bounded_int32 (vmin) (vmax)))
      (#k: parser_kind)
      (#t: Type)
      (#p: parser k t)
      (s: serializer p)
      #rrel
      #rel
      (input: slice rrel rel)
      (pos: U32.t)
      (h: HS.mem)
    : Lemma
      (requires
        (valid pk h input pos /\
          (let pos1 = get_valid_pos pk h input pos in
            let len = contents pk h input pos in
            U32.v pos1 + U32.v len < 4294967296 /\ valid_exact p h input pos1 (pos1 `U32.add` len)))
      )
      (ensures
        (valid pk h input pos /\
          (let pos1 = get_valid_pos pk h input pos in
            let len = contents pk h input pos in
            U32.v pos1 + U32.v len < 4294967296 /\ valid_exact p h input pos1 (pos1 `U32.add` len) /\
            (let x = contents_exact p h input pos1 (pos1 `U32.add` len) in
              Seq.length (serialize s x) == U32.v len /\
              valid_content_pos (parse_bounded_vlgen vmin vmax pk s)
                h
                input
                pos
                x
                (pos1 `U32.add` len))))) =
valid_facts (parse_bounded_vlgen (vmin) (vmax) pk s) h input pos;
parse_bounded_vlgen_unfold (vmin) (vmax) pk s (bytes_of_slice_from h input pos);
valid_facts pk h input pos;
let pos1 = get_valid_pos pk h input pos in
let len = contents pk h input pos in
let pos2 = pos1 `U32.add` len in
let x = contents_exact p h input pos1 pos2 in
valid_fldata_gen p (U32.v len) input pos1 h;
serialized_length_eq s x;
valid_exact_serialize s h input pos1 pos2
LowParse.Low.VLGen.fst.checked
prims.fst.checked LowStar.Buffer.fst.checked LowParse.Spec.VLGen.fst.checked LowParse.Low.VLData.fst.checked FStar.UInt64.fsti.checked FStar.UInt32.fsti.checked FStar.Seq.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.VLGen.fst
LowParse.Spec.DER.der_length_t Prims.l_and Prims.b2t Prims.op_LessThanOrEqual Prims.op_LessThan LowParse.Spec.Base.parser_kind LowParse.Spec.Base.parser LowParse.Spec.BoundedInt.bounded_int32 LowParse.Spec.Base.serializer LowParse.Slice.srel LowParse.Bytes.byte LowParse.Slice.slice FStar.UInt32.t FStar.Monotonic.HyperStack.mem LowParse.Low.Base.Spec.valid_exact_serialize Prims.unit LowParse.Low.Base.Spec.serialized_length_eq LowParse.Low.FLData.valid_fldata_gen FStar.UInt32.v LowParse.Low.Base.Spec.contents_exact FStar.UInt32.add LowParse.Low.Base.Spec.contents LowParse.Low.Base.Spec.get_valid_pos LowParse.Low.Base.Spec.valid_facts LowParse.Spec.VLGen.parse_bounded_vlgen_unfold LowParse.Slice.bytes_of_slice_from LowParse.Spec.VLGen.parse_bounded_vlgen_kind LowParse.Spec.VLData.parse_bounded_vldata_strong_t LowParse.Spec.VLGen.parse_bounded_vlgen LowParse.Low.Base.Spec.valid Prims.op_Addition LowParse.Low.Base.Spec.valid_exact Prims.squash Prims.eq2 Prims.int Prims.l_or Prims.op_GreaterThanOrEqual FStar.UInt.size FStar.UInt32.n FStar.Seq.Base.length LowParse.Spec.Base.serialize LowParse.Low.Base.Spec.valid_content_pos Prims.Nil FStar.Pervasives.pattern
module LowParse.Low.VLGen
include LowParse.Spec.VLGen
include LowParse.Low.VLData

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

#reset-options "--z3cliopt smt.arith.nl=false"

let valid_bounded_vlgen'
  (vmin: der_length_t)
  (vmax: der_length_t { vmin <= vmax /\ vmax < 4294967296 } )
  (#sk: parser_kind)
  (pk: parser sk (bounded_int32 (vmin) (vmax)))
  (#k: parser_kind)
  (#t: Type)
  (#p: parser k t)
  (s: serializer p)
  #rrel #rel
  (input: slice rrel rel)
  (pos: U32.t)
  (h: HS.mem)
: Lemma
  (requires (
    valid pk h input pos /\ (
    let pos1 = get_valid_pos pk h input pos in
    let len = contents pk h input pos in
    U32.v pos1 + U32.v len < 4294967296 /\
    valid (parse_fldata_strong s (U32.v len)) h input pos1
  )))
  (ensures (
    valid pk h input pos /\ (
    let pos1 = get_valid_pos pk h input pos in
    let len = contents pk h input pos in
    valid (parse_fldata_strong s (U32.v len)) h input pos1 /\ (
    let x = contents (parse_fldata_strong s (U32.v len)) h input pos1 in
    Seq.length (serialize s x) == U32.v len /\
    valid_content_pos (parse_bounded_vlgen vmin vmax pk s) h input pos x (pos1 `U32.add` len)
  ))))
= valid_facts (parse_bounded_vlgen (vmin) (vmax) pk s) h input pos;
  parse_bounded_vlgen_unfold_aux (vmin) (vmax) pk s (bytes_of_slice_from h input pos);
  valid_facts pk h input pos;
  let pos1 = get_valid_pos pk h input pos in
  let len = contents pk h input pos in
  valid_facts (parse_fldata_strong s (U32.v len)) h input pos1

let valid_bounded_vlgen
  (vmin: der_length_t)
  (vmax: der_length_t { vmin <= vmax /\ vmax < 4294967296 } )
  (#sk: parser_kind)
  (pk: parser sk (bounded_int32 (vmin) (vmax)))
  (#k: parser_kind)
  (#t: Type)
  (#p: parser k t)
  (s: serializer p)
  #rrel #rel
  (input: slice rrel rel)
  (pos: U32.t)
  (h: HS.mem)
: Lemma
  (requires (
    valid pk h input pos /\ (
    let pos1 = get_valid_pos pk h input pos in
    let len = contents pk h input pos in
    U32.v pos1 + U32.v len < 4294967296 /\
    valid_exact p h input pos1 (pos1 `U32.add` len)
  )))
  (ensures (
    valid pk h input pos /\ (
    let pos1 = get_valid_pos pk h input pos in
    let len = contents pk h input pos in
    U32.v pos1 + U32.v len < 4294967296 /\
    valid_exact p h input pos1 (pos1 `U32.add` len) /\ (
    let x = contents_exact p h input pos1 (pos1 `U32.add` len) in
    Seq.length (serialize s x) == U32.v len /\
    valid_content_pos (parse_bounded_vlgen vmin vmax pk s) h input pos x (pos1 `U32.add` len)
val valid_bounded_vlgen
      (vmin: der_length_t)
      (vmax: der_length_t{vmin <= vmax /\ vmax < 4294967296})
      (#sk: parser_kind)
      (pk: parser sk (bounded_int32 (vmin) (vmax)))
      (#k: parser_kind)
      (#t: Type)
      (#p: parser k t)
      (s: serializer p)
      (#rrel #rel: _)
      (input: slice rrel rel)
      (pos: U32.t)
      (h: HS.mem)
    : Lemma
      (requires
        (valid pk h input pos /\
          (let pos1 = get_valid_pos pk h input pos in
            let len = contents pk h input pos in
            U32.v pos1 + U32.v len < 4294967296 /\ valid_exact p h input pos1 (pos1 `U32.add` len)))
      )
      (ensures
        (valid pk h input pos /\
          (let pos1 = get_valid_pos pk h input pos in
            let len = contents pk h input pos in
            U32.v pos1 + U32.v len < 4294967296 /\ valid_exact p h input pos1 (pos1 `U32.add` len) /\
            (let x = contents_exact p h input pos1 (pos1 `U32.add` len) in
              Seq.length (serialize s x) == U32.v len /\
              valid_content_pos (parse_bounded_vlgen vmin vmax pk s)
                h
                input
                pos
                x
                (pos1 `U32.add` len)))))

    vmin: LowParse.Spec.DER.der_length_t ->
    vmax: LowParse.Spec.DER.der_length_t{vmin <= vmax /\ vmax < 4294967296} ->
    pk: LowParse.Spec.Base.parser sk (LowParse.Spec.BoundedInt.bounded_int32 vmin vmax) ->
    s: LowParse.Spec.Base.serializer p ->
    input: LowParse.Slice.slice rrel rel ->
    pos: FStar.UInt32.t ->
    h: FStar.Monotonic.HyperStack.mem
  -> FStar.Pervasives.Lemma
      (requires
        LowParse.Low.Base.Spec.valid pk h input pos /\
        (let pos1 = LowParse.Low.Base.Spec.get_valid_pos pk h input pos in
          let len = LowParse.Low.Base.Spec.contents pk h input pos in
          FStar.UInt32.v pos1 + FStar.UInt32.v len < 4294967296 /\
          LowParse.Low.Base.Spec.valid_exact p h input pos1 (FStar.UInt32.add pos1 len)))
      (ensures
        LowParse.Low.Base.Spec.valid pk h input pos /\
        (let pos1 = LowParse.Low.Base.Spec.get_valid_pos pk h input pos in
          let len = LowParse.Low.Base.Spec.contents pk h input pos in
          FStar.UInt32.v pos1 + FStar.UInt32.v len < 4294967296 /\
          LowParse.Low.Base.Spec.valid_exact p h input pos1 (FStar.UInt32.add pos1 len) /\
          (let x =
              LowParse.Low.Base.Spec.contents_exact p h input pos1 (FStar.UInt32.add pos1 len)
            in
            FStar.Seq.Base.length (LowParse.Spec.Base.serialize s x) == FStar.UInt32.v len /\
            LowParse.Low.Base.Spec.valid_content_pos (LowParse.Spec.VLGen.parse_bounded_vlgen vmin
                  vmax
                  pk
                  s)
              h
              input
              pos
              x
              (FStar.UInt32.add pos1 len))))