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_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))
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.Slice.srel LowParse.Bytes.byte LowParse.Slice.slice FStar.UInt32.t FStar.Monotonic.HyperStack.mem LowParse.Low.Base.Spec.valid Prims.op_Addition FStar.UInt32.v LowParse.Slice.__proj__Mkslice__item__len LowParse.Low.Base.Spec.valid_exact FStar.UInt32.add LowParse.Low.Base.Spec.contents LowParse.Low.Base.Spec.get_valid_pos Prims.logical
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)
val valid_deplen_decomp : 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) ->
    pp: LowParse.Spec.Base.parser pk pt ->
    input: LowParse.Slice.slice rrel rel ->
    pos: FStar.UInt32.t ->
    h: FStar.Monotonic.HyperStack.mem
  -> Prims.GTot Prims.logical

    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) ->
    pp: LowParse.Spec.Base.parser pk pt ->
    input: LowParse.Slice.slice rrel rel ->
    pos: FStar.UInt32.t ->
    h: FStar.Monotonic.HyperStack.mem
  -> Prims.GTot Prims.logical