exercises.linked_lists

From iris.heap_lang Require Import lang proofmode notation.
(* ################################ *)

Case Study: Linked Lists


Section linked_lists.
Context `{!heapGS Σ}.

In this chapter, we will study several functions on linked lists. To do this, we must first agree on what a linked list is. In HeapLang, we can implement linked lists as chains of pointers. We define this formally with a predicate, which we denote isList. This predicate turns a list of values xs into a predicate describing the structure of the linked list.
(* To Mansky, l is the head of xs? *)
Fixpoint isList (l : val) (xs : list val) : iProp Σ :=
  match xs with
  | [] => ⌜l = NONEV⌝
  | x :: xs => ∃ (hd : loc) l', ⌜l = SOMEV (#hd)⌝ ∗ hd ↦ (x, l') ∗ isList l' xs
  end.
Here, NONEV and SOMEV v are the value equivalents of NONE and SOME e.
We can now define HeapLang functions that act on lists, such as inc. The inc function recursively increments all the values of a list.
Definition inc : val :=
  rec: "inc" "l" :=
    match: "l" with
      NONE => #()
    | SOME "hd" =>
        let: "x" := Fst (! "hd") in
        let: "l'" := Snd (! "hd") in
        "hd" <- ("x" + #1, "l'");;
        "inc" "l'"
    end.

Intuitively, the specification we give for this function should state that the linked list should only contain integers and that, after executing the function, each integer has been incremented. As such, we parametrise the specification not by a list of values, but by a list of integers. We then map each integer to a HeapLang value using # _, allowing us to use the isList predicate.
(* To Mansky, I do not understand <*)
(*  *)
(* Print fmap.  *)
(* Print map. a special case of fmap on list  *)
Lemma inc_spec (l : val) (xs : list Z) :
  {{{ isList l ((λ x : Z, #x) <$> xs) }}}
    inc l
  {{{ RET #(); isList l ((λ x, #(x + 1)) <$> xs)}}}.
Proof.
  (* redo *)
  (*
    revert l.
  induction xs.
  - intros.   
    iIntros "P Q".
    simpl. 
    iDestruct "P" as "hd %l' C]". 
    iDestruct "C" as "(*)

The proof proceeds by structural induction in xs. As l changes in each iteration, we must universally quantify over it to strengthen the induction hypothesis.
  revert l.
  induction xs as [|x xs' IH].
  - (* Base Case: xs =  *)
  (*
    iIntros (l) "HA".  iIntros "HΦ".
Σ : gFunctors
heapGS0 : heapGS Σ
l : val
Φ : val → iPropI Σ
HA : l = InjLV () (1 / 1) "HΦ" : ▷ (⌜l = InjLV ()⌝ -∗ Φ ()) --------------------------------------∗ WP inc l {{ v, Φ v }} *)
    iIntros (l) "%Φ -> HΦ".
    wp_rec.
    wp_pures.
    by iApply "HΦ".
  - (* Induction step: xs = x :: xs' *)
    (* exercise *)
    (* the head is inc by 1 by inc definition, and rest by IH *)
    iIntros "%l %Φ HA HΦ".
    simpl.
    iDestruct "HA" as "(%ehd & %tail & %leqhd & ehd_defef & AAA)".
    (* iDestruct "HA" as "%ehd [%tail (%leqhd & ehd_defef & AAA)]".  *)
    wp_rec.
    rewrite -> leqhd.
    wp_pure.
    wp_pure.
    wp_pures.
    wp_load.
    wp_pures.
    wp_load.
    wp_pures.
    wp_store.
    iApply (IH with "[AAA]").
    + iApply "AAA".
    + iNext.
      iIntros "BBB".
      iApply "HΦ".
      iExists ehd.
      iExists tail.
      iFrame.
      done.
Qed.

The append function recursively descends l1, updating the links. Eventually, it reaches the tail, NONE, where it will replace it with l2.
Definition append : val :=
  rec: "append" "l1" "l2" :=
    match: "l1" with
      NONE => "l2"
    | SOME "hd" =>
        let: "x" := Fst (!"hd") in
        let: "l1'" := Snd (!"hd") in
        let: "r" := "append" "l1'" "l2" in
        "hd" <- ("x", "r");;
        SOME "hd"
    end.

If l1 and l2 represent the lists xs and ys respectively, then we expect that append l1 l2 will return a list representing xs ++ ys.
Lemma append_spec (l1 l2 : val) (xs ys : list val) :
  {{{ isList l1 xs ∗ isList l2 ys }}}
    append l1 l2
  {{{ l, RET l; isList l (xs ++ ys) }}}.
Proof.
  (*redo*)
  (*
  revert ys l1 l2.
  induction xs. 
  - intros. iIntros "-> l2_is_ys post".   
    simpl. 
    wp_rec. 
    wp_let.
    wp_match.
    by iApply "post".   
  - intros. iIntros "l1_is_a_xs l2_is_ys post".  
    wp_rec. 
    wp_let.
    simpl.
    iDestruct "l1_is_a_xs" as "(l' & -> & hd_pt & l'_is_xs)".
    wp_match.
    wp_load.   
    wp_proj. 
    wp_let.
    wp_load.
    wp_pures.
    wp_apply (IHxs with "l'_is_xs l2_is_ys hd_pt post"). 
    + iFrame.
    + iNext.
      iIntros "*)

  revert ys l1 l2.
  induction xs as [| x xs' IH]; simpl.
  (* exercise *)
  - iIntros "%ys %l1 %l2 %Φ".
    iIntros "[%l1isNull l2isys] post".
    rewrite l1isNull.
    unfold append.
    wp_rec.
    wp_let.
    wp_pures.
    iApply ("post" with "l2isys").
  - iIntros (ys l1 l2 Φ).
    iIntros "[(%hd & %l' & l1eqhd & hdptxl' & l'xs'islist) BBB] CCC".
    (* iDestruct "AAA" as "". 
    iIntros "AAA BBB CCC". 
    iDestruct "AAA" as "(l' & l1eqhd & hdptxl' & l'xs'islist)".  *)
    wp_rec.
    wp_let.
    iDestruct "l1eqhd" as %l1eqhd.
    rewrite l1eqhd.
    wp_pures.
    wp_load.
    wp_proj.
    wp_let.
    wp_load.
    wp_pures.
    (* each  is for one branch *)
    wp_apply (IH with "[l'xs'islist BBB] [hdptxl' CCC]").
    + iFrame.
    + iNext.
      iIntros "%l isList_l_xs'ys".
      wp_let.
      wp_store.
      wp_pure.
      iApply "CCC".
      iExists hd.
      iExists l.
      iFrame.
      done.
Qed.

We will implement reverse using a helper function called reverse_append, which takes two arguments, l and acc, and returns the list rev l ++ acc.
Definition reverse_append : val :=
  rec: "reverse_append" "l" "acc" :=
    match: "l" with
      NONE => "acc"
    | SOME "hd" =>
        let: "x" := Fst (! "hd") in
        let: "l'" := Snd (! "hd") in
        "hd" <- ("x", "acc");;
        "reverse_append" "l'" "l"
    end.

When acc is the empty list, it should thus simply return the reverse of l.
Definition reverse : val :=
  λ: "l", reverse_append "l" NONE.

Lemma reverse_append_spec (l acc : val) (xs ys : list val) :
  {{{ isList l xs ∗ isList acc ys }}}
    reverse_append l acc
  {{{ v, RET v; isList v (rev xs ++ ys) }}}.
Proof.
  revert l acc ys.
  induction xs as [| x xs' IH]; simpl.
  (* exercise *)
  - intros. iIntros "[-> acc_is_ys] post".
    wp_rec. wp_pures. by iApply "post".
  - intros.
    iIntros "A post".
    iDestruct "A" as "[B C]".
    iDestruct "B" as "[%hd [%l' (-> & E & F)]]".
    wp_rec.
    wp_let.
    wp_pures.
    wp_load.
    wp_pures.
    wp_load.
    wp_pures.
    wp_store.
    (* To Mansky: I learnt (x :: ys) from the solution, 
    but do not know exactly why.
    What is the next val to evalate?
    How to reduce InjRV  hd? *)
    wp_apply (IH l' (InjRV #hd) (x :: ys) with "[F C E] [post]").
    + iFrame. done.
    + iNext.
      rewrite <- app_assoc.
      done.


Qed.

Now, we use the specification of reverse_append to prove the specification of reverse.
Lemma reverse_spec (l : val) (xs : list val) :
  {{{ isList l xs }}}
    reverse l
  {{{ v, RET v; isList v (rev xs) }}}.
Proof.
  (* exercise *)
  unfold reverse.
  intros.
  iIntros "l_is_xs post".
  wp_lam.
  simpl.
  (*
  Check reverse_append_spec. 
  ∀ (l acc : val) (xs ys : list val) (Φ : val → iPropI Σ),
isList l xs ∗ isList acc ys -∗
▷ (∀ v : val, isList v (rev xs ++ ys) -∗ Φ v) -∗
WP reverse_append l acc {{ v, Φ v }}
*)
  wp_pure.
  wp_apply (reverse_append_spec l (InjLV #()) xs [] with "[l_is_xs]").
  - iFrame. done.
  - replace (rev xs ++ []) with (rev xs).
    + auto.
    + (*Search (?x ++  = ?x). *)
      rewrite app_nil_r.
      reflexivity.
Qed.

The specifications thus far have been rather straightforward. Now we will show a very general specification for fold_right.
(* apply each element of l to v, from right *)
Definition fold_right : val :=
  rec: "fold_right" "f" "v" "l" :=
    match: "l" with
      NONE => "v"
    | SOME "hd" =>
        let: "x" := Fst (! "hd") in
        let: "l'" := Snd (! "hd") in
        "f" "x" ("fold_right" "f" "v" "l'")
    end.
The following specification has a lot of moving parts, so let us go through them one by one.
  • l is a linked list representing xs, as seen by isList l xs in the precondition.
  • P is a predicate which all the values in xs should satisfy. This is written as [∗ list] x ∈ xs, P x. It is a recursively defined predicate, defined as follows: [∗ list] x ∈ [], P x := True [∗ list] x ∈ x0 :: xs, P x := P x0 ∗ [∗ list] x ∈ xs, P x
  • I is a predicate (think I for invariant) describing the relation between a list and the result of the fold.
  • a is the base value, so fold will return a for the empty list; this is captured by I [] a.
  • f is the folding function, which we assume satisfies: {{{ P x ∗ I ys a' }}} f x a' {{{ r, RET; I (x :: ys) r }}}. Intuitively, this says that if f is applied to an argument from the list (hence satisfying P) and a' is the result of folding ys, captured by I ys a', then the result r will be the result of folding f over x :: ys, captured by I (x :: ys) r in the postcondition.
  • The result r of folding must then satisfy I xs r.
  • Importantly, we do not change the original list. So we put isList l xs in the postcondition.
Note that Hoare triples are persistent, and persistent predicates are closed under universal quantification. Hence, in the proof, the assumption for f will move into the persistent context.

(*To Mansky, what is * list and ∈ ? Skipping it. *)
Lemma fold_right_spec P I (f a l : val) xs :
  {{{
    isList l xs ∗ ([∗ list] x ∈ xs, P x) ∗ I [] a ∗
    (∀ (x a' : val) ys,
      {{{ P x ∗ I ys a' }}} f x a' {{{ r, RET r; I (x :: ys) r }}})
  }}}
    fold_right f a l
  {{{ r, RET r; isList l xs ∗ I xs r}}}.

Proof.
  revert a l.
  induction xs as [|x xs IHxs].
  all: simpl.
  (* exercise *)
Admitted.

We can now sum over a list simply by folding an addition function over it.

Definition sum_list : val :=
  λ: "l",
    let: "f" := (λ: "x" "y", "x" + "y") in
    fold_right "f" #0 "l".

Lemma sum_list_spec l xs :
  {{{isList l ((λ x : Z, #x) <$> xs)}}}
    sum_list l
  {{{RET #(foldr Z.add 0 xs); isList l ((λ x : Z, #x) <$> xs)}}}.
Proof.
  iIntros (Φ) "Hl HΦ".
  wp_rec; wp_pures.
  wp_apply (fold_right_spec
    (λ x, ∃ i : Z, ⌜x = #i⌝)%I
    (λ xs y, ∃ ys, ⌜xs = (λ x : Z, #x) <$> ys⌝ ∗ ⌜y = #(foldr Z.add 0 ys)⌝)%I
    with "[Hl]"
  ).
  - iFrame.
    repeat iSplit.
    + iPureIntro; simpl.
      intros k v Hk.
      rewrite list_lookup_fmap in Hk.
      destruct (xs !! k) as [x|]; last done.
      injection Hk as <-.
      by exists x.
    + by iExists [].
    + clear.
      iIntros (x a' ys Φ) "!> [[%i ->] (%xs & -> & ->)] HΦ".
      wp_pures.
      iModIntro.
      iApply "HΦ".
      by iExists (i :: xs).
  - iIntros "%_ (Hl & %ys & %H & ->)".
    assert (Hinj:Inj eq eq (λ x : Z, #x)) by congruence.
    apply (inj _) in H.
    subst ys.
    by iApply "HΦ".
Qed.

End linked_lists.