heap_lang.v 8 KB
Newer Older
Ralf Jung's avatar
Ralf Jung committed
1
From iris.base_logic.lib Require Import gen_inv_heap.
2
From iris.program_logic Require Export weakestpre total_weakestpre.
3
4
5
From iris.heap_lang Require Import lang adequacy proofmode notation.
(* Import lang *again*. This used to break notation. *)
From iris.heap_lang Require Import lang.
6
Set Default Proof Using "Type".
Ralf Jung's avatar
Ralf Jung committed
7

8
Section tests.
9
  Context `{!heapG Σ}.
10
11
  Implicit Types P Q : iProp Σ.
  Implicit Types Φ : val  iProp Σ.
12

Robbert Krebbers's avatar
Robbert Krebbers committed
13
14
15
16
17
18
19
20
21
22
  Definition simpl_test :
    (10 = 4 + 6)%nat -
    WP let: "x" := ref #1 in "x" <- !"x";; !"x" {{ v, v = #1 }}.
  Proof.
    iIntros "?". wp_alloc l. repeat (wp_pure _) || wp_load || wp_store.
    match goal with
    | |- context [ (10 = 4 + 6)%nat ] => done
    end.
  Qed.

23
24
  Definition val_scope_test_1 := SOMEV (#(), #()).

25
  Definition heap_e : expr :=
26
    let: "x" := ref #1 in "x" <- !"x" + #1 ;; !"x".
27

Gregory Malecha's avatar
Gregory Malecha committed
28
  Lemma heap_e_spec E :  WP heap_e @ E {{ v, v = #2 }}.
29
  Proof.
30
    iIntros "". rewrite /heap_e. Show.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
31
32
    wp_alloc l as "?". wp_load. Show.
    wp_store. by wp_load.
33
  Qed.
34

35
  Definition heap_e2 : expr :=
36
37
    let: "x" := ref #1 in
    let: "y" := ref #1 in
38
    "x" <- !"x" + #1 ;; !"x".
39

Gregory Malecha's avatar
Gregory Malecha committed
40
  Lemma heap_e2_spec E :  WP heap_e2 @ E [{ v, v = #2 }].
41
  Proof.
42
    iIntros "". rewrite /heap_e2.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
43
44
    wp_alloc l as "Hl". Show. wp_alloc l'.
    wp_load. wp_store. wp_load. done.
45
46
  Qed.

47
48
49
50
51
  Definition heap_e3 : expr :=
    let: "x" := #true in
    let: "f" := λ: "z", "z" + #1 in
    if: "x" then "f" #0 else "f" #1.

Gregory Malecha's avatar
Gregory Malecha committed
52
  Lemma heap_e3_spec E :  WP heap_e3 @ E [{ v, v = #1 }].
53
54
55
56
57
  Proof.
    iIntros "". rewrite /heap_e3.
    by repeat (wp_pure _).
  Qed.

58
59
60
61
  Definition heap_e4 : expr :=
    let: "x" := (let: "y" := ref (ref #1) in ref "y") in
    ! ! !"x".

Gregory Malecha's avatar
Gregory Malecha committed
62
  Lemma heap_e4_spec :  WP heap_e4 [{ v,  v = #1  }].
63
  Proof.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
64
65
    rewrite /heap_e4. wp_alloc l. wp_alloc l'.
    wp_alloc l''. by repeat wp_load.
66
67
  Qed.

68
  Definition heap_e5 : expr :=
69
    let: "x" := ref (ref #1) in ! ! "x" + FAA (!"x") (#10 + #1).
70

Gregory Malecha's avatar
Gregory Malecha committed
71
  Lemma heap_e5_spec E :  WP heap_e5 @ E [{ v, v = #13 }].
72
  Proof.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
73
74
    rewrite /heap_e5. wp_alloc l. wp_alloc l'.
    wp_load. wp_faa. do 2 wp_load. by wp_pures.
75
76
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
77
78
  Definition heap_e6 : val := λ: "v", "v" = "v".

79
  Lemma heap_e6_spec (v : val) :
Gregory Malecha's avatar
Gregory Malecha committed
80
    val_is_unboxed v   WP heap_e6 v {{ w,  w = #true  }}.
81
  Proof. intros ?. wp_lam. wp_op. by case_bool_decide. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
82

Ralf Jung's avatar
Ralf Jung committed
83
  Definition heap_e7 : val := λ: "v", CmpXchg "v" #0 #1.
Robbert Krebbers's avatar
Robbert Krebbers committed
84

85
  Lemma heap_e7_spec_total l : l  #0 - WP heap_e7 #l [{_,  l  #1 }].
Ralf Jung's avatar
Ralf Jung committed
86
  Proof. iIntros. wp_lam. wp_cmpxchg_suc. auto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
87

88
89
  Check "heap_e7_spec".
  Lemma heap_e7_spec l : ^2 l  #0 - WP heap_e7 #l {{_,  l  #1 }}.
Ralf Jung's avatar
Ralf Jung committed
90
  Proof. iIntros. wp_lam. Show. wp_cmpxchg_suc. Show. auto. Qed.
91

92
  Definition FindPred : val :=
Robbert Krebbers's avatar
Robbert Krebbers committed
93
    rec: "pred" "x" "y" :=
94
95
      let: "yp" := "y" + #1 in
      if: "yp" < "x" then "pred" "x" "yp" else "y".
96
  Definition Pred : val :=
97
    λ: "x",
98
      if: "x"  #0 then -FindPred (-"x" + #2) #0 else FindPred "x" #0.
99

100
  Lemma FindPred_spec n1 n2 E Φ :
Robbert Krebbers's avatar
Robbert Krebbers committed
101
    n1 < n2 
102
    Φ #(n2 - 1) - WP FindPred #n2 #n1 @ E [{ Φ }].
103
  Proof.
104
105
    iIntros (Hn) "HΦ".
    iInduction (Z.gt_wf n2 n1) as [n1' _] "IH" forall (Hn).
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
106
    wp_rec. wp_pures. case_bool_decide; wp_if.
107
108
    - iApply ("IH" with "[%] [%] HΦ"); omega.
    - by assert (n1' = n2 - 1) as -> by omega.
109
110
  Qed.

111
  Lemma Pred_spec n E Φ : Φ #(n - 1) - WP Pred #n @ E [{ Φ }].
112
  Proof.
113
    iIntros "HΦ". wp_lam.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
114
115
116
    wp_op. case_bool_decide.
    - wp_apply FindPred_spec; first omega. wp_pures.
      by replace (n - 1) with (- (-n + 2 - 1)) by omega.
Robbert Krebbers's avatar
Robbert Krebbers committed
117
    - wp_apply FindPred_spec; eauto with omega.
118
  Qed.
Ralf Jung's avatar
Ralf Jung committed
119

120
  Lemma Pred_user E :
Gregory Malecha's avatar
Gregory Malecha committed
121
     WP let: "x" := Pred #42 in Pred "x" @ E [{ v, v = #40 }].
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
122
  Proof. iIntros "". wp_apply Pred_spec. by wp_apply Pred_spec. Qed.
123

Ralf Jung's avatar
Ralf Jung committed
124
125
126
  Lemma wp_apply_evar e P :
    P - ( Q Φ, Q - WP e {{ Φ }}) - WP e {{ _, True }}.
  Proof. iIntros "HP HW". wp_apply "HW". iExact "HP". Qed.
127

Ralf Jung's avatar
Ralf Jung committed
128
  Lemma wp_cmpxchg l v :
129
    val_is_unboxed v 
Ralf Jung's avatar
Ralf Jung committed
130
    l  v - WP CmpXchg #l v v {{ _, True }}.
131
  Proof.
Ralf Jung's avatar
Ralf Jung committed
132
    iIntros (?) "?". wp_cmpxchg as ? | ?. done. done.
133
134
  Qed.

Ralf Jung's avatar
Ralf Jung committed
135
  Lemma wp_alloc_split :
Gregory Malecha's avatar
Gregory Malecha committed
136
     WP Alloc #0 {{ _, True }}.
Ralf Jung's avatar
Ralf Jung committed
137
138
139
  Proof. wp_alloc l as "[Hl1 Hl2]". Show. done. Qed.

  Lemma wp_alloc_drop :
Gregory Malecha's avatar
Gregory Malecha committed
140
     WP Alloc #0 {{ _, True }}.
Ralf Jung's avatar
Ralf Jung committed
141
142
  Proof. wp_alloc l as "_". Show. done. Qed.

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
143
  Check "wp_nonclosed_value".
144
  Lemma wp_nonclosed_value :
Gregory Malecha's avatar
Gregory Malecha committed
145
     WP let: "x" := #() in (λ: "y", "x")%V #() {{ _, True }}.
146
147
  Proof. wp_let. wp_lam. Fail wp_pure _. Show. Abort.

Amin Timany's avatar
Amin Timany committed
148
  Lemma wp_alloc_array n : 0 < n 
Gregory Malecha's avatar
Gregory Malecha committed
149
150
151
     {{{ True }}}
        AllocN #n #0
      {{{ l, RET #l;  l ↦∗ replicate (Z.to_nat n) #0}}}.
Amin Timany's avatar
Amin Timany committed
152
  Proof.
153
    iIntros (? Φ) "!> _ HΦ".
Amin Timany's avatar
Amin Timany committed
154
155
156
157
    wp_alloc l as "?"; first done.
    by iApply "HΦ".
  Qed.

158
  Lemma twp_alloc_array n : 0 < n 
Gregory Malecha's avatar
Gregory Malecha committed
159
160
161
     [[{ True }]]
        AllocN #n #0
      [[{ l, RET #l; l ↦∗ replicate (Z.to_nat n) #0}]].
162
163
164
165
166
167
  Proof.
    iIntros (? Φ) "!> _ HΦ".
    wp_alloc l as "?"; first done. Show.
    by iApply "HΦ".
  Qed.

Ralf Jung's avatar
Ralf Jung committed
168
169
170
171
  Lemma wp_load_array l :
    {{{ l ↦∗ [ #0;#1;#2 ] }}} !(#l + #1) {{{ RET #1; True }}}.
  Proof.
    iIntros (Φ) "Hl HΦ". wp_op.
172
    wp_apply (wp_load_offset _ _ _ _ 1 with "Hl"); first done.
Ralf Jung's avatar
Ralf Jung committed
173
174
175
    iIntros "Hl". by iApply "HΦ".
  Qed.

176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
  Check "test_array_fraction_destruct".
  Lemma test_array_fraction_destruct l vs :
    l ↦∗ vs - l ↦∗{1/2} vs  l ↦∗{1/2} vs.
  Proof.
    iIntros "[Hl1 Hl2]". Show.
    by iFrame.
  Qed.

  Lemma test_array_fraction_combine l vs :
    l ↦∗{1/2} vs - l↦∗{1/2} vs - l ↦∗ vs.
  Proof.
    iIntros "Hl1 Hl2".
    iSplitL "Hl1"; by iFrame.
  Qed.

191
192
193
  Lemma test_array_app l vs1 vs2 :
    l ↦∗ (vs1 ++ vs2) - l ↦∗ (vs1 ++ vs2).
  Proof.
194
195
    iIntros "H". iDestruct (array_app with "H") as "[H1 H2]".
    iApply array_app. iSplitL "H1"; done.
196
197
  Qed.

198
199
200
201
202
203
  Lemma test_array_app_split l vs1 vs2 :
    l ↦∗ (vs1 ++ vs2) - l ↦∗{1/2} (vs1 ++ vs2).
  Proof.
    iIntros "[$ _]". (* splits the fraction, not the app *)
  Qed.

204
205
End tests.

Ralf Jung's avatar
Ralf Jung committed
206
Section notation_tests.
Ralf Jung's avatar
Ralf Jung committed
207
  Context `{!heapG Σ}.
