val live (x: t) (m: HS.mem) : Tot prop
let live
  (x: t)
  (m: HS.mem)
: Tot prop
= let read = U64.v (B.deref m x.Aux.position) in
  Aux.live x.Aux.base m /\
  B.live m x.Aux.position /\
  read <= U64.v (len_all x) /\
  read == Seq.length (Aux.get_read x.Aux.base m)
val live (x: t) (m: HS.mem) : Tot prop
let live (x: t) (m: HS.mem) : Tot prop =
let read = U64.v (B.deref m x.Aux.position) in
Aux.live x.Aux.base m /\ B.live m x.Aux.position /\ read <= U64.v (len_all x) /\
read == Seq.length (Aux.get_read x.Aux.base m)
EverParse3d.InputStream.Extern.fst.checked
prims.fst.checked LowStar.BufferOps.fst.checked LowStar.Buffer.fst.checked LowParse.Low.Base.fst.checked FStar.UInt8.fsti.checked FStar.UInt64.fsti.checked FStar.UInt32.fsti.checked FStar.Tactics.Typeclasses.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Ghost.fsti.checked EverParse3d.InputStream.Extern.Type.fst.checked EverParse3d.ErrorCode.fst.checked
EverParse3d.InputStream.Extern.fst
EverParse3d.InputStream.Extern.t FStar.Monotonic.HyperStack.mem Prims.l_and EverParse3d.InputStream.Extern.Base.live EverParse3d.InputStream.Extern.Type.__proj__Mkinput_buffer__item__base LowStar.Monotonic.Buffer.live FStar.Ghost.erased EverParse3d.ErrorCode.pos_t LowStar.Buffer.trivial_preorder EverParse3d.InputStream.Extern.Type.__proj__Mkinput_buffer__item__position Prims.b2t Prims.op_LessThanOrEqual FStar.UInt64.v EverParse3d.InputStream.Extern.len_all Prims.eq2 Prims.int Prims.l_or FStar.UInt.size FStar.UInt64.n Prims.op_GreaterThanOrEqual FStar.Seq.Base.length FStar.UInt8.t EverParse3d.InputStream.Extern.Base.get_read FStar.UInt.uint_t FStar.Ghost.reveal LowStar.Monotonic.Buffer.deref Prims.prop
module EverParse3d.InputStream.Extern

module B = LowStar.Buffer
module HS = FStar.HyperStack
module HST = FStar.HyperStack.ST
module U32 = FStar.UInt32
module U8 = FStar.UInt8
module U64 = FStar.UInt64
module LPE = EverParse3d.ErrorCode

module Aux = EverParse3d.InputStream.Extern.Type

inline_for_extraction
noextract
let t = Aux.input_buffer

let len_all
  (x: t)
: GTot LPE.pos_t
= if x.Aux.has_length
  then x.Aux.length
  else Aux.len_all x.Aux.base

let live
  (x: t)
  (m: HS.mem)
val live (x: t) (m: HS.mem) : Tot prop
x: EverParse3d.InputStream.Extern.t -> m: FStar.Monotonic.HyperStack.mem -> Prims.prop