lists.v 6.72 KB
Newer Older
1
(** TODO: this file should be updated to not break the C-language abstraction *)
2
From iris_c.vcgen Require Import proofmode.
3

4
Definition a_list_nil : val := λ:<>, c_ret NONEV.
5 6

Definition a_list_data : val := λ: "x",
7
   c_bind (λ: "s",
8 9
     match: "s" with
       NONE => assert: #false
10
     | SOME "l" => (c_bind (λ: "p", c_ret (Fst "p")) (c_load (c_ret "l")))
11 12 13
     end) "x".

Definition a_list_next : val := λ: "x",
14
   c_bind (λ: "s",
15 16
     match: "s" with
       NONE => assert: #false
17
     | SOME "l" => (c_bind (λ: "p", c_ret (Snd "p")) (c_load (c_ret "l")))
18 19
     end) "x".

Dan Frumin's avatar
Dan Frumin committed
20
(* TODO: generalize the function below to set an arbitrary node in the list *)
21
Definition a_list_set_next : val := λ: "x" "y",
22
  c_bind (λ: "xs",
23 24 25
    match: "xs" with
      NONE => assert: #false
    | SOME "l" =>
26 27 28 29 30
      c_bind (λ:"p",
         c_bind ( λ: "r",
           c_store (c_ret "l") (c_ret (Fst "p", "r")))
         (c_load "y"))
      (c_load (c_ret "l"))
31 32 33
    end) "x".

Definition a_list_store_next : val := λ: "x1" "x2",
34
  c_bind (λ: "p",
35 36
    match: Fst "p" with
      NONE => assert: #false
37 38
    | SOME "l" => c_bind (λ:"m", c_store (c_ret "l") (c_ret (Fst "m", Snd "p")))
                 (c_load (c_ret "l"))
39
    end)
40
  (c_par "x1" "x2").
41 42

Definition in_place_reverse : val := λ: "hd",
43
  c_bind (λ: "i", a_bind (λ: "j",
44
    a_while
45 46 47 48 49 50 51 52
      (λ:<>, a_un_op NegOp (c_bin_op EqOp (c_load (c_ret "i")) (c_ret NONEV)))
      (λ:<>, c_bind (λ: "k",
               a_list_store_next (c_load (c_ret "i")) (a_load (c_ret "j")) ;
               c_store (c_ret "j") (c_load (c_ret "i"))  ;
               c_store (c_ret "i") (c_load (c_ret "k")))
             (a_alloc 1 (a_list_next (c_load (c_ret "i"))))) ;
    (c_load (c_ret "j"))
  ) (a_alloc 1 (c_ret NONEV))) (a_alloc 1 (c_ret "hd")).
53

54
Section list_spec.
55
  Context `{cmonadG Σ}.
56 57 58 59

  Fixpoint is_list (hd : val) (xs : list val) : iProp Σ :=
    match xs with
    | [] => hd = NONEV
Dan Frumin's avatar
Dan Frumin committed
60
    | x :: xs =>  (l:cloc) hd', hd = SOMEV (cloc_to_val l)  l C (x,hd')  is_list hd' xs
61 62 63
  end%I.

  Lemma a_list_nil_spec R Φ:
64 65
    Φ NONEV - cwp (a_list_nil #()) R Φ.
  Proof. iIntros "H"; cwp_lam; by cwp_ret_value. Qed.
66 67

  Lemma a_list_next_spec (e: expr) R Φ :
68
    cwp e R (λ v,
Dan Frumin's avatar
Dan Frumin committed
69
        (l:cloc) hd x xs, v = SOMEV (cloc_to_val l)  l C (x, hd)  is_list hd xs 
70
          (l C (x, hd) - is_list hd xs - Φ hd)) -
71
    cwp (a_list_next e) R Φ.
72 73
  Proof.
    iIntros "H". rewrite/ a_list_next.
74 75
    cwp_apply (cwp_cwp R with "H").
    - iIntros (v) "H". cwp_lam. iApply cwp_bind. iApply (cwp_wand  with "H").
76
      iIntros (v0) "H". iDestruct "H" as (i hd x xs) "[->  [Hi [Hlst HΦ]]]".
77 78 79
      cwp_let. cwp_match. iApply cwp_bind.
      cwp_load_ret i. iIntros "Hi". iSpecialize ("HΦ" with "Hi Hlst").
      cwp_let. iApply cwp_ret. wp_proj. iFrame.
80 81 82
  Qed.
End list_spec.

Dan Frumin's avatar
Dan Frumin committed
83
Section in_place_reversal.
84
  Context `{cmonadG Σ}.
85

86
  Lemma a_list_store_next_spec e1 e2 Ψ1 Ψ2 R Φ :
87
    cwp e1 R (λ v,  (hd:cloc) x old,
Dan Frumin's avatar
Dan Frumin committed
88
      v = SOMEV (cloc_to_val hd)  hd C (x, old)  Ψ1 (x, SOMEV (cloc_to_val hd))) -
89
    cwp e2 R Ψ2 -
Dan Frumin's avatar
Dan Frumin committed
90
    ( (hd : cloc) x new, Ψ1 (x, SOMEV (cloc_to_val hd)) - Ψ2 new -
91
       (hd C[LLvl] (x, new) - Φ (x, new)%V)) -
92
    cwp (a_list_store_next e1 e2) R Φ.
93
  Proof.
94
    iIntros "H1 H2 HΦ".
