val footprint (x: t)
    : Ghost B.loc
      (requires True)
      (ensures (fun y -> B.address_liveness_insensitive_locs `B.loc_includes` y))
let footprint
  (x: t)
: Ghost B.loc
  (requires True)
  (ensures (fun y -> B.address_liveness_insensitive_locs `B.loc_includes` y))
= Aux.footprint x.Aux.base `B.loc_union` B.loc_buffer x.Aux.position
val footprint (x: t)
    : Ghost B.loc
      (requires True)
      (ensures (fun y -> B.address_liveness_insensitive_locs `B.loc_includes` y))
let footprint (x: t)
    : Ghost B.loc
      (requires True)
      (ensures (fun y -> B.address_liveness_insensitive_locs `B.loc_includes` y)) =
(Aux.footprint x.Aux.base) `B.loc_union` (B.loc_buffer x.Aux.position)
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 LowStar.Monotonic.Buffer.loc_union EverParse3d.InputStream.Extern.Base.footprint EverParse3d.InputStream.Extern.Type.__proj__Mkinput_buffer__item__base LowStar.Monotonic.Buffer.loc_buffer FStar.Ghost.erased EverParse3d.ErrorCode.pos_t LowStar.Buffer.trivial_preorder EverParse3d.InputStream.Extern.Type.__proj__Mkinput_buffer__item__position LowStar.Monotonic.Buffer.loc Prims.l_True LowStar.Monotonic.Buffer.loc_includes LowStar.Monotonic.Buffer.address_liveness_insensitive_locs
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)
: 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)

let footprint
  (x: t)
: Ghost B.loc
  (requires True)
val footprint (x: t)
    : Ghost B.loc
      (requires True)
      (ensures (fun y -> B.address_liveness_insensitive_locs `B.loc_includes` y))
x: EverParse3d.InputStream.Extern.t -> Prims.Ghost LowStar.Monotonic.Buffer.loc