val preserved
  (#t: _) (#b: B.buffer t) (p: perm b)
  (from: U32.t)
  (to: U32.t { U32.v from <= U32.v to /\ U32.v to <= B.length b })
  (h h' : HS.mem)
: Tot prop
let preserved #_ #b p from to h h' =
  (valid_perm h p /\ U32.v from <= U32.v to /\ U32.v to <= B.length b) ==>
  (valid_perm h' p /\ Seq.slice (B.deref h' p) (U32.v from) (U32.v to) `Seq.equal` Seq.slice (B.deref h p) (U32.v from) (U32.v to))
val preserved
  (#t: _) (#b: B.buffer t) (p: perm b)
  (from: U32.t)
  (to: U32.t { U32.v from <= U32.v to /\ U32.v to <= B.length b })
  (h h' : HS.mem)
: Tot prop
let preserved #_ #b p from to h h' =
(valid_perm h p /\ U32.v from <= U32.v to /\ U32.v to <= B.length b) ==>
(valid_perm h' p /\
  (Seq.slice (B.deref h' p) (U32.v from) (U32.v to))
  `Seq.equal`
  (Seq.slice (B.deref h p) (U32.v from) (U32.v to)))
EverParse3d.Readable.fst.checked
prims.fst.checked LowStar.BufferOps.fst.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Ghost.fsti.checked FStar.Classical.fsti.checked
EverParse3d.Readable.fst
LowStar.Buffer.buffer EverParse3d.Readable.perm FStar.UInt32.t Prims.l_and Prims.b2t Prims.op_LessThanOrEqual FStar.UInt32.v LowStar.Monotonic.Buffer.length LowStar.Buffer.trivial_preorder FStar.Monotonic.HyperStack.mem Prims.l_imp EverParse3d.Readable.valid_perm FStar.Seq.Base.equal Prims.bool FStar.Seq.Base.slice FStar.Ghost.reveal FStar.Seq.Base.seq LowStar.Monotonic.Buffer.deref FStar.Ghost.erased Prims.prop
module EverParse3d.Readable

let perm0 t = B.pointer (Ghost.erased (Seq.seq bool))

let perm_prop p b = B.loc_disjoint (B.loc_buffer b) (B.loc_buffer p) /\ True

let loc_perm p = B.loc_buffer p

let loc_perm_prop p = ()

let valid_perm h #_ #b p =
  B.live h b /\
  B.live h p /\
  Seq.length (B.deref h p) == B.length b

let valid_perm_prop h p = ()
val preserved
  (#t: _) (#b: B.buffer t) (p: perm b)
  (from: U32.t)
  (to: U32.t { U32.v from <= U32.v to /\ U32.v to <= B.length b })
  (h h' : HS.mem)
: Tot prop

    p: EverParse3d.Readable.perm b ->
    from: FStar.UInt32.t ->
    to:
      FStar.UInt32.t
        { FStar.UInt32.v from <= FStar.UInt32.v to /\
          FStar.UInt32.v to <= LowStar.Monotonic.Buffer.length b } ->
    h: FStar.Monotonic.HyperStack.mem ->
    h': FStar.Monotonic.HyperStack.mem
  -> Prims.prop