heap_lang.v 13.1 KB
Newer Older
Robbert Krebbers's avatar
Tests.    
Robbert Krebbers committed
1
From iris.base_logic.lib Require Import gen_inv_heap invariants.
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.
Ralf Jung's avatar
Ralf Jung committed
6
From iris.prelude Require Import options.
Ralf Jung's avatar
Ralf Jung committed
7

8
9
Unset Mangle Names.

10
Section tests.
11
  Context `{!heapGS Σ}.
12
13
  Implicit Types P Q : iProp Σ.
  Implicit Types Φ : val  iProp Σ.
14

Robbert Krebbers's avatar
Robbert Krebbers committed
15
16
17
18
19
20
21
22
23
24
  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.

25
26
  Definition val_scope_test_1 := SOMEV (#(), #()).

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

30
  Check "heap_e_spec".
Gregory Malecha's avatar
Gregory Malecha committed
31
  Lemma heap_e_spec E :  WP heap_e @ E {{ v, v = #2 }}.
32
  Proof.
33
    iIntros "". rewrite /heap_e. Show.
34
    wp_alloc l as "?". wp_pures. wp_bind (!_)%E. wp_load. Show. (* No fupd was added *)
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
35
    wp_store. by wp_load.
36
  Qed.
37

38
  Definition heap_e2 : expr :=
39
40
    let: "x" := ref #1 in
    let: "y" := ref #1 in
41
    "x" <- !"x" + #1 ;; !"x".
42

43
  Check "heap_e2_spec".
Gregory Malecha's avatar
Gregory Malecha committed
44
  Lemma heap_e2_spec E :  WP heap_e2 @ E [{ v, v = #2 }].
45
  Proof.
46
    iIntros "". rewrite /heap_e2.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
47
    wp_alloc l as "Hl". Show. wp_alloc l'.
48
49
    wp_pures. wp_bind (!_)%E. wp_load. Show. (* No fupd was added *)
    wp_store. wp_load. done.
50
51
  Qed.

52
53
54
55
56
  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
57
  Lemma heap_e3_spec E :  WP heap_e3 @ E [{ v, v = #1 }].
58
59
60
61
62
  Proof.
    iIntros "". rewrite /heap_e3.
    by repeat (wp_pure _).
  Qed.

63
64
65
66
  Definition heap_e4 : expr :=
    let: "x" := (let: "y" := ref (ref #1) in ref "y") in
    ! ! !"x".

Gregory Malecha's avatar
Gregory Malecha committed
67
  Lemma heap_e4_spec :  WP heap_e4 [{ v,  v = #1  }].
68
  Proof.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
69
70
    rewrite /heap_e4. wp_alloc l. wp_alloc l'.
    wp_alloc l''. by repeat wp_load.
71
72
  Qed.

73
  Definition heap_e5 : expr :=
74
    let: "x" := ref (ref #1) in ! ! "x" + FAA (!"x") (#10 + #1).
75

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

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

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

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

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

93
94
  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
95
  Proof. iIntros. wp_lam. Show. wp_cmpxchg_suc. Show. auto. Qed.
96

97
  Definition FindPred : val :=
Robbert Krebbers's avatar
Robbert Krebbers committed
98
    rec: "pred" "x" "y" :=
99
100
      let: "yp" := "y" + #1 in
      if: "yp" < "x" then "pred" "x" "yp" else "y".
101
  Definition Pred : val :=
102
    λ: "x",
103
      if: "x"  #0 then -FindPred (-"x" + #2) #0 else FindPred "x" #0.
104

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

116
  Lemma Pred_spec n E Φ : Φ #(n - 1) - WP Pred #n @ E [{ Φ }].
117
  Proof.
118
    iIntros "HΦ". wp_lam.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
119
    wp_op. case_bool_decide.
120
    - wp_smart_apply FindPred_spec; first lia. wp_pures.
121
      by replace (n - 1)%Z with (- (-n + 2 - 1))%Z by lia.
122
    - wp_smart_apply FindPred_spec; eauto with lia.
123
  Qed.
Ralf Jung's avatar
Ralf Jung committed
124

125
  Lemma Pred_user E :
Gregory Malecha's avatar
Gregory Malecha committed
126
     WP let: "x" := Pred #42 in Pred "x" @ E [{ v, v = #40 }].
127
  Proof. iIntros "". wp_apply Pred_spec. by wp_smart_apply Pred_spec. Qed.
128

Robbert Krebbers's avatar
Robbert Krebbers committed
129
130
131
132
133
134
135
136
137
  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.
138
    by replace (S n - 1)%Z with (n:Z) by lia.
Robbert Krebbers's avatar
Robbert Krebbers committed
139
140
141
142
  Qed.
  Lemma Id_twp (n : nat) :  WP Id #n [{ v,  v = #()  }].
  Proof.
    iInduction n as [|n] "IH"; wp_rec; wp_pures; first done.
143
    by replace (S n - 1)%Z with (n:Z) by lia.
Robbert Krebbers's avatar
Robbert Krebbers committed
144
145
  Qed.

Ralf Jung's avatar
Ralf Jung committed
146
147
148
149
  (* Make sure [wp_bind] works even when it changes nothing. *)
  Lemma wp_bind_nop (e : expr) :
     WP e + #0 {{ _, True }}.
  Proof. wp_bind (e + #0)%E. Abort.
Ralf Jung's avatar
Ralf Jung committed
150
151
152
  Lemma wp_bind_nop (e : expr) :
     WP e + #0 [{ _, True }].
  Proof. wp_bind (e + #0)%E. Abort.
Ralf Jung's avatar
Ralf Jung committed
153

154
155
  Check "wp_load_fail".
  Lemma wp_load_fail :
Ralf Jung's avatar
Ralf Jung committed
156
     WP Fork #() {{ _, True }}.
157
  Proof. Fail wp_load. Abort.
Ralf Jung's avatar
Ralf Jung committed
158
  Lemma twp_load_fail :
Ralf Jung's avatar
Ralf Jung committed
159
     WP Fork #() [{ _, True }].
160
161
  Proof. Fail wp_load. Abort.
  Check "wp_load_no_ptsto".
Ralf Jung's avatar
Ralf Jung committed
162
  Lemma wp_load_fail_no_ptsto (l : loc) :
163
164
165
166
167
     WP ! #l {{ _, True }}.
  Proof. Fail wp_load. Abort.

  Check "wp_store_fail".
  Lemma wp_store_fail :
Ralf Jung's avatar
Ralf Jung committed
168
     WP Fork #() {{ _, True }}.
169
  Proof. Fail wp_store. Abort.
Ralf Jung's avatar
Ralf Jung committed
170
  Lemma twp_store_fail :
Ralf Jung's avatar
Ralf Jung committed
171
     WP Fork #() [{ _, True }].
172
173
  Proof. Fail wp_store. Abort.
  Check "wp_store_no_ptsto".
Ralf Jung's avatar
Ralf Jung committed
174
  Lemma wp_store_fail_no_ptsto (l : loc) :
175
176
177
     WP #l <- #0 {{ _, True }}.
  Proof. Fail wp_store. Abort.

Tej Chajed's avatar
Tej Chajed committed
178
  Check "(t)wp_bind_fail".
Ralf Jung's avatar
Ralf Jung committed
179
  Lemma wp_bind_fail :  WP of_val #() {{ v, True }}.
Tej Chajed's avatar
Tej Chajed committed
180
  Proof. Fail wp_bind (!_)%E. Abort.
Ralf Jung's avatar
Ralf Jung committed
181
  Lemma twp_bind_fail :  WP of_val #() [{ v, True }].
Tej Chajed's avatar
Tej Chajed committed
182
183
  Proof. Fail wp_bind (!_)%E. Abort.

Ralf Jung's avatar
Ralf Jung committed
184
185
186
  Lemma wp_apply_evar e P :
    P - ( Q Φ, Q - WP e {{ Φ }}) - WP e {{ _, True }}.
  Proof. iIntros "HP HW". wp_apply "HW". iExact "HP". Qed.
187

Ralf Jung's avatar
Ralf Jung committed
188
  Lemma wp_pures_val (b : bool) :
Ralf Jung's avatar
Ralf Jung committed
189
     WP of_val #b {{ _, True }}.
Ralf Jung's avatar
Ralf Jung committed
190
  Proof. wp_pures. done. Qed.
Ralf Jung's avatar
Ralf Jung committed
191
  Lemma twp_pures_val (b : bool) :
Ralf Jung's avatar
Ralf Jung committed
192
     WP of_val #b [{ _, True }].
Ralf Jung's avatar
Ralf Jung committed
193
  Proof. wp_pures. done. Qed.
Ralf Jung's avatar
Ralf Jung committed
194

Ralf Jung's avatar
Ralf Jung committed
195
  Lemma wp_cmpxchg l v :
196
    val_is_unboxed v 
Ralf Jung's avatar
Ralf Jung committed
197
    l  v - WP CmpXchg #l v v {{ _, True }}.
198
  Proof.
Ralf Jung's avatar
Ralf Jung committed
199
    iIntros (?) "?". wp_cmpxchg as ? | ?; done.
200
201
  Qed.

Simon Hudon's avatar
Simon Hudon committed
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
  Lemma wp_xchg l (v v : val) :
    {{{ l  v }}}
      Xchg #l v
    {{{ RET v; l  v }}}.
  Proof.
    iIntros (Φ) "Hl HΦ".
    wp_xchg.
    iApply "HΦ" => //.
  Qed.

   Lemma twp_xchg l (v v : val) :
     l  v -
       WP  Xchg #l v [{ v, l  v }].
  Proof.
    iIntros "Hl".
    wp_xchg => //.
  Qed.

  Lemma wp_xchg_inv N l (v : val) :
    {{{ inv N ( v, l  v) }}}
      Xchg #l v
    {{{ v', RET v'; True }}}.
  Proof.
    iIntros (Φ) "Hl HΦ".
    iInv "Hl" as (v') "Hl" "Hclose".
    wp_xchg.
    iApply "HΦ".
    iApply "Hclose".
    iExists _ => //.
  Qed.

Ralf Jung's avatar
Ralf Jung committed
233
  Lemma wp_alloc_split :
Gregory Malecha's avatar
Gregory Malecha committed
234
     WP Alloc #0 {{ _, True }}.
Ralf Jung's avatar
Ralf Jung committed
235
236
237
  Proof. wp_alloc l as "[Hl1 Hl2]". Show. done. Qed.

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

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

246
247
  Lemma wp_alloc_array n :
    (0 < n)%Z 
Gregory Malecha's avatar
Gregory Malecha committed
248
249
     {{{ True }}}
        AllocN #n #0
250
      {{{ l, RET #l;  l ↦∗ replicate (Z.to_nat n) #0 }}}.
Amin Timany's avatar
Amin Timany committed
251
  Proof.
252
    iIntros (? Φ) "!> _ HΦ".
Amin Timany's avatar
Amin Timany committed
253
254
255
256
    wp_alloc l as "?"; first done.
    by iApply "HΦ".
  Qed.

257
258
  Lemma twp_alloc_array n :
    (0 < n)%Z 
Gregory Malecha's avatar
Gregory Malecha committed
259
260
     [[{ True }]]
        AllocN #n #0
261
      [[{ l, RET #l; l ↦∗ replicate (Z.to_nat n) #0 }]].
262
263
264
265
266
267
  Proof.
    iIntros (? Φ) "!> _ HΦ".
    wp_alloc l as "?"; first done. Show.
    by iApply "HΦ".
  Qed.

Ralf Jung's avatar
Ralf Jung committed
268
269
270
271
  Lemma wp_load_array l :
    {{{ l ↦∗ [ #0;#1;#2 ] }}} !(#l + #1) {{{ RET #1; True }}}.
  Proof.
    iIntros (Φ) "Hl HΦ". wp_op.
272
    wp_apply (wp_load_offset _ _ _ _ 1 with "Hl"); first done.
Ralf Jung's avatar
Ralf Jung committed
273
274
275
    iIntros "Hl". by iApply "HΦ".
  Qed.

276
277
  Check "test_array_fraction_destruct".
  Lemma test_array_fraction_destruct l vs :
278
    l ↦∗ vs - l ↦∗{#1/2} vs  l ↦∗{#1/2} vs.
279
280
281
282
283
284
  Proof.
    iIntros "[Hl1 Hl2]". Show.
    by iFrame.
  Qed.

  Lemma test_array_fraction_combine l vs :
285
    l ↦∗{#1/2} vs - l↦∗{#1/2} vs - l ↦∗ vs.
286
287
288
289
290
  Proof.
    iIntros "Hl1 Hl2".
    iSplitL "Hl1"; by iFrame.
  Qed.

291
292
293
  Lemma test_array_app l vs1 vs2 :
    l ↦∗ (vs1 ++ vs2) - l ↦∗ (vs1 ++ vs2).
  Proof.
294
295
    iIntros "H". iDestruct (array_app with "H") as "[H1 H2]".
    iApply array_app. iSplitL "H1"; done.
296
297
  Qed.

298
  Lemma test_array_app_split l vs1 vs2 :
299
    l ↦∗ (vs1 ++ vs2) - l ↦∗{#1/2} (vs1 ++ vs2).
300
301
302
303
  Proof.
    iIntros "[$ _]". (* splits the fraction, not the app *)
  Qed.

Ralf Jung's avatar
Ralf Jung committed
304
305
306
307
308
309
310
311
312
313
314
  Lemma test_wp_free l v :
    {{{ l  v }}} Free #l {{{ RET #(); True }}}.
  Proof.
    iIntros (Φ) "Hl HΦ". wp_free. iApply "HΦ". done.
  Qed.

  Lemma test_twp_free l v :
    [[{ l  v }]] Free #l [[{ RET #(); True }]].
  Proof.
    iIntros (Φ) "Hl HΦ". wp_free. iApply "HΦ". done.
  Qed.
315
316
317

  Check "test_wp_finish_fupd".
  Lemma test_wp_finish_fupd (v : val) :
Ralf Jung's avatar
Ralf Jung committed
318
     WP of_val v {{ v, |={}=> True }}.
319
320
321
322
323
324
  Proof.
    wp_pures. Show. (* No second fupd was added. *)
  Abort.

  Check "test_twp_finish_fupd".
  Lemma test_twp_finish_fupd (v : val) :
Ralf Jung's avatar
Ralf Jung committed
325
     WP of_val v [{ v, |={}=> True }].
326
327
328
  Proof.
    wp_pures. Show. (* No second fupd was added. *)
  Abort.
329
330
331
332
333
334
335
336
337
338

  Check "test_heaplang_not_unfolded".
  Lemma test_heaplang_not_unfolded :
    @{iPropI Σ} |={}=> True.
  Proof.
    cbn.
    Set Printing All.
    Show.
    Unset Printing All.
  Abort.
339
340
End tests.

341
Section mapsto_tests.
342
  Context `{!heapGS Σ}.
