val make_input_buffer_with_length
      (base: t)
      (position: B.pointer (Ghost.erased LPE.pos_t))
      (length: LPE.pos_t)
    : HST.Stack input_buffer
      (requires
        (fun h ->
            B.loc_disjoint (footprint base) (B.loc_buffer position) /\ B.live h position /\
            U64.v length <= U64.v (len_all base)))
      (ensures (fun h _ h' -> B.modifies (B.loc_buffer position) h h'))
let make_input_buffer_with_length
  (base: t)
  (position: B.pointer (Ghost.erased LPE.pos_t))
  (length: LPE.pos_t)
: HST.Stack input_buffer
  (requires (fun h ->
    B.loc_disjoint (footprint base) (B.loc_buffer position) /\
    B.live h position /\
    U64.v length <= U64.v (len_all base)
  ))
  (ensures (fun h _ h' ->
    B.modifies (B.loc_buffer position) h h' 
  ))
= position *= 0uL;
  {
    base = base;
    has_length = true;
    length = length;
    position = position;
    prf = ();
  }
val make_input_buffer_with_length
      (base: t)
      (position: B.pointer (Ghost.erased LPE.pos_t))
      (length: LPE.pos_t)
    : HST.Stack input_buffer
      (requires
        (fun h ->
            B.loc_disjoint (footprint base) (B.loc_buffer position) /\ B.live h position /\
            U64.v length <= U64.v (len_all base)))
      (ensures (fun h _ h' -> B.modifies (B.loc_buffer position) h h'))
let make_input_buffer_with_length
      (base: t)
      (position: B.pointer (Ghost.erased LPE.pos_t))
      (length: LPE.pos_t)
    : HST.Stack input_buffer
      (requires
        (fun h ->
            B.loc_disjoint (footprint base) (B.loc_buffer position) /\ B.live h position /\
            U64.v length <= U64.v (len_all base)))
      (ensures (fun h _ h' -> B.modifies (B.loc_buffer position) h h')) =
position *= 0uL;
{ base = base; has_length = true; length = length; position = position; prf = () }
EverParse3d.InputStream.Extern.Type.fst.checked
prims.fst.checked LowStar.BufferOps.fst.checked LowStar.Buffer.fst.checked FStar.UInt8.fsti.checked FStar.UInt64.fsti.checked FStar.UInt32.fsti.checked FStar.Pervasives.fsti.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Ghost.fsti.checked EverParse3d.InputStream.Extern.Base.fsti.checked EverParse3d.ErrorCode.fst.checked
EverParse3d.InputStream.Extern.Type.fst
EverParse3d.InputStream.Extern.Base.t LowStar.Buffer.pointer FStar.Ghost.erased EverParse3d.ErrorCode.pos_t EverParse3d.InputStream.Extern.Type.Mkinput_buffer EverParse3d.InputStream.Extern.Type.input_buffer Prims.unit LowStar.BufferOps.op_Star_Equals LowStar.Buffer.trivial_preorder FStar.Ghost.hide FStar.UInt64.__uint_to_t FStar.Monotonic.HyperStack.mem Prims.l_and LowStar.Monotonic.Buffer.loc_disjoint EverParse3d.InputStream.Extern.Base.footprint LowStar.Monotonic.Buffer.loc_buffer LowStar.Monotonic.Buffer.live Prims.b2t Prims.op_LessThanOrEqual FStar.UInt64.v EverParse3d.InputStream.Extern.Base.len_all LowStar.Monotonic.Buffer.modifies
module EverParse3d.InputStream.Extern.Type
include EverParse3d.InputStream.Extern.Base

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

noeq
type input_buffer = {
  base: t;
  has_length: bool;
  length: LPE.pos_t;
  position: B.pointer (Ghost.erased LPE.pos_t);
  prf: squash (
    B.loc_disjoint (footprint base) (B.loc_buffer position) /\
    (has_length == true ==> U64.v length <= U64.v (len_all base))
  );
}

open LowStar.BufferOps

let make_input_buffer
  (base: t)
  (position: B.pointer (Ghost.erased LPE.pos_t))
: HST.Stack input_buffer
  (requires (fun h ->
    B.loc_disjoint (footprint base) (B.loc_buffer position) /\
    B.live h position
  ))
  (ensures (fun h _ h' ->
    B.modifies (B.loc_buffer position) h h' 
  ))
= position *= 0uL;
  {
    base = base;
    has_length = false;
    length = 0uL;
    position = position;
    prf = ();
  }

let make_input_buffer_with_length
  (base: t)
  (position: B.pointer (Ghost.erased LPE.pos_t))
  (length: LPE.pos_t)
: HST.Stack input_buffer
  (requires (fun h ->
    B.loc_disjoint (footprint base) (B.loc_buffer position) /\
    B.live h position /\
    U64.v length <= U64.v (len_all base)
  ))
  (ensures (fun h _ h' ->
    B.modifies (B.loc_buffer position) h h'
val make_input_buffer_with_length
      (base: t)
      (position: B.pointer (Ghost.erased LPE.pos_t))
      (length: LPE.pos_t)
    : HST.Stack input_buffer
      (requires
        (fun h ->
            B.loc_disjoint (footprint base) (B.loc_buffer position) /\ B.live h position /\
            U64.v length <= U64.v (len_all base)))
      (ensures (fun h _ h' -> B.modifies (B.loc_buffer position) h h'))

    base: EverParse3d.InputStream.Extern.Base.t ->
    position: LowStar.Buffer.pointer (FStar.Ghost.erased EverParse3d.ErrorCode.pos_t) ->
    length: EverParse3d.ErrorCode.pos_t
  -> FStar.HyperStack.ST.Stack EverParse3d.InputStream.Extern.Type.input_buffer