val with_local
      (#a #b: Type)
      (#l1 #l2: _)
      (#req: hprop l1)
      (#ens: hpost l2)
      (init: b)
      (f: stl a init l1 l2 req ens)
    : ST a
      (requires fun h -> B.loc_includes (B.loc_not_unused_in h) l1 /\ req h)
      (ensures fun h0 x h1 -> B.modifies (l2 x) h0 h1 /\ ens h0 x h1)
val with_local
      (#a #b: Type)
      (#l1 #l2: _)
      (#req: hprop l1)
      (#ens: hpost l2)
      (init: b)
      (f: stl a init l1 l2 req ens)
    : ST a
      (requires fun h -> B.loc_includes (B.loc_not_unused_in h) l1 /\ req h)
      (ensures fun h0 x h1 -> B.modifies (l2 x) h0 h1 /\ ens h0 x h1)
let with_local
      (#a:Type)
      (#b:Type)
      (#l1:_)
      (#l2:_)
      (#req: hprop l1)
      (#ens: hpost l2)
      (init:b)
      (f: stl a init l1 l2 req ens)
  : ST a
    (requires fun h ->
       B.loc_includes (B.loc_not_unused_in h) l1 /\
       req h)
    (ensures fun h0 x h1 ->
       B.modifies (l2 x) h0 h1 /\
       ens h0 x h1)
  = let h = get () in
    B.loc_unused_in_not_unused_in_disjoint h;
    let fresh = B.malloc HS.root init 1ul in
    let h1 = get () in
    let res = f h fresh in
    let h2 = get () in
    let _ = B.free fresh in
    let h3 = get () in
    B.modifies_remove_new_locs (B.loc_addr_of_buffer fresh) (l2 res) (l2 res) h h1 h3;
    res
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

let hprop (l:Ghost.erased B.loc) =
  p:(HS.mem -> Type) { frameable l p }

let hpost (#a:Type) (l:a -> Ghost.erased B.loc) =
  p:(HS.mem -> a -> HS.mem -> Type) {
    forall h0 x. frameable (l x) (p h0 x)
  }

let stl (a:Type) #b (v:b) (l1:Ghost.erased B.loc) (l2: a -> Ghost.erased B.loc) (req:hprop l1) (ens:hpost l2) =
    hinit:HS.mem ->
    fresh:B.pointer b ->
    ST a
    (requires fun h ->
      B.modifies B.loc_none hinit h /\
      B.loc_disjoint (B.loc_addr_of_buffer fresh) l1 /\
      B.live h fresh /\
      B.get h fresh 0 == v /\
      req hinit)
    (ensures fun h0 x h1 ->
      B.live h1 fresh /\
      B.loc_disjoint (B.loc_addr_of_buffer fresh) (l2 x) /\
      B.modifies (B.loc_union (B.loc_buffer fresh) (l2 x)) h0 h1 /\
      ens hinit x 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
init: b -> f: WithLocal.stl a init l1 l2 req ens -> FStar.HyperStack.ST.ST a
FStar.Ghost.erased LowStar.Monotonic.Buffer.loc WithLocal.hprop WithLocal.hpost WithLocal.stl Prims.unit LowStar.Monotonic.Buffer.modifies_remove_new_locs LowStar.Monotonic.Buffer.loc_addr_of_buffer LowStar.Buffer.trivial_preorder FStar.Ghost.reveal FStar.Monotonic.HyperStack.mem FStar.HyperStack.ST.get LowStar.Monotonic.Buffer.free LowStar.Monotonic.Buffer.mbuffer Prims.l_and Prims.eq2 Prims.nat LowStar.Monotonic.Buffer.length FStar.UInt32.v FStar.UInt32.uint_to_t FStar.UInt32.t Prims.b2t Prims.op_Negation LowStar.Monotonic.Buffer.g_is_null FStar.Monotonic.HyperHeap.rid LowStar.Monotonic.Buffer.frameOf FStar.Monotonic.HyperHeap.root LowStar.Monotonic.Buffer.freeable LowStar.Buffer.malloc FStar.UInt32.__uint_to_t LowStar.Monotonic.Buffer.loc_unused_in_not_unused_in_disjoint LowStar.Monotonic.Buffer.loc_includes LowStar.Monotonic.Buffer.loc_not_unused_in LowStar.Monotonic.Buffer.modifies
let with_local
      (#a #b: Type)
      (#l1 #l2: _)
      (#req: hprop l1)
      (#ens: hpost l2)
      (init: b)
      (f: stl a init l1 l2 req ens)
    : ST a
      (requires fun h -> B.loc_includes (B.loc_not_unused_in h) l1 /\ req h)
      (ensures fun h0 x h1 -> B.modifies (l2 x) h0 h1 /\ ens h0 x h1) =
  
let h = get () in
B.loc_unused_in_not_unused_in_disjoint h;
let fresh = B.malloc HS.root init 1ul in
let h1 = get () in
let res = f h fresh in
let h2 = get () in
let _ = B.free fresh in
let h3 = get () in
B.modifies_remove_new_locs (B.loc_addr_of_buffer fresh) (l2 res) (l2 res) h h1 h3;
res