val llist_ptr' (#a: Type0) (r: t a) : vprop'
val llist_ptr' (#a: Type0) (r: t a) : vprop'
let llist_ptr' (#a:Type0) (r:t a) : vprop' =
  { hp = llist_ptr_sl r;
    t = list a;
    sel = llist_ptr_sel 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.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 -> Steel.Effect.Common.vprop'
Selectors.PtrLList.t Steel.Effect.Common.Mkvprop' Selectors.PtrLList.llist_ptr_sl Prims.list Selectors.PtrLList.llist_ptr_sel Steel.Effect.Common.vprop'
let llist_ptr' (#a: Type0) (r: t a) : vprop' =
  
{ hp = llist_ptr_sl r; t = list a; sel = llist_ptr_sel r }