val live_input_buffer
      (h: HS.mem)
      (#len: U32.t)
      (sl: input_buffer_t len)
      (perm_of: R.perm (slice_of sl).base)
    : GTot Type0
val live_input_buffer
      (h: HS.mem)
      (#len: U32.t)
      (sl: input_buffer_t len)
      (perm_of: R.perm (slice_of sl).base)
    : GTot Type0
let live_input_buffer
  (h: HS.mem)
  (#len: U32.t)
  (sl: input_buffer_t len)
  (perm_of: R.perm (slice_of sl).base)
: GTot Type0
= LPL.live_slice h (slice_of sl) /\
  R.valid_perm h perm_of
module EverParse3d.InputBuffer

module B = LowStar.Buffer
module HS = FStar.HyperStack
module HST = FStar.HyperStack.ST
module U32 = FStar.UInt32
module LPL = LowParse.Low.Base
module R = EverParse3d.Readable

inline_for_extraction
noextract
let triv = B.trivial_preorder LowParse.Bytes.byte

inline_for_extraction
noextract
val input_buffer_t (len: U32.t) : Type0

include LowParse.Low.Base

val slice_of (#len: U32.t) (x: input_buffer_t len) : GTot (sl: slice triv triv { sl.LPL.len == len })

inline_for_extraction
noextract
let slice_length (#len: U32.t) (x: input_buffer_t len) : Tot (v: U32.t { v == (slice_of x).LPL.len }) =
  len
/
prims.fst.checked LowStar.Buffer.fst.checked LowParse.Low.Base.fst.checked LowParse.Bytes.fsti.checked FStar.UInt32.fsti.checked FStar.Pervasives.fsti.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Ghost.fsti.checked EverParse3d.Readable.fsti.checked
EverParse3d.InputBuffer.fsti

    h: FStar.Monotonic.HyperStack.mem ->
    sl: EverParse3d.InputBuffer.input_buffer_t len ->
    perm_of: EverParse3d.Readable.perm (Mkslice?.base (EverParse3d.InputBuffer.slice_of sl))
  -> Prims.GTot Type0
FStar.Monotonic.HyperStack.mem FStar.UInt32.t EverParse3d.InputBuffer.input_buffer_t EverParse3d.Readable.perm LowParse.Bytes.byte LowParse.Slice.__proj__Mkslice__item__base EverParse3d.InputBuffer.triv EverParse3d.InputBuffer.slice_of Prims.l_and LowParse.Slice.live_slice EverParse3d.Readable.valid_perm
let live_input_buffer
      (h: HS.mem)
      (#len: U32.t)
      (sl: input_buffer_t len)
      (perm_of: R.perm (slice_of sl).base)
    : GTot Type0 =
  
LPL.live_slice h (slice_of sl) /\ R.valid_perm h perm_of