val recall (#inames: _) (#a:Type u#1) (#pcm:pcm a)
           (fact:property a)
           (r:erased (ref a pcm))
           (v:erased a)
           (w:witnessed r fact)
  : SteelAtomicU (erased a) inames
          (pts_to r v)
          (fun v1 -> pts_to r v)
          (requires fun _ -> True)
          (ensures fun _ v1 _ -> fact v1 /\ compatible pcm v v1)
let recall #inames #a #pcm fact r v w =
  let v1 = recall' fact r v w in
  rewrite_slprop (to_vprop Mem.(pts_to r v `star` pure (fact v1)))
                 (pts_to r v `star` pure (fact v1))
                 (fun _ -> ());
  elim_pure (fact v1);
  v1
val recall (#inames: _) (#a:Type u#1) (#pcm:pcm a)
           (fact:property a)
           (r:erased (ref a pcm))
           (v:erased a)
           (w:witnessed r fact)
  : SteelAtomicU (erased a) inames
          (pts_to r v)
          (fun v1 -> pts_to r v)
          (requires fun _ -> True)
          (ensures fun _ v1 _ -> fact v1 /\ compatible pcm v v1)
let recall #inames #a #pcm fact r v w =
let v1 = recall' fact r v w in
rewrite_slprop (to_vprop Mem.((pts_to r v) `star` (pure (fact v1))))
  ((pts_to r v) `star` (pure (fact v1)))
  (fun _ -> ());
elim_pure (fact v1);
v1
Steel.PCMReference.fst.checked
Steel.Memory.fsti.checked prims.fst.checked FStar.Set.fsti.checked FStar.Pervasives.fsti.checked FStar.PCM.fst.checked
Steel.PCMReference.fst
Steel.Memory.inames FStar.PCM.pcm Steel.Memory.property FStar.Ghost.erased Steel.Memory.ref Steel.Memory.witnessed FStar.Ghost.reveal Prims.unit Steel.Effect.Atomic.elim_pure Steel.Effect.Atomic.rewrite_slprop Steel.Effect.Common.to_vprop Steel.Memory.star Steel.Memory.pts_to Steel.Memory.pure Steel.Effect.Common.star Steel.PCMReference.pts_to Steel.Effect.Common.pure Steel.Memory.mem FStar.PCM.compatible Steel.PCMReference.recall'
(*
   Copyright 2020 Microsoft Research

   Licensed under the Apache License, Version 2.0 (the "License");
   you may not use this file except in compliance with the License.
   You may obtain a copy of the License at

       http://www.apache.org/licenses/LICENSE-2.0

   Unless required by applicable law or agreed to in writing, software
   distributed under the License is distributed on an "AS IS" BASIS,
   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
   See the License for the specific language governing permissions and
   limitations under the License.
*)


module Steel.PCMReference

module Mem = Steel.Memory

let read r v0 = let v = as_action (sel_action FStar.Set.empty r v0) in v
let write r v0 v1 = as_action (upd_action FStar.Set.empty r v0 v1)

val alloc' (#a:Type)
           (#pcm:pcm a)
           (x:a)
  : Steel (ref a pcm)
          (to_vprop Mem.emp)
          (fun r -> pts_to r x)
          (requires fun _ -> compatible pcm x x /\ pcm.refine x)
          (ensures fun _ _ _ -> True)

let alloc' x = as_action (alloc_action FStar.Set.empty x)

let alloc #_ #pcm x = rewrite_slprop emp (to_vprop Mem.emp) (fun _ -> reveal_emp ());
              compatible_refl pcm x;
              alloc' x

let free r x = as_action (free_action FStar.Set.empty r x)

val split'
          (#inames: _)
          (#a:Type)
          (#p:pcm a)
          (r:ref a p)
          (v0:erased a)
          (v1:erased a{composable p v0 v1})
  : SteelGhostT unit inames (pts_to r (op p v0 v1))
                (fun _ -> to_vprop Mem.(pts_to r v0 `star` pts_to r v1))

let split' #inames #a #p r v0 v1 = as_atomic_action_ghost (split_action inames r v0 v1)

let split #_ #a #p r v v0 v1 =
  let _:squash (composable p v0 v1) = () in
  rewrite_slprop (pts_to r v) (pts_to r (op p v0 v1)) (fun _ -> ());
  split' r v0 v1;
  rewrite_slprop (to_vprop Mem.(pts_to r v0 `star` pts_to r v1))
                 (pts_to r v0 `star` pts_to r v1)
                 (fun _ -> ())

val gather'
           (#inames: _)
           (#a:Type)
           (#p:FStar.PCM.pcm a)
           (r:ref a p)
           (v0:erased a)
           (v1:erased a)
  : SteelGhostT (_:unit{composable p v0 v1}) inames
           (to_vprop Mem.(pts_to r v0 `star` pts_to r v1))
           (fun _ -> pts_to r (op p v0 v1))

let gather' #inames r v0 v1 = as_atomic_action_ghost (gather_action inames r v0 v1)

let gather r v0 v1 =
  rewrite_slprop (pts_to r v0 `star` pts_to r v1)
                 (to_vprop Mem.(pts_to r v0 `star` pts_to r v1))
                 (fun _ -> ());
  gather' r v0 v1

val witness' (#inames: _) (#a:Type) (#pcm:pcm a)
            (r:erased (ref a pcm))
            (fact:stable_property pcm)
            (v:erased a)
            (_:fact_valid_compat fact v)
  : SteelAtomicUT (witnessed r fact) inames (pts_to r v)
                  (fun _ -> to_vprop Mem.(pts_to r v))

let witness' #inames r fact v _ = as_atomic_unobservable_action (Steel.Memory.witness inames r fact v ())

let witness r fact v s =
  let w = witness' r fact v s in
  w
  
val recall' (#inames: _) (#a:Type u#1) (#pcm:pcm a) (fact:property a)
           (r:erased (ref a pcm))
           (v:erased a)
           (w:witnessed r fact)
  : SteelAtomicUT (v1:erased a{compatible pcm v v1}) inames
           (to_vprop Mem.(pts_to r v))
           (fun v1 -> to_vprop Mem.(pts_to r v `star` pure (fact v1)))

let recall' #inames #a #pcm fact r v w = as_atomic_unobservable_action (Steel.Memory.recall #a #pcm #fact inames r v w)
val recall (#inames: _) (#a:Type u#1) (#pcm:pcm a)
           (fact:property a)
           (r:erased (ref a pcm))
           (v:erased a)
           (w:witnessed r fact)
  : SteelAtomicU (erased a) inames
          (pts_to r v)
          (fun v1 -> pts_to r v)
          (requires fun _ -> True)
          (ensures fun _ v1 _ -> fact v1 /\ compatible pcm v v1)

    fact: Steel.Memory.property a ->
    r: FStar.Ghost.erased (Steel.Memory.ref a pcm) ->
    v: FStar.Ghost.erased a ->
    w: Steel.Memory.witnessed (FStar.Ghost.reveal r) fact
  -> Steel.Effect.Atomic.SteelAtomicU (FStar.Ghost.erased a)