val pts_to_injective_eq (#a: Type)
                        (#opened:inames)
                        (#p0 #p1:perm)
                        (#v0 #v1: a)
                        (r: ref a)
  : STGhost unit opened
      (pts_to r p0 v0 `star` pts_to r p1 v1)
      (fun _ -> pts_to r p0 v0 `star` pts_to r p1 v0)
      (requires True)
      (ensures fun _ -> v0 == v1)
let pts_to_injective_eq
  #_ #_ #p0 #p1 #v0 #v1 r
= rewrite (pts_to r p0 v0) (RST.pts_to r.reveal p0 v0);
  rewrite (pts_to r p1 v1) (RST.pts_to r.reveal p1 v1);
  RST.pts_to_injective_eq #_ #_ #_ #_ #v0 #v1 r.reveal;
  rewrite (RST.pts_to r.reveal p0 v0) (pts_to r p0 v0);
  rewrite (RST.pts_to r.reveal p1 v0) (pts_to r p1 v0)
val pts_to_injective_eq (#a: Type)
                        (#opened:inames)
                        (#p0 #p1:perm)
                        (#v0 #v1: a)
                        (r: ref a)
  : STGhost unit opened
      (pts_to r p0 v0 `star` pts_to r p1 v1)
      (fun _ -> pts_to r p0 v0 `star` pts_to r p1 v0)
      (requires True)
      (ensures fun _ -> v0 == v1)
let pts_to_injective_eq #_ #_ #p0 #p1 #v0 #v1 r =
rewrite (pts_to r p0 v0) (RST.pts_to r.reveal p0 v0);
rewrite (pts_to r p1 v1) (RST.pts_to r.reveal p1 v1);
RST.pts_to_injective_eq #_ #_ #_ #_ #v0 #v1 r.reveal;
rewrite (RST.pts_to r.reveal p0 v0) (pts_to r p0 v0);
rewrite (RST.pts_to r.reveal p1 v0) (pts_to r p1 v0)
Steel.ST.GhostHigherReference.fst.checked
Steel.ST.HigherReference.fst.checked Steel.ST.Coercions.fsti.checked Steel.HigherReference.fsti.checked prims.fst.checked FStar.Pervasives.fsti.checked FStar.Ghost.fsti.checked
Steel.ST.GhostHigherReference.fst
Steel.Memory.inames Steel.FractionalPermission.perm Steel.ST.GhostHigherReference.ref Steel.ST.Util.rewrite Steel.ST.HigherReference.pts_to Steel.ST.GhostHigherReference.__proj__Hide__item__reveal Steel.ST.GhostHigherReference.pts_to Prims.unit Steel.ST.HigherReference.pts_to_injective_eq
module Steel.ST.GhostHigherReference

// needed because I need to know that `Steel.ST.HigherReference.ref a`
// can be turned into `Steel.HigherReference.ref a`
friend Steel.ST.HigherReference

module RST = Steel.ST.HigherReference
module R = Steel.HigherReference

module STC = Steel.ST.Coercions

// FIXME: WHY WHY WHY in `Ghost.reveal (ref a)` is `a` not strictly positive?

[@@erasable]
noeq
type ref' ([@@@strictly_positive] a : Type u#1) : Type0
= | Hide: (reveal: R.ref a) -> ref' a

let ref a = ref' a

let pts_to r p v = RST.pts_to r.reveal p v

let reveal_ref r = r.reveal

let hide_ref r = Hide r

let hide_reveal_ref r = ()

let reveal_pts_to r p x =
  equiv_refl (Steel.ST.HigherReference.pts_to (reveal_ref r) p x)

let pts_to_injective_eq
val pts_to_injective_eq (#a: Type)
                        (#opened:inames)
                        (#p0 #p1:perm)
                        (#v0 #v1: a)
                        (r: ref a)
  : STGhost unit opened
      (pts_to r p0 v0 `star` pts_to r p1 v1)
      (fun _ -> pts_to r p0 v0 `star` pts_to r p1 v0)
      (requires True)
      (ensures fun _ -> v0 == v1)
r: Steel.ST.GhostHigherReference.ref a -> Steel.ST.Effect.Ghost.STGhost Prims.unit