lifting.v 13.8 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 14
  heapG_gen_heapG :> gen_heapG loc val Σ;
  heapG_proph_mapG :> proph_mapG proph val Σ
15 16 17 18
}.

Instance heapG_irisG `{heapG Σ} : irisG heap_lang Σ := {
  iris_invG := heapG_invG;
19 20
  state_interp σ κs :=
    (gen_heap_ctx σ.1  proph_map_ctx κs σ.2)%I
21 22 23 24
}.

(** 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
25
  (at level 20, q at level 50, format "l  ↦{ q }  v") : bi_scope.
26
Notation "l ↦ v" :=
Robbert Krebbers's avatar
Robbert Krebbers committed
27
  (mapsto (L:=loc) (V:=val) l 1 v%V) (at level 20) : bi_scope.
28
Notation "l ↦{ q } -" := ( v, l {q} v)%I
Robbert Krebbers's avatar
Robbert Krebbers committed
29 30
  (at level 20, q at level 50, format "l  ↦{ q }  -") : bi_scope.
Notation "l ↦ -" := (l {1} -)%I (at level 20) : bi_scope.
31

32 33 34
Notation "p ⥱ v" := (p_mapsto p v) (at level 20, format "p ⥱ v") : bi_scope.
Notation "p ⥱ -" := ( v, p  v)%I (at level 20) : bi_scope.

35 36 37 38 39 40 41 42 43
(** 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
44
  | H : head_step ?e _ _ _ _ _ |- _ =>
45 46 47 48 49
     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.

50
Local Hint Extern 0 (atomic _ _) => solve_atomic.
51
Local Hint Extern 0 (head_reducible _ _) => eexists _, _, _; simpl.
Ralf Jung's avatar
fix TWP  
Ralf Jung committed
52
Local Hint Extern 0 (head_reducible_no_obs _ _) => eexists _, _; simpl.
53 54 55 56

Local Hint Constructors head_step.
Local Hint Resolve alloc_fresh.
Local Hint Resolve to_of_val.
57

Ralf Jung's avatar
fix TWP  
Ralf Jung committed
58
Local Ltac solve_exec_safe := intros; subst; do 3 eexists; econstructor; eauto.
59
Local Ltac solve_exec_puredet := simpl; intros; by inv_head_step.
60
Local Ltac solve_pure_exec :=
61 62
  unfold IntoVal in *;
  repeat match goal with H : AsVal _ |- _ => destruct H as [??] end; subst;
63
  apply det_head_step_pure_exec; [ solve_exec_safe | solve_exec_puredet ].
64

65 66
Class AsRec (e : expr) (f x : binder) (erec : expr) :=
  as_rec : e = Rec f x erec.
67 68
Instance AsRec_rec f x e : AsRec (Rec f x e) f x e := eq_refl.
Instance AsRec_rec_locked_val v f x e :
69 70 71
  AsRec (of_val v) f x e  AsRec (of_val (locked v)) f x e.
Proof. by unlock. Qed.

72
Instance pure_rec f x (erec e1 e2 : expr)
Robbert Krebbers's avatar
Robbert Krebbers committed
73
    `{!AsVal e2, AsRec e1 f x erec, Closed (f :b: x :b: []) erec} :
74
  PureExec True (App e1 e2) (subst' x e2 (subst' f e1 erec)).
75
Proof. unfold AsRec in *; solve_pure_exec. Qed.
76

77
Instance pure_unop op e v v' `{!IntoVal e v} :
78
  PureExec (un_op_eval op v = Some v') (UnOp op e) (of_val v').
79
Proof. solve_pure_exec. Qed.
80

81
Instance pure_binop op e1 e2 v1 v2 v' `{!IntoVal e1 v1, !IntoVal e2 v2} :
82
  PureExec (bin_op_eval op v1 v2 = Some v') (BinOp op e1 e2) (of_val v').
83
Proof. solve_pure_exec. Qed.
84

