val split (#inames: _)
          (#a:Type)
          (#p:pcm a)
          (r:ref a p)
          (v:erased a)
          (v0:erased a)
          (v1:erased a)
  : SteelGhost unit inames (pts_to r v)
               (fun _ -> pts_to r v0 `star` pts_to r v1)
               (requires fun _ ->
                 composable p v0 v1 /\
                 v == hide (op p v0 v1))
               (ensures fun _ _ _ -> True)
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 split (#inames: _)
          (#a:Type)
          (#p:pcm a)
          (r:ref a p)
          (v:erased a)
          (v0:erased a)
          (v1:erased a)
  : SteelGhost unit inames (pts_to r v)
               (fun _ -> pts_to r v0 `star` pts_to r v1)
               (requires fun _ ->
                 composable p v0 v1 /\
                 v == hide (op p v0 v1))
               (ensures fun _ _ _ -> True)
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 _ -> ())
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.ref FStar.Ghost.erased Steel.Effect.Atomic.rewrite_slprop Steel.Effect.Common.to_vprop Steel.Memory.star Steel.Memory.pts_to FStar.Ghost.reveal Steel.Effect.Common.star Steel.PCMReference.pts_to Steel.Memory.mem Prims.unit Steel.PCMReference.split' FStar.PCM.op Prims.squash FStar.PCM.composable
(*
   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)
val split (#inames: _)
          (#a:Type)
          (#p:pcm a)
          (r:ref a p)
          (v:erased a)
          (v0:erased a)
          (v1:erased a)
  : SteelGhost unit inames (pts_to r v)
               (fun _ -> pts_to r v0 `star` pts_to r v1)
               (requires fun _ ->
                 composable p v0 v1 /\
                 v == hide (op p v0 v1))
               (ensures fun _ _ _ -> True)

    r: Steel.Memory.ref a p ->
    v: FStar.Ghost.erased a ->
    v0: FStar.Ghost.erased a ->
    v1: FStar.Ghost.erased a
  -> Steel.Effect.Atomic.SteelGhost Prims.unit