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

Ralf Jung's avatar
Ralf Jung committed
11
12
(** Basic rules for language operations. *)

13
14
15
16
17
18
19
20
21
Class heapG Σ := HeapG {
  heapG_invG : invG Σ;
  heapG_gen_heapG :> gen_heapG loc val Σ
}.

Instance heapG_irisG `{heapG Σ} : irisG heap_lang Σ := {
  iris_invG := heapG_invG;
  state_interp := gen_heap_ctx
}.
22
Global Opaque iris_invG.
23
24
25
26
27
28
29
30
31
32

(** Override the notations so that scopes and coercions work out *)
Notation "l ↦{ q } v" := (mapsto (L:=loc) (V:=val) l q v%V)
  (at level 20, q at level 50, format "l  ↦{ q }  v") : uPred_scope.
Notation "l ↦ v" :=
  (mapsto (L:=loc) (V:=val) l 1 v%V) (at level 20) : uPred_scope.
Notation "l ↦{ q } -" := ( v, l {q} v)%I
  (at level 20, q at level 50, format "l  ↦{ q }  -") : uPred_scope.
Notation "l ↦ -" := (l {1} -)%I (at level 20) : uPred_scope.

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
43
  | H : _ = of_val ?v |- _ =>
     is_var v; destruct v; first[discriminate H|injection H as H]
44
45
46
47
48
49
50
51
52
53
54
55
  | H : head_step ?e _ _ _ _ |- _ =>
     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.

Local Hint Extern 0 (atomic _) => solve_atomic.
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

Ralf Jung's avatar
Ralf Jung committed
57
Section lifting.
58
Context `{heapG Σ}.
59
60
Implicit Types P Q : iProp Σ.
Implicit Types Φ : val  iProp Σ.
61
Implicit Types efs : list expr.
62
Implicit Types σ : state.
Ralf Jung's avatar
Ralf Jung committed
63

64
(** Bind. This bundles some arguments that wp_ectx_bind leaves as indices. *)
65
Lemma wp_bind {E e} K Φ :
66
  WP e @ E {{ v, WP fill K (of_val v) @ E {{ Φ }} }}  WP fill K e @ E {{ Φ }}.
67
Proof. exact: wp_ectx_bind. Qed.
Ralf Jung's avatar
Ralf Jung committed
68

69
Lemma wp_bindi {E e} Ki Φ :
Ralf Jung's avatar
Ralf Jung committed
70
71
72
73
  WP e @ E {{ v, WP fill_item Ki (of_val v) @ E {{ Φ }} }} 
     WP fill_item Ki e @ E {{ Φ }}.
Proof. exact: weakestpre.wp_bind. Qed.

74
(** Base axioms for core primitives of the language: Stateless reductions *)
75
Lemma wp_fork E e Φ :
76
   Φ (LitV LitUnit)   WP e {{ _, True }}  WP Fork e @ E {{ Φ }}.
77
Proof.
78
  rewrite -(wp_lift_pure_det_head_step (Fork e) (Lit LitUnit) [e]) //=; eauto.
79
  - by rewrite -step_fupd_intro // later_sep -(wp_value _ _ (Lit _)) // right_id.
80
  - intros; inv_head_step; eauto.
81
Qed.
82

83
84
85
Local Ltac solve_exec_safe := intros; subst; do 3 eexists; econstructor; eauto.
Local Ltac solve_exec_puredet := simpl; intros; by inv_head_step.
Local Ltac solve_pureexec :=
86
87
  apply hoist_pred_pureexec; intros; destruct_and?;
  apply det_head_step_pureexec; [ solve_exec_safe | solve_exec_puredet ].
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

Global Instance pure_rec f x erec e1 e2 v2 :
  PureExec (to_val e2 = Some v2  e1 = Rec f x erec  Closed (f :b: x :b: []) erec)
           (App e1 e2)
           (subst' x e2 (subst' f e1 erec)).
Proof. solve_pureexec. Qed.

