lifting.v 13.6 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 52 53 54 55
Local Hint Extern 0 (head_reducible _ _) => eexists _, _, _; simpl.

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

57
Local Ltac solve_exec_safe := intros; subst; do 4 eexists; econstructor; eauto.
58
Local Ltac solve_exec_puredet := simpl; intros; by inv_head_step.
59
Local Ltac solve_pure_exec :=
60 61
  unfold IntoVal in *;
  repeat match goal with H : AsVal _ |- _ => destruct H as [??] end; subst;
62
  apply det_head_step_pure_exec; [ solve_exec_safe | solve_exec_puredet ].
63

64 65
Class AsRec (e : expr) (f x : binder) (erec : expr) :=
  as_rec : e = Rec f x erec.
66 67
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 :
68 69 70
  AsRec (of_val v) f x e  AsRec (of_val (locked v)) f x e.
Proof. by unlock. Qed.

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

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

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

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

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

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

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

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

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

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

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

130
(** Heap *)
131
Lemma wp_alloc s E e v :
132
  IntoVal e v 
133
  {{{ True }}} Alloc e @ s; E {{{ l, RET LitV (LitLoc l); l  v }}}.
134
Proof.
135
  iIntros (<- Φ) "_ HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
136 137 138
  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. }
139
  iNext; iIntros (κ κs' v2 σ2 efs [Hstep ->]); inv_head_step.
140 141 142
  iMod (@gen_heap_alloc with "Hσ") as "[Hσ Hl]"; first done.
  iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
Qed.
143 144 145 146
Lemma twp_alloc s E e v :
  IntoVal e v 
  [[{ True }]] Alloc e @ s; E [[{ l, RET LitV (LitLoc l); l  v }]].
Proof.
147
  iIntros (<- Φ) "_ HΦ". iApply twp_lift_atomic_head_step_no_fork; auto.
148 149 150
  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. }
151
  iIntros (κ κs' v2 σ2 efs [Hstep ->]); inv_head_step.
152 153 154
  iMod (@gen_heap_alloc with "Hσ") as "[Hσ Hl]"; first done.
  iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
Qed.
155

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

175
Lemma wp_store s E l v' e v :
176
  IntoVal e v 
177
  {{{  l  v' }}} Store (Lit (LitLoc l)) e @ s; E {{{ RET LitV LitUnit; l  v }}}.
178
Proof.
179
  iIntros (<- Φ) ">Hl HΦ".
180
  iApply wp_lift_atomic_head_step_no_fork; auto.
181 182 183 184 185
  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.
186
  iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
187
  iModIntro. iSplit=>//. iFrame. by iApply "HΦ".
188
Qed.
189 190 191 192
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.
193
  iIntros (<- Φ) "Hl HΦ".
194
  iApply twp_lift_atomic_head_step_no_fork; auto.
195 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. }
  iIntros (κ κs' v2 σ2 efs [Hstep ->]); inv_head_step.
200
  iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
201
  iModIntro. iSplit=>//. iFrame. by iApply "HΦ".
202
Qed.
203

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

227
Lemma wp_cas_suc s E l e1 v1 e2 v2 :
Ralf Jung's avatar
Ralf Jung committed
228
  IntoVal e1 v1  IntoVal e2 v2  vals_cas_compare_safe v1 v1 
229
  {{{  l  v1 }}} CAS (Lit (LitLoc l)) e1 e2 @ s; E
230 231
  {{{ RET LitV (LitBool true); l  v2 }}}.
Proof.
Ralf Jung's avatar
Ralf Jung committed
232
  iIntros (<- <- ? Φ) ">Hl HΦ".
233
  iApply wp_lift_atomic_head_step_no_fork; auto.
234 235 236 237 238
  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.
239
  iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
240
  iModIntro. iSplit=>//. iFrame. by iApply "HΦ".
241
Qed.
242
Lemma twp_cas_suc s E l e1 v1 e2 v2 :
Ralf Jung's avatar
Ralf Jung committed
243
  IntoVal e1 v1  IntoVal e2 v2  vals_cas_compare_safe v1 v1 
244 245 246
  [[{ l  v1 }]] CAS (Lit (LitLoc l)) e1 e2 @ s; E
  [[{ RET LitV (LitBool true); l  v2 }]].
Proof.
Ralf Jung's avatar
Ralf Jung committed
247
  iIntros (<- <- ? Φ) "Hl HΦ".
248
  iApply twp_lift_atomic_head_step_no_fork; auto.
249 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. }
  iIntros (κ κs' v2' σ2 efs [Hstep ->]); inv_head_step.
254
  iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
255
  iModIntro. iSplit=>//. iFrame. by iApply "HΦ".
256
Qed.
257

Ralf Jung's avatar
Ralf Jung committed
258
Lemma wp_faa s E l i1 e2 i2 :
259
  IntoVal e2 (LitV (LitInt i2)) 
Ralf Jung's avatar
Ralf Jung committed
260
  {{{  l  LitV (LitInt i1) }}} FAA (Lit (LitLoc l)) e2 @ s; E
261 262
  {{{ RET LitV (LitInt i1); l  LitV (LitInt (i1 + i2)) }}}.
Proof.
263
  iIntros (<- Φ) ">Hl HΦ".
264
  iApply wp_lift_atomic_head_step_no_fork; auto.
265 266 267 268 269
  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.
270
  iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
271
  iModIntro. iSplit=>//. iFrame. by iApply "HΦ".
272
Qed.
273 274 275 276 277
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.
278
  iIntros (<- Φ) "Hl HΦ".
279
  iApply twp_lift_atomic_head_step_no_fork; auto.
280 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. }
  iIntros (κ κs' v2' σ2 efs [Hstep ->]); inv_head_step.
285
  iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
286
  iModIntro. iSplit=>//. iFrame. by iApply "HΦ".
287
Qed.
288 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

(** 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
329
End lifting.