llist.v 8.64 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1 2 3
(** This file defines a separation logic representation predicates [llist] for
mutable linked-lists. It comes with a small library of operations (head, pop,
lookup, length, append, prepend, snoc, split). *)
Robbert Krebbers's avatar
Robbert Krebbers committed
4 5 6
From iris.heap_lang Require Export proofmode notation.
From iris.heap_lang Require Import assert.

Robbert Krebbers's avatar
Robbert Krebbers committed
7
(**  *)
Robbert Krebbers's avatar
Robbert Krebbers committed
8 9 10
Fixpoint llist `{heapG Σ} {A} (I : A  val  iProp Σ)
    (l : loc) (xs : list A) : iProp Σ :=
  match xs with
Robbert Krebbers's avatar
Robbert Krebbers committed
11
  | [] => l  NONEV
Robbert Krebbers's avatar
Robbert Krebbers committed
12
  | x :: xs =>  (v : val) (l' : loc), I x v  l  SOMEV (v,#l')  llist I l' xs
Robbert Krebbers's avatar
Robbert Krebbers committed
13 14 15 16
  end%I.
Arguments llist : simpl never.

Definition lnil : val := λ: <>, ref NONE.
Robbert Krebbers's avatar
Robbert Krebbers committed
17
Definition lcons : val := λ: "x" "l", "l" <- SOME ("x", ref (!"l")).
Robbert Krebbers's avatar
Robbert Krebbers committed
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

Definition lisnil : val := λ: "l",
  match: !"l" with
    SOME "p" => #false
  | NONE => #true
  end.

Definition lhead : val := λ: "l",
  match: !"l" with
    SOME "p" => Fst "p"
  | NONE => assert: #false
  end.

Definition lpop : val := λ: "l",
  match: !"l" with
    SOME "p" => "l" <- !(Snd "p");; Fst "p"
  | NONE => assert: #false
  end.

Definition llookup : val :=
  rec: "go" "l" "n" :=
    if: "n" = #0 then lhead "l" else
    match: !"l" with
      SOME "p" => "go" (Snd "p") ("n" - #1)
    | NONE => assert: #false
    end.

Definition llength : val :=
  rec: "go" "l" :=
    match: !"l" with
      NONE => #0
    | SOME "p" => #1 + "go" (Snd "p")
    end.

Definition lapp : val :=
  rec: "go" "l" "k" :=
    match: !"l" with
      NONE => "l" <- !"k"
    | SOME "p" => "go" (Snd "p") "k"
    end.
Definition lprep : val := λ: "l" "k",
  lapp "k" "l";; "l" <- !"k".

Definition lsnoc : val :=
  rec: "go" "l" "x" :=
    match: !"l" with
      NONE => "l" <- SOME ("x", ref NONE)
    | SOME "p" => "go" (Snd "p") "x"
    end.

Definition lsplit_at : val :=
  rec: "go" "l" "n" :=
    if: "n"  #0 then let: "k" := ref (! "l") in "l" <- NONE;; "k" else
    match: !"l" with
      NONE => ref NONE
    | SOME "p" => "go" (Snd "p") ("n" - #1)
    end.

Definition lsplit : val := λ: "l", lsplit_at "l" (llength "l" `quot` #2).

Section lists.
Robbert Krebbers's avatar
Robbert Krebbers committed
79
Context `{heapG Σ} {A} (I : A  val  iProp Σ).
Robbert Krebbers's avatar
Robbert Krebbers committed
80
Implicit Types i : nat.
Robbert Krebbers's avatar
Robbert Krebbers committed
81 82 83
Implicit Types xs : list A.
Implicit Types l : loc.
Local Arguments llist {_ _ _} _ _ !_ /.
Robbert Krebbers's avatar
Robbert Krebbers committed
84

85 86 87 88 89 90 91 92 93
Lemma llist_fmap {B} (J : B  val  iProp Σ) (f : A  B) l xs :
   ( x v, I x v - J (f x) v) -
  llist I l xs - llist J l (f <$> xs).
