-
Notifications
You must be signed in to change notification settings - Fork 5
/
Copy pathheap_lang.v
196 lines (161 loc) · 5.65 KB
/
heap_lang.v
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
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
From iris.program_logic Require Export weakestpre total_weakestpre.
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.
Set Default Proof Using "Type".
Section tests.
Context `{heapG Σ}.
Implicit Types P Q : iProp Σ.
Implicit Types Φ : val → iProp Σ.
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.
Definition val_scope_test_1 := SOMEV (#(), #()).
Definition heap_e : expr :=
let: "x" := ref #1 in "x" <- !"x" + #1 ;; !"x".
Lemma heap_e_spec E : WP heap_e @ E {{ v, ⌜v = #2⌝ }}%I.
Proof.
iIntros "". rewrite /heap_e. Show.
wp_alloc l as "?". wp_load. Show.
wp_store. by wp_load.
Qed.
Definition heap_e2 : expr :=
let: "x" := ref #1 in
let: "y" := ref #1 in
"x" <- !"x" + #1 ;; !"x".
Lemma heap_e2_spec E : WP heap_e2 @ E [{ v, ⌜v = #2⌝ }]%I.
Proof.
iIntros "". rewrite /heap_e2.
wp_alloc l as "Hl". Show. wp_alloc l'.
wp_load. wp_store. wp_load. done.
Qed.
Definition heap_e3 : expr :=
let: "x" := #true in
let: "f" := λ: "z", "z" + #1 in
if: "x" then "f" #0 else "f" #1.
Lemma heap_e3_spec E : WP heap_e3 @ E [{ v, ⌜v = #1⌝ }]%I.
Proof.
iIntros "". rewrite /heap_e3.
by repeat (wp_pure _).
Qed.
Definition heap_e4 : expr :=
let: "x" := (let: "y" := ref (ref #1) in ref "y") in
! ! !"x".
Lemma heap_e4_spec : WP heap_e4 [{ v, ⌜ v = #1 ⌝ }]%I.
Proof.
rewrite /heap_e4. wp_alloc l. wp_alloc l'.
wp_alloc l''. by repeat wp_load.
Qed.
Definition heap_e5 : expr :=
let: "x" := ref (ref #1) in ! ! "x" + FAA (!"x") (#10 + #1).
Lemma heap_e5_spec E : WP heap_e5 @ E [{ v, ⌜v = #13⌝ }]%I.
Proof.
rewrite /heap_e5. wp_alloc l. wp_alloc l'.
wp_load. wp_faa. do 2 wp_load. by wp_pures.
Qed.
Definition heap_e6 : val := λ: "v", "v" = "v".
Lemma heap_e6_spec (v : val) : (WP heap_e6 v {{ w, ⌜ w = #true ⌝ }})%I.
Proof. wp_lam. wp_op. by case_bool_decide. Qed.
Definition FindPred : val :=
rec: "pred" "x" "y" :=
let: "yp" := "y" + #1 in
if: "yp" < "x" then "pred" "x" "yp" else "y".
Definition Pred : val :=
λ: "x",
if: "x" ≤ #0 then -FindPred (-"x" + #2) #0 else FindPred "x" #0.
Lemma FindPred_spec n1 n2 E Φ :
n1 < n2 →
Φ #(n2 - 1) -∗ WP FindPred #n2 #n1 @ E [{ Φ }].
Proof.
iIntros (Hn) "HΦ".
iInduction (Z.gt_wf n2 n1) as [n1' _] "IH" forall (Hn).
wp_rec. wp_pures. case_bool_decide; wp_if.
- iApply ("IH" with "[%] [%] HΦ"); omega.
- by assert (n1' = n2 - 1) as -> by omega.
Qed.
Lemma Pred_spec n E Φ : Φ #(n - 1) -∗ WP Pred #n @ E [{ Φ }].
Proof.
iIntros "HΦ". wp_lam.
wp_op. case_bool_decide.
- wp_apply FindPred_spec; first omega. wp_pures.
by replace (n - 1) with (- (-n + 2 - 1)) by omega.
- wp_apply FindPred_spec; eauto with omega.
Qed.
Lemma Pred_user E :
WP let: "x" := Pred #42 in Pred "x" @ E [{ v, ⌜v = #40⌝ }]%I.
Proof. iIntros "". wp_apply Pred_spec. by wp_apply Pred_spec. Qed.
Lemma wp_apply_evar e P :
P -∗ (∀ Q Φ, Q -∗ WP e {{ Φ }}) -∗ WP e {{ _, True }}.
Proof. iIntros "HP HW". wp_apply "HW". iExact "HP". Qed.
Lemma wp_cas l v :
val_is_unboxed v →
l ↦ v -∗ WP CAS #l v v {{ _, True }}.
Proof.
iIntros (?) "?". wp_cas as ? | ?. done. done.
Qed.
Lemma wp_alloc_split :
WP Alloc #0 {{ _, True }}%I.
Proof. wp_alloc l as "[Hl1 Hl2]". Show. done. Qed.
Lemma wp_alloc_drop :
WP Alloc #0 {{ _, True }}%I.
Proof. wp_alloc l as "_". Show. done. Qed.
Check "wp_nonclosed_value".
Lemma wp_nonclosed_value :
WP let: "x" := #() in (λ: "y", "x")%V #() {{ _, True }}%I.
Proof. wp_let. wp_lam. Fail wp_pure _. Show. Abort.
End tests.
Section printing_tests.
Context `{heapG Σ}.
(* 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. *)
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.
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.
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.
End printing_tests.
Section error_tests.
Context `{heapG Σ}.
Check "not_cas".
Lemma not_cas :
(WP #() #() {{ _, True }})%I.
Proof.
Fail wp_cas_suc.
Abort.
End error_tests.
Lemma heap_e_adequate σ : adequate NotStuck heap_e σ (λ v _, v = #2).
Proof. eapply (heap_adequacy heapΣ)=> ?. by apply heap_e_spec. Qed.