85
Instance pure_if_true e1 e2 : PureExec True (If (Lit (LitBool true)) e1 e2) e1.
86
Proof. solve_pure_exec. Qed.
87

88
Instance pure_if_false e1 e2 : PureExec True (If (Lit (LitBool false)) e1 e2) e2.
89
Proof. solve_pure_exec. Qed.
90

91
Instance pure_fst e1 e2 v1 `{!IntoVal e1 v1, !AsVal e2} :
92
  PureExec True (Fst (Pair e1 e2)) e1.
93
Proof. solve_pure_exec. Qed.
94

95
Instance pure_snd e1 e2 v2 `{!AsVal e1, !IntoVal e2 v2} :
96
  PureExec True (Snd (Pair e1 e2)) e2.
97
Proof. solve_pure_exec. Qed.
98

99
Instance pure_case_inl e0 v e1 e2 `{!IntoVal e0 v} :
100
  PureExec True (Case (InjL e0) e1 e2) (App e1 e0).
101
Proof. solve_pure_exec. Qed.
102

103
Instance pure_case_inr e0 v e1 e2 `{!IntoVal e0 v} :
104
  PureExec True (Case (InjR e0) e1 e2) (App e2 e0).
105
Proof. solve_pure_exec. Qed.
106

107 108 109 110 111 112 113
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
114
(** Fork: Not using Texan triples to avoid some unnecessary [True] *)
115
Lemma wp_fork s E e Φ :
Ralf Jung's avatar
Ralf Jung committed
116
   WP e @ s;  {{ _, True }} -  Φ (LitV LitUnit) - WP Fork e @ s; E {{ Φ }}.
117
Proof.
Ralf Jung's avatar
Ralf Jung committed
118
  iIntros "He HΦ".
119
  iApply wp_lift_pure_det_head_step; [eauto|intros; inv_head_step; eauto|].
120 121
  iModIntro; iNext; iIntros "!> /= {$He}". by iApply wp_value.
Qed.
122

123
Lemma twp_fork s E e Φ :
Ralf Jung's avatar
Ralf Jung committed
124
  WP e @ s;  [{ _, True }] - Φ (LitV LitUnit) - WP Fork e @ s; E [{ Φ }].
125
Proof.
Ralf Jung's avatar
Ralf Jung committed
126
  iIntros "He HΦ".
127
  iApply twp_lift_pure_det_head_step; [eauto|intros; inv_head_step; eauto|].
128 129 130
  iIntros "!> /= {$He}". by iApply twp_value.
Qed.

131
(** Heap *)
132
Lemma wp_alloc s E e v :
Robbert Krebbers's avatar
Robbert Krebbers committed
133
  IntoVal e v 
134
  {{{ True }}} Alloc e @ s; E {{{ l, RET LitV (LitLoc l); l  v }}}.
135
Proof.
136
  iIntros (<- Φ) "_ HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
137 138 139
  iIntros (σ1 κs) "[Hσ Hκs] !>"; iSplit.
  (* TODO (MR) this used to be done by eauto. Why does it not work any more? *)
  { iPureIntro. repeat eexists. by apply alloc_fresh. }
