val 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 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))))
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
val 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 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))))
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
  let input' = { base = input.base; len = pos_end } in
  valid_facts p h input' pos_begin
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
LowParse.Spec.Base.parser_kind LowParse.Spec.Base.parser FStar.Monotonic.HyperStack.mem LowParse.Slice.srel LowParse.Bytes.byte LowParse.Slice.slice FStar.UInt32.t Prims.op_AmpAmp Prims.op_LessThanOrEqual FStar.UInt32.v LowParse.Slice.__proj__Mkslice__item__len LowParse.Low.Base.Spec.valid_facts LowParse.Slice.Mkslice LowParse.Slice.__proj__Mkslice__item__base Prims.bool Prims.unit LowParse.Low.Base.Spec.valid_exact_equiv LowParse.Slice.live_slice Prims.squash Prims.l_iff LowParse.Low.Base.Spec.valid_exact Prims.l_and Prims.b2t LowParse.Low.Base.Spec.valid_pos 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
val 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 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))))

    p: LowParse.Spec.Base.parser k t ->
    h: FStar.Monotonic.HyperStack.mem ->
    input: LowParse.Slice.slice rrel rel ->
    pos_begin: FStar.UInt32.t ->
    pos_end: FStar.UInt32.t
  -> FStar.Pervasives.Lemma (requires LowParse.Slice.live_slice h input)
      (ensures
        LowParse.Low.Base.Spec.valid_exact p h input pos_begin pos_end <==>
        FStar.UInt32.v pos_begin <= FStar.UInt32.v pos_end /\
        FStar.UInt32.v pos_end <= FStar.UInt32.v (Mkslice?.len input) /\
        (let input' = LowParse.Slice.Mkslice (Mkslice?.base input) pos_end in
          LowParse.Low.Base.Spec.valid_pos p h input' pos_begin pos_end))