val drop
  (#len: Ghost.erased U32.t)
  (sl: input_buffer_t len)
  (from: Ghost.erased U32.t)
  (to: Ghost.erased U32.t { U32.v from <= U32.v to /\ U32.v to <= U32.v (slice_of sl).LPL.len })
  (perm_of: R.perm (slice_of sl).base)
: HST.Stack unit
  (requires (fun h ->
    R.readable h perm_of from to
  ))
  (ensures (fun h _ h' ->
    B.modifies (R.loc_perm perm_of) h h' /\
    live_input_buffer h' sl perm_of /\
    R.preserved perm_of 0ul from h h' /\
    R.preserved perm_of to (B.len (slice_of sl).LPL.base) h h' /\
    R.unreadable h' perm_of from to
  ))
let drop #len base from to perm_of =
    R.drop #byte #base perm_of from to
val drop
  (#len: Ghost.erased U32.t)
  (sl: input_buffer_t len)
  (from: Ghost.erased U32.t)
  (to: Ghost.erased U32.t { U32.v from <= U32.v to /\ U32.v to <= U32.v (slice_of sl).LPL.len })
  (perm_of: R.perm (slice_of sl).base)
: HST.Stack unit
  (requires (fun h ->
    R.readable h perm_of from to
  ))
  (ensures (fun h _ h' ->
    B.modifies (R.loc_perm perm_of) h h' /\
    live_input_buffer h' sl perm_of /\
    R.preserved perm_of 0ul from h h' /\
    R.preserved perm_of to (B.len (slice_of sl).LPL.base) h h' /\
    R.unreadable h' perm_of from to
  ))
let drop #len base from to perm_of =
R.drop #byte #base perm_of from to
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.Ghost.erased FStar.UInt32.t EverParse3d.InputBuffer.input_buffer_t FStar.Ghost.reveal Prims.l_and Prims.b2t Prims.op_LessThanOrEqual FStar.UInt32.v LowParse.Slice.__proj__Mkslice__item__len EverParse3d.InputBuffer.triv EverParse3d.InputBuffer.slice_of EverParse3d.Readable.perm LowParse.Bytes.byte LowParse.Slice.__proj__Mkslice__item__base EverParse3d.Readable.drop Prims.unit
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

let input_buffer_t len =
  (base: B.buffer LPL.byte { U32.v len <= B.length base })

let slice_of #len x =
  { LPL.base = x; LPL.len = len }
val drop
  (#len: Ghost.erased U32.t)
  (sl: input_buffer_t len)
  (from: Ghost.erased U32.t)
  (to: Ghost.erased U32.t { U32.v from <= U32.v to /\ U32.v to <= U32.v (slice_of sl).LPL.len })
  (perm_of: R.perm (slice_of sl).base)
: HST.Stack unit
  (requires (fun h ->
    R.readable h perm_of from to
  ))
  (ensures (fun h _ h' ->
    B.modifies (R.loc_perm perm_of) h h' /\
    live_input_buffer h' sl perm_of /\
    R.preserved perm_of 0ul from h h' /\
    R.preserved perm_of to (B.len (slice_of sl).LPL.base) h h' /\
    R.unreadable h' perm_of from to
  ))

    sl: EverParse3d.InputBuffer.input_buffer_t (FStar.Ghost.reveal len) ->
    from: FStar.Ghost.erased FStar.UInt32.t ->
    to:
      FStar.Ghost.erased FStar.UInt32.t
        { FStar.UInt32.v (FStar.Ghost.reveal from) <= FStar.UInt32.v (FStar.Ghost.reveal to) /\
          FStar.UInt32.v (FStar.Ghost.reveal to) <=
          FStar.UInt32.v (Mkslice?.len (EverParse3d.InputBuffer.slice_of sl)) } ->
    perm_of: EverParse3d.Readable.perm (Mkslice?.base (EverParse3d.InputBuffer.slice_of sl))
  -> FStar.HyperStack.ST.Stack Prims.unit