val read0
      (#[FStar.Tactics.Typeclasses.tcresolve ()] _extra_t: Aux.extra_t)
      (x: t)
      (position: LPE.pos_t)
      (n: U64.t)
      (dst: B.buffer U8.t)
    : HST.Stack (B.buffer U8.t)
      (requires
        (fun h ->
            live x h /\ B.live h dst /\ B.loc_disjoint (footprint x) (B.loc_buffer dst) /\
            U64.v position == Seq.length (get_read x h) /\ B.length dst == U64.v n /\
            Seq.length (get_remaining x h) >= U64.v n))
      (ensures
        (fun h dst' h' ->
            let s = get_remaining x h in
            B.modifies ((B.loc_buffer dst) `B.loc_union` (perm_footprint x)) h h' /\
            (B.as_seq h' dst') `Seq.equal` (Seq.slice s 0 (U64.v n)) /\ live x h' /\ B.live h' dst /\
            B.live h' dst' /\
            ((B.loc_buffer dst) `B.loc_union` (footprint x)) `B.loc_includes` (B.loc_buffer dst') /\
            get_remaining x h' == Seq.slice s (U64.v n) (Seq.length s)))
let read0
    (#[FStar.Tactics.Typeclasses.tcresolve ()] _extra_t: Aux.extra_t)
    (x: t)
    (position: LPE.pos_t)
    (n: U64.t)
    (dst: B.buffer U8.t)
:   HST.Stack (B.buffer U8.t)
    (requires (fun h ->
      live x h /\
      B.live h dst /\
      B.loc_disjoint (footprint x) (B.loc_buffer dst) /\
      U64.v position == Seq.length (get_read x h) /\
      B.length dst == U64.v n /\
      Seq.length (get_remaining x h) >= U64.v n
    ))
    (ensures (fun h dst' h' ->
      let s = get_remaining x h in
      B.modifies (B.loc_buffer dst `B.loc_union` perm_footprint x) h h' /\
      B.as_seq h' dst' `Seq.equal` Seq.slice s 0 (U64.v n) /\
      live x h' /\
      B.live h' dst /\
      B.live h' dst' /\
      (B.loc_buffer dst `B.loc_union` footprint x) `B.loc_includes` B.loc_buffer dst' /\
      get_remaining x h' == Seq.slice s (U64.v n) (Seq.length s)
    ))
=
  let h0 = HST.get () in
  let dst = Aux.read x.Aux.base n dst in
  let h1 = HST.get () in
  x.Aux.position *= Ghost.hide (position `U64.add` n);
  let h2 = HST.get () in
  Aux.preserved x.Aux.base (B.loc_buffer x.Aux.position) h1 h2;
  assert (
      let s = get_remaining x h0 in
      live x h2 /\
      get_remaining x h2 `Seq.equal` Seq.slice s (U64.v n) (Seq.length s)
  );
  dst
val read0
      (#[FStar.Tactics.Typeclasses.tcresolve ()] _extra_t: Aux.extra_t)
      (x: t)
      (position: LPE.pos_t)
      (n: U64.t)
      (dst: B.buffer U8.t)
    : HST.Stack (B.buffer U8.t)
      (requires
        (fun h ->
            live x h /\ B.live h dst /\ B.loc_disjoint (footprint x) (B.loc_buffer dst) /\
            U64.v position == Seq.length (get_read x h) /\ B.length dst == U64.v n /\
            Seq.length (get_remaining x h) >= U64.v n))
      (ensures
        (fun h dst' h' ->
            let s = get_remaining x h in
            B.modifies ((B.loc_buffer dst) `B.loc_union` (perm_footprint x)) h h' /\
            (B.as_seq h' dst') `Seq.equal` (Seq.slice s 0 (U64.v n)) /\ live x h' /\ B.live h' dst /\
            B.live h' dst' /\
            ((B.loc_buffer dst) `B.loc_union` (footprint x)) `B.loc_includes` (B.loc_buffer dst') /\
            get_remaining x h' == Seq.slice s (U64.v n) (Seq.length s)))
let read0
      (#[FStar.Tactics.Typeclasses.tcresolve ()] _extra_t: Aux.extra_t)
      (x: t)
      (position: LPE.pos_t)
      (n: U64.t)
      (dst: B.buffer U8.t)
    : HST.Stack (B.buffer U8.t)
      (requires
        (fun h ->
            live x h /\ B.live h dst /\ B.loc_disjoint (footprint x) (B.loc_buffer dst) /\
            U64.v position == Seq.length (get_read x h) /\ B.length dst == U64.v n /\
            Seq.length (get_remaining x h) >= U64.v n))
      (ensures
        (fun h dst' h' ->
            let s = get_remaining x h in
            B.modifies ((B.loc_buffer dst) `B.loc_union` (perm_footprint x)) h h' /\
            (B.as_seq h' dst') `Seq.equal` (Seq.slice s 0 (U64.v n)) /\ live x h' /\ B.live h' dst /\
            B.live h' dst' /\
            ((B.loc_buffer dst) `B.loc_union` (footprint x)) `B.loc_includes` (B.loc_buffer dst') /\
            get_remaining x h' == Seq.slice s (U64.v n) (Seq.length s))) =
let h0 = HST.get () in
let dst = Aux.read x.Aux.base n dst in
let h1 = HST.get () in
x.Aux.position *= Ghost.hide (position `U64.add` n);
let h2 = HST.get () in
Aux.preserved x.Aux.base (B.loc_buffer x.Aux.position) h1 h2;
assert (let s = get_remaining x h0 in
    live x h2 /\ (get_remaining x h2) `Seq.equal` (Seq.slice s (U64.v n) (Seq.length s)));
dst
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.Base.extra_t EverParse3d.InputStream.Extern.t EverParse3d.ErrorCode.pos_t FStar.UInt64.t LowStar.Buffer.buffer FStar.UInt8.t Prims.unit Prims._assert Prims.l_and EverParse3d.InputStream.Extern.live FStar.Seq.Base.equal EverParse3d.InputStream.Extern.get_remaining FStar.Seq.Base.slice FStar.UInt64.v FStar.Seq.Base.length FStar.Seq.Base.seq EverParse3d.InputStream.Extern.Base.preserved EverParse3d.InputStream.Extern.Type.__proj__Mkinput_buffer__item__base LowStar.Monotonic.Buffer.loc_buffer FStar.Ghost.erased LowStar.Buffer.trivial_preorder EverParse3d.InputStream.Extern.Type.__proj__Mkinput_buffer__item__position FStar.Monotonic.HyperStack.mem FStar.HyperStack.ST.get LowStar.BufferOps.op_Star_Equals FStar.Ghost.hide FStar.UInt64.add EverParse3d.InputStream.Extern.Base.read LowStar.Monotonic.Buffer.live LowStar.Monotonic.Buffer.loc_disjoint EverParse3d.InputStream.Extern.footprint Prims.eq2 Prims.int Prims.l_or FStar.UInt.size FStar.UInt64.n Prims.b2t Prims.op_GreaterThanOrEqual EverParse3d.InputStream.Extern.get_read LowStar.Monotonic.Buffer.length LowStar.Monotonic.Buffer.modifies LowStar.Monotonic.Buffer.loc_union EverParse3d.InputStream.Extern.perm_footprint LowStar.Monotonic.Buffer.as_seq LowStar.Monotonic.Buffer.loc_includes
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))
    (ensures (B.loc_not_unused_in h `B.loc_includes` footprint x))
= Aux.live_not_unused_in x.Aux.base h

let get_all (x: t) : Ghost (Seq.seq U8.t)
    (requires True)
    (ensures (fun y -> Seq.length y == U64.v (len_all x)))
= Seq.slice (Aux.get_all x.Aux.base) 0 (U64.v (len_all x))

let get_remaining (x: t) (h: HS.mem) : Ghost (Seq.seq U8.t)
    (requires (live x h))
    (ensures (fun y -> Seq.length y <= U64.v (len_all x)))
= let r = U64.v (B.deref h x.Aux.position) in
  Seq.slice (get_all x) r (U64.v (len_all x))

let get_read (x: t) (h: HS.mem) : Ghost (Seq.seq U8.t)
    (requires (live x h))
    (ensures (fun y -> get_all x `Seq.equal` (y `Seq.append` get_remaining x h)))
= Aux.get_read x.Aux.base h

let preserved
    (x: t)
    (l: B.loc)
    (h: HS.mem)
    (h' : HS.mem)
:   Lemma
    (requires (live x h /\ B.modifies l h h' /\ B.loc_disjoint (footprint x) l))
    (ensures (
      live x h' /\
      get_remaining x h' == get_remaining x h /\
      get_read x h' == get_read x h
    ))
=
  Aux.preserved x.Aux.base l h h'

open LowStar.BufferOps

inline_for_extraction
noextract
let has
    (#[FStar.Tactics.Typeclasses.tcresolve ()] _extra_t: Aux.extra_t)
    (x: t)
    (_: unit)
    (position: LPE.pos_t)
    (n: U64.t)
:   HST.Stack bool
    (requires (fun h ->
      live x h /\
      U64.v position == Seq.length (get_read x h)
    ))
    (ensures (fun h res h' ->
      B.modifies B.loc_none h h' /\
      (res == true <==> Seq.length (get_remaining x h) >= U64.v n)
    ))
=
  if x.Aux.has_length
  then
    n `U64.lte` (x.Aux.length `U64.sub` position)
  else
    Aux.has x.Aux.base n

#push-options "--z3rlimit 64 --fuel 0 --ifuel 1 --z3cliopt smt.arith.nl=false --using_facts_from '* -FStar.Tactics -FStar.Reflection -FStar.Seq.Properties.slice_slice'"
#restart-solver
inline_for_extraction
noextract
let read0
    (#[FStar.Tactics.Typeclasses.tcresolve ()] _extra_t: Aux.extra_t)
    (x: t)
    (position: LPE.pos_t)
    (n: U64.t)
    (dst: B.buffer U8.t)
:   HST.Stack (B.buffer U8.t)
    (requires (fun h ->
      live x h /\
      B.live h dst /\
      B.loc_disjoint (footprint x) (B.loc_buffer dst) /\
      U64.v position == Seq.length (get_read x h) /\
      B.length dst == U64.v n /\
      Seq.length (get_remaining x h) >= U64.v n
    ))
    (ensures (fun h dst' h' ->
      let s = get_remaining x h in
      B.modifies (B.loc_buffer dst `B.loc_union` perm_footprint x) h h' /\
      B.as_seq h' dst' `Seq.equal` Seq.slice s 0 (U64.v n) /\
      live x h' /\
      B.live h' dst /\
      B.live h' dst' /\
      (B.loc_buffer dst `B.loc_union` footprint x) `B.loc_includes` B.loc_buffer dst' /\
      get_remaining x h' == Seq.slice s (U64.v n) (Seq.length s)
val read0
      (#[FStar.Tactics.Typeclasses.tcresolve ()] _extra_t: Aux.extra_t)
      (x: t)
      (position: LPE.pos_t)
      (n: U64.t)
      (dst: B.buffer U8.t)
    : HST.Stack (B.buffer U8.t)
      (requires
        (fun h ->
            live x h /\ B.live h dst /\ B.loc_disjoint (footprint x) (B.loc_buffer dst) /\
            U64.v position == Seq.length (get_read x h) /\ B.length dst == U64.v n /\
            Seq.length (get_remaining x h) >= U64.v n))
      (ensures
        (fun h dst' h' ->
            let s = get_remaining x h in
            B.modifies ((B.loc_buffer dst) `B.loc_union` (perm_footprint x)) h h' /\
            (B.as_seq h' dst') `Seq.equal` (Seq.slice s 0 (U64.v n)) /\ live x h' /\ B.live h' dst /\
            B.live h' dst' /\
            ((B.loc_buffer dst) `B.loc_union` (footprint x)) `B.loc_includes` (B.loc_buffer dst') /\
            get_remaining x h' == Seq.slice s (U64.v n) (Seq.length s)))

    x: EverParse3d.InputStream.Extern.t ->
    position: EverParse3d.ErrorCode.pos_t ->
    n: FStar.UInt64.t ->
    dst: LowStar.Buffer.buffer FStar.UInt8.t
  -> FStar.HyperStack.ST.Stack (LowStar.Buffer.buffer FStar.UInt8.t)