lifting.v 14.2 KB
Newer Older
1
From iris.algebra Require Import auth gmap.
2
From iris.base_logic Require Export gen_heap.
3 4
From iris.program_logic Require Export weakestpre.
From iris.program_logic Require Import ectx_lifting total_ectx_lifting.
5
From iris.heap_lang Require Export lang proph_map.
6
From iris.heap_lang Require Import tactics.
7
From iris.proofmode Require Import tactics.
Ralf Jung's avatar
Ralf Jung committed
8
From stdpp Require Import fin_maps.
9
Set Default Proof Using "Type".
Ralf Jung's avatar
Ralf Jung committed
10

11 12
Class heapG Σ := HeapG {
  heapG_invG : invG Σ;
13
  heapG_gen_heapG :> gen_heapG loc val Σ;
14
  heapG_proph_mapG :> proph_mapG proph_id val Σ
15 16
}.

17
Instance heapG_irisG `{!heapG Σ} : irisG heap_lang Σ := {
18
  iris_invG := heapG_invG;
19 20
  state_interp σ κs _ :=
    (gen_heap_ctx σ.(heap)  proph_map_ctx κs σ.(used_proph_id))%I;
21
  fork_post _ := True%I;
22 23 24 25
}.

(** Override the notations so that scopes and coercions work out *)
Notation "l ↦{ q } v" := (mapsto (L:=loc) (V:=val) l q v%V)
Robbert Krebbers's avatar
Robbert Krebbers committed
26
  (at level 20, q at level 50, format "l  ↦{ q }  v") : bi_scope.
27
Notation "l ↦ v" :=
Robbert Krebbers's avatar
Robbert Krebbers committed
28
  (mapsto (L:=loc) (V:=val) l 1 v%V) (at level 20) : bi_scope.
29
Notation "l ↦{ q } -" := ( v, l {q} v)%I
Robbert Krebbers's avatar
Robbert Krebbers committed
30 31
  (at level 20, q at level 50, format "l  ↦{ q }  -") : bi_scope.
Notation "l ↦ -" := (l {1} -)%I (at level 20) : bi_scope.
32

33 34 35 36 37 38 39 40 41
(** The tactic [inv_head_step] performs inversion on hypotheses of the shape
[head_step]. The tactic will discharge head-reductions starting from values, and
simplifies hypothesis related to conversions from and to values, and finite map
operations. This tactic is slightly ad-hoc and tuned for proving our lifting
lemmas. *)
Ltac inv_head_step :=
  repeat match goal with
  | _ => progress simplify_map_eq/= (* simplify memory stuff *)
  | H : to_val _ = Some _ |- _ => apply of_to_val in H
42
  | H : head_step ?e _ _ _ _ _ |- _ =>
43 44 45 46 47
     try (is_var e; fail 1); (* inversion yields many goals if [e] is a variable
     and can thus better be avoided. *)
     inversion H; subst; clear H
  end.

Tej Chajed's avatar
Tej Chajed committed
48 49
Local Hint Extern 0 (head_reducible _ _) => eexists _, _, _, _; simpl : core.
Local Hint Extern 0 (head_reducible_no_obs _ _) => eexists _, _, _; simpl : core.
50

51
(* [simpl apply] is too stupid, so we need extern hints here. *)
Tej Chajed's avatar
Tej Chajed committed
52 53 54 55 56 57
Local Hint Extern 1 (head_step _ _ _ _ _ _) => econstructor : core.
Local Hint Extern 0 (head_step (CAS _ _ _) _ _ _ _ _) => eapply CasSucS : core.
Local Hint Extern 0 (head_step (CAS _ _ _) _ _ _ _ _) => eapply CasFailS : core.
Local Hint Extern 0 (head_step (Alloc _) _ _ _ _ _) => apply alloc_fresh : core.
Local Hint Extern 0 (head_step NewProph _ _ _ _ _) => apply new_proph_id_fresh : core.
Local Hint Resolve to_of_val : core.
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
Instance into_val_val v : IntoVal (Val v) v.
Proof. done. Qed.
Instance as_val_val v : AsVal (Val v).
Proof. by eexists. Qed.

Local Ltac solve_atomic :=
  apply strongly_atomic_atomic, ectx_language_atomic;
    [inversion 1; naive_solver
    |apply ectxi_language_sub_redexes_are_values; intros [] **; naive_solver].

Instance alloc_atomic s v : Atomic s (Alloc (Val v)).
Proof. solve_atomic. Qed.
Instance load_atomic s v : Atomic s (Load (Val v)).
Proof. solve_atomic. Qed.
Instance store_atomic s v1 v2 : Atomic s (Store (Val v1) (Val v2)).
Proof. solve_atomic. Qed.
Instance cas_atomic s v0 v1 v2 : Atomic s (CAS (Val v0) (Val v1) (Val v2)).
Proof. solve_atomic. Qed.
Instance faa_atomic s v1 v2 : Atomic s (FAA (Val v1) (Val v2)).
Proof. solve_atomic. Qed.
Instance fork_atomic s e : Atomic s (Fork e).
Proof. solve_atomic. Qed.
Instance skip_atomic s  : Atomic s Skip.
Proof. solve_atomic. Qed.
Instance new_proph_atomic s : Atomic s NewProph.
Proof. solve_atomic. Qed.
Instance resolve_proph_atomic s v1 v2 : Atomic s (ResolveProph (Val v1) (Val v2)).
Proof. solve_atomic. Qed.

Ralf Jung's avatar
fix TWP  
Ralf Jung committed
88
Local Ltac solve_exec_safe := intros; subst; do 3 eexists; econstructor; eauto.
89
Local Ltac solve_exec_puredet := simpl; intros; by inv_head_step.
90
Local Ltac solve_pure_exec :=
91
  subst; intros ?; apply nsteps_once, pure_head_step_pure_step;
92
    constructor; [solve_exec_safe | solve_exec_puredet].
93

94 95 96 97 98 99 100 101 102 103 104 105 106 107
(** The behavior of the various [wp_] tactics with regard to lambda differs in
the following way:

- [wp_pures] does *not* reduce lambdas/recs that are hidden behind a definition.
- [wp_rec] and [wp_lam] reduce lambdas/recs that are hidden behind a definition.

To realize this behavior, we define the class [AsRecV v f x erec], which takes a
value [v] as its input, and turns it into a [RecV f x erec] via the instance
[AsRecV_recv : AsRecV (RecV f x e) f x e]. We register this instance via
[Hint Extern] so that it is only used if [v] is syntactically a lambda/rec, and
not if [v] contains a lambda/rec that is hidden behind a definition.

To make sure that [wp_rec] and [wp_lam] do reduce lambdas/recs that are hidden
behind a definition, we activate [AsRecV_recv] by hand in these tactics. *)
108 109
Class AsRecV (v : val) (f x : binder) (erec : expr) :=
  as_recv : v = RecV f x erec.
110 111 112 113
Hint Mode AsRecV ! - - - : typeclass_instances.
Definition AsRecV_recv f x e : AsRecV (RecV f x e) f x e := eq_refl.
Hint Extern 0 (AsRecV (RecV _ _ _) _ _ _) =>
  apply AsRecV_recv : typeclass_instances.
114

115 116 117 118 119 120 121 122 123 124 125 126
Instance pure_recc f x (erec : expr) :
  PureExec True 1 (Rec f x erec) (Val $ RecV f x erec).
Proof. solve_pure_exec. Qed.
Instance pure_pairc (v1 v2 : val) :
  PureExec True 1 (Pair (Val v1) (Val v2)) (Val $ PairV v1 v2).
Proof. solve_pure_exec. Qed.
Instance pure_injlc (v : val) :
  PureExec True 1 (InjL $ Val v) (Val $ InjLV v).
Proof. solve_pure_exec. Qed.
Instance pure_injrc (v : val) :
  PureExec True 1 (InjR $ Val v) (Val $ InjRV v).
Proof. solve_pure_exec. Qed.
127

128
Instance pure_beta f x (erec : expr) (v1 v2 : val) `{!AsRecV v1 f x erec} :
129 130 131 132 133
  PureExec True 1 (App (Val v1) (Val v2)) (subst' x v2 (subst' f v1 erec)).
