Pulse.Lib.DoublyLinkedList.fst

module Pulse.Lib.DoublyLinkedList
open Pulse.Lib.Pervasives
open Pulse.Lib.Stick.Util
open FStar.List.Tot
module T = FStar.Tactics
module I = Pulse.Lib.Stick.Util
module FA = Pulse.Lib.Forall.Util

noeq
type node (t:Type0) = {
    value : t;
    dllprev : option (node_ptr t);
    dllnext : option (node_ptr t);
}

and node_ptr (t:Type0) = ref (node t)

noeq
type dllist (t:Type0) = {
  head: option (node_ptr t);
  tail: option (node_ptr t);
}

let rec is_list_suffix
  #t
  (x:node_ptr t)
  ([@@@equate_by_smt] l:list t {Cons? l})
  ([@@@equate_by_smt] prev:option (node_ptr t))
  ([@@@equate_by_smt] tail:node_ptr t)
  : Tot vprop (decreases l)
  = match l with
    | [] -> emp
    | [n] ->
      exists* (v:node t).
        pts_to x v **
        pure (v.value == n /\
          v.dllnext == None /\
          v.dllprev == prev /\
          x == tail)
    | n::ns ->
      exists* (v:node t) (np:node_ptr t).
        pts_to x v **
        is_list_suffix np ns (Some x) tail **
        pure (v.value == n /\
          v.dllprev == prev /\
          v.dllnext == (Some np))

let is_list #t
  (x:dllist t)
  ([@@@equate_by_smt] l:list t)
  : Tot vprop (decreases l)
  = match l with
    | [] ->
        pure (x == { head = None; tail = None })
    | ns ->
        exists* (hp tp:node_ptr t).
          is_list_suffix hp ns None tp **
          pure (x.head == (Some hp) /\ x.tail == (Some tp))

```pulse
fn mk_empty (#t:Type) (_:unit)
  requires emp
  returns  p : dllist t
  ensures  is_list p []
{
  let p = { head = None; tail = None } <: dllist t;
  fold (is_list p []);
  p
}
``` 

