val input_buffer_t (len: U32.t) : Type0
let input_buffer_t len =
  (base: B.buffer LPL.byte { U32.v len <= B.length base })
val input_buffer_t (len: U32.t) : Type0
let input_buffer_t len =
(base: B.buffer LPL.byte {U32.v len <= B.length base})
EverParse3d.InputBuffer.fst.checked
prims.fst.checked LowStar.Buffer.fst.checked LowParse.Low.Base.fst.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.fst
FStar.UInt32.t LowStar.Buffer.buffer LowParse.Bytes.byte Prims.b2t Prims.op_LessThanOrEqual FStar.UInt32.v LowStar.Monotonic.Buffer.length LowStar.Buffer.trivial_preorder
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
module G = FStar.Ghost

open LowParse.Low.Base
val input_buffer_t (len: U32.t) : Type0
len: FStar.UInt32.t -> Type0