val intro_vptr0 (#opened: _) (#a: Type0) (r: ref a) (p: perm)
    : SteelGhost unit
      opened
      (A.varrayp r p)
      (fun _ -> vptr0 r p)
      (fun _ -> True)
      (fun h _ h' ->
          let s = A.aselp r p h in
          Seq.length s == 1 /\ h' (vptr0 r p) == Seq.index s 0)
let intro_vptr0
  (#opened: _)
  (#a: Type0)
  (r: ref a)
  (p: perm)
: SteelGhost unit opened
    (A.varrayp r p)
    (fun _ -> vptr0 r p)
    (fun _ -> True)
    (fun h _ h' ->
      let s = A.aselp r p h in
      Seq.length s == 1 /\
      h' (vptr0 r p) == Seq.index s 0
    )
= A.varrayp_not_null r p;
  intro_vrefine (A.varrayp r p) (vptr0_refine r);
  intro_vrewrite (A.varrayp r p `vrefine` vptr0_refine r) (vptr0_rewrite r p);
  change_equal_slprop (vptr1 r p) (vptr0 r p)
val intro_vptr0 (#opened: _) (#a: Type0) (r: ref a) (p: perm)
    : SteelGhost unit
      opened
      (A.varrayp r p)
      (fun _ -> vptr0 r p)
      (fun _ -> True)
      (fun h _ h' ->
          let s = A.aselp r p h in
          Seq.length s == 1 /\ h' (vptr0 r p) == Seq.index s 0)
let intro_vptr0 (#opened: _) (#a: Type0) (r: ref a) (p: perm)
    : SteelGhost unit
      opened
      (A.varrayp r p)
      (fun _ -> vptr0 r p)
      (fun _ -> True)
      (fun h _ h' ->
          let s = A.aselp r p h in
          Seq.length s == 1 /\ h' (vptr0 r p) == Seq.index s 0) =
A.varrayp_not_null r p;
intro_vrefine (A.varrayp r p) (vptr0_refine r);
intro_vrewrite ((A.varrayp r p) `vrefine` (vptr0_refine r)) (vptr0_rewrite r p);
change_equal_slprop (vptr1 r p) (vptr0 r p)
Steel.ArrayRef.fst.checked
Steel.Array.fsti.checked prims.fst.checked FStar.SizeT.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked
Steel.ArrayRef.fst
Steel.Memory.inames Steel.ArrayRef.ref Steel.FractionalPermission.perm Steel.Effect.Atomic.change_equal_slprop Steel.ArrayRef.vptr1 Steel.ArrayRef.vptr0 Prims.unit Steel.Effect.Atomic.intro_vrewrite Steel.Effect.Common.vrefine Steel.Array.varrayp Steel.ArrayRef.vptr0_refine Steel.ArrayRef.vptr0_rewrite Steel.Effect.Atomic.intro_vrefine Steel.Array.varrayp_not_null Steel.Effect.Common.vprop Steel.Effect.Common.rmem Prims.l_True Prims.l_and Prims.eq2 Prims.int FStar.Seq.Base.length FStar.Seq.Base.index FStar.Seq.Properties.lseq Steel.ST.Array.length Steel.Array.aselp
module Steel.ArrayRef

module A = Steel.Array

let null #a = A.null #a

let is_null r = A.is_null r

let vptr0_refine
  (#a: Type0)
  (r: ref a)
  (s: Seq.lseq a (A.length r))
: Tot prop
= Seq.length s == 1

let vptr0_rewrite
  (#a: Type)
  (r: ref a)
  (p: perm)
  (s: normal (vrefine_t (A.varrayp r p) (vptr0_refine r)))
: Tot a
= Seq.index s 0

[@@__steel_reduce__; __reduce__]
let vptr1
  (#a: Type0)
  (r: ref a)
  (p: perm)
: Tot vprop
= A.varrayp r p `vrefine`
  vptr0_refine r `vrewrite`
  vptr0_rewrite r p

[@@__steel_reduce__]
let vptr0
  (#a: Type0)
  (r: ref a)
  (p: perm)
: Tot vprop
= vptr1 r p

let intro_vptr0
  (#opened: _)
  (#a: Type0)
  (r: ref a)
  (p: perm)
: SteelGhost unit opened
    (A.varrayp r p)
    (fun _ -> vptr0 r p)
    (fun _ -> True)
    (fun h _ h' ->
      let s = A.aselp r p h in
      Seq.length s == 1 /\
      h' (vptr0 r p) == Seq.index s 0
val intro_vptr0 (#opened: _) (#a: Type0) (r: ref a) (p: perm)
    : SteelGhost unit
      opened
      (A.varrayp r p)
      (fun _ -> vptr0 r p)
      (fun _ -> True)
      (fun h _ h' ->
          let s = A.aselp r p h in
          Seq.length s == 1 /\ h' (vptr0 r p) == Seq.index s 0)
r: Steel.ArrayRef.ref a -> p: Steel.FractionalPermission.perm
  -> Steel.Effect.Atomic.SteelGhost Prims.unit