val valid_equiv
  (#rrel #rel: _)
  (#k: parser_kind)
  (#t: Type)
  (p: parser k t)
  (h: HS.mem)
  (s: slice rrel rel)
  (pos: U32.t)
: Lemma
  (valid p h s pos <==> valid' p h s pos)
let valid_equiv
  (#rrel #rel: _)
  (#k: parser_kind)
  (#t: Type)
  (p: parser k t)
  (h: HS.mem)
  (s: slice rrel rel)
  (pos: U32.t)
: Lemma
  (valid p h s pos <==> valid' p h s pos)
= assert_norm (valid p h s pos <==> valid' p h s pos)
val valid_equiv
  (#rrel #rel: _)
  (#k: parser_kind)
  (#t: Type)
  (p: parser k t)
  (h: HS.mem)
  (s: slice rrel rel)
  (pos: U32.t)
: Lemma
  (valid p h s pos <==> valid' p h s pos)
let valid_equiv
      (#rrel #rel: _)
      (#k: parser_kind)
      (#t: Type)
      (p: parser k t)
      (h: HS.mem)
      (s: slice rrel rel)
      (pos: U32.t)
    : Lemma (valid p h s pos <==> valid' p h s pos) =
assert_norm (valid p h s pos <==> valid' p h s pos)
LowParse.Low.Base.Spec.fst.checked
prims.fst.checked LowStar.Monotonic.Buffer.fsti.checked LowParse.Math.fst.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Classical.fsti.checked
LowParse.Low.Base.Spec.fst
LowParse.Slice.srel LowParse.Bytes.byte LowParse.Spec.Base.parser_kind LowParse.Spec.Base.parser FStar.Monotonic.HyperStack.mem LowParse.Slice.slice FStar.UInt32.t FStar.Pervasives.assert_norm Prims.l_iff LowParse.Low.Base.Spec.valid LowParse.Low.Base.Spec.valid' Prims.unit Prims.l_True Prims.squash Prims.Nil FStar.Pervasives.pattern
module LowParse.Low.Base.Spec

module M = LowParse.Math
module B = LowStar.Monotonic.Buffer
module U32 = FStar.UInt32
module HS = FStar.HyperStack
module HST = FStar.HyperStack.ST
module Seq = FStar.Seq

let valid
  (#rrel #rel: _)
  (#k: parser_kind)
  (#t: Type)
  (p: parser k t)
  (h: HS.mem)
  (s: slice rrel rel)
  (pos: U32.t)
: GTot Type0
= valid' p h s pos

let valid_equiv
  (#rrel #rel: _)
  (#k: parser_kind)
  (#t: Type)
  (p: parser k t)
  (h: HS.mem)
  (s: slice rrel rel)
  (pos: U32.t)
: Lemma
val valid_equiv
  (#rrel #rel: _)
  (#k: parser_kind)
  (#t: Type)
  (p: parser k t)
  (h: HS.mem)
  (s: slice rrel rel)
  (pos: U32.t)
: Lemma
  (valid p h s pos <==> valid' p h s pos)

    p: LowParse.Spec.Base.parser k t ->
    h: FStar.Monotonic.HyperStack.mem ->
    s: LowParse.Slice.slice rrel rel ->
    pos: FStar.UInt32.t
  -> FStar.Pervasives.Lemma
    (ensures LowParse.Low.Base.Spec.valid p h s pos <==> LowParse.Low.Base.Spec.valid' p h s pos)