heap_lang.v 8.57 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Φ"); lia.
    - by assert (n1' = n2 - 1) as -> by lia.
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
    wp_op. case_bool_decide.
115
116
117
    - wp_apply FindPred_spec; first lia. wp_pures.
      by replace (n - 1) with (- (-n + 2 - 1)) by lia.
    - wp_apply FindPred_spec; eauto with lia.
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

Robbert Krebbers's avatar
Robbert Krebbers committed
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
  Definition Id : val :=
    rec: "go" "x" :=
      if: "x" = #0 then #() else "go" ("x" - #1).

  (** These tests specially test the handling of the [vals_compare_safe]
  side-condition of the [=] operator. *)
  Lemma Id_wp (n : nat) :  WP Id #n {{ v,  v = #()  }}.
  Proof.
    iInduction n as [|n] "IH"; wp_rec; wp_pures; first done.
    by replace (S n - 1) with (n:Z) by lia.
  Qed.
  Lemma Id_twp (n : nat) :  WP Id #n [{ v,  v = #()  }].
  Proof.
    iInduction n as [|n] "IH"; wp_rec; wp_pures; first done.
    by replace (S n - 1) with (n:Z) by lia.
  Qed.

Ralf Jung's avatar
Ralf Jung committed
141
142
143
  Lemma wp_apply_evar e P :
    P - ( Q Φ, Q - WP e {{ Φ }}) - WP e {{ _, True }}.
  Proof. iIntros "HP HW". wp_apply "HW". iExact "HP". Qed.
144

Ralf Jung's avatar
Ralf Jung committed
145
  Lemma wp_cmpxchg l v :
146
    val_is_unboxed v 
Ralf Jung's avatar
Ralf Jung committed
147
    l  v - WP CmpXchg #l v v {{ _, True }}.
148
  Proof.
Ralf Jung's avatar
Ralf Jung committed
149
    iIntros (?) "?". wp_cmpxchg as ? | ?. done. done.
150
151
  Qed.

Ralf Jung's avatar
Ralf Jung committed
152
  Lemma wp_alloc_split :
Gregory Malecha's avatar
Gregory Malecha committed
153
     WP Alloc #0 {{ _, True }}.
Ralf Jung's avatar
Ralf Jung committed
154
155
156
  Proof. wp_alloc l as "[Hl1 Hl2]". Show. done. Qed.

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

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

Amin Timany's avatar
Amin Timany committed
165
  Lemma wp_alloc_array n : 0 < n 
Gregory Malecha's avatar
Gregory Malecha committed
166
167
168
     {{{ True }}}
        AllocN #n #0
      {{{ l, RET #l;  l ↦∗ replicate (Z.to_nat n) #0}}}.
Amin Timany's avatar
Amin Timany committed
169
  Proof.
170
    iIntros (? Φ) "!> _ HΦ".
Amin Timany's avatar
Amin Timany committed
171
172
173
174
    wp_alloc l as "?"; first done.
    by iApply "HΦ".
  Qed.

175
  Lemma twp_alloc_array n : 0 < n 
Gregory Malecha's avatar
Gregory Malecha committed
176
177
178
     [[{ True }]]
        AllocN #n #0
      [[{ l, RET #l; l ↦∗ replicate (Z.to_nat n) #0}]].
179
180
181
182
183
184
  Proof.
    iIntros (? Φ) "!> _ HΦ".
    wp_alloc l as "?"; first done. Show.
    by iApply "HΦ".
  Qed.

Ralf Jung's avatar
Ralf Jung committed
185
186
187
188
  Lemma wp_load_array l :
    {{{ l ↦∗ [ #0;#1;#2 ] }}} !(#l + #1) {{{ RET #1; True }}}.
  Proof.
    iIntros (Φ) "Hl HΦ". wp_op.
189
    wp_apply (wp_load_offset _ _ _ _ 1 with "Hl"); first done.
Ralf Jung's avatar
Ralf Jung committed
190
191
192
    iIntros "Hl". by iApply "HΦ".
  Qed.

193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
  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.

208
209
210
  Lemma test_array_app l vs1 vs2 :
    l ↦∗ (vs1 ++ vs2) - l ↦∗ (vs1 ++ vs2).
  Proof.
211
212
    iIntros "H". iDestruct (array_app with "H") as "[H1 H2]".
    iApply array_app. iSplitL "H1"; done.
213
214
  Qed.

215
216
217
218
219
220
  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.

221
222
End tests.

Ralf Jung's avatar
Ralf Jung committed
223
224
225
226
Section notation_tests.
  Context `{!heapG Σ, inv_heapG loc val Σ}.

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

231
Section printing_tests.
232
  Context `{!heapG Σ}.
233

234
235
236
237
238
239
  Lemma ref_print :
    True - WP let: "f" := (λ: "x", "x") in ref ("f" #10) {{ _, True }}.
  Proof.
    iIntros "_". Show.
  Abort.

240
241
242
243
  (* 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. *)

244
245
246
247
248
249
250
251
252
  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.

253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
  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
271
272
273
274
275
276
277
278
279
  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.

280
End printing_tests.
281

282
Section error_tests.
283
  Context `{!heapG Σ}.
284

Ralf Jung's avatar
Ralf Jung committed
285
286
  Check "not_cmpxchg".
  Lemma not_cmpxchg :
Gregory Malecha's avatar
Gregory Malecha committed
287
     WP #() #() {{ _, True }}.
288
  Proof.
Ralf Jung's avatar
Ralf Jung committed
289
    Fail wp_cmpxchg_suc.
290
  Abort.
291
292
End error_tests.

293
Lemma heap_e_adequate σ : adequate NotStuck heap_e σ (λ v _, v = #2).
294
Proof. eapply (heap_adequacy heapΣ)=> ?. by apply heap_e_spec. Qed.