let norm_tac (_:unit) : T.Tac unit =
    T.mapply (`vprop_equiv_refl)

```pulse
ghost
fn intro_is_list_singleton
  (#t:Type)
  (x : node_ptr t) (n : t)
  requires
      exists* (v:node t).
        pts_to x v **
        pure (v.value == n /\
          v.dllnext == None /\
          v.dllprev == None)
  ensures
    is_list_suffix x [n] None x
{
  // fold (is_list_suffix x [n] None x);
  rewrite_by 
    (exists* (v:node t).
      pts_to x v **
      pure (v.value == n /\
        v.dllnext == None /\
        v.dllprev == None /\
        x == x))
    (is_list_suffix x [n] None x)
    norm_tac
    ();
}
```

```pulse
fn push_empty (#t:Type) (l : dllist t) (x : t)
  requires is_list l []
  returns  l' : dllist t
  ensures  is_list l' [x]
{
  rewrite (is_list l [])
       as (pure (l == ({ head = None; tail = None } <: dllist t)));
  let vnode = { 
    value = x;
    dllprev = None;
    dllnext = None;
  };
  let node = alloc vnode;

  assert (
    pts_to node vnode **
    pure (vnode.value == x /\
      vnode.dllnext == None /\
      vnode.dllprev == None /\
      node == node));

  intro_is_list_singleton node x;
  
  let l' = {
    head = Some node;
    tail = Some node;
  };
  
  fold (is_list l' [x]);
  l'
}
```

```pulse
ghost
fn is_list_null_head_ptr
  (#t:Type)
  (l : dllist t)
  (#xs : erased (list t))
  requires
    is_list l xs **
    pure (l.head == None) 
  ensures
    is_list l xs **
    pure (l.tail == None /\ xs == [])
{
  let xss = reveal xs;
  match xss {
    Nil -> {
      unfold (is_list l []);
      fold (is_list l []);
      ()
    }
    Cons y ys -> {
      rewrite (is_list l xs) as (is_list l (y::ys));
      rewrite_by (is_list l (y::ys))
            (exists* (hp: node_ptr t) (tp: node_ptr t).
            is_list_suffix hp (y::ys) None tp **
            pure (l.head == Some hp /\ l.tail == Some tp))
            norm_tac
            ();
      assert (pure (Some? l.head));
      unreachable();
    }
  }
}
```

```pulse
ghost
fn is_list_not_null_head_ptr
  (#t:Type)
  (l : dllist t)
  (#xs : erased (list t))
  requires
    is_list l xs **
    pure (Some? l.head) 
  ensures
    // (exists* (hp: node_ptr t) (tp: node_ptr t).
    //   is_list_suffix hp xs None tp **
    //   pure (l.head == Some hp /\ l.tail == Some tp)) **
    is_list l xs ** 
    (pure (Cons? xs /\ xs == ((Cons?.hd xs)::(Cons?.tl xs))))
{
  let xss = reveal xs;
  match xss {
    Nil -> {
      unfold (is_list l []);
      fold (is_list l []);
      unreachable();
    }
    Cons y ys -> {
      // rewrite (is_list l xs) as (is_list l (y::ys));
      // rewrite_by (is_list l (y::ys))
      //       (exists* (hp: node_ptr t) (tp: node_ptr t).
      //       is_list_suffix hp (y::ys) None tp **
      //       pure (l.head == Some hp /\ l.tail == Some tp))
      //       norm_tac
            ();
      unfold (is_list l (y::ys));
      assert (pure (xs == y::ys));
      fold (is_list l (y::ys));
      // assert (pure (Some? l.head));
    }
  }
}
```

module T = FStar.Tactics.V2
let tac () : T.Tac unit =
  T.dump "1"; 
  vprop_equiv_norm ();
  T.dump "2"

#set-options "--debug SMTFail"

```pulse
fn push_front (#t:Type) (l : dllist t) (x : t)
  (#xs:erased (list t))
  requires is_list l xs
  returns  l' : dllist t
  ensures  is_list l' (x::xs)
{
  match l.head {
    None -> {
      is_list_null_head_ptr l;
      push_empty l x
    }
    Some hp -> {
      is_list_not_null_head_ptr l;
      let y = (hide (Cons?.hd xs)); // is there syntax to avoid the explicit "hide?"
      let ys = (hide (Cons?.tl xs)); // is there syntax to avoid the explicit "hide?"
      rewrite (is_list l xs) as (is_list l (Cons (reveal y) (reveal ys)));
      unfold (is_list l (Cons (reveal y) (reveal ys)));

      with (hpg tp:node_ptr _). _;
      assert (is_list_suffix hpg (reveal y :: reveal ys) None tp);
      rewrite each hpg as hp;
      assume_ (pure (Cons? ys));
      (* NOTE: I am assuming we are in the case of length >= 2.
      This is just so we can unfold the is_list_suffix, set the back
      pointer, and fold back again. This is probably better done
      by factoring this logic out into a separate function that goes
      roughly from
        is_list_suffix x l prev tail
      to
        is_list_suffix x l prev' tail
      by setting the dllprev pointer. *)

      (* Alloc new node, set forward pointer *)
      let nhv = { value = x; dllprev = None; dllnext = l.head };
      let nh = alloc nhv;
      let l' = { head = (Some nh); tail = l.tail };
      
      (* awful *)
      rewrite_by
        (is_list_suffix hp (reveal y :: reveal ys) None tp) 
        (exists* (v:node t) (np:node_ptr t).
          pts_to hp v **
          is_list_suffix np (reveal ys) (Some hp) tp **
          pure (v.value == reveal y /\
            v.dllprev == None /\
            v.dllnext == (Some np)))
        T.tadmit
        ();
      with v np. _;

      (* Add back pointer to old head *)
      let vv = !hp;
      let vv' = { vv with dllprev = Some nh };
      hp := vv';
      
      (* awful again *)
      rewrite_by
        (exists* (v:node t) (np:node_ptr t).
          pts_to hp v **
          is_list_suffix np (reveal ys) (Some hp) tp **
          pure (v.value == reveal y /\
            v.dllprev == Some nh /\
            v.dllnext == (Some np)))
        (is_list_suffix hp (reveal y :: reveal ys) (Some nh) tp) 
        T.tadmit
        ();

      (* awful again x2 *)
      rewrite_by
        (exists* (v:node t) (np:node_ptr t).
          pts_to np v **
          is_list_suffix hp (reveal y :: reveal ys) (Some nh) tp **
          pure (v.value == x /\
            v.dllprev == None /\
            v.dllnext == (Some hp)))
        (is_list_suffix nh (x :: reveal y :: reveal ys) None tp) 
        T.tadmit
        ();
 
      assert (is_list_suffix nh (x :: reveal y :: reveal ys) None tp);
      
      fold (is_list l' (x :: reveal y :: reveal ys));
      rewrite (is_list l' (x :: reveal y :: reveal ys))
           as (is_list l' (x::xs));
           
      l'
    }
  }
}
``` 

```pulse
fn push_back (#t:Type) (l : dllist t) (x : t)
  (#xs:erased (list t))
  requires is_list l xs
  returns  l' : dllist t
  ensures  is_list l' (List.Tot.append xs [x])
{
  match l.head {
    None -> {
      is_list_null_head_ptr l;
      let l' = push_empty l x;
      rewrite (is_list l' [x]) as (is_list l' (List.Tot.append xs [x]));
      l'
    }
    Some hp -> {
      admit();
    }
  }
}
```