val live_not_unused_in (x: t) (h: HS.mem)
    : Lemma (requires (live x h)) (ensures ((B.loc_not_unused_in h) `B.loc_includes` (footprint x)))
let live_not_unused_in
    (x: t)
    (h: HS.mem)
:   Lemma
    (requires (live x h))
    (ensures (B.loc_not_unused_in h `B.loc_includes` footprint x))
= Aux.live_not_unused_in x.Aux.base h
val live_not_unused_in (x: t) (h: HS.mem)
    : Lemma (requires (live x h)) (ensures ((B.loc_not_unused_in h) `B.loc_includes` (footprint x)))
let live_not_unused_in (x: t) (h: HS.mem)
    : Lemma (requires (live x h)) (ensures ((B.loc_not_unused_in h) `B.loc_includes` (footprint x))) =
Aux.live_not_unused_in x.Aux.base h
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 EverParse3d.InputStream.Extern.Base.live_not_unused_in EverParse3d.InputStream.Extern.Type.__proj__Mkinput_buffer__item__base Prims.unit EverParse3d.InputStream.Extern.live Prims.squash LowStar.Monotonic.Buffer.loc_includes LowStar.Monotonic.Buffer.loc_not_unused_in EverParse3d.InputStream.Extern.footprint Prims.Nil FStar.Pervasives.pattern
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)
  (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

let perm_footprint
  (x: t)
: Ghost B.loc
  (requires True)
  (ensures (fun y -> footprint x `B.loc_includes` y))
= footprint x

let live_not_unused_in
    (x: t)
    (h: HS.mem)
:   Lemma
    (requires (live x h))
val live_not_unused_in (x: t) (h: HS.mem)
    : Lemma (requires (live x h)) (ensures ((B.loc_not_unused_in h) `B.loc_includes` (footprint x)))
x: EverParse3d.InputStream.Extern.t -> h: FStar.Monotonic.HyperStack.mem
  -> FStar.Pervasives.Lemma (requires EverParse3d.InputStream.Extern.live x h)
      (ensures
        LowStar.Monotonic.Buffer.loc_includes (LowStar.Monotonic.Buffer.loc_not_unused_in h)
          (EverParse3d.InputStream.Extern.footprint x))