val stl : a: Type ->
    v: b ->
    l1: FStar.Ghost.erased LowStar.Monotonic.Buffer.loc ->
    l2: (_: a -> FStar.Ghost.erased LowStar.Monotonic.Buffer.loc) ->
    req: WithLocal.hprop l1 ->
    ens: WithLocal.hpost l2
  -> Type
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)
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)
  }
/
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

    a: Type ->
    v: b ->
    l1: FStar.Ghost.erased LowStar.Monotonic.Buffer.loc ->
    l2: (_: a -> FStar.Ghost.erased LowStar.Monotonic.Buffer.loc) ->
    req: WithLocal.hprop l1 ->
    ens: WithLocal.hpost l2
  -> Type
FStar.Ghost.erased LowStar.Monotonic.Buffer.loc WithLocal.hprop WithLocal.hpost FStar.Monotonic.HyperStack.mem LowStar.Buffer.pointer Prims.l_and LowStar.Monotonic.Buffer.modifies LowStar.Monotonic.Buffer.loc_none LowStar.Monotonic.Buffer.loc_disjoint LowStar.Monotonic.Buffer.loc_addr_of_buffer LowStar.Buffer.trivial_preorder FStar.Ghost.reveal LowStar.Monotonic.Buffer.live Prims.eq2 LowStar.Monotonic.Buffer.get LowStar.Monotonic.Buffer.loc_union LowStar.Monotonic.Buffer.loc_buffer
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)