343

344
345
346
  (* Test that the different versions of mapsto work with the tactics, parses,
     and prints correctly. *)

347
348
  (* Loading from a persistent points-to predicate in the _persistent_ context. *)
  Lemma persistent_mapsto_load_persistent l v :
349
    {{{ l ↦□ v }}} ! #l {{{ RET v; True }}}.
350
  Proof. iIntros (Φ) "#Hl HΦ". Show. wp_load. by iApply "HΦ". Qed.
351
352
353

  (* Loading from a persistent points-to predicate in the _spatial_ context. *)
  Lemma persistent_mapsto_load_spatial l v :
354
    {{{ l ↦□ v }}} ! #l {{{ RET v; True }}}.
355
356
357
  Proof. iIntros (Φ) "Hl HΦ". wp_load. by iApply "HΦ". Qed.

  Lemma persistent_mapsto_twp_load_persistent l v :
358
    [[{ l ↦□ v }]] ! #l [[{ RET v; True }]].
359
360
361
  Proof. iIntros (Φ) "#Hl HΦ". wp_load. by iApply "HΦ". Qed.

  Lemma persistent_mapsto_twp_load_spatial l v :
362
    [[{ l ↦□ v }]] ! #l [[{ RET v; True }]].
363
364
365
  Proof. iIntros (Φ) "Hl HΦ". wp_load. by iApply "HΦ". Qed.

  Lemma persistent_mapsto_load l (n : nat) :
