val slice_length (#len: U32.t) (x: input_buffer_t len) : Tot (v: U32.t{v == (slice_of x).LPL.len})
val slice_length (#len: U32.t) (x: input_buffer_t len) : Tot (v: U32.t{v == (slice_of x).LPL.len})
let slice_length (#len: U32.t) (x: input_buffer_t len) : Tot (v: U32.t { v == (slice_of x).LPL.len }) =
  len
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
/
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
x: EverParse3d.InputBuffer.input_buffer_t len
  -> v: FStar.UInt32.t{v == Mkslice?.len (EverParse3d.InputBuffer.slice_of x)}
FStar.UInt32.t EverParse3d.InputBuffer.input_buffer_t Prims.eq2 LowParse.Slice.__proj__Mkslice__item__len EverParse3d.InputBuffer.triv EverParse3d.InputBuffer.slice_of
let slice_length (#len: U32.t) (x: input_buffer_t len) : Tot (v: U32.t{v == (slice_of x).LPL.len}) =
  
len