val llist_ptr_sl (#a:Type0) (r:t a) : slprop u#1
val llist_ptr_sl (#a:Type0) (r:t a) : slprop u#1
let llist_ptr_sl ptr = Mem.h_exists (llist_ptr_sl' ptr)
module Selectors.PtrLList

open FStar.Ghost
open Steel.FractionalPermission
module Mem = Steel.Memory

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

#push-options "--__no_positivity"
noeq
type cell (a:Type0) = {
  next : ref (cell a);
  data : ref a;
}
#pop-options

let next #a (c:cell a) : t a = c.next
let data #a (c:cell a) : ref a = c.data
let mk_cell #a (n: t a) (d:ref a) = {
  next = n;
  data = d
}

let null_llist #a = null
let is_null #a ptr = is_null ptr

let rec llist_ptr_sl' (#a:Type0) (ptr:t a) (l:list (cell a * a))
  : Tot slprop (decreases l)
  = match l with
    | [] -> Mem.pure (ptr == null_llist)
    | (hd, v) :: tl ->
      pts_to_sl ptr full_perm hd `Mem.star`
      llist_ptr_sl' (next hd) tl `Mem.star`
      pts_to_sl (data hd) full_perm v `Mem.star`
      Mem.pure (ptr =!= null_llist)
/
Steel.Reference.fsti.checked Steel.Memory.fsti.checked Steel.FractionalPermission.fst.checked Steel.Effect.Atomic.fsti.checked Steel.Effect.fsti.checked prims.fst.checked FStar.Tactics.Effect.fsti.checked FStar.Tactics.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Ghost.fsti.checked FStar.Classical.fsti.checked
Selectors.PtrLList.fst
r: Selectors.PtrLList.t a -> Steel.Memory.slprop
Selectors.PtrLList.t Steel.Memory.h_exists Prims.list FStar.Pervasives.Native.tuple2 Selectors.PtrLList.cell Selectors.PtrLList.llist_ptr_sl' Steel.Memory.slprop
let llist_ptr_sl ptr =
  
Mem.h_exists (llist_ptr_sl' ptr)