140
  iNext; iIntros (κ κs' v2 σ2 efs [Hstep ->]); inv_head_step.
141 142 143
  iMod (@gen_heap_alloc with "Hσ") as "[Hσ Hl]"; first done.
  iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
Qed.
144 145 146 147
Lemma twp_alloc s E e v :
  IntoVal e v 
  [[{ True }]] Alloc e @ s; E [[{ l, RET LitV (LitLoc l); l  v }]].
Proof.
148
  iIntros (<- Φ) "_ HΦ". iApply twp_lift_atomic_head_step_no_fork; auto.
149 150 151
  iIntros (σ1 κs) "[Hσ Hκs] !>"; iSplit.
  (* TODO (MR) this used to be done by eauto. Why does it not work any more? *)
  { iPureIntro. repeat eexists. by apply alloc_fresh. }
Ralf Jung's avatar
fix TWP  
Ralf Jung committed
152
  iIntros (κ v2 σ2 efs Hstep); inv_head_step.
153
  iMod (@gen_heap_alloc with "Hσ") as "[Hσ Hl]"; first done.
Ralf Jung's avatar
fix TWP  
Ralf Jung committed
154
  iModIntro; iSplit=> //. iSplit; first done. iFrame. by iApply "HΦ".
155
Qed.
156

157 158
Lemma wp_load s E l q v :
  {{{  l {q} v }}} Load (Lit (LitLoc l)) @ s; E {{{ RET v; l {q} v }}}.
159 160
Proof.
  iIntros (Φ) ">Hl HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
161
  iIntros (σ1 κs) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
162
  iSplit; first by eauto.
163
  iNext; iIntros (κ κs' v2 σ2 efs [Hstep ->]); inv_head_step.
164 165
  iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
Qed.
166 167 168 169
Lemma twp_load s E l q v :
  [[{ l {q} v }]] Load (Lit (LitLoc l)) @ s; E [[{ RET v; l {q} v }]].
Proof.
  iIntros (Φ) "Hl HΦ". iApply twp_lift_atomic_head_step_no_fork; auto.
170
  iIntros (σ1 κs) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
171
  iSplit; first by eauto.
Ralf Jung's avatar
fix TWP  
Ralf Jung committed
172 173
  iIntros (κ v2 σ2 efs Hstep); inv_head_step.
  iModIntro; iSplit=> //. iSplit; first done. iFrame. by iApply "HΦ".
174
Qed.
175

176
Lemma wp_store s E l v' e v :
Robbert Krebbers's avatar
Robbert Krebbers committed
177
  IntoVal e v 
178
  {{{  l  v' }}} Store (Lit (LitLoc l)) e @ s; E {{{ RET LitV LitUnit; l  v }}}.
179
Proof.
180
  iIntros (<- Φ) ">Hl HΦ".
181
  iApply wp_lift_atomic_head_step_no_fork; auto.
182 183 184 185 186
  iIntros (σ1 κs) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
  iSplit.
  (* TODO (MR) this used to be done by eauto. Why does it not work any more? *)
  { iPureIntro. repeat eexists. constructor; eauto. }
  iNext; iIntros (κ κs' v2 σ2 efs [Hstep ->]); inv_head_step.
187
  iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
188
  iModIntro. iSplit=>//. iFrame. by iApply "HΦ".
189
Qed.
190 191 192 193
Lemma twp_store s E l v' e v :
  IntoVal e v 
  [[{ l  v' }]] Store (Lit (LitLoc l)) e @ s; E [[{ RET LitV LitUnit; l  v }]].
Proof.
194
  iIntros (<- Φ) "Hl HΦ".
195
  iApply twp_lift_atomic_head_step_no_fork; auto.
196 197 198 199
  iIntros (σ1 κs) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
  iSplit.
  (* TODO (MR) this used to be done by eauto. Why does it not work any more? *)
  { iPureIntro. repeat eexists. constructor; eauto. }
Ralf Jung's avatar
fix TWP  
Ralf Jung committed
200
  iIntros (κ v2 σ2 efs Hstep); inv_head_step.
201
  iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
Ralf Jung's avatar
fix TWP  
Ralf Jung committed
202
  iModIntro. iSplit=>//. iSplit; first done. iFrame. by iApply "HΦ".
203
Qed.
204

205
Lemma wp_cas_fail s E l q v' e1 v1 e2 :
Ralf Jung's avatar
Ralf Jung committed
206
  IntoVal e1 v1  AsVal e2  v'  v1  vals_cas_compare_safe v' v1 
207
  {{{  l {q} v' }}} CAS (Lit (LitLoc l)) e1 e2 @ s; E
208 209
  {{{ RET LitV (LitBool false); l {q} v' }}}.
Proof.
Ralf Jung's avatar
Ralf Jung committed
210
  iIntros (<- [v2 <-] ?? Φ) ">Hl HΦ".
211
  iApply wp_lift_atomic_head_step_no_fork; auto.
212
  iIntros (σ1 κs) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
213
  iSplit; first by eauto. iNext; iIntros (κ κs' v2' σ2 efs [Hstep ->]); inv_head_step.
214 215
  iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
Qed.
216
Lemma twp_cas_fail s E l q v' e1 v1 e2 :
Ralf Jung's avatar
Ralf Jung committed
217
  IntoVal e1 v1  AsVal e2  v'  v1  vals_cas_compare_safe v' v1 
218 219 220
  [[{ l {q} v' }]] CAS (Lit (LitLoc l)) e1 e2 @ s; E
  [[{ RET LitV (LitBool false); l {q} v' }]].
Proof.
Ralf Jung's avatar
Ralf Jung committed
221
  iIntros (<- [v2 <-] ?? Φ) "Hl HΦ".
222
  iApply twp_lift_atomic_head_step_no_fork; auto.
223
  iIntros (σ1 κs) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
Ralf Jung's avatar
fix TWP  
Ralf Jung committed
224 225
  iSplit; first by eauto. iIntros (κ v2' σ2 efs Hstep); inv_head_step.
  iModIntro; iSplit=> //. iSplit; first done. iFrame. by iApply "HΦ".
226
Qed.
227

228
Lemma wp_cas_suc s E l e1 v1 e2 v2 :
Ralf Jung's avatar
Ralf Jung committed
229
  IntoVal e1 v1  IntoVal e2 v2  vals_cas_compare_safe v1 v1 
230
  {{{  l  v1 }}} CAS (Lit (LitLoc l)) e1 e2 @ s; E
231 232
  {{{ RET LitV (LitBool true); l  v2 }}}.
Proof.
Ralf Jung's avatar
Ralf Jung committed
233
  iIntros (<- <- ? Φ) ">Hl HΦ".
234
  iApply wp_lift_atomic_head_step_no_fork; auto.
235 236 237 238 239
  iIntros (σ1 κs) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
  iSplit.
  (* TODO (MR) this used to be done by eauto. Why does it not work any more? *)
  { iPureIntro. repeat eexists. by econstructor. }
  iNext; iIntros (κ κs' v2' σ2 efs [Hstep ->]); inv_head_step.
240
  iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
241
  iModIntro. iSplit=>//. iFrame. by iApply "HΦ".
242
Qed.
243
Lemma twp_cas_suc s E l e1 v1 e2 v2 :
Ralf Jung's avatar
Ralf Jung committed
244
  IntoVal e1 v1  IntoVal e2 v2  vals_cas_compare_safe v1 v1 
245 246 247
  [[{ l  v1 }]] CAS (Lit (LitLoc l)) e1 e2 @ s; E
  [[{ RET LitV (LitBool true); l  v2 }]].
Proof.
Ralf Jung's avatar
Ralf Jung committed
248
  iIntros (<- <- ? Φ) "Hl HΦ".
249
  iApply twp_lift_atomic_head_step_no_fork; auto.
250 251 252 253
  iIntros (σ1 κs) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
  iSplit.
  (* TODO (MR) this used to be done by eauto. Why does it not work any more? *)
  { iPureIntro. repeat eexists. by econstructor. }
Ralf Jung's avatar
fix TWP  
Ralf Jung committed
254
  iIntros (κ v2' σ2 efs Hstep); inv_head_step.
255
  iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
Ralf Jung's avatar
fix TWP  
Ralf Jung committed
256
  iModIntro. iSplit=>//. iSplit; first done. iFrame. by iApply "HΦ".
257
Qed.
258

Ralf Jung's avatar
Ralf Jung committed
259
Lemma wp_faa s E l i1 e2 i2 :
260
  IntoVal e2 (LitV (LitInt i2)) 
Ralf Jung's avatar
Ralf Jung committed
261
  {{{  l  LitV (LitInt i1) }}} FAA (Lit (LitLoc l)) e2 @ s; E
262 263
  {{{ RET LitV (LitInt i1); l  LitV (LitInt (i1 + i2)) }}}.
Proof.
264
  iIntros (<- Φ) ">Hl HΦ".
265
  iApply wp_lift_atomic_head_step_no_fork; auto.
266 267 268 269 270
  iIntros (σ1 κs) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
  iSplit.
  (* TODO (MR) this used to be done by eauto. Why does it not work any more? *)
  { iPureIntro. repeat eexists. by constructor. }
  iNext; iIntros (κ κs' v2' σ2 efs [Hstep ->]); inv_head_step.
271
  iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
272
  iModIntro. iSplit=>//. iFrame. by iApply "HΦ".
273
Qed.
274 275 276 277 278
Lemma twp_faa s E l i1 e2 i2 :
  IntoVal e2 (LitV (LitInt i2)) 
  [[{ l  LitV (LitInt i1) }]] FAA (Lit (LitLoc l)) e2 @ s; E
  [[{ RET LitV (LitInt i1); l  LitV (LitInt (i1 + i2)) }]].
Proof.
279
  iIntros (<- Φ) "Hl HΦ".
280
  iApply twp_lift_atomic_head_step_no_fork; auto.
281 282 283 284
  iIntros (σ1 κs) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
  iSplit.
  (* TODO (MR) this used to be done by eauto. Why does it not work any more? *)
  { iPureIntro. repeat eexists. by constructor. }
Ralf Jung's avatar
fix TWP  
Ralf Jung committed
285
  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 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329

(** Lifting lemmas for creating and resolving prophecy variables *)
Lemma wp_new_proph :
  {{{ True }}} NewProph {{{ (p : proph), RET (LitV (LitProphecy p)); p  - }}}.
Proof.
  iIntros (Φ) "_ HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
  iIntros (σ1 κs) "[Hσ HR] !>". iDestruct "HR" as (R [Hfr Hdom]) "HR". iSplit.
  (* TODO (MR) this used to be done by eauto. Why does it not work any more? *)
  { iPureIntro. repeat eexists. by apply new_proph_fresh. }
  unfold cons_obs. simpl.
  iNext; iIntros (κ κs' v2 σ2 efs [Hstep ->]). inv_head_step.
  iMod ((@proph_map_alloc _ _ _ _ _ _ _ p) with "HR") as "[HR Hp]".
  { 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.
  - iApply "HΦ". by iExists _.
Qed.

Lemma wp_resolve_proph e1 e2 p v w:
  IntoVal e1 (LitV (LitProphecy p)) 
  IntoVal e2 w 
  {{{ p  v }}} ResolveProph e1 e2 {{{ RET (LitV LitUnit); v = Some w }}}.
Proof.
  iIntros (<- <- Φ) "Hp HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
  iIntros (σ1 κs) "[Hσ HR] !>". iDestruct "HR" as (R [Hfr Hdom]) "HR".
  iDestruct (@proph_map_valid with "HR Hp") as %Hlookup. iSplit.
  (* TODO (MR) this used to be done by eauto. Why does it not work any more? *)
  { iPureIntro. repeat eexists. by constructor. }
  unfold cons_obs. simpl.
  iNext; iIntros (κ κs' v2 σ2 efs [Hstep ->]); inv_head_step. iApply fupd_frame_l.
  iSplit=> //. iFrame.
  iMod ((@proph_map_remove _ _ _ _ _ _ _ p0) with "HR Hp") as "Hp". iModIntro.
  iSplitR "HΦ".
  - iExists _. iFrame. iPureIntro. split; first by eapply first_resolve_delete.
    rewrite dom_delete. rewrite <- difference_empty_L. by eapply difference_mono.
  - iApply "HΦ". iPureIntro. by eapply first_resolve_eq.
Qed.

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