lifting.v 7.27 KB
Newer Older
1
From iris.base_logic Require Export gen_heap.
Dan Frumin's avatar
Dan Frumin committed
2
From iris.program_logic Require Export weakestpre lifting.
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
  | 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.

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

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 66
Lemma wp_bind {E e} K Φ :
  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 70 71
Lemma wp_bindi {E e} Ki Φ :
  WP e @ E {{ v, WP fill_item Ki (of_val v) @ E {{ Φ }} }} 
     WP fill_item Ki e @ E {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
72 73
Proof. exact: weakestpre.wp_bind. Qed.

74
(** Base axioms for core primitives of the language: Stateless reductions *)
75 76
Lemma wp_fork E e Φ :
   Φ (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
Local Ltac solve_exec_safe := intros; subst; do 3 eexists; econstructor; eauto.
Local Ltac solve_exec_puredet := simpl; intros; by inv_head_step.
85
Local Ltac solve_pure_exec :=
86
  unfold IntoVal, AsVal in *; subst;
Robbert Krebbers's avatar
Robbert Krebbers committed
87
  repeat match goal with H : is_Some _ |- _ => destruct H as [??] end;
88
  apply det_head_step_pure_exec; [ solve_exec_safe | solve_exec_puredet ].
89

90 91 92 93 94 95 96
Class AsRec (e : expr) (f x : binder) (erec : expr) :=
  as_rec : e = Rec f x erec.
Global Instance AsRec_rec f x e : AsRec (Rec f x e) f x e := eq_refl.
Global Instance AsRec_rec_locked_val v f x e :
  AsRec (of_val v) f x e  AsRec (of_val (locked v)) f x e.
Proof. by unlock. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
97 98
Global Instance pure_rec f x (erec e1 e2 : expr)
    `{!AsVal e2, AsRec e1 f x erec, Closed (f :b: x :b: []) erec} :
99
  PureExec True (App e1 e2) (subst' x e2 (subst' f e1 erec)).
100
Proof. unfold AsRec in *; solve_pure_exec. Qed.
101

102 103
Global Instance pure_unop op e v v' `{!IntoVal e v} :
  PureExec (un_op_eval op v = Some v') (UnOp op e) (of_val v').
104
Proof. solve_pure_exec. Qed.
105

106 107
Global Instance pure_binop op e1 e2 v1 v2 v' `{!IntoVal e1 v1, !IntoVal e2 v2} :
  PureExec (bin_op_eval op v1 v2 = Some v') (BinOp op e1 e2) (of_val v').
108
Proof. solve_pure_exec. Qed.
109

110 111
Global Instance pure_if_true e1 e2 :
  PureExec True (If (Lit (LitBool true)) e1 e2) e1.
112
Proof. solve_pure_exec. Qed.
113

114 115
Global Instance pure_if_false e1 e2 :
  PureExec True (If (Lit (LitBool false)) e1 e2) e2.
116
Proof. solve_pure_exec. Qed.
117

Robbert Krebbers's avatar
Robbert Krebbers committed
118
Global Instance pure_fst e1 e2 v1 `{!IntoVal e1 v1, !AsVal e2} :
119
  PureExec True (Fst (Pair e1 e2)) e1.
120
Proof. solve_pure_exec. Qed.
121

Robbert Krebbers's avatar
Robbert Krebbers committed
122
Global Instance pure_snd e1 e2 v2 `{!AsVal e1, !IntoVal e2 v2} :
123
  PureExec True (Snd (Pair e1 e2)) e2.
124
Proof. solve_pure_exec. Qed.
125

126 127
Global Instance pure_case_inl e0 v e1 e2 `{!IntoVal e0 v} :
  PureExec True (Case (InjL e0) e1 e2) (App e1 e0).
128
Proof. solve_pure_exec. Qed.
129

130 131
Global Instance pure_case_inr e0 v e1 e2 `{!IntoVal e0 v} :
  PureExec True (Case (InjR e0) e1 e2) (App e2 e0).
132
Proof. solve_pure_exec. Qed.
133 134

(** Heap *)
135
Lemma wp_alloc E e v :
Robbert Krebbers's avatar
Robbert Krebbers committed
136
  IntoVal e v 
137
  {{{ True }}} Alloc e @ E {{{ l, RET LitV (LitLoc l); l  v }}}.
138
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
139
  iIntros (<-%of_to_val Φ) "_ HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
140 141 142 143 144 145
  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.

146 147
Lemma wp_load E l q v :
  {{{  l {q} v }}} Load (Lit (LitLoc l)) @ E {{{ RET v; l {q} v }}}.
148 149 150 151 152 153 154 155
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.

156
Lemma wp_store E l v' e v :
Robbert Krebbers's avatar
Robbert Krebbers committed
157
  IntoVal e v 
158
  {{{  l  v' }}} Store (Lit (LitLoc l)) e @ E {{{ RET LitV LitUnit; l  v }}}.
159 160 161 162 163 164 165 166 167
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.

168
Lemma wp_cas_fail E l q v' e1 v1 e2 :
Robbert Krebbers's avatar
Robbert Krebbers committed
169
  IntoVal e1 v1  AsVal e2  v'  v1 
170
  {{{  l {q} v' }}} CAS (Lit (LitLoc l)) e1 e2 @ E
171 172
  {{{ RET LitV (LitBool false); l {q} v' }}}.
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
173
  iIntros (<-%of_to_val [v2 <-%of_to_val] ? Φ) ">Hl HΦ".
174 175 176 177 178 179
  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.

180
Lemma wp_cas_suc E l e1 v1 e2 v2 :
Robbert Krebbers's avatar
Robbert Krebbers committed
181
  IntoVal e1 v1  IntoVal e2 v2 
182
  {{{  l  v1 }}} CAS (Lit (LitLoc l)) e1 e2 @ E
183 184 185 186 187 188 189 190 191
  {{{ 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.
Ralf Jung's avatar
Ralf Jung committed
192
End lifting.