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 18
}.

Instance heapG_irisG `{heapG Σ} : irisG heap_lang Σ := {
  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
Class AsRecV (v : val) (f x : binder) (erec : expr) :=
  as_recv : v = RecV f x erec.
Instance AsRecV_recv f x e : AsRecV (RecV f x e) f x e := eq_refl.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
97 98 99 100 101 102 103

(* Pure reductions are automatically performed before any wp_ tactics
   handling impure operations. Since we do not want these tactics to
   unfold locked terms, we do not register this instance explicitely,
   but only activate it by hand in the `wp_rec` tactic, where we
   *actually* want it to unlock. *)
Lemma AsRecV_recv_locked v f x e :
104
  AsRecV v f x e  AsRecV (locked v) f x e.
105 106
Proof. by unlock. Qed.

107 108 109 110 111 112 113 114 115 116 117 118
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.
119

120 121 122 123 124 125
Instance pure_beta f x (erec : expr) (v1 v2 : val) `{AsRecV v1 f x erec} :
  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').
126
Proof. solve_pure_exec. Qed.
127

128 129
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').
130
Proof. solve_pure_exec. Qed.
131

132
Instance pure_if_true e1 e2 : PureExec True 1 (If (Val $ LitV $ LitBool true) e1 e2) e1.
133
Proof. solve_pure_exec. Qed.
134

135
Instance pure_if_false e1 e2 : PureExec True 1 (If (Val $ LitV  $ LitBool false) e1 e2) e2.
136
Proof. solve_pure_exec. Qed.
137

138 139
Instance pure_fst v1 v2 :
  PureExec True 1 (Fst (Val $ PairV v1 v2)) (Val v1).
140
Proof. solve_pure_exec. Qed.
141

142 143
Instance pure_snd v1 v2 :
  PureExec True 1 (Snd (Val $ PairV v1 v2)) (Val v2).
144
Proof. solve_pure_exec. Qed.
145

146 147
Instance pure_case_inl v e1 e2 :
  PureExec True 1 (Case (Val $ InjLV v) e1 e2) (App e1 (Val v)).
148
Proof. solve_pure_exec. Qed.
149

150 151
Instance pure_case_inr v e1 e2 :
  PureExec True 1 (Case (Val $ InjRV v) e1 e2) (App e2 (Val v)).
152
Proof. solve_pure_exec. Qed.
153