366
    {{{ l  #n }}} Store #l (! #l + #5) ;; ! #l {{{ RET #(n + 5); l ↦□ #(n + 5) }}}.
367
368
369
370
371
372
373
  Proof.
    iIntros (Φ) "Hl HΦ".
    wp_load. wp_store.
    iMod (mapsto_persist with "Hl") as "#Hl".
    wp_load. by iApply "HΦ".
  Qed.

374
375
376
  (* Loading from the general mapsto for any [dfrac]. *)
  Lemma general_mapsto dq l v :
    [[{ l {dq} v }]] ! #l [[{ RET v; True }]].
Simon Hudon's avatar
Simon Hudon committed
377
  Proof.
378
379
380
    iIntros (Φ) "Hl HΦ". Show. wp_load. by iApply "HΦ".
  Qed.

Ralf Jung's avatar
Ralf Jung committed
381
382
383
384
385
  (* Make sure that we can split a mapsto containing an evar. *)
  Lemma mapsto_evar_iSplit l v :
    l {#1 / 2} v -   q, l {#1 / 2 + q} v.
  Proof. iIntros "H". iExists _. iSplitL; first by iAssumption. Abort.

386
387
388
389
390
391
392
393
  Lemma mapsto_frame_1 l v q1 q2 :
    l {#q1} v - l {#q2} v - l {#q1 + q2} v.
  Proof. iIntros "H1 H2". iFrame "H1". iExact "H2". Qed.

  Lemma mapsto_frame_2 l v q :
    l {#q/2} v - l {#q/2} v - l {#q} v.
  Proof. iIntros "H1 H2". iFrame "H1". iExact "H2". Qed.

394
End mapsto_tests.
395

Ralf Jung's avatar
Ralf Jung committed
396
Section inv_mapsto_tests.
397
  Context `{!heapGS Σ}.
Ralf Jung's avatar
Ralf Jung committed
398
399

  (* Make sure these parse and type-check. *)
Ralf Jung's avatar
Ralf Jung committed
400
  Lemma inv_mapsto_own_test (l : loc) :  l _(λ _, True) #5. Abort.
401
  Lemma inv_mapsto_test (l : loc) :  l _(λ _, True) . Abort.
Ralf Jung's avatar
Ralf Jung committed
402
403

  (* Make sure [setoid_rewrite] works. *)
Ralf Jung's avatar
Ralf Jung committed
404
405
  Lemma inv_mapsto_setoid_rewrite (l : loc) (I : val  Prop) :
    ( v, I v  I #true) 
406
     l _(λ v, I v) .
Ralf Jung's avatar
Ralf Jung committed
407
408
409
410
  Proof.
    iIntros (Heq). setoid_rewrite Heq. Show.
  Abort.
End inv_mapsto_tests.
Ralf Jung's avatar
Ralf Jung committed
411

Robbert Krebbers's avatar
Tests.    
Robbert Krebbers committed
412
Section atomic.
413
  Context `{!heapGS Σ}.
414
  Implicit Types P Q : iProp Σ.
Robbert Krebbers's avatar
Tests.    
Robbert Krebbers committed
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438

  (* These tests check if a side-condition for [Atomic] is generated *)
  Check "wp_iMod_fupd_atomic".
  Lemma wp_iMod_fupd_atomic E1 E2 P :
    (|={E1,E2}=> P) - WP #() #() @ E1 {{ _, True }}.
  Proof.
    iIntros "H". iMod "H". Show.
  Abort.

  Check "wp_iInv_atomic".
  Lemma wp_iInv_atomic N E P :
     N  E 
    inv N P - WP #() #() @ E {{ _, True }}.
  Proof.
    iIntros (?) "H". iInv "H" as "H" "Hclose". Show.
  Abort.
  Check "wp_iInv_atomic_acc".
  Lemma wp_iInv_atomic_acc N E P :
     N  E 
    inv N P - WP #() #() @ E {{ _, True }}.
  Proof.
    (* Test if a side-condition for [Atomic] is generated *)
    iIntros (?) "H". iInv "H" as "H". Show.
  Abort.
Simon Hudon's avatar
Simon Hudon committed
439

Robbert Krebbers's avatar
Tests.    
Robbert Krebbers committed
440
441
End atomic.

442
Section error_tests.
443
  Context `{!heapGS Σ}.
444

Ralf Jung's avatar
Ralf Jung committed
445
446
  Check "not_cmpxchg".
  Lemma not_cmpxchg :
Gregory Malecha's avatar
Gregory Malecha committed
447
     WP #() #() {{ _, True }}.
448
  Proof.
Ralf Jung's avatar
Ralf Jung committed
449
    Fail wp_cmpxchg_suc.
450
  Abort.
451
452
End error_tests.

Ralf Jung's avatar
Ralf Jung committed
453
(* Test a closed proof *)
454
Lemma heap_e_adequate σ : adequate NotStuck heap_e σ (λ v _, v = #2).
Ralf Jung's avatar
Ralf Jung committed
455
Proof. eapply (heap_adequacy heapΣ)=> ?. iIntros "_". by iApply heap_e_spec. Qed.