val v_ptrlist
      (#a: Type0)
      (#p: vprop)
      (r: t a)
      (h: rmem p {FStar.Tactics.with_tactic selector_tactic (can_be_split p (llist_ptr r) /\ True)})
    : GTot (list a)
val v_ptrlist
      (#a: Type0)
      (#p: vprop)
      (r: t a)
      (h: rmem p {FStar.Tactics.with_tactic selector_tactic (can_be_split p (llist_ptr r) /\ True)})
    : GTot (list a)
let v_ptrlist (#a:Type0) (#p:vprop) (r:t a)
  (h:rmem p{FStar.Tactics.with_tactic selector_tactic (can_be_split p (llist_ptr r) /\ True)}) : GTot (list a)
  = h (llist_ptr r)
module Selectors.PtrLList

open Steel.Memory
open Steel.Effect.Atomic
open Steel.Effect
open Steel.Reference

module L = FStar.List.Tot

/// This module provides a variant of linked lists, where the list elements are themselves pointers.

/// Abstract type for a cell storing a value of type [a]
val cell (a:Type0) : Type0
/// A list is a reference to a cell
let t (a:Type0) = ref (cell a)

(* Helpers to manipulate cells while keeping its definition abstract *)

val next (#a:Type0) (c:cell a) : t a
val data (#a:Type0) (c:cell a) : ref a
val mk_cell (#a:Type0) (n: t a) (d:ref a)
  : Pure (cell a)
    (requires True)
    (ensures fun c ->
      next c == n /\
      data c == d)

/// The null list pointer
val null_llist (#a:Type) : t a

/// Lifting the null pointer check to empty lists
val is_null (#a:Type) (ptr:t a) : (b:bool{b <==> ptr == null_llist})

/// Separation logic predicate stating that reference [r] points to a valid list in memory
val llist_ptr_sl (#a:Type0) (r:t a) : slprop u#1
/// Selector a list of pointers of type [a]. Returns an F* list of the elements
/// that each poitner stores
val llist_ptr_sel (#a:Type0) (r:t a) : selector (list a) (llist_ptr_sl r)

/// Combines the two above into a linked list vprop
[@@__steel_reduce__]
let llist_ptr' (#a:Type0) (r:t a) : vprop' =
  { hp = llist_ptr_sl r;
    t = list a;
    sel = llist_ptr_sel r}
unfold
let llist_ptr (#a:Type0) (r:t a) = VUnit (llist_ptr' r)

/// A wrapper to access a list selector more easily.
/// Ensuring that the corresponding llist_ptr vprop is in the context is done by
/// calling a variant of the framing tactic, as defined in Steel.Effect.Common
/
Steel.Reference.fsti.checked Steel.Memory.fsti.checked Steel.Effect.Atomic.fsti.checked Steel.Effect.fsti.checked prims.fst.checked FStar.Tactics.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked
Selectors.PtrLList.fsti

    r: Selectors.PtrLList.t a ->
    h:
      Steel.Effect.Common.rmem p
        { FStar.Tactics.Effect.with_tactic Steel.Effect.Common.selector_tactic
            (Steel.Effect.Common.can_be_split p (Selectors.PtrLList.llist_ptr r) /\ Prims.l_True) }
  -> Prims.GTot (Prims.list a)
Steel.Effect.Common.vprop Selectors.PtrLList.t Steel.Effect.Common.rmem FStar.Tactics.Effect.with_tactic Steel.Effect.Common.selector_tactic Prims.l_and Steel.Effect.Common.can_be_split Selectors.PtrLList.llist_ptr Prims.l_True Prims.list
let v_ptrlist
      (#a: Type0)
      (#p: vprop)
      (r: t a)
      (h: rmem p {FStar.Tactics.with_tactic selector_tactic (can_be_split p (llist_ptr r) /\ True)})
    : GTot (list a) =
  
h (llist_ptr r)