Ralf Jung's avatar
Ralf Jung committed
208
209

  (* Make sure these parse and type-check. *)
Ralf Jung's avatar
Ralf Jung committed
210
  Lemma inv_mapsto_own_test (l : loc) :  l _(λ _, True) #5. Abort.
Ralf Jung's avatar
Ralf Jung committed
211
212
213
  Lemma inv_mapsto_test (l : loc) :  l ↦□ (λ _, True). Abort.
End notation_tests.

214
Section printing_tests.
215
  Context `{!heapG Σ}.
216

217
218
219
220
221
222
  Lemma ref_print :
    True - WP let: "f" := (λ: "x", "x") in ref ("f" #10) {{ _, True }}.
  Proof.
    iIntros "_". Show.
  Abort.

223
224
225
226
  (* These terms aren't even closed, but that's not what this is about.  The
  length of the variable names etc. has been carefully chosen to trigger
  particular behavior of the Coq pretty printer. *)

227
228
229
230
231
232
233
234
235
  Lemma wp_print_long_expr (fun1 fun2 fun3 : expr) :
    True - WP let: "val1" := fun1 #() in
       let: "val2" := fun2 "val1" in
       let: "val3" := fun3 "val2" in
       if: "val1" = "val2" then "val" else "val3"  {{ _, True }}.
  Proof.
    iIntros "_". Show.
  Abort.

236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
  Lemma wp_print_long_expr (fun1 fun2 fun3 : expr) Φ :
    True - WP let: "val1" := fun1 #() in
       let: "val2" := fun2 "val1" in
       let: "v" := fun3 "v" in
       if: "v" = "v" then "v" else "v"  {{ Φ }}.
  Proof.
    iIntros "_". Show.
  Abort.

  Lemma wp_print_long_expr (fun1 fun2 fun3 : expr) Φ E :
    True - WP let: "val1" := fun1 #() in
       let: "val2" := fun2 "val1" in
       let: "v" := fun3 "v" in
       if: "v" = "v" then "v" else "v" @ E {{ Φ }}.
  Proof.
    iIntros "_". Show.
  Abort.

Ralf Jung's avatar
Ralf Jung committed
254
255
256
257
258
259
260
261
262
  Lemma texan_triple_long_expr (fun1 fun2 fun3 : expr) :
    {{{ True }}}
       let: "val1" := fun1 #() in
       let: "val2" := fun2 "val1" in
       let: "val3" := fun3 "val2" in
       if: "val1" = "val2" then "val" else "val3"
    {{{ (x y : val) (z : Z), RET (x, y, #z); True }}}.
  Proof. Show. Abort.

263
End printing_tests.
264

265
Section error_tests.
266
  Context `{!heapG Σ}.
267

Ralf Jung's avatar
Ralf Jung committed
268
269
  Check "not_cmpxchg".
  Lemma not_cmpxchg :
Gregory Malecha's avatar
Gregory Malecha committed
270
     WP #() #() {{ _, True }}.
271
  Proof.
Ralf Jung's avatar
Ralf Jung committed
272
    Fail wp_cmpxchg_suc.
273
  Abort.
274
275
End error_tests.

276
Lemma heap_e_adequate σ : adequate NotStuck heap_e σ (λ v _, v = #2).
Ralf Jung's avatar
Ralf Jung committed
277
Proof. eapply (heap_adequacy heapΣ)=> ?. iIntros "_". by iApply heap_e_spec. Qed.