154 155 156 157 158 159 160
Section lifting.
Context `{heapG Σ}.
Implicit Types P Q : iProp Σ.
Implicit Types Φ : val  iProp Σ.
Implicit Types efs : list expr.
Implicit Types σ : state.

Ralf Jung's avatar
Ralf Jung committed
161
(** Fork: Not using Texan triples to avoid some unnecessary [True] *)
162
Lemma wp_fork s E e Φ :
Ralf Jung's avatar
Ralf Jung committed
163
   WP e @ s;  {{ _, True }} -  Φ (LitV LitUnit) - WP Fork e @ s; E {{ Φ }}.
164
Proof.
165 166 167
  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.
168
Qed.
169

170
Lemma twp_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 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.
176 177
Qed.

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

198
Lemma wp_load s E l q v :
199
  {{{  l {q} v }}} Load (Val $ LitV $ LitLoc l) @ s; E {{{ RET v; l {q} v }}}.
200 201
Proof.
  iIntros (Φ) ">Hl HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
202
  iIntros (σ1 κ κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
203
  iSplit; first by eauto. iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
204 205
  iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
Qed.
206
Lemma twp_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 twp_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. iIntros (κ v2 σ2 efs Hstep); inv_head_step.
Ralf Jung's avatar
fix TWP  
Ralf Jung committed
212
  iModIntro; iSplit=> //. iSplit; first done. iFrame. by iApply "HΦ".
213
Qed.
214

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

238 239 240
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
241 242
  {{{ RET LitV (LitBool false); l {q} v' }}}.
Proof.
243
  iIntros (?? Φ) ">Hl HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
244
  iIntros (σ1 κ κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
245
  iSplit; first by eauto. iNext; iIntros (v2' σ2 efs Hstep); inv_head_step.
246 247
  iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
Qed.
248 249 250
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
251 252
  [[{ RET LitV (LitBool false); l {q} v' }]].
Proof.
253
  iIntros (?? Φ) "Hl HΦ". iApply twp_lift_atomic_head_step_no_fork; auto.
254
  iIntros (σ1 κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
Ralf Jung's avatar
fix TWP  
Ralf Jung committed
255 256
  iSplit; first by eauto. iIntros (κ v2' σ2 efs Hstep); inv_head_step.
  iModIntro; iSplit=> //. iSplit; first done. iFrame. by iApply "HΦ".
257
Qed.
258

259 260 261
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
262 263
  {{{ RET LitV (LitBool true); l  v2 }}}.
Proof.
264
  iIntros (? Φ) ">Hl HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
265
  iIntros (σ1 κ κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
266
  iSplit; first by eauto. iNext; iIntros (v2' σ2 efs Hstep); inv_head_step.
267
  iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
268
  iModIntro. iSplit=>//. iFrame. by iApply "HΦ".
269
Qed.
270 271 272
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
273 274
  [[{ RET LitV (LitBool true); l  v2 }]].
Proof.
275
  iIntros (? Φ) "Hl HΦ". iApply twp_lift_atomic_head_step_no_fork; auto.
276
  iIntros (σ1 κs n) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
277
  iSplit; first by eauto. iIntros (κ v2' σ2 efs Hstep); inv_head_step.
278
  iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
Ralf Jung's avatar
fix TWP  
Ralf Jung committed
279
  iModIntro. iSplit=>//. iSplit; first done. iFrame. by iApply "HΦ".
280
Qed.
281

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

(** Lifting lemmas for creating and resolving prophecy variables *)
Lemma wp_new_proph :
305
  {{{ True }}} NewProph {{{ v (p : proph_id), RET (LitV (LitProphecy p)); proph p v }}}.
306 307
Proof.
  iIntros (Φ) "_ HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
308
  iIntros (σ1 κ κs n) "[Hσ HR] !>". iDestruct "HR" as (R [Hfr Hdom]) "HR".
309 310 311
  iSplit; first by eauto.
  iNext; iIntros (v2 σ2 efs Hstep). inv_head_step.
  iMod (@proph_map_alloc with "HR") as "[HR Hp]".
312 313 314 315 316 317
  { intro Hin. apply (iffLR (elem_of_subseteq _ _) Hdom) in Hin. done. }
  iModIntro; iSplit=> //. iFrame. iSplitL "HR".
  - iExists _. iSplit; last done.
    iPureIntro. split.
    + apply first_resolve_insert; auto.
    + rewrite dom_insert_L. by apply union_mono_l.
Ralf Jung's avatar
Ralf Jung committed
318
  - iApply "HΦ". done.
319 320
Qed.

321 322 323 324
Lemma wp_resolve_proph p v w:
  {{{ proph p v }}}
    ResolveProph (Val $ LitV $ LitProphecy p) (Val w)
  {{{ RET (LitV LitUnit); v = Some w }}}.
325
Proof.
326
  iIntros (Φ) "Hp HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
327
  iIntros (σ1 κ κs n) "[Hσ HR] !>". iDestruct "HR" as (R [Hfr Hdom]) "HR".
328 329 330
  iDestruct (@proph_map_valid with "HR Hp") as %Hlookup.
  iSplit; first by eauto.
  iNext; iIntros (v2 σ2 efs Hstep); inv_head_step. iApply fupd_frame_l.
331
  iSplit=> //. iFrame.
Ralf Jung's avatar
Ralf Jung committed
332
  iMod (@proph_map_remove with "HR Hp") as "Hp". iModIntro.
333 334
  iSplitR "HΦ".
  - iExists _. iFrame. iPureIntro. split; first by eapply first_resolve_delete.
335
    rewrite dom_delete. set_solver.
336 337
  - iApply "HΦ". iPureIntro. by eapply first_resolve_eq.
Qed.
Ralf Jung's avatar
Ralf Jung committed
338
End lifting.