-
Notifications
You must be signed in to change notification settings - Fork 0
Expand file tree
/
Copy pathatomic.v
More file actions
128 lines (105 loc) · 3.96 KB
/
atomic.v
File metadata and controls
128 lines (105 loc) · 3.96 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
From iris.proofmode Require Import tactics.
From iris.program_logic Require Export atomic.
From iris.heap_lang Require Import proofmode notation atomic_heap.
Set Default Proof Using "Type".
Section tests.
Context `{!heapG Σ} {aheap: atomic_heap Σ}.
Import atomic_heap.notation.
(* FIXME: removing the `val` type annotation breaks printing. *)
Lemma test_awp_apply_without (Q : iProp Σ) (l : loc) v :
Q -∗ l ↦ v -∗ WP !#l {{ _, Q }}.
Proof.
iIntros "HQ Hl". awp_apply load_spec without "HQ". Show.
iAaccIntro with "Hl"; eauto with iFrame.
Qed.
End tests.
(* Test if we get reasonable error messages with non-laterable assertions in the context. *)
Section error.
Context `{!heapG Σ} {aheap: atomic_heap Σ}.
Import atomic_heap.notation.
Check "non_laterable".
Lemma non_laterable (P : iProp Σ) (l : loc) :
P -∗ WP !#l {{ _, True }}.
Proof.
iIntros "HP". wp_apply load_spec. Fail iAuIntro.
Restart.
iIntros "HP". Fail awp_apply load_spec.
Abort.
End error.
(* Test if AWP and the AU obtained from AWP print. *)
Check "printing".
Section printing.
Context `{!heapG Σ}.
Definition code : expr := #().
Lemma print_both_quant (P : val → iProp Σ) :
⊢ <<< ∀ x, P x >>> code @ ⊤ <<< ∃ y, P y, RET #() >>>.
Proof.
Show. iIntros (Φ) "AU". Show.
iPoseProof (aupd_aacc with "AU") as "?". Show.
Abort.
Lemma print_first_quant l :
⊢ <<< ∀ x, l ↦ x >>> code @ ⊤ <<< l ↦ x, RET #() >>>.
Proof.
Show. iIntros (Φ) "AU". Show.
iPoseProof (aupd_aacc with "AU") as "?". Show.
Abort.
Lemma print_second_quant l :
⊢ <<< l ↦ #() >>> code @ ⊤ <<< ∃ y, l ↦ y, RET #() >>>.
Proof.
Show. iIntros (Φ) "AU". Show.
iPoseProof (aupd_aacc with "AU") as "?". Show.
Abort.
Lemma print_no_quant l :
⊢ <<< l ↦ #() >>> code @ ⊤ <<< l ↦ #(), RET #() >>>.
Proof.
Show. iIntros (Φ) "AU". Show.
iPoseProof (aupd_aacc with "AU") as "?". Show.
Abort.
Check "Now come the long pre/post tests".
Lemma print_both_quant_long l :
⊢ <<< ∀ x, l ↦ x ∗ l ↦ x >>> code @ ⊤ <<< ∃ y, l ↦ y, RET #() >>>.
Proof.
Show. iIntros (Φ) "AU". Show.
Abort.
Lemma print_both_quant_longpre l :
⊢ <<< ∀ x, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>> code @ ⊤ <<< ∃ y, l ↦ y, RET #() >>>.
Proof.
Show. iIntros (Φ) "AU". Show.
Abort.
Lemma print_both_quant_longpost l :
⊢ <<< ∀ xx, l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>> code @ ⊤ <<< ∃ yyyy, l ↦ yyyy ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx, RET #() >>>.
Proof.
Show. iIntros (Φ) "?". Show.
Abort.
Lemma print_first_quant_long l :
⊢ <<< ∀ x, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>> code @ ⊤ <<< l ↦ x, RET #() >>>.
Proof.
Show. iIntros (Φ) "AU". Show.
Abort.
Lemma print_second_quant_long l x :
⊢ <<< l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>> code @ ⊤ <<< ∃ y, l ↦ y, RET #() >>>.
Proof.
Show. iIntros (Φ) "AU". Show.
Abort.
Lemma print_no_quant_long l x :
⊢ <<< l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>> code @ ⊤ <<< l ↦ #(), RET #() >>>.
Proof.
Show. iIntros (Φ) "AU". Show.
Abort.
Lemma print_no_quant_longpre l xx yyyy :
⊢ <<< l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>> code @ ⊤ <<< l ↦ yyyy, RET #() >>>.
Proof.
Show. iIntros (Φ) "AU". Show.
Abort.
Lemma print_no_quant_longpost l xx yyyy :
⊢ <<< l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>> code @ ⊤ <<< l ↦ yyyy ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx, RET #() >>>.
Proof.
Show. iIntros (Φ) "AU". Show.
Abort.
Check "Prettification".
Lemma iMod_prettify (P : val → iProp Σ) :
⊢ <<< ∀ x, P x >>> !#0 @ ⊤ <<< ∃ y, P y, RET #() >>>.
Proof.
iIntros (Φ) "AU". iMod "AU". Show.
Abort.
End printing.