heap_lang.v 13.2 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.
6
Set Default Proof Using "Type".
Ralf Jung's avatar
Ralf Jung committed
7

8
9
Unset Mangle Names.

10
Section tests.
11
  Context `{!heapG Σ}.
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
179
180
181
182
183
  Check "(t)wp_bind_fail".
  Lemma wp_bind_fail :  WP #() {{ v, True }}.
  Proof. Fail wp_bind (!_)%E. Abort.
  Lemma twp_bind_fail :  WP #() [{ v, True }].
  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
189
190
  Lemma wp_pures_val (b : bool) :
     WP #b {{ _, True }}.
  Proof. wp_pures. done. Qed.
Ralf Jung's avatar
Ralf Jung committed
191
192
193
  Lemma twp_pures_val (b : bool) :
     WP #b [{ _, True }].
  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. done.
200
201
  Qed.

Ralf Jung's avatar
Ralf Jung committed
202
  Lemma wp_alloc_split :
Gregory Malecha's avatar
Gregory Malecha committed
203
     WP Alloc #0 {{ _, True }}.
Ralf Jung's avatar
Ralf Jung committed
204
205
206
  Proof. wp_alloc l as "[Hl1 Hl2]". Show. done. Qed.

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

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

215
216
  Lemma wp_alloc_array n :
    (0 < n)%Z 
Gregory Malecha's avatar
Gregory Malecha committed
217
218
     {{{ True }}}
        AllocN #n #0
219
      {{{ l, RET #l;  l ↦∗ replicate (Z.to_nat n) #0 }}}.
Amin Timany's avatar
Amin Timany committed
220
  Proof.
221
    iIntros (? Φ) "!> _ HΦ".
Amin Timany's avatar
Amin Timany committed
222
223
224
225
    wp_alloc l as "?"; first done.
    by iApply "HΦ".
  Qed.

226
227
  Lemma twp_alloc_array n :
    (0 < n)%Z 
Gregory Malecha's avatar
Gregory Malecha committed
228
229
     [[{ True }]]
        AllocN #n #0
230
      [[{ l, RET #l; l ↦∗ replicate (Z.to_nat n) #0 }]].
231
232
233
234
235
236
  Proof.
    iIntros (? Φ) "!> _ HΦ".
    wp_alloc l as "?"; first done. Show.
    by iApply "HΦ".
  Qed.

Ralf Jung's avatar
Ralf Jung committed
237
238
239
240
  Lemma wp_load_array l :
    {{{ l ↦∗ [ #0;#1;#2 ] }}} !(#l + #1) {{{ RET #1; True }}}.
  Proof.
    iIntros (Φ) "Hl HΦ". wp_op.
241
    wp_apply (wp_load_offset _ _ _ _ 1 with "Hl"); first done.
Ralf Jung's avatar
Ralf Jung committed
242
243
244
    iIntros "Hl". by iApply "HΦ".
  Qed.

245
246
  Check "test_array_fraction_destruct".
  Lemma test_array_fraction_destruct l vs :
247
    l ↦∗ vs - l ↦∗{#1/2} vs  l ↦∗{#1/2} vs.
248
249
250
251
252
253
  Proof.
    iIntros "[Hl1 Hl2]". Show.
    by iFrame.
  Qed.

  Lemma test_array_fraction_combine l vs :
254
    l ↦∗{#1/2} vs - l↦∗{#1/2} vs - l ↦∗ vs.
255
256
257
258
259
  Proof.
    iIntros "Hl1 Hl2".
    iSplitL "Hl1"; by iFrame.
  Qed.

260
261
262
  Lemma test_array_app l vs1 vs2 :
    l ↦∗ (vs1 ++ vs2) - l ↦∗ (vs1 ++ vs2).
  Proof.
263
264
    iIntros "H". iDestruct (array_app with "H") as "[H1 H2]".
    iApply array_app. iSplitL "H1"; done.
265
266
  Qed.

267
  Lemma test_array_app_split l vs1 vs2 :
268
    l ↦∗ (vs1 ++ vs2) - l ↦∗{#1/2} (vs1 ++ vs2).
269
270
271
272
  Proof.
    iIntros "[$ _]". (* splits the fraction, not the app *)
  Qed.

Ralf Jung's avatar
Ralf Jung committed
273
274
275
276
277
278
279
280
281
282
283
  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.
284
285
286
287
288
289
290
291
292
293
294
295
296
297

  Check "test_wp_finish_fupd".
  Lemma test_wp_finish_fupd (v : val) :
     WP v {{ v, |={}=> True }}.
  Proof.
    wp_pures. Show. (* No second fupd was added. *)
  Abort.

  Check "test_twp_finish_fupd".
  Lemma test_twp_finish_fupd (v : val) :
     WP v [{ v, |={}=> True }].
  Proof.
    wp_pures. Show. (* No second fupd was added. *)
  Abort.
298
299
End tests.

300
Section mapsto_tests.
301
302
  Context `{!heapG Σ}.