Global Instance pure_unop op e v v' :
  PureExec (to_val e = Some v  un_op_eval op v = Some v')
           (UnOp op e)
           (of_val v').
Proof. solve_pureexec. Qed.

Global Instance pure_binop op e1 e2 v1 v2 v' :
  PureExec (to_val e1 = Some v1  to_val e2 = Some v2  bin_op_eval op v1 v2 = Some v')
           (BinOp op e1 e2)
           (of_val v').
Proof. solve_pureexec. Qed.

Global Instance pure_if_true e1 e2 :
  PureExec True (If (Lit (LitBool true)) e1 e2) e1.
Proof. solve_pureexec. Qed.

Global Instance pure_if_false e1 e2 :
  PureExec True (If (Lit (LitBool false)) e1 e2) e2.
Proof. solve_pureexec. Qed.

Global Instance pure_fst e1 e2 v1 v2 :
  PureExec (to_val e1 = Some v1  to_val e2 = Some v2)
           (Fst (Pair e1 e2))
           e1.
Proof. solve_pureexec. Qed.

Global Instance pure_snd e1 e2 v1 v2 :
  PureExec (to_val e1 = Some v1  to_val e2 = Some v2)
           (Snd (Pair e1 e2))
           e2.
Proof. solve_pureexec. Qed.

Global Instance pure_case_inl e0 v e1 e2  :
  PureExec (to_val e0 = Some v) (Case (InjL e0) e1 e2) (App e1 e0).
Proof. solve_pureexec. Qed.

Global Instance pure_case_inr e0 v e1 e2  :
  PureExec (to_val e0 = Some v) (Case (InjR e0) e1 e2) (App e2 e0).
Proof. solve_pureexec. Qed.
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

(** Heap *)
Lemma wp_alloc E e v :
  to_val e = Some v 
  {{{ True }}} Alloc e @ E {{{ l, RET LitV (LitLoc l); l  v }}}.
Proof.
  iIntros (<-%of_to_val Φ) "HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
  iIntros (σ1) "Hσ !>"; iSplit; first by auto.
  iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
  iMod (@gen_heap_alloc with "Hσ") as "[Hσ Hl]"; first done.
  iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
Qed.

Lemma wp_load E l q v :
  {{{  l {q} v }}} Load (Lit (LitLoc l)) @ E {{{ RET v; l {q} v }}}.
Proof.
  iIntros (Φ) ">Hl HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
  iIntros (σ1) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
  iSplit; first by eauto.
  iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
  iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
Qed.

Lemma wp_store E l v' e v :
  to_val e = Some v 
  {{{  l  v' }}} Store (Lit (LitLoc l)) e @ E {{{ RET LitV LitUnit; l  v }}}.
Proof.
  iIntros (<-%of_to_val Φ) ">Hl HΦ".
  iApply wp_lift_atomic_head_step_no_fork; auto.
  iIntros (σ1) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
  iSplit; first by eauto. iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
  iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
  iModIntro. iSplit=>//. by iApply "HΦ".
Qed.

Lemma wp_cas_fail E l q v' e1 v1 e2 v2 :
  to_val e1 = Some v1  to_val e2 = Some v2  v'  v1 
  {{{  l {q} v' }}} CAS (Lit (LitLoc l)) e1 e2 @ E
  {{{ RET LitV (LitBool false); l {q} v' }}}.
Proof.
  iIntros (<-%of_to_val <-%of_to_val ? Φ) ">Hl HΦ".
  iApply wp_lift_atomic_head_step_no_fork; auto.
  iIntros (σ1) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
  iSplit; first by eauto. iNext; iIntros (v2' σ2 efs Hstep); inv_head_step.
  iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
Qed.

Lemma wp_cas_suc E l e1 v1 e2 v2 :
  to_val e1 = Some v1  to_val e2 = Some v2 
  {{{  l  v1 }}} CAS (Lit (LitLoc l)) e1 e2 @ E
  {{{ RET LitV (LitBool true); l  v2 }}}.
Proof.
  iIntros (<-%of_to_val <-%of_to_val Φ) ">Hl HΦ".
  iApply wp_lift_atomic_head_step_no_fork; auto.
  iIntros (σ1) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
  iSplit; first by eauto. iNext; iIntros (v2' σ2 efs Hstep); inv_head_step.
  iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
  iModIntro. iSplit=>//. by iApply "HΦ".
Qed.
193
194
195
196
197

(** Proof rules for derived constructs *)
Lemma wp_seq E e1 e2 Φ :
  is_Some (to_val e1)  Closed [] e2 
   WP e2 @ E {{ Φ }}  WP Seq e1 e2 @ E {{ Φ }}.
198
Proof. iIntros ([? ?] ?). rewrite -wp_pure'; by eauto. Qed.
199
200
201
202
203
204
205

Lemma wp_skip E Φ :  Φ (LitV LitUnit)  WP Skip @ E {{ Φ }}.
Proof. rewrite -wp_seq; last eauto. by rewrite -wp_value. Qed.

Lemma wp_match_inl E e0 x1 e1 x2 e2 Φ :
  is_Some (to_val e0)  Closed (x1 :b: []) e1 
   WP subst' x1 e0 e1 @ E {{ Φ }}  WP Match (InjL e0) x1 e1 x2 e2 @ E {{ Φ }}.
206
Proof. iIntros ([? ?] ?) "?". rewrite -!wp_pure'; by eauto. Qed.
207
208
209
210

Lemma wp_match_inr E e0 x1 e1 x2 e2 Φ :
  is_Some (to_val e0)  Closed (x2 :b: []) e2 
   WP subst' x2 e0 e2 @ E {{ Φ }}  WP Match (InjR e0) x1 e1 x2 e2 @ E {{ Φ }}.
211
Proof. iIntros ([? ?] ?) "?". rewrite -!wp_pure'; by eauto. Qed.
212

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