val frameable : l: FStar.Ghost.erased LowStar.Monotonic.Buffer.loc ->
    p: (_: FStar.Monotonic.HyperStack.mem -> Type0)
  -> Prims.logical
let frameable (l:Ghost.erased B.loc) (p:HS.mem -> Type) =
    forall h0 h1 l'.
      p h0 /\
      B.loc_disjoint l l' /\
      B.modifies l' h0 h1
      ==> p h1
module WithLocal
module B = LowStar.Buffer
module HS = FStar.HyperStack
open FStar.HyperStack.ST

let eloc = Ghost.erased B.loc

let loc_buf (x:B.pointer 'a)
  : Ghost.erased B.loc
  = B.loc_buffer x
/
prims.fst.checked LowStar.Buffer.fst.checked FStar.UInt32.fsti.checked FStar.Pervasives.fsti.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Ghost.fsti.checked
WithLocal.fst

    l: FStar.Ghost.erased LowStar.Monotonic.Buffer.loc ->
    p: (_: FStar.Monotonic.HyperStack.mem -> Type0)
  -> Prims.logical
FStar.Ghost.erased LowStar.Monotonic.Buffer.loc FStar.Monotonic.HyperStack.mem Prims.l_Forall Prims.l_imp Prims.l_and LowStar.Monotonic.Buffer.loc_disjoint FStar.Ghost.reveal LowStar.Monotonic.Buffer.modifies Prims.logical
let frameable (l: Ghost.erased B.loc) (p: (HS.mem -> Type)) =
  
forall h0 h1 l'. p h0 /\ B.loc_disjoint l l' /\ B.modifies l' h0 h1 ==> p h1