val intro_vptr (#opened: _) (#a: Type0) (r: ref a)
    : SteelGhost unit
      opened
      (A.varray r)
      (fun _ -> vptr r)
      (fun _ -> True)
      (fun h0 _ h1 -> A.asel r h0 == Seq.create 1 (sel r h1))
let intro_vptr (#opened: _)
  (#a: Type0)
  (r: ref a)
: SteelGhost unit opened
    (A.varray r)
    (fun _ -> vptr r)
    (fun _ -> True)
    (fun h0 _ h1 -> A.asel r h0 == Seq.create 1 (sel r h1))
  = intro_vptrp r full_perm
val intro_vptr (#opened: _) (#a: Type0) (r: ref a)
    : SteelGhost unit
      opened
      (A.varray r)
      (fun _ -> vptr r)
      (fun _ -> True)
      (fun h0 _ h1 -> A.asel r h0 == Seq.create 1 (sel r h1))
let intro_vptr (#opened: _) (#a: Type0) (r: ref a)
    : SteelGhost unit
      opened
      (A.varray r)
      (fun _ -> vptr r)
      (fun _ -> True)
      (fun h0 _ h1 -> A.asel r h0 == Seq.create 1 (sel r h1)) =
intro_vptrp r full_perm
Steel.ArrayRef.fsti.checked
Steel.Memory.fsti.checked Steel.FractionalPermission.fst.checked Steel.Effect.Common.fsti.checked Steel.Effect.Atomic.fsti.checked Steel.Effect.fsti.checked Steel.Array.fsti.checked prims.fst.checked FStar.Tactics.fst.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked
Steel.ArrayRef.fsti
Steel.Memory.inames Steel.ArrayRef.ref Steel.ArrayRef.intro_vptrp Steel.FractionalPermission.full_perm Prims.unit Steel.Array.varray Steel.ArrayRef.vptr Steel.Effect.Common.vprop Steel.Effect.Common.rmem Prims.l_True Prims.eq2 FStar.Seq.Base.seq Steel.Array.asel FStar.Seq.Base.create Steel.ArrayRef.sel
module Steel.ArrayRef

open Steel.FractionalPermission
open Steel.Memory
open Steel.Effect.Common
open Steel.Effect
open Steel.Effect.Atomic

module A = Steel.Array

(** This module provides the same interface as Steel.Reference, however, it builds on top
    of Steel.Array to enable the interoperation between arrays and references.
    Similarly to C, a reference is defined as an array of length 1 *)

/// An abstract datatype for references
inline_for_extraction
let ref (a : Type0) : Type0 = (r: A.array a { A.length r == 1 \/ r == A.null })

/// The null pointer
[@@ noextract_to "krml"]
inline_for_extraction
val null (#a:Type0) : ref a

/// Checking whether a pointer is null can be done in a decidable way
[@@ noextract_to "krml"]
inline_for_extraction
val is_null (#a:Type0) (r:ref a) : (b:bool{b <==> r == null})

/// An abstract separation logic predicate stating that reference [r] is valid in memory.

val ptrp (#a:Type0) (r:ref a) ([@@@smt_fallback] p: perm) : slprop u#1

[@@ __steel_reduce__; __reduce__]
unfold
let ptr (#a:Type0) (r:ref a) : slprop u#1 = ptrp r full_perm

/// A selector for references, returning the value of type [a] stored in memory

val ptrp_sel (#a:Type0) (r:ref a) (p: perm) : selector a (ptrp r p)

[@@ __steel_reduce__; __reduce__]
unfold
let ptr_sel (#a:Type0) (r:ref a) : selector a (ptr r) = ptrp_sel r full_perm

/// Combining the separation logic predicate and selector into a vprop
[@@ __steel_reduce__]
let vptr' #a r p : vprop' =
  {hp = ptrp r p;
   t = a;
   sel = ptrp_sel r p}

[@@ __steel_reduce__]
unfold
let vptrp (#a: Type) (r: ref a) ([@@@smt_fallback] p: perm) = VUnit (vptr' r p)

[@@ __steel_reduce__; __reduce__]
unfold
let vptr r = vptrp r full_perm

/// A wrapper to access a reference selector more easily.
/// Ensuring that the corresponding ptr vprop is in the context is done by
/// calling a variant of the framing tactic, as defined in Steel.Effect.Common

[@@ __steel_reduce__]
let selp (#a:Type) (#p:vprop) (r:ref a) (pr: perm)
  (h:rmem p{FStar.Tactics.with_tactic selector_tactic (can_be_split p (vptrp r pr) /\ True)})
  = h (vptrp r pr)

[@@ __steel_reduce__]
let sel (#a:Type) (#p:vprop) (r:ref a)
  (h:rmem p{FStar.Tactics.with_tactic selector_tactic (can_be_split p (vptr r) /\ True)})
  = h (vptr r)

/// Stateful lemmas to interoperate between Steel arrays and this module

val intro_vptrp
  (#opened: _)
  (#a: Type0)
  (r: ref a)
  (p: perm)
: SteelGhost unit opened
    (A.varrayp r p)
    (fun _ -> vptrp r p)
    (fun _ -> True)
    (fun h0 _ h1 ->
      Seq.create 1 (selp r p h1) == A.aselp r p h0
    )

val elim_vptrp
  (#opened: _)
  (#a: Type0)
  (r: ref a)
  (p: perm)
: SteelGhost unit opened
    (vptrp r p)
    (fun _ -> A.varrayp r p)
    (fun _ -> True)
    (fun h0 _ h1 ->
      A.aselp r p h1 == Seq.create 1 (selp r p h0)
    )

let intro_vptr (#opened: _)
  (#a: Type0)
  (r: ref a)
: SteelGhost unit opened
    (A.varray r)
    (fun _ -> vptr r)
    (fun _ -> True)
val intro_vptr (#opened: _) (#a: Type0) (r: ref a)
    : SteelGhost unit
      opened
      (A.varray r)
      (fun _ -> vptr r)
      (fun _ -> True)
      (fun h0 _ h1 -> A.asel r h0 == Seq.create 1 (sel r h1))
r: Steel.ArrayRef.ref a -> Steel.Effect.Atomic.SteelGhost Prims.unit