95 96 97
    cwp_apply (cwp_cwp with "H1"); iIntros (v1) "H1"; cwp_lam.
    cwp_apply (cwp_cwp with "H2"); iIntros (v2) "H2"; cwp_lam.
    iApply cwp_bind. iApply (cwp_par with "H1 H2").
98 99
    iIntros "!>" (w1 w2) "H1 H2 !>".
    iDestruct "H1" as (hd x nxt ->) "(Hhd & HΨ1)".
100 101
    do 4 cwp_pure _. iApply cwp_bind. cwp_load_ret hd. iIntros "Hd".
    cwp_let. iApply c_store_ret. do 2 cwp_proj; cwp_ret_value.
102 103
    iExists (x, nxt)%V. iFrame. iIntros "Hd".
    iSpecialize ("HΦ" $! hd x with "HΨ1 H2"). by iApply "HΦ".
104 105 106 107
  Qed.

  Lemma in_place_reverse_spec (hd:val) xs R:
    is_list hd xs -
108
    cwp (in_place_reverse hd) R (λ v, is_list v (reverse xs)).
109
  Proof.
110 111 112
    iIntros "Hlst". cwp_lam.
    iApply cwp_bind; cwp_alloc_ret i "[Hi _]".
    iApply cwp_bind; cwp_alloc_ret j "[Hj _]".
113 114 115
    compute[cloc_add]. rewrite !Nat.add_0_r.
    assert ((i.1, i.2) = i) as -> by (destruct i; auto).
    assert ((j.1, j.2) = j) as -> by (destruct j; auto).
116
    iApply a_sequence_spec'. iNext.
117 118
    iApply (a_while_inv_spec ( ls rs rhd hd, i C hd  is_list hd ls 
      j C rhd  is_list rhd rs  (reverse rs)++ls=xs)%I with "[Hlst Hj Hi]").
119 120 121
    - iExists xs, [], (InjLV #()), hd; eauto with iFrame.
    - iModIntro; iIntros "H". clear hd.
      iDestruct "H" as (ls rs rhd hd) "(Hi & Hls & Hj & Hrs & %)".
122
      iApply a_un_op_spec. iApply (c_bin_op_spec _ _
123
        (λ x, x = hd  i C hd)%I (λ x, x = NONEV)%I  with "[Hi] [] [-]").
124
      { cwp_load_ret i. } { cwp_ret_value. }
125
      iNext. iIntros (? ?) "[-> Hi ] ->". destruct ls.
126 127
      + rewrite{1}/ is_list. iDestruct "Hls" as "->".
        iExists #true; iSplit; first done. iExists #false; iSplit; first done.
128
        iLeft; iSplit; first done. do 2 iModIntro. cwp_load_ret j.
129
        iIntros "_". simplify_eq /=. by rewrite app_nil_r reverse_involutive.
130 131
      + iDestruct "Hls" as (l lnxt) "(-> & Hl & Hls)". fold is_list.
        iExists #false; iSplit; first done; iExists #true; iSplit; first done.
132
        iRight. iSplit; first done. iApply cwp_bind.
Dan Frumin's avatar
Dan Frumin committed
133
        iNext. iApply (a_alloc_spec _ _ (λ v, v = #1) with "[] [-]")%I.
134
        { iApply cwp_ret. by wp_value_head. }
Dan Frumin's avatar
Dan Frumin committed
135
        iApply a_list_next_spec.
136
        cwp_load_ret i. iIntros "Hi". iExists l, lnxt, v, ls.
137
        iSplit; first done. iFrame. iIntros "Hl Hls".
Dan Frumin's avatar
Dan Frumin committed
138
        iNext. iIntros (? ->). iExists 1%nat; iSplit; eauto.
139
        iIntros (k) "[Hk _]". cwp_let. iApply a_sequence_spec'; iNext.
140 141
        compute[cloc_add]. rewrite !Nat.add_0_r.
        assert ((k.1, k.2) = k) as -> by (destruct k; auto).
142
        iApply (a_list_store_next_spec _ _
143 144
          (λ z, z = (v, SOMEV (cloc_to_val l))  i C (SOMEV (cloc_to_val l))  )%I
          (λ v, v = rhd  j C rhd)%I  with "[Hi Hl] [Hj]").
145 146
        { cwp_load_ret i. eauto 42 with iFrame. }
        { cwp_load_ret j. }
Dan Frumin's avatar
Dan Frumin committed
147 148 149
        iIntros (a0 ? ?) "(% & Hi)  (% & Hj)". simplify_eq/=.
        (* TODO: this is annoying *)
        assert (a0 = l) as ->. { by destruct l,a0; simplify_eq/=. }
150
        iIntros "Hl". iModIntro. iApply a_sequence_spec'; iNext.
151
        iApply (a_move_spec with "[$Hj $Hi Hls Hrs Hk Hl]").
152
        iIntros "Hi Hj". iModIntro.
153
        iApply (a_move_spec with "[$Hi $Hk Hls Hrs Hj Hl]").
Dan Frumin's avatar
Dan Frumin committed
154
        iIntros "Hk Hi". iModIntro. iExists ls, (v :: rs), (InjRV (cloc_to_val l)), lnxt.
155 156 157 158
        iFrame. iSplit.
        * iExists l, rhd; iSplit; first done; iFrame.
        * iPureIntro. simplify_eq. by rewrite cons_middle assoc -reverse_cons.
  Qed.
Dan Frumin's avatar
Dan Frumin committed
159
End in_place_reversal.
Dan Frumin's avatar
Dan Frumin committed
160