val valid_deplen_len
      (min: nat)
      (max: nat{min <= max /\ max < 4294967296})
      (#hk: parser_kind)
      (#ht: Type)
      (hp: parser hk ht)
      (dlf: (ht -> Tot (bounded_int32 min max)))
      (#pk: parser_kind)
      (#pt: Type)
      (#pp: parser pk pt)
      (ps: serializer pp)
      (#rrel #rel: _)
      (input: slice rrel rel)
      (pos: U32.t)
      (h: HS.mem)
    : Lemma
      (requires
        (valid (parse_deplen min max hp dlf ps) h input pos) /\
        (valid_deplen_decomp min max hp dlf pp input pos h))
      (ensures
        (let pos_payload = get_valid_pos hp h input pos in
          let len_payload = dlf (contents hp h input pos) in
          let input' = { base = input.base; len = (pos_payload `U32.add` len_payload) } in
          valid pp h input' pos_payload /\
          (let pos_end' = get_valid_pos pp h input' pos_payload in
            let pos_end = get_valid_pos (parse_deplen min max hp dlf ps) h input pos in
            pos_end == pos_end')))
let valid_deplen_len
  (min: nat)
  (max: nat { min <= max /\ max < 4294967296 } )
  (#hk: parser_kind)
  (#ht: Type)
  (hp: parser hk ht)
  (dlf: ht -> Tot (bounded_int32 min max) )
  (#pk: parser_kind)
  (#pt: Type)
  (#pp: parser pk pt)
  (ps: serializer pp)
  #rrel #rel
  (input: slice rrel rel)
  (pos: U32.t)
  (h: HS.mem)
: Lemma
  (requires (valid (parse_deplen min max hp dlf ps) h input pos) /\
            (valid_deplen_decomp min max hp dlf pp input pos h))
  (ensures (let pos_payload = get_valid_pos hp h input pos in
           let len_payload = dlf (contents hp h input pos) in
           let input' = { base = input.base; len = (pos_payload `U32.add` len_payload); } in
           valid pp h input' pos_payload /\
           (let pos_end' = get_valid_pos pp h input' pos_payload in
           let pos_end = get_valid_pos (parse_deplen min max hp dlf ps) h input pos in
           pos_end == pos_end')))
= valid_facts (parse_deplen min max hp dlf ps) h input pos;
  valid_facts hp h input pos;
  parse_deplen_unfold2 min max hp dlf ps (bytes_of_slice_from h input pos);
  if valid_dec hp h input pos then
  begin
    let pos_payload = get_valid_pos hp h input pos in
    let len = dlf (contents hp h input pos) in
    if U32.v pos_payload + U32.v len <= U32.v input.len then
    begin
      let pos_end = pos_payload `U32.add` len in
      valid_exact_equiv pp h input pos_payload pos_end;      
      valid_exact_valid_pos_equiv pp h input pos_payload pos_end;
      let input' = { base = input.base; len = pos_end; } in
      valid_pos_get_valid_pos pp h input' pos_payload pos_end
    end
  end
val valid_deplen_len
      (min: nat)
      (max: nat{min <= max /\ max < 4294967296})
      (#hk: parser_kind)
      (#ht: Type)
      (hp: parser hk ht)
      (dlf: (ht -> Tot (bounded_int32 min max)))
      (#pk: parser_kind)
      (#pt: Type)
      (#pp: parser pk pt)
      (ps: serializer pp)
      (#rrel #rel: _)
      (input: slice rrel rel)
      (pos: U32.t)
      (h: HS.mem)
    : Lemma
      (requires
        (valid (parse_deplen min max hp dlf ps) h input pos) /\
        (valid_deplen_decomp min max hp dlf pp input pos h))
      (ensures
        (let pos_payload = get_valid_pos hp h input pos in
          let len_payload = dlf (contents hp h input pos) in
          let input' = { base = input.base; len = (pos_payload `U32.add` len_payload) } in
          valid pp h input' pos_payload /\
          (let pos_end' = get_valid_pos pp h input' pos_payload in
            let pos_end = get_valid_pos (parse_deplen min max hp dlf ps) h input pos in
            pos_end == pos_end')))
let valid_deplen_len
      (min: nat)
      (max: nat{min <= max /\ max < 4294967296})
      (#hk: parser_kind)
      (#ht: Type)
      (hp: parser hk ht)
      (dlf: (ht -> Tot (bounded_int32 min max)))
      (#pk: parser_kind)
      (#pt: Type)
      (#pp: parser pk pt)
      (ps: serializer pp)
      #rrel
      #rel
      (input: slice rrel rel)
      (pos: U32.t)
      (h: HS.mem)
    : Lemma
      (requires
        (valid (parse_deplen min max hp dlf ps) h input pos) /\
        (valid_deplen_decomp min max hp dlf pp input pos h))
      (ensures
        (let pos_payload = get_valid_pos hp h input pos in
          let len_payload = dlf (contents hp h input pos) in
          let input' = { base = input.base; len = (pos_payload `U32.add` len_payload) } in
          valid pp h input' pos_payload /\
          (let pos_end' = get_valid_pos pp h input' pos_payload in
            let pos_end = get_valid_pos (parse_deplen min max hp dlf ps) h input pos in
            pos_end == pos_end'))) =
valid_facts (parse_deplen min max hp dlf ps) h input pos;
valid_facts hp h input pos;
parse_deplen_unfold2 min max hp dlf ps (bytes_of_slice_from h input pos);
if valid_dec hp h input pos
then
  let pos_payload = get_valid_pos hp h input pos in
  let len = dlf (contents hp h input pos) in
  if U32.v pos_payload + U32.v len <= U32.v input.len
  then
    let pos_end = pos_payload `U32.add` len in
    valid_exact_equiv pp h input pos_payload pos_end;
    valid_exact_valid_pos_equiv pp h input pos_payload pos_end;
    let input' = { base = input.base; len = pos_end } in
    valid_pos_get_valid_pos pp h input' pos_payload pos_end
LowParse.Low.DepLen.fst.checked
prims.fst.checked LowStar.Monotonic.Buffer.fsti.checked LowParse.Spec.DepLen.fst.checked LowParse.Low.Combinators.fsti.checked LowParse.Low.Base.fst.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
LowParse.Low.DepLen.fst
Prims.nat 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_dec Prims.op_Addition FStar.UInt32.v LowParse.Slice.__proj__Mkslice__item__len LowParse.Low.Base.Spec.valid_pos_get_valid_pos LowParse.Slice.Mkslice LowParse.Slice.__proj__Mkslice__item__base Prims.unit LowParse.Low.DepLen.valid_exact_valid_pos_equiv LowParse.Low.Base.Spec.valid_exact_equiv FStar.UInt32.add Prims.bool LowParse.Low.Base.Spec.contents LowParse.Low.Base.Spec.get_valid_pos LowParse.Spec.DepLen.parse_deplen_unfold2 LowParse.Slice.bytes_of_slice_from LowParse.Low.Base.Spec.valid_facts LowParse.Spec.DepLen.parse_deplen_kind LowParse.Spec.DepLen.parse_deplen_data_t LowParse.Spec.DepLen.parse_deplen LowParse.Low.Base.Spec.valid LowParse.Low.DepLen.valid_deplen_decomp Prims.squash Prims.eq2 Prims.Nil FStar.Pervasives.pattern
module LowParse.Low.DepLen
include LowParse.Spec.DepLen

include LowParse.Low.Base
include LowParse.Low.Combinators

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

let valid_exact_valid_pos_equiv
  (#k: parser_kind)
  (#t: Type)
  (p: parser k t)
  (h: HS.mem)
  #rrel #rel
  (input: slice rrel rel)
  (pos_begin: U32.t)
  (pos_end: U32.t)
: Lemma
  (requires live_slice h input)
  (ensures
    ((valid_exact p h input pos_begin pos_end)
    <==>
    (U32.v pos_begin <= U32.v pos_end /\
    U32.v pos_end <= U32.v input.len /\
    (let input' = { base = input.base; len = pos_end; } in
    valid_pos p h input' pos_begin pos_end))))
= valid_exact_equiv p h input pos_begin pos_end;
  if U32.v pos_begin <= U32.v pos_end && U32.v pos_end <= U32.v input.len then
  begin
    let input' = { base = input.base; len = pos_end; } in
    valid_facts p h input' pos_begin
  end

(* the validity lemma says it is equivalent to have a valid header followed by a valid payload and
   have a valid piece of deplen data *)

let valid_deplen_decomp
  (min: nat)
  (max: nat { min <= max /\ max < 4294967296 } )
  (#hk: parser_kind)
  (#ht: Type)
  (hp: parser hk ht)
  (dlf: ht -> Tot (bounded_int32 min max) )
  (#pk: parser_kind)
  (#pt: Type)
  (pp: parser pk pt)
  #rrel #rel
  (input: slice rrel rel)
  (pos: U32.t)
  (h: HS.mem)
= valid hp h input pos /\ 
    (let pos_payload = get_valid_pos hp h input pos in
    let len = dlf (contents hp h input pos) in
    U32.v pos_payload + U32.v len <= U32.v input.len /\ 
    valid_exact pp h input pos_payload (pos_payload `U32.add` len))

let valid_deplen
  (min: nat)
  (max: nat { min <= max /\ max < 4294967296 } )
  (#hk: parser_kind)
  (#ht: Type)
  (hp: parser hk ht)
  (dlf: ht -> Tot (bounded_int32 min max) )
  (#pk: parser_kind)
  (#pt: Type)
  (#pp: parser pk pt)
  (ps: serializer pp)
  #rrel #rel
  (input: slice rrel rel)
  (pos: U32.t)
  (h: HS.mem)
: Lemma
  (requires live_slice h input)
  (ensures 
    ((valid (parse_deplen min max hp dlf ps) h input pos)
    <==>
    (valid_deplen_decomp min max hp dlf pp input pos h)))
= valid_facts (parse_deplen min max hp dlf ps) h input pos;
  valid_facts hp h input pos;
  parse_deplen_unfold2 min max hp dlf ps (bytes_of_slice_from h input pos);
  if valid_dec hp h input pos then
  begin
    let pos_payload = get_valid_pos hp h input pos in
    let len = dlf (contents hp h input pos) in
    if U32.v pos_payload + U32.v len <= U32.v input.len then
    begin
      let pos_end = pos_payload `U32.add` len in
      valid_exact_equiv pp h input pos_payload pos_end;
      match parse pp (bytes_of_slice_from_to h input pos_payload pos_end) with
      | None -> ()
      | Some (_, consumed) -> if consumed = U32.v len then
        valid_exact_serialize ps h input pos_payload pos_end
    end
  end

let valid_deplen_len
  (min: nat)
  (max: nat { min <= max /\ max < 4294967296 } )
  (#hk: parser_kind)
  (#ht: Type)
  (hp: parser hk ht)
  (dlf: ht -> Tot (bounded_int32 min max) )
  (#pk: parser_kind)
  (#pt: Type)
  (#pp: parser pk pt)
  (ps: serializer pp)
  #rrel #rel
  (input: slice rrel rel)
  (pos: U32.t)
  (h: HS.mem)
: Lemma
  (requires (valid (parse_deplen min max hp dlf ps) h input pos) /\
            (valid_deplen_decomp min max hp dlf pp input pos h))
  (ensures (let pos_payload = get_valid_pos hp h input pos in
           let len_payload = dlf (contents hp h input pos) in
           let input' = { base = input.base; len = (pos_payload `U32.add` len_payload); } in
           valid pp h input' pos_payload /\
           (let pos_end' = get_valid_pos pp h input' pos_payload in
           let pos_end = get_valid_pos (parse_deplen min max hp dlf ps) h input pos in
val valid_deplen_len
      (min: nat)
      (max: nat{min <= max /\ max < 4294967296})
      (#hk: parser_kind)
      (#ht: Type)
      (hp: parser hk ht)
      (dlf: (ht -> Tot (bounded_int32 min max)))
      (#pk: parser_kind)
      (#pt: Type)
      (#pp: parser pk pt)
      (ps: serializer pp)
      (#rrel #rel: _)
      (input: slice rrel rel)
      (pos: U32.t)
      (h: HS.mem)
    : Lemma
      (requires
        (valid (parse_deplen min max hp dlf ps) h input pos) /\
        (valid_deplen_decomp min max hp dlf pp input pos h))
      (ensures
        (let pos_payload = get_valid_pos hp h input pos in
          let len_payload = dlf (contents hp h input pos) in
          let input' = { base = input.base; len = (pos_payload `U32.add` len_payload) } in
          valid pp h input' pos_payload /\
          (let pos_end' = get_valid_pos pp h input' pos_payload in
            let pos_end = get_valid_pos (parse_deplen min max hp dlf ps) h input pos in
            pos_end == pos_end')))

    min: Prims.nat ->
    max: Prims.nat{min <= max /\ max < 4294967296} ->
    hp: LowParse.Spec.Base.parser hk ht ->
    dlf: (_: ht -> LowParse.Spec.BoundedInt.bounded_int32 min max) ->
    ps: LowParse.Spec.Base.serializer pp ->
    input: LowParse.Slice.slice rrel rel ->
    pos: FStar.UInt32.t ->
    h: FStar.Monotonic.HyperStack.mem
  -> FStar.Pervasives.Lemma
      (requires
        LowParse.Low.Base.Spec.valid (LowParse.Spec.DepLen.parse_deplen min max hp dlf ps)
          h
          input
          pos /\ LowParse.Low.DepLen.valid_deplen_decomp min max hp dlf pp input pos h)
      (ensures
        (let pos_payload = LowParse.Low.Base.Spec.get_valid_pos hp h input pos in
          let len_payload = dlf (LowParse.Low.Base.Spec.contents hp h input pos) in
          let input' =
            LowParse.Slice.Mkslice (Mkslice?.base input) (FStar.UInt32.add pos_payload len_payload)
          in
          LowParse.Low.Base.Spec.valid pp h input' pos_payload /\
          (let pos_end' = LowParse.Low.Base.Spec.get_valid_pos pp h input' pos_payload in
            let pos_end =
              LowParse.Low.Base.Spec.get_valid_pos (LowParse.Spec.DepLen.parse_deplen min
                    max
                    hp
                    dlf
                    ps)
                h
                input
                pos
            in
            pos_end == pos_end')))