val ind_ptr_sl' (#a: Type0) (r: ref (ref a)) (p: ref a) : slprop u#1
val ind_ptr_sl' (#a: Type0) (r: ref (ref a)) (p: ref a) : slprop u#1
let ind_ptr_sl' (#a:Type0) (r:ref (ref a)) (p: ref a) : slprop u#1 =
  pts_to_sl r full_perm p `Mem.star` ptr p
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)

let llist_ptr_sl ptr = Mem.h_exists (llist_ptr_sl' ptr)

val llist_ptr_sel' (#a:Type0) (ptr:t a) : selector' (list (cell a * a)) (llist_ptr_sl ptr)

let llist_ptr_sel' #a ptr = fun h -> id_elim_exists (llist_ptr_sl' ptr) h

let llist_ptr_sl'_witinv (#a:Type) (ptr:t a)
  : Lemma (is_witness_invariant (llist_ptr_sl' ptr))
  = let rec aux (ptr:t a) (x y:list (cell a * a)) (m:mem) : Lemma
        (requires interp (llist_ptr_sl' ptr x) m /\ interp (llist_ptr_sl' ptr y) m)
        (ensures x == y)
        (decreases x)
     = match x with
       | [] -> begin match y with
         | [] -> ()
         | (hd, v)::tl ->
           Mem.pure_interp (ptr == null_llist) m;
           Mem.pure_star_interp
             (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)
             (ptr =!= null_llist) m;
           Mem.pure_interp (ptr =!= null_llist) m
         end
       | (hd1, v1)::tl1 -> begin match y with
         | [] ->
           Mem.pure_interp (ptr == null_llist) m;
           Mem.pure_star_interp
             (pts_to_sl ptr full_perm hd1 `Mem.star`
              llist_ptr_sl' (next hd1) tl1 `Mem.star`
              pts_to_sl (data hd1) full_perm v1)
             (ptr =!= null_llist) m;
           Mem.pure_interp (ptr =!= null_llist) m
         | (hd2, v2)::tl2 ->
           pts_to_witinv ptr full_perm;
           pts_to_witinv (data hd1) full_perm;
           aux (next hd1) tl1 tl2 m

       end


    in Classical.forall_intro_3 (Classical.move_requires_3 (aux ptr))

let llist_sel_depends_only_on (#a:Type0) (ptr:t a)
  (m0:Mem.hmem (llist_ptr_sl ptr)) (m1:mem{disjoint m0 m1})
  : Lemma (llist_ptr_sel' ptr m0 == llist_ptr_sel' ptr (Mem.join m0 m1))
  = let l1 = reveal (id_elim_exists (llist_ptr_sl' ptr) m0) in
    let l2 = reveal (id_elim_exists (llist_ptr_sl' ptr) (Mem.join m0 m1)) in

    llist_ptr_sl'_witinv ptr;
    Mem.elim_wi (llist_ptr_sl' ptr) l1 l2 (Mem.join m0 m1)

let llist_sel_depends_only_on_core (#a:Type0) (ptr:t a)
  (m0:Mem.hmem (llist_ptr_sl ptr))
  : Lemma (llist_ptr_sel' ptr m0 == llist_ptr_sel' ptr (core_mem m0))
  = let l1 = reveal (id_elim_exists (llist_ptr_sl' ptr) m0) in
    let l2 = reveal (id_elim_exists (llist_ptr_sl' ptr) (core_mem m0)) in

    llist_ptr_sl'_witinv ptr;
    Mem.elim_wi (llist_ptr_sl' ptr) l1 l2 (core_mem m0)

val llist_ptr_sel_cell (#a:Type0) (ptr:t a) : selector (list (cell a * a)) (llist_ptr_sl ptr)
let llist_ptr_sel_cell #a ptr =
  Classical.forall_intro_2 (llist_sel_depends_only_on ptr);
  Classical.forall_intro (llist_sel_depends_only_on_core ptr);
  llist_ptr_sel' ptr

let rec datas (#a:Type) (l:list (cell a * a)) : list a =
  match l with
  | [] -> []
  | (_, v)::tl -> v :: datas tl

let llist_ptr_sel ptr = fun h -> datas (llist_ptr_sel_cell ptr h)

[@@__steel_reduce__]
let llist_cell' #a r : vprop' =
  {hp = llist_ptr_sl r;
   t = list (cell a * a);
   sel = llist_ptr_sel_cell r}
unfold
let llist_cell (#a:Type0) (r:t a) = VUnit (llist_cell' r)

[@@ __steel_reduce__]
let v_cell (#a:Type0) (#p:vprop) (r:t a)
  (h:rmem p{FStar.Tactics.with_tactic selector_tactic (can_be_split p (llist_cell r) /\ True)}) : GTot (list (cell a * a))
  = h (llist_cell r)

(* Indirection pointer on a pointer. Should become a generic module at some point *)
/
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: Steel.Reference.ref (Steel.Reference.ref a) -> p: Steel.Reference.ref a -> Steel.Memory.slprop
Steel.Reference.ref Steel.Memory.star Steel.Reference.pts_to_sl Steel.FractionalPermission.full_perm Steel.Reference.ptr Steel.Memory.slprop
let ind_ptr_sl' (#a: Type0) (r: ref (ref a)) (p: ref a) : slprop u#1 =
  
(pts_to_sl r full_perm p) `Mem.star` (ptr p)