Proof.
  iIntros "#Hf Hll". iInduction xs as [|x xs] "IH" forall (l); csimpl; auto.
  iDestruct "Hll" as (v l') "(Hx & Hl & Hll)". iExists _, _. iFrame "Hl".
  iSplitL "Hx". by iApply "Hf". by iApply "IH".
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
94
Lemma lnil_spec :
Robbert Krebbers's avatar
Robbert Krebbers committed
95
  {{{ True }}} lnil #() {{{ l, RET #l; llist I l [] }}}.
Robbert Krebbers's avatar
Robbert Krebbers committed
96 97
Proof. iIntros (Φ _) "HΦ". wp_lam. wp_alloc l. by iApply "HΦ". Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
98 99
Lemma lcons_spec l x xs v :
  {{{ llist I l xs  I x v }}} lcons v #l {{{ RET #(); llist I l (x :: xs) }}}.
Robbert Krebbers's avatar
Robbert Krebbers committed
100
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
101
  iIntros (Φ) "[Hll Hx] HΦ". wp_lam. destruct xs as [|x' xs]; simpl; wp_pures.
Robbert Krebbers's avatar
Robbert Krebbers committed
102
  - wp_load. wp_alloc k. wp_store. iApply "HΦ"; eauto with iFrame.
Robbert Krebbers's avatar
Robbert Krebbers committed
103 104
  - iDestruct "Hll" as (v' l') "(HIx' & Hl & Hll)".
    wp_load. wp_alloc k. wp_store. iApply "HΦ"; eauto 10 with iFrame.
Robbert Krebbers's avatar
Robbert Krebbers committed
105 106
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
107 108
Lemma lisnil_spec l xs:
  {{{ llist I l xs }}}
Robbert Krebbers's avatar
Robbert Krebbers committed
109
    lisnil #l
Robbert Krebbers's avatar
Robbert Krebbers committed
110
  {{{ RET #(if xs is [] then true else false); llist I l xs }}}.
Robbert Krebbers's avatar
Robbert Krebbers committed
111
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
112
  iIntros (Φ) "Hll HΦ". wp_lam. destruct xs as [|x xs]; simpl; wp_pures.
Robbert Krebbers's avatar
Robbert Krebbers committed
113
  - wp_load; wp_pures. by iApply "HΦ".
Robbert Krebbers's avatar
Robbert Krebbers committed
114
  - iDestruct "Hll" as (v l') "(HIx & Hl & Hll)".
Robbert Krebbers's avatar
Robbert Krebbers committed
115 116 117
    wp_load; wp_pures. iApply "HΦ"; eauto with iFrame.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
118 119 120 121 122
(** Not the nicest spec, they leaks *)
Lemma lhead_spec_aux l x xs :
  {{{ llist I l (x :: xs) }}}
    lhead #l
  {{{ v (l' : loc), RET v; I x v  l  SOMEV (v,#l')  llist I l' xs }}}.
Robbert Krebbers's avatar
Robbert Krebbers committed
123
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
124
  iIntros (Φ) "/=". iDestruct 1 as (v l') "(HIx & Hl & Hll)". iIntros "HΦ".
Robbert Krebbers's avatar
Robbert Krebbers committed
125 126
  wp_lam. wp_load; wp_pures. iApply "HΦ"; eauto with iFrame.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
127 128
Lemma lpop_spec_aux l l' v xs :
  {{{ l  SOMEV (v,#l')  llist I l' xs }}} lpop #l {{{ RET v; llist I l xs }}}.
Robbert Krebbers's avatar
Robbert Krebbers committed
129
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
130 131
  iIntros (Φ) "[Hl Hll] HΦ".
  wp_lam. wp_load. wp_pures. destruct xs as [|x' xs]; simpl; wp_pures.
Robbert Krebbers's avatar
Robbert Krebbers committed
132
  - wp_load. wp_store. wp_pures. iApply "HΦ"; eauto with iFrame.
Robbert Krebbers's avatar
Robbert Krebbers committed
133
  - iDestruct "Hll" as (v' l'') "(HIx' & Hl' & Hll)".
Robbert Krebbers's avatar
Robbert Krebbers committed
134 135 136
    wp_load. wp_store. wp_pures. iApply "HΦ"; eauto with iFrame.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158
Lemma lhead_spec l x xs :
  {{{ llist I l (x :: xs) }}}
    lhead #l
  {{{ v, RET v; I x v  (I x v - llist I l (x :: xs)) }}}.
Proof.
  iIntros (Φ) "Hll HΦ". wp_apply (lhead_spec_aux with "Hll").
  iIntros (v l') "(HIx&?&?)". iApply "HΦ". iIntros "{$HIx} HIx".
  simpl; eauto with iFrame.
Qed.

Lemma lpop_spec l x xs :
  {{{ llist I l (x :: xs) }}} lpop #l {{{ v, RET v; I x v  llist I l xs }}}.
Proof.
  iIntros (Φ) "/=". iDestruct 1 as (v l') "(HIx & Hl & Hll)". iIntros "HΦ".
  wp_apply (lpop_spec_aux with "[$]"); iIntros "Hll". iApply "HΦ"; iFrame.
Qed.

Lemma llookup_spec l i xs x :
  xs !! i = Some x 
  {{{ llist I l xs }}}
    llookup #l #i
  {{{ v, RET v; I x v  (I x v - llist I l xs) }}}.
Robbert Krebbers's avatar
Robbert Krebbers committed
159 160
Proof.
  iIntros (Hi Φ) "Hll HΦ".
Robbert Krebbers's avatar
Robbert Krebbers committed
161
  iInduction xs as [|x' xs] "IH" forall (l i x Hi Φ); [done|simpl; wp_rec; wp_pures].
Robbert Krebbers's avatar
Robbert Krebbers committed
162
  destruct i as [|i]; simplify_eq/=; wp_pures.
Robbert Krebbers's avatar
Robbert Krebbers committed
163 164 165
  - wp_apply (lhead_spec with "Hll"); iIntros (v) "[HI Hll]".
    iApply "HΦ"; eauto with iFrame.
  - iDestruct "Hll" as (v l') "(HIx' & Hl' & Hll)". wp_load; wp_pures.
Robbert Krebbers's avatar
Robbert Krebbers committed
166
    rewrite Nat2Z.inj_succ Z.sub_1_r Z.pred_succ.
Robbert Krebbers's avatar
Robbert Krebbers committed
167 168
    wp_apply ("IH" with "[//] Hll"); iIntros (v') "[HIx Hll]".
    iApply "HΦ". iIntros "{$HIx} HIx". iExists v, l'. iFrame. by iApply "Hll".
Robbert Krebbers's avatar
Robbert Krebbers committed
169 170
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
171 172
Lemma llength_spec l xs :
  {{{ llist I l xs }}} llength #l {{{ RET #(length xs); llist I l xs }}}.
Robbert Krebbers's avatar
Robbert Krebbers committed
173 174
Proof.
  iIntros (Φ) "Hll HΦ".
Robbert Krebbers's avatar
Robbert Krebbers committed
175
  iInduction xs as [|x xs] "IH" forall (l Φ); simpl; wp_rec; wp_pures.
Robbert Krebbers's avatar
Robbert Krebbers committed
176
  - wp_load; wp_pures. by iApply "HΦ".
Robbert Krebbers's avatar
Robbert Krebbers committed
177
  - iDestruct "Hll" as (v l') "(HIx & Hl' & Hll)". wp_load; wp_pures.
Robbert Krebbers's avatar
Robbert Krebbers committed
178 179 180 181
    wp_apply ("IH" with "Hll"); iIntros "Hll". wp_pures.
    rewrite (Nat2Z.inj_add 1). iApply "HΦ"; eauto with iFrame.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
182 183
Lemma lapp_spec l1 l2 xs1 xs2 :
  {{{ llist I l1 xs1  llist I l2 xs2 }}}
Robbert Krebbers's avatar
Robbert Krebbers committed
184
    lapp #l1 #l2
Robbert Krebbers's avatar
Robbert Krebbers committed
185
  {{{ RET #(); llist I l1 (xs1 ++ xs2)  l2  - }}}.
Robbert Krebbers's avatar
Robbert Krebbers committed
186 187
Proof.
  iIntros (Φ) "[Hll1 Hll2] HΦ".
Robbert Krebbers's avatar
Robbert Krebbers committed
188 189
  iInduction xs1 as [|x1 xs1] "IH" forall (l1 Φ); simpl; wp_rec; wp_pures.
  - wp_load. wp_pures. destruct xs2 as [|x2 xs2]; simpl; wp_pures.
Robbert Krebbers's avatar
Robbert Krebbers committed
190
    + wp_load. wp_store. iApply "HΦ". eauto with iFrame.
Robbert Krebbers's avatar
Robbert Krebbers committed
191
    + iDestruct "Hll2" as (v2 l2') "(HIx2 & Hl2 & Hll2)". wp_load. wp_store.
Robbert Krebbers's avatar
Robbert Krebbers committed
192
      iApply "HΦ". iSplitR "Hl2"; eauto 10 with iFrame.
Robbert Krebbers's avatar
Robbert Krebbers committed
193
  - iDestruct "Hll1" as (v1 l') "(HIx1 & Hl1 & Hll1)". wp_load; wp_pures.
Robbert Krebbers's avatar
Robbert Krebbers committed
194 195 196 197
    wp_apply ("IH" with "Hll1 Hll2"); iIntros "[Hll Hl2]".
    iApply "HΦ"; eauto with iFrame.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
198 199
Lemma lprep_spec l1 l2 xs1 xs2 :
  {{{ llist I l1 xs2  llist I l2 xs1 }}}
Robbert Krebbers's avatar
Robbert Krebbers committed
200
    lprep #l1 #l2
Robbert Krebbers's avatar
Robbert Krebbers committed
201
  {{{ RET #(); llist I l1 (xs1 ++ xs2)  l2  - }}}.
Robbert Krebbers's avatar
Robbert Krebbers committed
202 203 204
Proof.
  iIntros (Φ) "[Hll1 Hll2] HΦ". wp_lam.
  wp_apply (lapp_spec with "[$Hll2 $Hll1]"); iIntros "[Hll2 Hl1]".
Robbert Krebbers's avatar
Robbert Krebbers committed
205
  iDestruct "Hl1" as (w) "Hl1". destruct (xs1 ++ xs2) as [|x xs]; simpl; wp_pures.
Robbert Krebbers's avatar
Robbert Krebbers committed
206
  - wp_load. wp_store. iApply "HΦ"; eauto with iFrame.
Robbert Krebbers's avatar
Robbert Krebbers committed
207
  - iDestruct "Hll2" as (v l') "(HIx & Hl2 & Hll2)". wp_load. wp_store.
Robbert Krebbers's avatar
Robbert Krebbers committed
208 209 210
    iApply "HΦ"; iSplitR "Hl2"; eauto with iFrame.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
211 212
Lemma lsnoc_spec l xs x v :
  {{{ llist I l xs  I x v }}} lsnoc #l v {{{ RET #(); llist I l (xs ++ [x]) }}}.
Robbert Krebbers's avatar
Robbert Krebbers committed
213
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
214 215
  iIntros (Φ) "[Hll HIx] HΦ".
  iInduction xs as [|x' xs] "IH" forall (l Φ); simpl; wp_rec; wp_pures.
Robbert Krebbers's avatar
Robbert Krebbers committed
216
  - wp_load. wp_alloc k. wp_store. iApply "HΦ"; eauto with iFrame.
Robbert Krebbers's avatar
Robbert Krebbers committed
217 218
  - iDestruct "Hll" as (v' l') "(HIx' & Hl & Hll)". wp_load; wp_pures.
    wp_apply ("IH" with "Hll HIx"); iIntros "Hll". iApply "HΦ"; eauto with iFrame.
Robbert Krebbers's avatar
Robbert Krebbers committed
219 220
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
221 222
Lemma lsplit_at_spec l xs (n : nat) :
  {{{ llist I l xs }}}
Robbert Krebbers's avatar
Robbert Krebbers committed
223
    lsplit_at #l #n
Robbert Krebbers's avatar
Robbert Krebbers committed
224
  {{{ k, RET #k; llist I l (take n xs)  llist I k (drop n xs) }}}.
Robbert Krebbers's avatar
Robbert Krebbers committed
225 226
Proof.
  iIntros (Φ) "Hll HΦ".
Robbert Krebbers's avatar
Robbert Krebbers committed
227
  iInduction xs as [|x xs] "IH" forall (l n Φ); simpl; wp_rec; wp_pures.
Robbert Krebbers's avatar
Robbert Krebbers committed
228 229 230
  - destruct n as [|n]; simpl; wp_pures.
    + wp_load. wp_alloc k. wp_store. iApply "HΦ"; iFrame.
    + wp_load. wp_alloc k. iApply "HΦ"; iFrame.
Robbert Krebbers's avatar
Robbert Krebbers committed
231
  - iDestruct "Hll" as (v l') "(HIx & Hl & Hll)". destruct n as [|n]; simpl; wp_pures.
Robbert Krebbers's avatar
Robbert Krebbers committed
232 233 234 235 236 237
    + wp_load. wp_alloc k. wp_store. iApply "HΦ"; eauto with iFrame.
    + wp_load; wp_pures. rewrite Nat2Z.inj_succ Z.sub_1_r Z.pred_succ.
      wp_apply ("IH" with "[$]"); iIntros (k) "[Hll Hlk]".
      iApply "HΦ"; eauto with iFrame.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
238 239
Lemma lsplit_spec l xs :
  {{{ llist I l xs }}}
Robbert Krebbers's avatar
Robbert Krebbers committed
240
    lsplit #l
Robbert Krebbers's avatar
Robbert Krebbers committed
241
  {{{ k xs1 xs2, RET #k;  xs = xs1 ++ xs2   llist I l xs1  llist I k xs2 }}}.
Robbert Krebbers's avatar
Robbert Krebbers committed
242 243 244 245 246 247 248 249
Proof.
  iIntros (Φ) "Hl HΦ". wp_lam.
  wp_apply (llength_spec with "Hl"); iIntros "Hl". wp_pures.
  rewrite Z.quot_div_nonneg; [|lia..]. rewrite -(Z2Nat_inj_div _ 2).
  wp_apply (lsplit_at_spec with "Hl"); iIntros (k) "[Hl Hk]".
  iApply "HΦ". iFrame. by rewrite take_drop.
Qed.
End lists.