303
304
305
  (* Test that the different versions of mapsto work with the tactics, parses,
     and prints correctly. *)

306
307
  (* Loading from a persistent points-to predicate in the _persistent_ context. *)
  Lemma persistent_mapsto_load_persistent l v :
308
    {{{ l ↦□ v }}} ! #l {{{ RET v; True }}}.
309
  Proof. iIntros (Φ) "#Hl HΦ". Show. wp_load. by iApply "HΦ". Qed.
310
311
312

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

  Lemma persistent_mapsto_twp_load_persistent l v :
317
    [[{ l ↦□ v }]] ! #l [[{ RET v; True }]].
318
319
320
  Proof. iIntros (Φ) "#Hl HΦ". wp_load. by iApply "HΦ". Qed.

  Lemma persistent_mapsto_twp_load_spatial l v :
321
    [[{ l ↦□ v }]] ! #l [[{ RET v; True }]].
322
323
324
  Proof. iIntros (Φ) "Hl HΦ". wp_load. by iApply "HΦ". Qed.

  Lemma persistent_mapsto_load l (n : nat) :
325
    {{{ l  #n }}} Store #l (! #l + #5) ;; ! #l {{{ RET #(n + 5); l ↦□ #(n + 5) }}}.
326
327
328
329
330
331
332
  Proof.
    iIntros (Φ) "Hl HΦ".
    wp_load. wp_store.
    iMod (mapsto_persist with "Hl") as "#Hl".
    wp_load. by iApply "HΦ".
  Qed.

333
334
335
336
337
338
339
340
  (* Loading from the general mapsto for any [dfrac]. *)
  Lemma general_mapsto dq l v :
    [[{ l {dq} v }]] ! #l [[{ RET v; True }]].
  Proof. 
    iIntros (Φ) "Hl HΦ". Show. wp_load. by iApply "HΦ".
  Qed.

End mapsto_tests.
341

Ralf Jung's avatar
Ralf Jung committed
342
Section inv_mapsto_tests.
Ralf Jung's avatar
Ralf Jung committed
343
  Context `{!heapG Σ}.
Ralf Jung's avatar
Ralf Jung committed
344
345

  (* Make sure these parse and type-check. *)
Ralf Jung's avatar
Ralf Jung committed
346
  Lemma inv_mapsto_own_test (l : loc) :  l _(λ _, True) #5. Abort.
347
  Lemma inv_mapsto_test (l : loc) :  l _(λ _, True) . Abort.
Ralf Jung's avatar
Ralf Jung committed
348
349

  (* Make sure [setoid_rewrite] works. *)
Ralf Jung's avatar
Ralf Jung committed
350
351
  Lemma inv_mapsto_setoid_rewrite (l : loc) (I : val  Prop) :
    ( v, I v  I #true) 
352
     l _(λ v, I v) .
Ralf Jung's avatar
Ralf Jung committed
353
354
355
356
  Proof.
    iIntros (Heq). setoid_rewrite Heq. Show.
  Abort.
End inv_mapsto_tests.
Ralf Jung's avatar
Ralf Jung committed
357

Robbert Krebbers's avatar
Tests.    
Robbert Krebbers committed
358
359
Section atomic.
  Context `{!heapG Σ}.
360
  Implicit Types P Q : iProp Σ.
Robbert Krebbers's avatar
Tests.    
Robbert Krebbers committed
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386

  (* 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.
End atomic.

387
Section printing_tests.
388
  Context `{!heapG Σ}.
389

390
391
392
393
394
395
  Lemma ref_print :
    True - WP let: "f" := (λ: "x", "x") in ref ("f" #10) {{ _, True }}.
  Proof.
    iIntros "_". Show.
  Abort.

396
397
398
399
  (* 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. *)

400
401
402
403
404
405
406
407
408
  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.

409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
  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
427
428
429
430
431
432
433
434
435
  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.

436
End printing_tests.
437

438
Section error_tests.
439
  Context `{!heapG Σ}.
440

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

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