val llist_ptr_sl'_witinv (#a: Type) (ptr: t a) : Lemma (is_witness_invariant (llist_ptr_sl' ptr))
val llist_ptr_sl'_witinv (#a: Type) (ptr: t a) : Lemma (is_witness_invariant (llist_ptr_sl' ptr))
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))
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
/
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
ptr: Selectors.PtrLList.t a
  -> FStar.Pervasives.Lemma
    (ensures Steel.Memory.is_witness_invariant (Selectors.PtrLList.llist_ptr_sl' ptr))
Selectors.PtrLList.t FStar.Classical.forall_intro_3 Prims.list FStar.Pervasives.Native.tuple2 Selectors.PtrLList.cell Steel.Memory.mem Prims.l_imp Prims.l_and Steel.Memory.interp Selectors.PtrLList.llist_ptr_sl' Prims.eq2 FStar.Classical.move_requires_3 Prims.unit Prims.squash Prims.Nil FStar.Pervasives.pattern Steel.Memory.pure_interp Prims.l_not Selectors.PtrLList.null_llist Steel.Memory.pure_star_interp Steel.Memory.star Steel.Reference.pts_to_sl Steel.FractionalPermission.full_perm Selectors.PtrLList.next Selectors.PtrLList.data Steel.Reference.pts_to_witinv Prims.l_True Steel.Memory.is_witness_invariant
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
  | [] ->
    (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)
  | (hd1, v1) :: tl1 ->
    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
in
Classical.forall_intro_3 (Classical.move_requires_3 (aux ptr))