Proof. unfold AsRecV in *. solve_pure_exec. Qed.

Instance pure_unop op v v' :
  PureExec (un_op_eval op v = Some v') 1 (UnOp op (Val v)) (Val v').
134
Proof. solve_pure_exec. Qed.
135

136 137
Instance pure_binop op v1 v2 v' :
  PureExec (bin_op_eval op v1 v2 = Some v') 1 (BinOp op (Val v1) (Val v2)) (Val v').
138
Proof. solve_pure_exec. Qed.
139

140
Instance pure_if_true e1 e2 : PureExec True 1 (If (Val $ LitV $ LitBool true) e1 e2) e1.
141
Proof. solve_pure_exec. Qed.
142

143
Instance pure_if_false e1 e2 : PureExec True 1 (If (Val $ LitV  $ LitBool false) e1 e2) e2.
144
Proof. solve_pure_exec. Qed.
145

146 147
Instance pure_fst v1 v2 :
  PureExec True 1 (Fst (Val $ PairV v1 v2)) (Val v1).
148
Proof. solve_pure_exec. Qed.
149

150 151
Instance pure_snd v1 v2 :
  PureExec True 1 (Snd (Val $ PairV v1 v2)) (Val v2).
152
Proof. solve_pure_exec. Qed.
153

154 155
Instance pure_case_inl v e1 e2 :
  PureExec True 1 (Case (Val $ InjLV v) e1 e2) (App e1 (Val v)).
