val hprop : l: FStar.Ghost.erased LowStar.Monotonic.Buffer.loc -> Type
let hprop (l:Ghost.erased B.loc) =
  p:(HS.mem -> Type) { frameable l p }
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

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
/
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 -> Type
FStar.Ghost.erased LowStar.Monotonic.Buffer.loc FStar.Monotonic.HyperStack.mem WithLocal.frameable
let hprop (l: Ghost.erased B.loc) =
  
p: (HS.mem -> Type){frameable l p}