iris-tutorial/linked_lists.v at master · gonzaloUr/iris-tutorial · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
From iris.heap_lang Require Import lang proofmode notation.

Section linked_lists.
  Context `{!heapGS Σ}.

  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.

  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.

  Lemma inc_spec (l : val) (xs : list Z) :
    {{{ isList l ((λ x : Z, #x) <$> xs) }}}
      inc l
    {{{ RET #(); isList l ((λ x, #(x + 1)) <$> xs)}}}.
  Proof.
    revert l.
    induction xs as [| x xs' IH].
    - simpl.
      iIntros (l Φ) "-> HΦ".
      wp_rec.
      wp_pures.
      by iApply "HΦ".
    - simpl.
      iIntros (l Φ) "H HΦ".
      iDestruct "H" as (hd l') "(%Hl & Hl_hd & Hl_l')".
      rewrite Hl.
      wp_rec.
      wp_pures.
      wp_load.
      wp_pures.
      wp_load.
      wp_pures.
      wp_store.
      iApply (IH l' Φ with "Hl_l'").
      iNext.
      iIntros "Hl'".
      iApply "HΦ".
      iExists hd, l'.
      iFrame.
      done.
  Qed.

  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.

  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.
    revert ys l1 l2.
    induction xs as [| x xs' IH]; simpl.
    - iIntros (ys l1 l2).
      iIntros (Φ) "[-> H] HΦ".
      wp_rec.
      wp_pures.
      iModIntro.
      iApply ("HΦ" with "H").
    - iIntros (ys l1 l2 Φ) "[Hl'_xs' Hl2_ys] HΦ".
      iDestruct "Hl'_xs'" as (hd l') "(%Hl1 & Hhd & Hl'_xs')".
      wp_rec.
      wp_let.
      rewrite Hl1.
      wp_pures.
      wp_load.
      wp_pures.
      wp_load.
      wp_pures.
      wp_bind (append l' l2)%V.
      iCombine "Hl'_xs' Hl2_ys" as "H".
      iApply (IH ys l' l2 with "H").
      iNext.
      iIntros (l) "Hl".
      wp_pures.
      wp_store.
      wp_pures.
      iModIntro.
      iApply "HΦ".
      iExists hd, l.
      iSplitR "Hhd Hl".
      * done.
      * iFrame.
  Qed.
End linked_lists.