156
Proof. solve_pure_exec. Qed.
157

158 159
Instance pure_case_inr v e1 e2 :
  PureExec True 1 (Case (Val $ InjRV v) e1 e2) (App e2 (Val v)).
160
Proof. solve_pure_exec. Qed.
161

162
Section lifting.
163
Context `{!heapG Σ}.
164 165 166 167 168
Implicit Types P Q : iProp Σ.
Implicit Types Φ : val  iProp Σ.
Implicit Types efs : list expr.
Implicit Types σ : state.

Ralf Jung's avatar
Ralf Jung committed
169
(** Fork: Not using Texan triples to avoid some unnecessary [True] *)
170
Lemma wp_fork s E e Φ :
Ralf Jung's avatar
Ralf Jung committed
171
   WP e @ s;  {{ _, True }} -  Φ (LitV LitUnit) - WP Fork e @ s; E {{ Φ }}.
172
Proof.
173 174 175
  iIntros "He HΦ". iApply wp_lift_atomic_head_step; [done|].
  iIntros (σ1 κ κs n) "Hσ !>"; iSplit; first by eauto.
  iNext; iIntros (v2 σ2 efs Hstep); inv_head_step. by iFrame.
176
Qed.
177

178
Lemma twp_fork s E e Φ :
Ralf Jung's avatar
Ralf Jung committed
179
  WP e @ s;  [{ _, True }] - Φ (LitV LitUnit) - WP Fork e @ s; E [{ Φ }].
180
Proof.
181 182 183
  iIntros "He HΦ". iApply twp_lift_atomic_head_step; [done|].
  iIntros (σ1 κs n) "Hσ !>"; iSplit; first by eauto.
  iIntros (κ v2 σ2 efs Hstep); inv_head_step. by iFrame.
184 185
Qed.

186
(** Heap *)
187 188
Lemma wp_alloc s E v :
  {{{ True }}} Alloc (Val v) @ s; E {{{ l, RET LitV (LitLoc l); l  v }}}.
189
Proof.
190
  iIntros (Φ) "_ HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
191
  iIntros (σ1 κ κs n) "[Hσ Hκs] !>"; iSplit; first by auto.
192
  iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
193 194 195
  iMod (@gen_heap_alloc with "Hσ") as "[Hσ Hl]"; first done.
  iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
Qed.
196 197
Lemma twp_alloc s E v :
  [[{ True }]] Alloc (Val v) @ s; E [[{ l, RET LitV (LitLoc l); l  v }]].
198
Proof.
199
  iIntros (Φ) "_ HΦ". iApply twp_lift_atomic_head_step_no_fork; auto.
200
  iIntros (σ1 κs n) "[Hσ Hκs] !>"; iSplit; first by auto.
Ralf Jung's avatar
fix TWP  
Ralf Jung committed
201
  iIntros (κ v2 σ2 efs Hstep); inv_head_step.
202
  iMod (@gen_heap_alloc with "Hσ") as "[Hσ Hl]"; first done.
Ralf Jung's avatar
fix TWP  
Ralf Jung committed
203
  iModIntro; iSplit=> //. iSplit; first done. iFrame. by iApply "HΦ".
204
Qed.
205

206
Lemma wp_load s E l q v :
207
  {{{  l {q} v }}} Load (Val $ LitV $ LitLoc l) @ s; E {{{ RET v; l {q} v }}}.
208 209
Proof.
  iIntros (Φ) ">Hl HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
210
  iIntros (σ1 κ κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
211
  iSplit; first by eauto. iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
212 213
  iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
Qed.
214
Lemma twp_load s E l q v :
215
  [[{ l {q} v }]] Load (Val $ LitV $ LitLoc l) @ s; E [[{ RET v; l {q} v }]].
216 217
Proof.
  iIntros (Φ) "Hl HΦ". iApply twp_lift_atomic_head_step_no_fork; auto.
218
  iIntros (σ1 κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
219
  iSplit; first by eauto. iIntros (κ v2 σ2 efs Hstep); inv_head_step.
Ralf Jung's avatar
fix TWP  
Ralf Jung committed
220
  iModIntro; iSplit=> //. iSplit; first done. iFrame. by iApply "HΦ".
221
Qed.
222

223 224 225
Lemma wp_store s E l v' v :
  {{{  l  v' }}} Store (Val $ LitV (LitLoc l)) (Val v) @ s; E
  {{{ RET LitV LitUnit; l  v }}}.
226
Proof.
227
  iIntros (Φ) ">Hl HΦ".
228
  iApply wp_lift_atomic_head_step_no_fork; auto.
229
  iIntros (σ1 κ κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
230
  iSplit; first by eauto. iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
231
  iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
232
  iModIntro. iSplit=>//. iFrame. by iApply "HΦ".
233
Qed.
234 235 236
Lemma twp_store s E l v' v :
  [[{ l  v' }]] Store (Val $ LitV $ LitLoc l) (Val v) @ s; E
  [[{ RET LitV LitUnit; l  v }]].
237
Proof.
238
  iIntros (Φ) "Hl HΦ".
239
  iApply twp_lift_atomic_head_step_no_fork; auto.
240
  iIntros (σ1 κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
241
  iSplit; first by eauto. iIntros (κ v2 σ2 efs Hstep); inv_head_step.
242
  iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
Ralf Jung's avatar
fix TWP  
Ralf Jung committed
243
  iModIntro. iSplit=>//. iSplit; first done. iFrame. by iApply "HΦ".
244
Qed.
245

246 247 248
Lemma wp_cas_fail s E l q v' v1 v2 :
  v'  v1  vals_cas_compare_safe v' v1 
  {{{  l {q} v' }}} CAS (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
249 250
  {{{ RET LitV (LitBool false); l {q} v' }}}.
Proof.
251
  iIntros (?? Φ) ">Hl HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
252
  iIntros (σ1 κ κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
253
  iSplit; first by eauto. iNext; iIntros (v2' σ2 efs Hstep); inv_head_step.
254 255
  iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
Qed.
256 257 258
Lemma twp_cas_fail s E l q v' v1 v2 :
  v'  v1  vals_cas_compare_safe v' v1 
  [[{ l {q} v' }]] CAS (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
259 260
  [[{ RET LitV (LitBool false); l {q} v' }]].
Proof.
261
  iIntros (?? Φ) "Hl HΦ". iApply twp_lift_atomic_head_step_no_fork; auto.
262
  iIntros (σ1 κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
Ralf Jung's avatar
fix TWP  
Ralf Jung committed
263 264
  iSplit; first by eauto. iIntros (κ v2' σ2 efs Hstep); inv_head_step.
  iModIntro; iSplit=> //. iSplit; first done. iFrame. by iApply "HΦ".
265
Qed.
266

267 268 269
Lemma wp_cas_suc s E l v1 v2 :
  vals_cas_compare_safe v1 v1 
  {{{  l  v1 }}} CAS (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
270 271
  {{{ RET LitV (LitBool true); l  v2 }}}.
Proof.
272
  iIntros (? Φ) ">Hl HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
273
  iIntros (σ1 κ κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
274
  iSplit; first by eauto. iNext; iIntros (v2' σ2 efs Hstep); inv_head_step.
275
  iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
276
  iModIntro. iSplit=>//. iFrame. by iApply "HΦ".
277
Qed.
278 279 280
Lemma twp_cas_suc s E l v1 v2 :
  vals_cas_compare_safe v1 v1 
  [[{ l  v1 }]] CAS (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
281 282
  [[{ RET LitV (LitBool true); l  v2 }]].
Proof.
283
  iIntros (? Φ) "Hl HΦ". iApply twp_lift_atomic_head_step_no_fork; auto.
284
  iIntros (σ1 κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
285
  iSplit; first by eauto. iIntros (κ v2' σ2 efs Hstep); inv_head_step.
286
  iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
Ralf Jung's avatar
fix TWP  
Ralf Jung committed
287
  iModIntro. iSplit=>//. iSplit; first done. iFrame. by iApply "HΦ".
288
Qed.
289

290 291
Lemma wp_faa s E l i1 i2 :
  {{{  l  LitV (LitInt i1) }}} FAA (Val $ LitV $ LitLoc l) (Val $ LitV $ LitInt i2) @ s; E
292 293
  {{{ RET LitV (LitInt i1); l  LitV (LitInt (i1 + i2)) }}}.
Proof.
294
  iIntros (Φ) ">Hl HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
295
  iIntros (σ1 κ κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
296
  iSplit; first by eauto. iNext; iIntros (v2' σ2 efs Hstep); inv_head_step.
297
  iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
298
  iModIntro. iSplit=>//. iFrame. by iApply "HΦ".
299
Qed.
300 301
Lemma twp_faa s E l i1 i2 :
  [[{ l  LitV (LitInt i1) }]] FAA (Val $ LitV $ LitLoc l) (Val $ LitV $ LitInt i2) @ s; E
302 303
  [[{ RET LitV (LitInt i1); l  LitV (LitInt (i1 + i2)) }]].
Proof.
304
  iIntros (Φ) "Hl HΦ". iApply twp_lift_atomic_head_step_no_fork; auto.
305
  iIntros (σ1 κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
306
  iSplit; first by eauto. iIntros (κ e2 σ2 efs Hstep); inv_head_step.
307
  iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
Ralf Jung's avatar
fix TWP  
Ralf Jung committed
308
  iModIntro. iSplit=>//. iSplit; first done. iFrame. by iApply "HΦ".
309
Qed.
310 311

Lemma wp_new_proph :
312
  {{{ True }}} NewProph {{{ vs p, RET (LitV (LitProphecy p)); proph p vs }}}.
313 314
Proof.
  iIntros (Φ) "_ HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
315
  iIntros (σ1 κ κs n) "[Hσ HR] !>". iSplit; first by eauto.
316
  iNext; iIntros (v2 σ2 efs Hstep). inv_head_step.
317 318
  iMod (proph_map_new_proph p with "HR") as "[HR Hp]"; first done.
  iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
319 320
Qed.

321 322 323 324
Lemma wp_resolve_proph p vs v :
  {{{ proph p vs }}}
    ResolveProph (Val $ LitV $ LitProphecy p) (Val v)
  {{{ vs', RET (LitV LitUnit); vs = v::vs'  proph p vs' }}}.
325
Proof.
326
  iIntros (Φ) "Hp HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
327 328 329 330 331 332
  iIntros (σ1 κ κs n) "[Hσ HR] !>". iSplit; first by eauto.
  iNext; iIntros (v2 σ2 efs Hstep). inv_head_step.
  iMod (proph_map_resolve_proph p v κs with "[HR Hp]") as "HPost"; first by iFrame.
  iModIntro. iFrame. iSplitR; first done.
  iDestruct "HPost" as (vs') "[HEq [HR Hp]]". iFrame.
  iApply "HΦ". iFrame.
333
Qed.
334

Ralf Jung's avatar
Ralf Jung committed
335
End lifting.