val valid_perm (h: HS.mem) (#t: _) (#b: B.buffer t) (p: perm b) : GTot Type0
let valid_perm h #_ #b p =
  B.live h b /\
  B.live h p /\
  Seq.length (B.deref h p) == B.length b
val valid_perm (h: HS.mem) (#t: _) (#b: B.buffer t) (p: perm b) : GTot Type0
let valid_perm h #_ #b p =
B.live h b /\ B.live h p /\ Seq.length (B.deref h p) == B.length b
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
FStar.Monotonic.HyperStack.mem LowStar.Buffer.buffer EverParse3d.Readable.perm Prims.l_and LowStar.Monotonic.Buffer.live LowStar.Buffer.trivial_preorder FStar.Ghost.erased FStar.Seq.Base.seq Prims.bool Prims.eq2 Prims.nat FStar.Seq.Base.length FStar.Ghost.reveal LowStar.Monotonic.Buffer.deref LowStar.Monotonic.Buffer.length
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 = ()
val valid_perm (h: HS.mem) (#t: _) (#b: B.buffer t) (p: perm b) : GTot Type0
h: FStar.Monotonic.HyperStack.mem -> p: EverParse3d.Readable.perm b -> Prims.GTot Type0